MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f18(3,3,0,3,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) 1. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A && A >= C] (?,1) 2. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 && A >= C] (?,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,D,D,-3,4,0,J,K,L,M,N,O,P,Q,R) True (?,1) 4. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= G && G >= I] (?,1) 5. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,E,F,G,G + H,I,J,K,L,M,N,O,P,Q,R) [G >= 1 && G >= I] (?,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,K,K,K,3,-6,0,P,Q,R) True (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= M && M >= O] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,M + N,O,P,Q,R) [M >= 1 && M >= O] (?,1) 9. f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,Q,Q,Q) [4 >= F] (?,1) 10. f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,Q,Q,Q) [F >= 5] (?,1) 11. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,N,R) [O >= 1 + M] (?,1) 12. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,F,G,H,I,J,H,L,M,N,O,P,Q,R) [I >= 1 + G] (?,1) 13. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f18(A,B,C,B,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + A] (?,1) Signature: {(f0,18);(f10,18);(f18,18);(f25,18);(f33,18);(f40,18);(f48,18);(f52,18)} Flow Graph: [0->{3},1->{1,2,13},2->{1,2,13},3->{4,5,12},4->{4,5,12},5->{4,5,12},6->{7,8,11},7->{7,8,11},8->{7,8,11} ,9->{},10->{},11->{9,10},12->{6},13->{3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f18(3,3,0,3,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) 1. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A && A >= C] (?,1) 2. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 && A >= C] (?,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,D,D,-3,4,0,J,K,L,M,N,O,P,Q,R) True (1,1) 4. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= G && G >= I] (?,1) 5. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,E,F,G,G + H,I,J,K,L,M,N,O,P,Q,R) [G >= 1 && G >= I] (?,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,K,K,K,3,-6,0,P,Q,R) True (1,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= M && M >= O] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,M + N,O,P,Q,R) [M >= 1 && M >= O] (?,1) 9. f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,Q,Q,Q) [4 >= F] (1,1) 10. f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,Q,Q,Q) [F >= 5] (1,1) 11. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,N,R) [O >= 1 + M] (1,1) 12. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,F,G,H,I,J,H,L,M,N,O,P,Q,R) [I >= 1 + G] (1,1) 13. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f18(A,B,C,B,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + A] (1,1) Signature: {(f0,18);(f10,18);(f18,18);(f25,18);(f33,18);(f40,18);(f48,18);(f52,18)} Flow Graph: [0->{3},1->{1,2,13},2->{1,2,13},3->{4,5,12},4->{4,5,12},5->{4,5,12},6->{7,8,11},7->{7,8,11},8->{7,8,11} ,9->{},10->{},11->{9,10},12->{6},13->{3}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2) ,(1,13) ,(2,1) ,(2,13) ,(3,4) ,(3,5) ,(4,5) ,(4,12) ,(5,4) ,(5,12) ,(6,7) ,(6,11) ,(7,8) ,(7,11) ,(8,7) ,(8,11)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f18(3,3,0,3,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) 1. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A && A >= C] (?,1) 2. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 && A >= C] (?,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,D,D,-3,4,0,J,K,L,M,N,O,P,Q,R) True (1,1) 4. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= G && G >= I] (?,1) 5. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,E,F,G,G + H,I,J,K,L,M,N,O,P,Q,R) [G >= 1 && G >= I] (?,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,K,K,K,3,-6,0,P,Q,R) True (1,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= M && M >= O] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,M + N,O,P,Q,R) [M >= 1 && M >= O] (?,1) 9. f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,Q,Q,Q) [4 >= F] (1,1) 10. f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,Q,Q,Q) [F >= 5] (1,1) 11. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f48(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,N,R) [O >= 1 + M] (1,1) 12. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,F,G,H,I,J,H,L,M,N,O,P,Q,R) [I >= 1 + G] (1,1) 13. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f18(A,B,C,B,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + A] (1,1) Signature: {(f0,18);(f10,18);(f18,18);(f25,18);(f33,18);(f40,18);(f48,18);(f52,18)} Flow Graph: [0->{3},1->{1},2->{2},3->{12},4->{4},5->{5},6->{8},7->{7},8->{8},9->{},10->{},11->{9,10},12->{6},13->{3}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1,2,4,5,7,9,10,11,13] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f18(3,3,0,3,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,D,D,-3,4,0,J,K,L,M,N,O,P,Q,R) True (1,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,K,K,K,3,-6,0,P,Q,R) True (1,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,M + N,O,P,Q,R) [M >= 1 && M >= O] (?,1) 12. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,F,G,H,I,J,H,L,M,N,O,P,Q,R) [I >= 1 + G] (1,1) Signature: {(f0,18);(f10,18);(f18,18);(f25,18);(f33,18);(f40,18);(f48,18);(f52,18)} Flow Graph: [0->{3},3->{12},6->{8},8->{8},12->{6}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f18(3,3,0,3,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f25(A,B,C,D,D,D,-3,4,0,J,K,L,M,N,O,P,Q,R) True (?,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,K,K,K,3,-6,0,P,Q,R) True (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,M + N,O,P,Q,R) [M >= 1 && M >= O] (?,1) 12. f25(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,F,G,H,I,J,H,L,M,N,O,P,Q,R) [I >= 1 + G] (?,1) 13. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) Signature: {(exitus616,18);(f0,18);(f10,18);(f18,18);(f25,18);(f33,18);(f40,18);(f48,18);(f52,18)} Flow Graph: [0->{3},3->{12},6->{8,13},8->{8,13},12->{6},13->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,3,6,8,12,13] | `- p:[8] c: [] MAYBE