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,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: ArgumentFilter [1,3,4,7,9,10,11,13,15,16,17] + Details: We remove following argument positions: [1,3,4,7,9,10,11,13,15,16,17]. * Step 2: UnreachableRules MAYBE + Considered Problem: Rules: 0. f0(A,C,F,G,I,M,O) -> f18(3,0,F,G,I,M,O) True (1,1) 1. f10(A,C,F,G,I,M,O) -> f10(A,C,F,G,I,M,O) [0 >= A && A >= C] (?,1) 2. f10(A,C,F,G,I,M,O) -> f10(A,C,F,G,I,M,O) [A >= 1 && A >= C] (?,1) 3. f18(A,C,F,G,I,M,O) -> f25(A,C,D,-3,0,M,O) True (?,1) 4. f25(A,C,F,G,I,M,O) -> f25(A,C,F,G,I,M,O) [0 >= G && G >= I] (?,1) 5. f25(A,C,F,G,I,M,O) -> f25(A,C,F,G,I,M,O) [G >= 1 && G >= I] (?,1) 6. f33(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,3,0) True (?,1) 7. f40(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,M,O) [0 >= M && M >= O] (?,1) 8. f40(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,M,O) [M >= 1 && M >= O] (?,1) 9. f48(A,C,F,G,I,M,O) -> f52(A,C,F,G,I,M,O) [4 >= F] (?,1) 10. f48(A,C,F,G,I,M,O) -> f52(A,C,F,G,I,M,O) [F >= 5] (?,1) 11. f40(A,C,F,G,I,M,O) -> f48(A,C,F,G,I,M,O) [O >= 1 + M] (?,1) 12. f25(A,C,F,G,I,M,O) -> f33(A,C,F,G,I,M,O) [I >= 1 + G] (?,1) 13. f10(A,C,F,G,I,M,O) -> f18(A,C,F,G,I,M,O) [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: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1,2,13] * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,C,F,G,I,M,O) -> f18(3,0,F,G,I,M,O) True (1,1) 3. f18(A,C,F,G,I,M,O) -> f25(A,C,D,-3,0,M,O) True (?,1) 4. f25(A,C,F,G,I,M,O) -> f25(A,C,F,G,I,M,O) [0 >= G && G >= I] (?,1) 5. f25(A,C,F,G,I,M,O) -> f25(A,C,F,G,I,M,O) [G >= 1 && G >= I] (?,1) 6. f33(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,3,0) True (?,1) 7. f40(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,M,O) [0 >= M && M >= O] (?,1) 8. f40(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,M,O) [M >= 1 && M >= O] (?,1) 9. f48(A,C,F,G,I,M,O) -> f52(A,C,F,G,I,M,O) [4 >= F] (?,1) 10. f48(A,C,F,G,I,M,O) -> f52(A,C,F,G,I,M,O) [F >= 5] (?,1) 11. f40(A,C,F,G,I,M,O) -> f48(A,C,F,G,I,M,O) [O >= 1 + M] (?,1) 12. f25(A,C,F,G,I,M,O) -> f33(A,C,F,G,I,M,O) [I >= 1 + G] (?,1) Signature: {(f0,18);(f10,18);(f18,18);(f25,18);(f33,18);(f40,18);(f48,18);(f52,18)} Flow Graph: [0->{3},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}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(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 4: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,C,F,G,I,M,O) -> f18(3,0,F,G,I,M,O) True (1,1) 3. f18(A,C,F,G,I,M,O) -> f25(A,C,D,-3,0,M,O) True (?,1) 4. f25(A,C,F,G,I,M,O) -> f25(A,C,F,G,I,M,O) [0 >= G && G >= I] (?,1) 5. f25(A,C,F,G,I,M,O) -> f25(A,C,F,G,I,M,O) [G >= 1 && G >= I] (?,1) 6. f33(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,3,0) True (?,1) 7. f40(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,M,O) [0 >= M && M >= O] (?,1) 8. f40(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,M,O) [M >= 1 && M >= O] (?,1) 9. f48(A,C,F,G,I,M,O) -> f52(A,C,F,G,I,M,O) [4 >= F] (?,1) 10. f48(A,C,F,G,I,M,O) -> f52(A,C,F,G,I,M,O) [F >= 5] (?,1) 11. f40(A,C,F,G,I,M,O) -> f48(A,C,F,G,I,M,O) [O >= 1 + M] (?,1) 12. f25(A,C,F,G,I,M,O) -> f33(A,C,F,G,I,M,O) [I >= 1 + G] (?,1) Signature: {(f0,18);(f10,18);(f18,18);(f25,18);(f33,18);(f40,18);(f48,18);(f52,18)} Flow Graph: [0->{3},3->{12},4->{4},5->{5},6->{8},7->{7},8->{8},9->{},10->{},11->{9,10},12->{6}] + Applied Processor: FromIts + Details: () * Step 5: Unfold MAYBE + Considered Problem: Rules: f0(A,C,F,G,I,M,O) -> f18(3,0,F,G,I,M,O) True f18(A,C,F,G,I,M,O) -> f25(A,C,D,-3,0,M,O) True f25(A,C,F,G,I,M,O) -> f25(A,C,F,G,I,M,O) [0 >= G && G >= I] f25(A,C,F,G,I,M,O) -> f25(A,C,F,G,I,M,O) [G >= 1 && G >= I] f33(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,3,0) True f40(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,M,O) [0 >= M && M >= O] f40(A,C,F,G,I,M,O) -> f40(A,C,F,G,I,M,O) [M >= 1 && M >= O] f48(A,C,F,G,I,M,O) -> f52(A,C,F,G,I,M,O) [4 >= F] f48(A,C,F,G,I,M,O) -> f52(A,C,F,G,I,M,O) [F >= 5] f40(A,C,F,G,I,M,O) -> f48(A,C,F,G,I,M,O) [O >= 1 + M] f25(A,C,F,G,I,M,O) -> f33(A,C,F,G,I,M,O) [I >= 1 + G] Signature: {(f0,18);(f10,18);(f18,18);(f25,18);(f33,18);(f40,18);(f48,18);(f52,18)} Rule Graph: [0->{3},3->{12},4->{4},5->{5},6->{8},7->{7},8->{8},9->{},10->{},11->{9,10},12->{6}] + Applied Processor: Unfold + Details: () * Step 6: AddSinks MAYBE + Considered Problem: Rules: f0.0(A,C,F,G,I,M,O) -> f18.3(3,0,F,G,I,M,O) True f18.3(A,C,F,G,I,M,O) -> f25.12(A,C,D,-3,0,M,O) True f25.4(A,C,F,G,I,M,O) -> f25.4(A,C,F,G,I,M,O) [0 >= G && G >= I] f25.5(A,C,F,G,I,M,O) -> f25.5(A,C,F,G,I,M,O) [G >= 1 && G >= I] f33.6(A,C,F,G,I,M,O) -> f40.8(A,C,F,G,I,3,0) True f40.7(A,C,F,G,I,M,O) -> f40.7(A,C,F,G,I,M,O) [0 >= M && M >= O] f40.8(A,C,F,G,I,M,O) -> f40.8(A,C,F,G,I,M,O) [M >= 1 && M >= O] f48.9(A,C,F,G,I,M,O) -> f52.13(A,C,F,G,I,M,O) [4 >= F] f48.10(A,C,F,G,I,M,O) -> f52.13(A,C,F,G,I,M,O) [F >= 5] f40.11(A,C,F,G,I,M,O) -> f48.9(A,C,F,G,I,M,O) [O >= 1 + M] f40.11(A,C,F,G,I,M,O) -> f48.10(A,C,F,G,I,M,O) [O >= 1 + M] f25.12(A,C,F,G,I,M,O) -> f33.6(A,C,F,G,I,M,O) [I >= 1 + G] Signature: {(f0.0,7) ;(f18.3,7) ;(f25.12,7) ;(f25.4,7) ;(f25.5,7) ;(f33.6,7) ;(f40.11,7) ;(f40.7,7) ;(f40.8,7) ;(f48.10,7) ;(f48.9,7) ;(f52.13,7)} Rule Graph: [0->{1},1->{11},2->{2},3->{3},4->{6},5->{5},6->{6},7->{},8->{},9->{7},10->{8},11->{4}] + Applied Processor: AddSinks + Details: () * Step 7: Failure MAYBE + Considered Problem: Rules: f0.0(A,C,F,G,I,M,O) -> f18.3(3,0,F,G,I,M,O) True f18.3(A,C,F,G,I,M,O) -> f25.12(A,C,D,-3,0,M,O) True f25.4(A,C,F,G,I,M,O) -> f25.4(A,C,F,G,I,M,O) [0 >= G && G >= I] f25.5(A,C,F,G,I,M,O) -> f25.5(A,C,F,G,I,M,O) [G >= 1 && G >= I] f33.6(A,C,F,G,I,M,O) -> f40.8(A,C,F,G,I,3,0) True f40.7(A,C,F,G,I,M,O) -> f40.7(A,C,F,G,I,M,O) [0 >= M && M >= O] f40.8(A,C,F,G,I,M,O) -> f40.8(A,C,F,G,I,M,O) [M >= 1 && M >= O] f48.9(A,C,F,G,I,M,O) -> f52.13(A,C,F,G,I,M,O) [4 >= F] f48.10(A,C,F,G,I,M,O) -> f52.13(A,C,F,G,I,M,O) [F >= 5] f40.11(A,C,F,G,I,M,O) -> f48.9(A,C,F,G,I,M,O) [O >= 1 + M] f40.11(A,C,F,G,I,M,O) -> f48.10(A,C,F,G,I,M,O) [O >= 1 + M] f25.12(A,C,F,G,I,M,O) -> f33.6(A,C,F,G,I,M,O) [I >= 1 + G] f52.13(A,C,F,G,I,M,O) -> exitus616(A,C,F,G,I,M,O) True f52.13(A,C,F,G,I,M,O) -> exitus616(A,C,F,G,I,M,O) True f40.7(A,C,F,G,I,M,O) -> exitus616(A,C,F,G,I,M,O) True f25.5(A,C,F,G,I,M,O) -> exitus616(A,C,F,G,I,M,O) True f25.4(A,C,F,G,I,M,O) -> exitus616(A,C,F,G,I,M,O) True f40.8(A,C,F,G,I,M,O) -> exitus616(A,C,F,G,I,M,O) True Signature: {(exitus616,7) ;(f0.0,7) ;(f18.3,7) ;(f25.12,7) ;(f25.4,7) ;(f25.5,7) ;(f33.6,7) ;(f40.11,7) ;(f40.7,7) ;(f40.8,7) ;(f48.10,7) ;(f48.9,7) ;(f52.13,7)} Rule Graph: [0->{1},1->{11},2->{2,16},3->{3,15},4->{6},5->{5,14},6->{6,17},7->{13},8->{12},9->{7},10->{8},11->{4}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | +- p:[5] c: [] | +- p:[3] c: [] | +- p:[2] c: [] | `- p:[6] c: [] MAYBE