MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(1,B,C,D,E,F,G,H,I,J,S,R,0,1,S,S,S) [0 >= S && K >= 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f21(1,B,C,D,E,F,G,H,I,J,S,R,0,1,S,S,S) [S >= 1 && K >= 1] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f21(1,B,C,D,E,F,G,H,I,J,K,R,K,N,O,P,Q) [0 >= K] (1,1) 3. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [-1*M >= 0 && A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && A >= 0] (?,1) 4. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f29(0,B,R,D,E,F,G,0,R,R,K,L,M,N,O,P,Q) [-1*M >= 0 && -1 + A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && A >= 1] (?,1) 5. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(1,S,C,0,R,R,R,H,I,J,K,L,M,N,O,P,Q) [-1*H >= 0 (?,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && R >= 1000 + C] 6. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(A,S,C,0,R,R,R,H,I,J,K,L,M,N,O,P,Q) [-1*H >= 0 (?,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && 999 + C >= R] Signature: {(f0,17);(f21,17);(f29,17);(f41,17)} Flow Graph: [0->{3},1->{4},2->{4},3->{3},4->{5,6},5->{3},6->{3}] + Applied Processor: ArgumentFilter [1,3,4,5,6,8,9,11,13,14,15,16] + Details: We remove following argument positions: [1,3,4,5,6,8,9,11,13,14,15,16]. * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,C,H,K,M) -> f41(1,C,H,S,0) [0 >= S && K >= 1] (1,1) 1. f0(A,C,H,K,M) -> f21(1,C,H,S,0) [S >= 1 && K >= 1] (1,1) 2. f0(A,C,H,K,M) -> f21(1,C,H,K,K) [0 >= K] (1,1) 3. f41(A,C,H,K,M) -> f41(A,C,H,K,M) [-1*M >= 0 && A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && A >= 0] (?,1) 4. f21(A,C,H,K,M) -> f29(0,R,0,K,M) [-1*M >= 0 && -1 + A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && A >= 1] (?,1) 5. f29(A,C,H,K,M) -> f41(1,C,H,K,M) [-1*H >= 0 (?,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && R >= 1000 + C] 6. f29(A,C,H,K,M) -> f41(A,C,H,K,M) [-1*H >= 0 (?,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && 999 + C >= R] Signature: {(f0,17);(f21,17);(f29,17);(f41,17)} Flow Graph: [0->{3},1->{4},2->{4},3->{3},4->{5,6},5->{3},6->{3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f0(A,C,H,K,M) -> f41(1,C,H,S,0) [0 >= S && K >= 1] (1,1) 1. f0(A,C,H,K,M) -> f21(1,C,H,S,0) [S >= 1 && K >= 1] (1,1) 2. f0(A,C,H,K,M) -> f21(1,C,H,K,K) [0 >= K] (1,1) 3. f41(A,C,H,K,M) -> f41(A,C,H,K,M) [-1*M >= 0 && A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && A >= 0] (?,1) 4. f21(A,C,H,K,M) -> f29(0,R,0,K,M) [-1*M >= 0 && -1 + A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && A >= 1] (1,1) 5. f29(A,C,H,K,M) -> f41(1,C,H,K,M) [-1*H >= 0 (1,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && R >= 1000 + C] 6. f29(A,C,H,K,M) -> f41(A,C,H,K,M) [-1*H >= 0 (1,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && 999 + C >= R] Signature: {(f0,17);(f21,17);(f29,17);(f41,17)} Flow Graph: [0->{3},1->{4},2->{4},3->{3},4->{5,6},5->{3},6->{3}] + Applied Processor: AddSinks + Details: () * Step 4: Failure MAYBE + Considered Problem: Rules: 0. f0(A,C,H,K,M) -> f41(1,C,H,S,0) [0 >= S && K >= 1] (1,1) 1. f0(A,C,H,K,M) -> f21(1,C,H,S,0) [S >= 1 && K >= 1] (1,1) 2. f0(A,C,H,K,M) -> f21(1,C,H,K,K) [0 >= K] (1,1) 3. f41(A,C,H,K,M) -> f41(A,C,H,K,M) [-1*M >= 0 && A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && A >= 0] (?,1) 4. f21(A,C,H,K,M) -> f29(0,R,0,K,M) [-1*M >= 0 && -1 + A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && A >= 1] (?,1) 5. f29(A,C,H,K,M) -> f41(1,C,H,K,M) [-1*H >= 0 (?,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && R >= 1000 + C] 6. f29(A,C,H,K,M) -> f41(A,C,H,K,M) [-1*H >= 0 (?,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && 999 + C >= R] 7. f41(A,C,H,K,M) -> exitus616(A,C,H,K,M) True (?,1) Signature: {(exitus616,5);(f0,17);(f21,17);(f29,17);(f41,17)} Flow Graph: [0->{3,7},1->{4},2->{4},3->{3,7},4->{5,6},5->{3,7},6->{3,7},7->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7] | `- p:[3] c: [] MAYBE