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,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] (?,1) 12. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] (?,1) 13. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] (?,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] (?,1) 15. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] (?,1) 16. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] (?,1) 17. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V,2 + W) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (?,1) 22. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] (?,1) Signature: {(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,19,20,21},5->{8,18},6->{8,18},7->{8,18},8->{9 ,10,11,12,13,17},9->{14,15,16},10->{14,15,16},11->{9,10,11,12,13,17},12->{9,10,11,12,13,17},13->{9,10,11,12 ,13,17},14->{9,10,11,12,13,17},15->{9,10,11,12,13,17},16->{9,10,11,12,13,17},17->{8,18},18->{5,6,7,19,20,21} ,19->{},20->{},21->{},22->{1,23},23->{5,6,7,19,20,21}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,19) ,(4,21) ,(11,9) ,(11,10) ,(11,12) ,(12,9) ,(12,10) ,(12,11) ,(12,13) ,(13,9) ,(13,10) ,(13,11) ,(13,13) ,(14,12) ,(15,11) ,(15,13) ,(16,11) ,(16,13) ,(23,5) ,(23,6) ,(23,7) ,(23,19) ,(23,21)] * 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,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] (?,1) 12. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] (?,1) 13. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] (?,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] (?,1) 15. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] (?,1) 16. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] (?,1) 17. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V,2 + W) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (?,1) 22. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] (?,1) Signature: {(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{14,15,16},10->{14,15,16},11->{11,13,17},12->{12,17},13->{12,17},14->{9,10,11,13,17},15->{9,10 ,12,17},16->{9,10,12,17},17->{8,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{20}] + 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,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [A = 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U ,V ,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [0 >= A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [A >= 2] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S ,T,U,V ,W) [0 >= I && H >= I] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S ,T,U,V ,W) [I >= 2 && H >= I] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V ,W) [H >= 1 && I = 1] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && 0 >= Q && J >= K] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && Q >= 2 && J >= K] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V ,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V ,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V ,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q ,X,Y,Z,A1,B1 ,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q ,X,Y,Z,A1,B1 ,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1 ,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V ,2 + W) [H + -1*I >= 0 && K >= 1 + J] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [0 >= 2 + A && I >= 1 + H] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [A >= 0 && I >= 1 + H] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [I >= 1 + H && 1 + A = 0] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] Signature: {(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Rule Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{14,15,16},10->{14,15,16},11->{11,13,17},12->{12,17},13->{12,17},14->{9,10,11,13,17},15->{9,10 ,12,17},16->{9,10,12,17},17->{8,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{20}] + 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,17,18,19,20,21,22,23] | +- p:[5,18,6,7,17,8,11,14,9,15,10,16,12,13] c: [5,6,7,18] | | | `- p:[8,17,11,14,9,15,10,16,12,13] c: [11] | | | `- p:[8,17,12,13,14,9,15,10,16] c: [12] | | | `- p:[8,17,13,14,9,15,10,16] c: [13] | | | `- p:[8,17,14,9,15,10,16] c: [14] | | | `- p:[8,17,15,9,16,10] c: [15] | | | `- p:[8,17,16,9,10] c: [9] | | | `- p:[8,17,16,10] c: [10,16] | | | `- p:[8,17] c: [8,17] | `- p:[1,22,2] c: [1,22] | `- p:[2] c: [2] * 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,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [A = 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U ,V ,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [0 >= A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [A >= 2] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S ,T,U,V ,W) [0 >= I && H >= I] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S ,T,U,V ,W) [I >= 2 && H >= I] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V ,W) [H >= 1 && I = 1] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && 0 >= Q && J >= K] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && Q >= 2 && J >= K] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V ,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V ,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V ,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q ,X,Y,Z,A1,B1 ,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q ,X,Y,Z,A1,B1 ,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1 ,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V ,2 + W) [H + -1*I >= 0 && K >= 1 + J] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [0 >= 2 + A && I >= 1 + H] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [A >= 0 && I >= 1 + H] f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [I >= 1 + H && 1 + A = 0] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] Signature: {(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Rule Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{14,15,16},10->{14,15,16},11->{11,13,17},12->{12,17},13->{12,17},14->{9,10,11,13,17},15->{9,10 ,12,17},16->{9,10,12,17},17->{8,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{20}] ,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] | +- p:[5,18,6,7,17,8,11,14,9,15,10,16,12,13] c: [5,6,7,18] | | | `- p:[8,17,11,14,9,15,10,16,12,13] c: [11] | | | `- p:[8,17,12,13,14,9,15,10,16] c: [12] | | | `- p:[8,17,13,14,9,15,10,16] c: [13] | | | `- p:[8,17,14,9,15,10,16] c: [14] | | | `- p:[8,17,15,9,16,10] c: [15] | | | `- p:[8,17,16,9,10] c: [9] | | | `- p:[8,17,16,10] c: [10,16] | | | `- p:[8,17] c: [8,17] | `- p:[1,22,2] c: [1,22] | `- p:[2] c: [2]) + Applied Processor: CloseWith True + Details: () YES