YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [B >= 1 + A && C >= 1] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [B >= 1 + A && 0 >= C] (?,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,X,Y,Z,A1,B1,C1) -> f0(A,1 + B,E1,D1,E1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [A >= B && D1 >= 1 + C] (?,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,X,Y,Z,A1,B1,C1) -> f0(A,1 + B,C,D1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [A >= B && C >= D1] (?,1) 5. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 6. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] (?,1) 7. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] (?,1) 8. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 9. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f89(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] (?,1) 10. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,1 + L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] (?,1) 11. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] (?,1) 12. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] 13. f89(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 14. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] 15. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f74(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] 16. f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f80(A,B,C,D,E,F,G,D1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 18. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 19. f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] (?,1) 20. f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] (?,1) 21. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f188(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,D1,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 22. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f181(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] (?,1) 23. f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f171(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] 24. f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f173(A,B,C,D,E,F,G,D1,I,J,1 + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] 25. f188(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f201(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 26. f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f218(A,B,0,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,0,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 27. f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] 28. f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] 29. f218(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 30. f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 31. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f99(A,B,C,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] (?,1) 32. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] (?,1) 33. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 34. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f115(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,1,A1,B1,C1) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 35. f115(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f0,29) ;(f104,29) ;(f115,29) ;(f161,29) ;(f171,29) ;(f173,29) ;(f181,29) ;(f188,29) ;(f201,29) ;(f211,29) ;(f218,29) ;(f43,29) ;(f44,29) ;(f54,29) ;(f57,29) ;(f67,29) ;(f71,29) ;(f74,29) ;(f80,29) ;(f89,29) ;(f99,29) ;(start,29)} Flow Graph: [0->{1,2,3,4},1->{5},2->{},3->{1,2,3,4},4->{1,2,3,4},5->{6,7,31,32},6->{},7->{8},8->{9,10,11,12},9->{13} ,10->{9,10,11,12},11->{14,15},12->{14,15},13->{16},14->{9,10,11,12},15->{17},16->{19,20},17->{18},18->{14 ,15},19->{21,22},20->{23,24},21->{25},22->{21,22},23->{19,20},24->{23,24},25->{26,27,28},26->{29},27->{30} ,28->{30},29->{6,7,31,32},30->{6,7,31,32},31->{33},32->{8},33->{34},34->{35},35->{16}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(5,31),(5,32),(29,7),(29,32)] * Step 2: FromIts YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [B >= 1 + A && C >= 1] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [B >= 1 + A && 0 >= C] (?,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,X,Y,Z,A1,B1,C1) -> f0(A,1 + B,E1,D1,E1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [A >= B && D1 >= 1 + C] (?,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,X,Y,Z,A1,B1,C1) -> f0(A,1 + B,C,D1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [A >= B && C >= D1] (?,1) 5. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 6. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] (?,1) 7. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] (?,1) 8. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 9. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f89(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] (?,1) 10. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,1 + L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] (?,1) 11. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] (?,1) 12. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] 13. f89(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 14. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] 15. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f74(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] 16. f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f80(A,B,C,D,E,F,G,D1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 18. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 19. f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] (?,1) 20. f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] (?,1) 21. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f188(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,D1,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 22. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f181(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] (?,1) 23. f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f171(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] 24. f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f173(A,B,C,D,E,F,G,D1,I,J,1 + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] 25. f188(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f201(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 26. f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f218(A,B,0,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,0,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 27. f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] 28. f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] 29. f218(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 30. f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 31. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f99(A,B,C,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] (?,1) 32. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] (?,1) 33. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 34. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f115(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,1,A1,B1,C1) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 35. f115(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f0,29) ;(f104,29) ;(f115,29) ;(f161,29) ;(f171,29) ;(f173,29) ;(f181,29) ;(f188,29) ;(f201,29) ;(f211,29) ;(f218,29) ;(f43,29) ;(f44,29) ;(f54,29) ;(f57,29) ;(f67,29) ;(f71,29) ;(f74,29) ;(f80,29) ;(f89,29) ;(f99,29) ;(start,29)} Flow Graph: [0->{1,2,3,4},1->{5},2->{},3->{1,2,3,4},4->{1,2,3,4},5->{6,7},6->{},7->{8},8->{9,10,11,12},9->{13},10->{9 ,10,11,12},11->{14,15},12->{14,15},13->{16},14->{9,10,11,12},15->{17},16->{19,20},17->{18},18->{14,15} ,19->{21,22},20->{23,24},21->{25},22->{21,22},23->{19,20},24->{23,24},25->{26,27,28},26->{29},27->{30} ,28->{30},29->{6,31},30->{6,7,31,32},31->{33},32->{8},33->{34},34->{35},35->{16}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) True f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [B >= 1 + A && C >= 1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [B >= 1 + A && 0 >= C] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f0(A,1 + B,E1,D1,E1,F,G,H,I,J,K,L,M ,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [A >= B && D1 >= 1 + C] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f0(A,1 + B,C,D1,E,F,G,H,I,J,K,L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [A >= B && C >= D1] f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,1,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f89(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,1 + L,0,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f89(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f74(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f80(A,B,C,D,E,F,G,D1,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f188(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,D1,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f181(A,1 + B,C,D,E,F,G,H,I,J,K,L,M ,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f171(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M ,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f173(A,B,C,D,E,F,G,D1,I,J,1 + K,L,M ,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f188(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f201(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f218(A,B,0,D,E,F,G,H,0,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,0,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] f218(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f99(A,B,C,D,E,F,G,H,0,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f115(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,1,A1,B1 ,C1) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f115(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [-1*I >= 0 && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f0,29) ;(f104,29) ;(f115,29) ;(f161,29) ;(f171,29) ;(f173,29) ;(f181,29) ;(f188,29) ;(f201,29) ;(f211,29) ;(f218,29) ;(f43,29) ;(f44,29) ;(f54,29) ;(f57,29) ;(f67,29) ;(f71,29) ;(f74,29) ;(f80,29) ;(f89,29) ;(f99,29) ;(start,29)} Rule Graph: [0->{1,2,3,4},1->{5},2->{},3->{1,2,3,4},4->{1,2,3,4},5->{6,7},6->{},7->{8},8->{9,10,11,12},9->{13},10->{9 ,10,11,12},11->{14,15},12->{14,15},13->{16},14->{9,10,11,12},15->{17},16->{19,20},17->{18},18->{14,15} ,19->{21,22},20->{23,24},21->{25},22->{21,22},23->{19,20},24->{23,24},25->{26,27,28},26->{29},27->{30} ,28->{30},29->{6,31},30->{6,7,31,32},31->{33},32->{8},33->{34},34->{35},35->{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,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35] | +- p:[3,4] c: [4] | | | `- p:[3] c: [3] | `- p:[7,30,27,25,21,19,16,13,9,8,32,10,14,11,12,18,17,15,35,34,33,31,29,26,23,20,24,22,28] c: [26,29,31,33,34,35] | `- p:[7,30,27,25,21,19,16,13,9,8,32,10,14,11,12,18,17,15,23,20,24,22,28] c: [32] | `- p:[7,30,27,25,21,19,16,13,9,8,10,14,11,12,18,17,15,23,20,24,22,28] c: [7,8,21,25,27,28,30] | +- p:[10,14,11,12,18,17,15] c: [15,17,18] | | | `- p:[10,14,11,12] c: [11,12,14] | | | `- p:[10] c: [10] | +- p:[20,23,24] c: [24] | | | `- p:[20,23] c: [20,23] | `- p:[22] c: [22] * Step 4: CloseWith YES + Considered Problem: (Rules: start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) True f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [B >= 1 + A && C >= 1] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [B >= 1 + A && 0 >= C] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f0(A,1 + B,E1,D1,E1,F,G,H,I,J,K,L,M ,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [A >= B && D1 >= 1 + C] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f0(A,1 + B,C,D1,E,F,G,H,I,J,K,L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [A >= B && C >= D1] f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,1,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f89(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,1 + L,0,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f89(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f67(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f74(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f80(A,B,C,D,E,F,G,D1,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f71(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f171(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f188(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,D1,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f181(A,1 + B,C,D,E,F,G,H,I,J,K,L,M ,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f171(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M ,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f173(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f173(A,B,C,D,E,F,G,D1,I,J,1 + K,L,M ,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f188(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f201(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f218(A,B,0,D,E,F,G,H,0,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,0,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] f201(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] f218(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f211(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f54(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N ,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f99(A,B,C,D,E,F,G,H,0,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P ,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f115(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,1,A1,B1 ,C1) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f115(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f161(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1 ,C1) [-1*I >= 0 && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f0,29) ;(f104,29) ;(f115,29) ;(f161,29) ;(f171,29) ;(f173,29) ;(f181,29) ;(f188,29) ;(f201,29) ;(f211,29) ;(f218,29) ;(f43,29) ;(f44,29) ;(f54,29) ;(f57,29) ;(f67,29) ;(f71,29) ;(f74,29) ;(f80,29) ;(f89,29) ;(f99,29) ;(start,29)} Rule Graph: [0->{1,2,3,4},1->{5},2->{},3->{1,2,3,4},4->{1,2,3,4},5->{6,7},6->{},7->{8},8->{9,10,11,12},9->{13},10->{9 ,10,11,12},11->{14,15},12->{14,15},13->{16},14->{9,10,11,12},15->{17},16->{19,20},17->{18},18->{14,15} ,19->{21,22},20->{23,24},21->{25},22->{21,22},23->{19,20},24->{23,24},25->{26,27,28},26->{29},27->{30} ,28->{30},29->{6,31},30->{6,7,31,32},31->{33},32->{8},33->{34},34->{35},35->{16}] ,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,31,32,33,34,35] | +- p:[3,4] c: [4] | | | `- p:[3] c: [3] | `- p:[7,30,27,25,21,19,16,13,9,8,32,10,14,11,12,18,17,15,35,34,33,31,29,26,23,20,24,22,28] c: [26,29,31,33,34,35] | `- p:[7,30,27,25,21,19,16,13,9,8,32,10,14,11,12,18,17,15,23,20,24,22,28] c: [32] | `- p:[7,30,27,25,21,19,16,13,9,8,10,14,11,12,18,17,15,23,20,24,22,28] c: [7,8,21,25,27,28,30] | +- p:[10,14,11,12,18,17,15] c: [15,17,18] | | | `- p:[10,14,11,12] c: [11,12,14] | | | `- p:[10] c: [10] | +- p:[20,23,24] c: [24] | | | `- p:[20,23] c: [20,23] | `- p:[22] c: [22]) + Applied Processor: CloseWith True + Details: () YES