YES * Step 1: UnsatPaths YES + 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: 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 2: FromIts YES + 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->{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 3: Decompose YES + Considered Problem: Rules: 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] 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] 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] 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] 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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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] 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: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | `- p:[3,8,7,9,6,11,5,13,4,14,15,12] c: [15] | `- p:[3,8,7,9,6,11,5,13,4,14,12] c: [14] | `- p:[3,8,7,9,6,11,5,13,4,12] c: [13] | +- p:[5] c: [5] | +- p:[6] c: [6] | +- p:[7] c: [7] | `- p:[4] c: [4] * Step 4: CloseWith YES + Considered Problem: (Rules: 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] 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] 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] 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] 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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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 && -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,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] 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->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | `- p:[3,8,7,9,6,11,5,13,4,14,15,12] c: [15] | `- p:[3,8,7,9,6,11,5,13,4,14,12] c: [14] | `- p:[3,8,7,9,6,11,5,13,4,12] c: [13] | +- p:[5] c: [5] | +- p:[6] c: [6] | +- p:[7] c: [7] | `- p:[4] c: [4]) + Applied Processor: CloseWith True + Details: () YES