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) -> f13(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B >= 0 && A >= B] (?,1) 4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f23(A,B,C,S,T,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 6. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1 + F,S,T,U,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] 9. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f46(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] 13. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] 14. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] 15. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f33(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] 16. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B >= 0 && B >= 1 + A] (?,1) Signature: {(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{3,16},2->{3,16},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16} ,9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: ArgumentFilter [3,6,7,8,11,12,13,14,15,16,17] + Details: We remove following argument positions: [3,6,7,8,11,12,13,14,15,16,17]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,E,F,J,K) -> f13(1,B,C,E,F,J,K) [A = 1] (1,1) 1. f0(A,B,C,E,F,J,K) -> f17(A,1,C,E,F,J,K) [0 >= A] (1,1) 2. f0(A,B,C,E,F,J,K) -> f17(A,1,C,E,F,J,K) [A >= 2] (1,1) 3. f17(A,B,C,E,F,J,K) -> f23(A,B,1 + B,T,1,J,K) [-1 + B >= 0 && A >= B] (?,1) 4. f23(A,B,C,E,F,J,K) -> f23(A,B,C,T,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 5. f33(A,B,C,E,F,J,K) -> f33(A,B,C,E,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 6. f46(A,B,C,E,F,J,K) -> f46(A,B,C,E,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 7. f60(A,B,C,E,F,J,K) -> f60(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] 8. f60(A,B,C,E,F,J,K) -> f17(A,1 + B,C,E,F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] 9. f46(A,B,C,E,F,J,K) -> f60(A,B,C,E,1,S,B) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] 10. f33(A,B,C,E,F,J,K) -> f13(A,B,A,E,F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] 11. f33(A,B,C,E,F,J,K) -> f46(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] 12. f33(A,B,C,E,F,J,K) -> f46(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] 13. f23(A,B,C,E,F,J,K) -> f33(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] 14. f23(A,B,C,E,F,J,K) -> f33(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] 15. f23(A,B,C,E,F,J,K) -> f33(A,B,C,0,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] 16. f17(A,B,C,E,F,J,K) -> f13(A,B,C,E,F,J,K) [-1 + B >= 0 && B >= 1 + A] (?,1) Signature: {(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{3,16},2->{3,16},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16} ,9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3) ,(2,16) ,(3,13) ,(3,14) ,(3,15) ,(11,9) ,(12,9) ,(13,10) ,(13,11) ,(13,12) ,(14,10) ,(14,11) ,(14,12) ,(15,10) ,(15,11) ,(15,12)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,B,C,E,F,J,K) -> f13(1,B,C,E,F,J,K) [A = 1] (1,1) 1. f0(A,B,C,E,F,J,K) -> f17(A,1,C,E,F,J,K) [0 >= A] (1,1) 2. f0(A,B,C,E,F,J,K) -> f17(A,1,C,E,F,J,K) [A >= 2] (1,1) 3. f17(A,B,C,E,F,J,K) -> f23(A,B,1 + B,T,1,J,K) [-1 + B >= 0 && A >= B] (?,1) 4. f23(A,B,C,E,F,J,K) -> f23(A,B,C,T,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 5. f33(A,B,C,E,F,J,K) -> f33(A,B,C,E,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 6. f46(A,B,C,E,F,J,K) -> f46(A,B,C,E,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 7. f60(A,B,C,E,F,J,K) -> f60(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] 8. f60(A,B,C,E,F,J,K) -> f17(A,1 + B,C,E,F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] 9. f46(A,B,C,E,F,J,K) -> f60(A,B,C,E,1,S,B) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] 10. f33(A,B,C,E,F,J,K) -> f13(A,B,A,E,F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] 11. f33(A,B,C,E,F,J,K) -> f46(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] 12. f33(A,B,C,E,F,J,K) -> f46(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] 13. f23(A,B,C,E,F,J,K) -> f33(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] 14. f23(A,B,C,E,F,J,K) -> f33(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] 15. f23(A,B,C,E,F,J,K) -> f33(A,B,C,0,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] 16. f17(A,B,C,E,F,J,K) -> f13(A,B,C,E,F,J,K) [-1 + B >= 0 && B >= 1 + A] (?,1) Signature: {(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Flow Graph: [0->{},1->{16},2->{3},3->{4},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16},9->{7,8},10->{} ,11->{6},12->{6},13->{5},14->{5},15->{5},16->{}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f0(A,B,C,E,F,J,K) -> f13(1,B,C,E,F,J,K) [A = 1] f0(A,B,C,E,F,J,K) -> f17(A,1,C,E,F,J,K) [0 >= A] f0(A,B,C,E,F,J,K) -> f17(A,1,C,E,F,J,K) [A >= 2] f17(A,B,C,E,F,J,K) -> f23(A,B,1 + B,T,1,J,K) [-1 + B >= 0 && A >= B] f23(A,B,C,E,F,J,K) -> f23(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33(A,B,C,E,F,J,K) -> f33(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f46(A,B,C,E,F,J,K) -> f46(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f60(A,B,C,E,F,J,K) -> f60(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] f60(A,B,C,E,F,J,K) -> f17(A,1 + B,C,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] f46(A,B,C,E,F,J,K) -> f60(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] f33(A,B,C,E,F,J,K) -> f13(A,B,A,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] f33(A,B,C,E,F,J,K) -> f46(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] f33(A,B,C,E,F,J,K) -> f46(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] f23(A,B,C,E,F,J,K) -> f33(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] f23(A,B,C,E,F,J,K) -> f33(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] f23(A,B,C,E,F,J,K) -> f33(A,B,C,0,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] f17(A,B,C,E,F,J,K) -> f13(A,B,C,E,F,J,K) [-1 + B >= 0 && B >= 1 + A] Signature: {(f0,18);(f13,18);(f17,18);(f23,18);(f33,18);(f46,18);(f60,18)} Rule Graph: [0->{},1->{16},2->{3},3->{4},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16},9->{7,8},10->{} ,11->{6},12->{6},13->{5},14->{5},15->{5},16->{}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f0.0(A,B,C,E,F,J,K) -> f13.17(1,B,C,E,F,J,K) [A = 1] f0.1(A,B,C,E,F,J,K) -> f17.16(A,1,C,E,F,J,K) [0 >= A] f0.2(A,B,C,E,F,J,K) -> f17.3(A,1,C,E,F,J,K) [A >= 2] f17.3(A,B,C,E,F,J,K) -> f23.4(A,B,1 + B,T,1,J,K) [-1 + B >= 0 && A >= B] f23.4(A,B,C,E,F,J,K) -> f23.4(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.13(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.14(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.15(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.10(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.11(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.12(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f46.6(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f46.6(A,B,C,E,F,J,K) -> f46.9(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f60.7(A,B,C,E,F,J,K) -> f60.7(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] f60.7(A,B,C,E,F,J,K) -> f60.8(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] f60.8(A,B,C,E,F,J,K) -> f17.3(A,1 + B,C,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] f60.8(A,B,C,E,F,J,K) -> f17.16(A,1 + B,C,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] f46.9(A,B,C,E,F,J,K) -> f60.7(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] f46.9(A,B,C,E,F,J,K) -> f60.8(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] f33.10(A,B,C,E,F,J,K) -> f13.17(A,B,A,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] f33.11(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] f33.12(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] f23.13(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] f23.14(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] f23.15(A,B,C,E,F,J,K) -> f33.5(A,B,C,0,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] f17.16(A,B,C,E,F,J,K) -> f13.17(A,B,C,E,F,J,K) [-1 + B >= 0 && B >= 1 + A] Signature: {(f0.0,7) ;(f0.1,7) ;(f0.2,7) ;(f13.17,7) ;(f17.16,7) ;(f17.3,7) ;(f23.13,7) ;(f23.14,7) ;(f23.15,7) ;(f23.4,7) ;(f33.10,7) ;(f33.11,7) ;(f33.12,7) ;(f33.5,7) ;(f46.6,7) ;(f46.9,7) ;(f60.7,7) ;(f60.8,7)} Rule Graph: [0->{},1->{26},2->{3},3->{4,5,6,7},4->{4,5,6,7},5->{23},6->{24},7->{25},8->{8,9,10,11},9->{20},10->{21} ,11->{22},12->{12,13},13->{18,19},14->{14,15},15->{16,17},16->{3},17->{26},18->{14,15},19->{16,17},20->{} ,21->{12,13},22->{12,13},23->{8,9,10,11},24->{8,9,10,11},25->{8,9,10,11},26->{}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose MAYBE + Considered Problem: Rules: f0.0(A,B,C,E,F,J,K) -> f13.17(1,B,C,E,F,J,K) [A = 1] f0.1(A,B,C,E,F,J,K) -> f17.16(A,1,C,E,F,J,K) [0 >= A] f0.2(A,B,C,E,F,J,K) -> f17.3(A,1,C,E,F,J,K) [A >= 2] f17.3(A,B,C,E,F,J,K) -> f23.4(A,B,1 + B,T,1,J,K) [-1 + B >= 0 && A >= B] f23.4(A,B,C,E,F,J,K) -> f23.4(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.13(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.14(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.15(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.10(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.11(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.12(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f46.6(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f46.6(A,B,C,E,F,J,K) -> f46.9(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f60.7(A,B,C,E,F,J,K) -> f60.7(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] f60.7(A,B,C,E,F,J,K) -> f60.8(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] f60.8(A,B,C,E,F,J,K) -> f17.3(A,1 + B,C,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] f60.8(A,B,C,E,F,J,K) -> f17.16(A,1 + B,C,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] f46.9(A,B,C,E,F,J,K) -> f60.7(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] f46.9(A,B,C,E,F,J,K) -> f60.8(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] f33.10(A,B,C,E,F,J,K) -> f13.17(A,B,A,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] f33.11(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] f33.12(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] f23.13(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] f23.14(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] f23.15(A,B,C,E,F,J,K) -> f33.5(A,B,C,0,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] f17.16(A,B,C,E,F,J,K) -> f13.17(A,B,C,E,F,J,K) [-1 + B >= 0 && B >= 1 + A] f13.17(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f13.17(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f13.17(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f13.17(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True Signature: {(exitus616,7) ;(f0.0,7) ;(f0.1,7) ;(f0.2,7) ;(f13.17,7) ;(f17.16,7) ;(f17.3,7) ;(f23.13,7) ;(f23.14,7) ;(f23.15,7) ;(f23.4,7) ;(f33.10,7) ;(f33.11,7) ;(f33.12,7) ;(f33.5,7) ;(f46.6,7) ;(f46.9,7) ;(f60.7,7) ;(f60.8,7)} Rule Graph: [0->{30},1->{26},2->{3},3->{4,5,6,7},4->{4,5,6,7},5->{23},6->{24},7->{25},8->{8,9,10,11},9->{20},10->{21} ,11->{22},12->{12,13},13->{18,19},14->{14,15},15->{16,17},16->{3},17->{26},18->{14,15},19->{16,17},20->{28} ,21->{12,13},22->{12,13},23->{8,9,10,11},24->{8,9,10,11},25->{8,9,10,11},26->{27,29}] + 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,18,19,20,21,22,23,24,25,26,27,28,29,30] | `- p:[3,16,15,14,18,13,12,21,10,8,23,5,4,24,6,25,7,22,11,19] c: [3,5,6,7,10,11,13,15,16,18,19,21,22,23,24,25] | +- p:[14] c: [14] | +- p:[12] c: [12] | +- p:[8] c: [8] | `- p:[4] c: [4] * Step 7: AbstractSize MAYBE + Considered Problem: (Rules: f0.0(A,B,C,E,F,J,K) -> f13.17(1,B,C,E,F,J,K) [A = 1] f0.1(A,B,C,E,F,J,K) -> f17.16(A,1,C,E,F,J,K) [0 >= A] f0.2(A,B,C,E,F,J,K) -> f17.3(A,1,C,E,F,J,K) [A >= 2] f17.3(A,B,C,E,F,J,K) -> f23.4(A,B,1 + B,T,1,J,K) [-1 + B >= 0 && A >= B] f23.4(A,B,C,E,F,J,K) -> f23.4(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.13(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.14(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f23.4(A,B,C,E,F,J,K) -> f23.15(A,B,C,T,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.10(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.11(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f33.5(A,B,C,E,F,J,K) -> f33.12(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f46.6(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f46.6(A,B,C,E,F,J,K) -> f46.9(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f60.7(A,B,C,E,F,J,K) -> f60.7(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] f60.7(A,B,C,E,F,J,K) -> f60.8(A,B,C,E,1 + F,J,-1 + K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && J >= F] f60.8(A,B,C,E,F,J,K) -> f17.3(A,1 + B,C,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] f60.8(A,B,C,E,F,J,K) -> f17.16(A,1 + B,C,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + K >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + A + B >= 0 && A + -1*K >= 0 && -1 + A >= 0 && F >= 1 + J] f46.9(A,B,C,E,F,J,K) -> f60.7(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] f46.9(A,B,C,E,F,J,K) -> f60.8(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B] f33.10(A,B,C,E,F,J,K) -> f13.17(A,B,A,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] f33.11(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] f33.12(A,B,C,E,F,J,K) -> f46.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] f23.13(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] f23.14(A,B,C,E,F,J,K) -> f33.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] f23.15(A,B,C,E,F,J,K) -> f33.5(A,B,C,0,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && -2 + B + F >= 0 && -2 + A + F >= 0 && 1 + B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] f17.16(A,B,C,E,F,J,K) -> f13.17(A,B,C,E,F,J,K) [-1 + B >= 0 && B >= 1 + A] f13.17(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f13.17(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f13.17(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f13.17(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True Signature: {(exitus616,7) ;(f0.0,7) ;(f0.1,7) ;(f0.2,7) ;(f13.17,7) ;(f17.16,7) ;(f17.3,7) ;(f23.13,7) ;(f23.14,7) ;(f23.15,7) ;(f23.4,7) ;(f33.10,7) ;(f33.11,7) ;(f33.12,7) ;(f33.5,7) ;(f46.6,7) ;(f46.9,7) ;(f60.7,7) ;(f60.8,7)} Rule Graph: [0->{30},1->{26},2->{3},3->{4,5,6,7},4->{4,5,6,7},5->{23},6->{24},7->{25},8->{8,9,10,11},9->{20},10->{21} ,11->{22},12->{12,13},13->{18,19},14->{14,15},15->{16,17},16->{3},17->{26},18->{14,15},19->{16,17},20->{28} ,21->{12,13},22->{12,13},23->{8,9,10,11},24->{8,9,10,11},25->{8,9,10,11},26->{27,29}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30] | `- p:[3,16,15,14,18,13,12,21,10,8,23,5,4,24,6,25,7,22,11,19] c: [3,5,6,7,10,11,13,15,16,18,19,21,22,23,24,25] | +- p:[14] c: [14] | +- p:[12] c: [12] | +- p:[8] c: [8] | `- p:[4] c: [4]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,E,F,J,K,0.0,0.0.0,0.0.1,0.0.2,0.0.3] f0.0 ~> f13.17 [A <= K, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f0.1 ~> f17.16 [A <= A, B <= K, C <= C, E <= E, F <= F, J <= J, K <= K] f0.2 ~> f17.3 [A <= A, B <= K, C <= C, E <= E, F <= F, J <= J, K <= K] f17.3 ~> f23.4 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J, K <= K] f23.4 ~> f23.4 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] f23.4 ~> f23.13 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] f23.4 ~> f23.14 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] f23.4 ~> f23.15 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] f33.5 ~> f33.5 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f33.5 ~> f33.10 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f33.5 ~> f33.11 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f33.5 ~> f33.12 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f46.6 ~> f46.6 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f46.6 ~> f46.9 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f60.7 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= A + F, J <= J, K <= A + F] f60.7 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= A + F, J <= J, K <= A + F] f60.8 ~> f17.3 [A <= A, B <= C, C <= C, E <= E, F <= F, J <= J, K <= K] f60.8 ~> f17.16 [A <= A, B <= C, C <= C, E <= E, F <= F, J <= J, K <= K] f46.9 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= unknown, K <= B] f46.9 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= unknown, K <= B] f33.10 ~> f13.17 [A <= A, B <= B, C <= A, E <= E, F <= F, J <= J, K <= K] f33.11 ~> f46.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f33.12 ~> f46.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f23.13 ~> f33.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f23.14 ~> f33.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f23.15 ~> f33.5 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J, K <= K] f17.16 ~> f13.17 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f13.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f13.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f13.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f13.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] + Loop: [0.0 <= K + A + B] f17.3 ~> f23.4 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J, K <= K] f60.8 ~> f17.3 [A <= A, B <= C, C <= C, E <= E, F <= F, J <= J, K <= K] f60.7 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= A + F, J <= J, K <= A + F] f60.7 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= A + F, J <= J, K <= A + F] f46.9 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= unknown, K <= B] f46.6 ~> f46.9 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f46.6 ~> f46.6 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f33.11 ~> f46.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f33.5 ~> f33.11 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f33.5 ~> f33.5 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f23.13 ~> f33.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f23.4 ~> f23.13 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] f23.4 ~> f23.4 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] f23.14 ~> f33.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f23.4 ~> f23.14 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] f23.15 ~> f33.5 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J, K <= K] f23.4 ~> f23.15 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] f33.12 ~> f46.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f33.5 ~> f33.12 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] f46.9 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= unknown, K <= B] + Loop: [0.0.0 <= F + J] f60.7 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= A + F, J <= J, K <= A + F] + Loop: [0.0.1 <= B + F] f46.6 ~> f46.6 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] + Loop: [0.0.2 <= B + F] f33.5 ~> f33.5 [A <= A, B <= B, C <= C, E <= E, F <= C, J <= J, K <= K] + Loop: [0.0.3 <= B + F] f23.4 ~> f23.4 [A <= A, B <= B, C <= C, E <= unknown, F <= C, J <= J, K <= K] + Applied Processor: AbstractFlow + Details: () * Step 9: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,E,F,J,K,0.0,0.0.0,0.0.1,0.0.2,0.0.3] f0.0 ~> f13.17 [K ~=> A] f0.1 ~> f17.16 [K ~=> B] f0.2 ~> f17.3 [K ~=> B] f17.3 ~> f23.4 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f23.4 ~> f23.4 [C ~=> F,huge ~=> E] f23.4 ~> f23.13 [C ~=> F,huge ~=> E] f23.4 ~> f23.14 [C ~=> F,huge ~=> E] f23.4 ~> f23.15 [C ~=> F,huge ~=> E] f33.5 ~> f33.5 [C ~=> F] f33.5 ~> f33.10 [C ~=> F] f33.5 ~> f33.11 [C ~=> F] f33.5 ~> f33.12 [C ~=> F] f46.6 ~> f46.6 [C ~=> F] f46.6 ~> f46.9 [C ~=> F] f60.7 ~> f60.7 [A ~+> F,A ~+> K,F ~+> F,F ~+> K] f60.7 ~> f60.8 [A ~+> F,A ~+> K,F ~+> F,F ~+> K] f60.8 ~> f17.3 [C ~=> B] f60.8 ~> f17.16 [C ~=> B] f46.9 ~> f60.7 [B ~=> K,K ~=> F,huge ~=> J] f46.9 ~> f60.8 [B ~=> K,K ~=> F,huge ~=> J] f33.10 ~> f13.17 [A ~=> C] f33.11 ~> f46.6 [K ~=> F] f33.12 ~> f46.6 [K ~=> F] f23.13 ~> f33.5 [K ~=> F] f23.14 ~> f33.5 [K ~=> F] f23.15 ~> f33.5 [K ~=> E,K ~=> F] f17.16 ~> f13.17 [] f13.17 ~> exitus616 [] f13.17 ~> exitus616 [] f13.17 ~> exitus616 [] f13.17 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f17.3 ~> f23.4 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f60.8 ~> f17.3 [C ~=> B] f60.7 ~> f60.8 [A ~+> F,A ~+> K,F ~+> F,F ~+> K] f60.7 ~> f60.7 [A ~+> F,A ~+> K,F ~+> F,F ~+> K] f46.9 ~> f60.7 [B ~=> K,K ~=> F,huge ~=> J] f46.6 ~> f46.9 [C ~=> F] f46.6 ~> f46.6 [C ~=> F] f33.11 ~> f46.6 [K ~=> F] f33.5 ~> f33.11 [C ~=> F] f33.5 ~> f33.5 [C ~=> F] f23.13 ~> f33.5 [K ~=> F] f23.4 ~> f23.13 [C ~=> F,huge ~=> E] f23.4 ~> f23.4 [C ~=> F,huge ~=> E] f23.14 ~> f33.5 [K ~=> F] f23.4 ~> f23.14 [C ~=> F,huge ~=> E] f23.15 ~> f33.5 [K ~=> E,K ~=> F] f23.4 ~> f23.15 [C ~=> F,huge ~=> E] f33.12 ~> f46.6 [K ~=> F] f33.5 ~> f33.12 [C ~=> F] f46.9 ~> f60.8 [B ~=> K,K ~=> F,huge ~=> J] + Loop: [F ~+> 0.0.0,J ~+> 0.0.0] f60.7 ~> f60.7 [A ~+> F,A ~+> K,F ~+> F,F ~+> K] + Loop: [B ~+> 0.0.1,F ~+> 0.0.1] f46.6 ~> f46.6 [C ~=> F] + Loop: [B ~+> 0.0.2,F ~+> 0.0.2] f33.5 ~> f33.5 [C ~=> F] + Loop: [B ~+> 0.0.3,F ~+> 0.0.3] f23.4 ~> f23.4 [C ~=> F,huge ~=> E] + Applied Processor: Lare + Details: Unknown bound. MAYBE