NO * Step 1: UnsatPaths NO + 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,X,Y) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [V >= 4 && A1 >= 0 && B1 >= 1] (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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [2 >= V && A1 >= 0 && B1 >= 1] (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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,3,1,B1,C1) [A1 >= 0 && B1 >= 1 && V = 3] (1,1) 3. f20(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) -> f26(A,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1*I >= 0 (?,1) && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && D >= 1 && 0 >= A] 4. f20(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) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1*I >= 0 (?,1) && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && 0 >= D && 0 >= A] 5. f20(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) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1*I >= 0 (?,1) && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && A >= 1] 6. f26(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) -> f26(A,B,1 + C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && E >= 1 + C && 0 >= Z && A1 >= 1] 7. f26(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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && E >= 1 + C && 0 >= Z && 0 >= A1] 8. f26(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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && Z >= 1 && E >= 1 + C] 9. f26(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) -> f68(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) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && C >= E] 10. f33(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) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && J >= 0] 11. f33(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) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && 0 >= 2 + J] 12. f33(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) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && 1 + J = 0] 13. f33(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) -> f39(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) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && H >= 1 + I] 14. f68(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) -> f71(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) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && U >= 1] 15. f68(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) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= U] 16. 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) -> 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) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && A + I >= 0 && 1 + -1*A + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && A + D >= 0 && 1 + -1*A + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && A + C >= 0 && -1*A + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + A + X >= 0 && -1*A + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + A + -1*W >= 0 && 2 + -1*A + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + A + W >= 0 && -1*A + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && A + U >= 0 && -1*A + U >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0] 17. f39(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) -> f68(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) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H] 18. f39(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,A1,N,O,B1,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && B1 >= 1 && A1 >= 1 && H >= 1 + I && 0 >= Z] 19. f39(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && H >= 1 + I && Z >= 1] 20. f39(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) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,C1,C1,B1,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= B1 && A1 >= 1 && H >= 1 + I && 0 >= Z] 21. f39(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) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,B1,B1,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= A1 && H >= 1 + I && 0 >= Z] 22. f52(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && 0 >= 1 + O] 23. f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,1,Z,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Q = 3] 24. f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Q >= 4] 25. f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && 2 >= Q] 26. f52(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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Z >= 2 && Q = 3] 27. f52(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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && 0 >= Z && Q = 3] 28. f59(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,10,Z,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + O >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + O >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + O >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + O >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + O >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + O + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + O + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + O + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && O + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + O >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + O >= 0 && B + -1*L >= 0 && O >= 0 && -1*L + O >= 0 && -1*L >= 0 && S >= 11] 29. f59(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,S,Z,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + O >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + O >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + O >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + O >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + O >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + O + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + O + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + O + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && O + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + O >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + O >= 0 && B + -1*L >= 0 && O >= 0 && -1*L + O >= 0 && -1*L >= 0 && 10 >= S] 30. f63(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) -> f26(A,B,1 + C,D,E,F,G,H,I,L,K,L,M,N,O,P,Q,R,S,T,1 + U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && 10 + I + -1*S >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && 9 + H + -1*S >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && 9 + E + -1*S >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && 10 + D + -1*S >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && 10 + C + -1*S >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 9 + -1*S + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 11 + -1*S + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && 9 + -1*S + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 10 + -1*S + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 11 + -1*B + -1*S >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && 10 + B + -1*S >= 0 && B + -1*L >= 0 && 10 + -1*S >= 0 && 10 + -1*L + -1*S >= 0 && -1*L >= 0 && O >= 0] 31. f63(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && 10 + I + -1*S >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && 9 + H + -1*S >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && 9 + E + -1*S >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && 10 + D + -1*S >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && 10 + C + -1*S >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 9 + -1*S + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 11 + -1*S + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && 9 + -1*S + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 10 + -1*S + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 11 + -1*B + -1*S >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && 10 + B + -1*S >= 0 && B + -1*L >= 0 && 10 + -1*S >= 0 && 10 + -1*L + -1*S >= 0 && -1*L >= 0 && 0 >= 1 + O] Signature: {(f0,25);(f20,25);(f26,25);(f33,25);(f39,25);(f52,25);(f59,25);(f63,25);(f68,25);(f71,25)} Flow Graph: [0->{3,4,5},1->{3,4,5},2->{3,4,5},3->{6,7,8,9},4->{6,7,8,9},5->{6,7,8,9},6->{6,7,8,9},7->{10,11,12,13} ,8->{10,11,12,13},9->{14,15},10->{10,11,12,13},11->{10,11,12,13},12->{17,18,19,20,21},13->{17,18,19,20,21} ,14->{16},15->{16},16->{16},17->{14,15},18->{6,7,8,9},19->{6,7,8,9},20->{22,23,24,25,26,27},21->{22,23,24,25 ,26,27},22->{6,7,8,9},23->{28,29},24->{28,29},25->{28,29},26->{14,15},27->{14,15},28->{30,31},29->{30,31} ,30->{6,7,8,9},31->{6,7,8,9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(10,11) ,(10,12) ,(10,13) ,(11,10) ,(11,12) ,(11,13) ,(12,18) ,(12,19) ,(12,20) ,(12,21) ,(13,17)] * Step 2: FromIts NO + 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,X,Y) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [V >= 4 && A1 >= 0 && B1 >= 1] (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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [2 >= V && A1 >= 0 && B1 >= 1] (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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,3,1,B1,C1) [A1 >= 0 && B1 >= 1 && V = 3] (1,1) 3. f20(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) -> f26(A,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1*I >= 0 (?,1) && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && D >= 1 && 0 >= A] 4. f20(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) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1*I >= 0 (?,1) && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && 0 >= D && 0 >= A] 5. f20(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) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1*I >= 0 (?,1) && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && A >= 1] 6. f26(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) -> f26(A,B,1 + C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && E >= 1 + C && 0 >= Z && A1 >= 1] 7. f26(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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && E >= 1 + C && 0 >= Z && 0 >= A1] 8. f26(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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && Z >= 1 && E >= 1 + C] 9. f26(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) -> f68(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) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && C >= E] 10. f33(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) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && J >= 0] 11. f33(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) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && 0 >= 2 + J] 12. f33(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) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && 1 + J = 0] 13. f33(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) -> f39(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) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && H >= 1 + I] 14. f68(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) -> f71(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) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && U >= 1] 15. f68(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) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= U] 16. 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) -> 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) [I >= 0 (?,1) && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && A + I >= 0 && 1 + -1*A + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && A + D >= 0 && 1 + -1*A + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && A + C >= 0 && -1*A + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + A + X >= 0 && -1*A + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + A + -1*W >= 0 && 2 + -1*A + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + A + W >= 0 && -1*A + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && A + U >= 0 && -1*A + U >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0] 17. f39(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) -> f68(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) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H] 18. f39(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,A1,N,O,B1,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && B1 >= 1 && A1 >= 1 && H >= 1 + I && 0 >= Z] 19. f39(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && H >= 1 + I && Z >= 1] 20. f39(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) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,C1,C1,B1,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= B1 && A1 >= 1 && H >= 1 + I && 0 >= Z] 21. f39(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) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,B1,B1,P,Q,R,S,T,U,V,W,X,Y) [I >= 0 (?,1) && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= A1 && H >= 1 + I && 0 >= Z] 22. f52(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && 0 >= 1 + O] 23. f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,1,Z,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Q = 3] 24. f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Q >= 4] 25. f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && 2 >= Q] 26. f52(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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Z >= 2 && Q = 3] 27. f52(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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && 0 >= Z && Q = 3] 28. f59(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,10,Z,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + O >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + O >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + O >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + O >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + O >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + O + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + O + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + O + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && O + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + O >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + O >= 0 && B + -1*L >= 0 && O >= 0 && -1*L + O >= 0 && -1*L >= 0 && S >= 11] 29. f59(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,S,Z,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + O >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + O >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + O >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + O >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + O >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + O + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + O + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + O + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && O + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + O >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + O >= 0 && B + -1*L >= 0 && O >= 0 && -1*L + O >= 0 && -1*L >= 0 && 10 >= S] 30. f63(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) -> f26(A,B,1 + C,D,E,F,G,H,I,L,K,L,M,N,O,P,Q,R,S,T,1 + U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && 10 + I + -1*S >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && 9 + H + -1*S >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && 9 + E + -1*S >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && 10 + D + -1*S >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && 10 + C + -1*S >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 9 + -1*S + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 11 + -1*S + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && 9 + -1*S + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 10 + -1*S + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 11 + -1*B + -1*S >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && 10 + B + -1*S >= 0 && B + -1*L >= 0 && 10 + -1*S >= 0 && 10 + -1*L + -1*S >= 0 && -1*L >= 0 && O >= 0] 31. f63(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [-1 + H + -1*I >= 0 (?,1) && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && 10 + I + -1*S >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && 9 + H + -1*S >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && 9 + E + -1*S >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && 10 + D + -1*S >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && 10 + C + -1*S >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 9 + -1*S + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 11 + -1*S + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && 9 + -1*S + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 10 + -1*S + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 11 + -1*B + -1*S >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && 10 + B + -1*S >= 0 && B + -1*L >= 0 && 10 + -1*S >= 0 && 10 + -1*L + -1*S >= 0 && -1*L >= 0 && 0 >= 1 + O] Signature: {(f0,25);(f20,25);(f26,25);(f33,25);(f39,25);(f52,25);(f59,25);(f63,25);(f68,25);(f71,25)} Flow Graph: [0->{3,4,5},1->{3,4,5},2->{3,4,5},3->{6,7,8,9},4->{6,7,8,9},5->{6,7,8,9},6->{6,7,8,9},7->{10,11,12,13} ,8->{10,11,12,13},9->{14,15},10->{10},11->{11},12->{17},13->{18,19,20,21},14->{16},15->{16},16->{16},17->{14 ,15},18->{6,7,8,9},19->{6,7,8,9},20->{22,23,24,25,26,27},21->{22,23,24,25,26,27},22->{6,7,8,9},23->{28,29} ,24->{28,29},25->{28,29},26->{14,15},27->{14,15},28->{30,31},29->{30,31},30->{6,7,8,9},31->{6,7,8,9}] + Applied Processor: FromIts + Details: () * Step 3: CloseWith NO + 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,X,Y) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0 ,V,1,B1 ,C1) [V >= 4 && A1 >= 0 && B1 >= 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V ,1,B1 ,C1) [2 >= V && A1 >= 0 && B1 >= 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,3 ,1,B1 ,C1) [A1 >= 0 && B1 >= 1 && V = 3] f20(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) -> f26(A,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [-1*I >= 0 && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && D >= 1 && 0 >= A] f20(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) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [-1*I >= 0 && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && 0 >= D && 0 >= A] f20(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) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [-1*I >= 0 && D + -1*I >= 0 && -1 + -1*I + X >= 0 && -1 + -1*I + W >= 0 && 1 + -1*I + -1*W >= 0 && -1*I + U >= 0 && -1*I + -1*U >= 0 && I >= 0 && D + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && I + -1*U >= 0 && D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && D + -1*U >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + -1*U + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + -1*U + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + -1*U + W >= 0 && -1*U >= 0 && U >= 0 && A >= 1] f26(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) -> f26(A,B,1 + C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X ,Y) [I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && E >= 1 + C && 0 >= Z && A1 >= 1] f26(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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W,X ,Y) [I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && E >= 1 + C && 0 >= Z && 0 >= A1] f26(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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W,X ,Y) [I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && Z >= 1 && E >= 1 + C] f26(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) -> f68(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) [I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && C >= E] f33(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) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U ,V,W,X ,Y) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && J >= 0] f33(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) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U ,V,W,X ,Y) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && 0 >= 2 + J] f33(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) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V ,W,X ,Y) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H && 1 + J = 0] f33(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) -> f39(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) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && H >= 1 + I] f68(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) -> f71(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) [I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && U >= 1] f68(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) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= U] 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) -> 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) [I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && A + I >= 0 && 1 + -1*A + I >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && A + D >= 0 && 1 + -1*A + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && A + C >= 0 && -1*A + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + A + X >= 0 && -1*A + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + A + -1*W >= 0 && 2 + -1*A + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + A + W >= 0 && -1*A + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && A + U >= 0 && -1*A + U >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0] f39(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) -> f68(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) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && I >= H] f39(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,A1,N,O,B1,Q,R,S,T ,U,V,W,X ,Y) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && B1 >= 1 && A1 >= 1 && H >= 1 + I && 0 >= Z] f39(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,M,N,O,P,Q,R,S,T,U ,V,W,X ,Y) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && H >= 1 + I && Z >= 1] f39(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) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,C1,C1,B1,Q,R,S,T,U ,V,W,X ,Y) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= B1 && A1 >= 1 && H >= 1 + I && 0 >= Z] f39(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) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,B1,B1,P,Q,R,S,T,U ,V,W,X ,Y) [I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 1 + -1*B >= 0 && B >= 0 && 0 >= A1 && H >= 1 + I && 0 >= Z] f52(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U ,V,W,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && 0 >= 1 + O] f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,1,Z,T,U,V,W ,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Q = 3] f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W ,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Q >= 4] f52(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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W ,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && 2 >= Q] f52(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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W ,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && Z >= 2 && Q = 3] f52(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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W ,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + -1*L >= 0 && -1*L >= 0 && O >= 0 && 0 >= Z && Q = 3] f59(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,10,Z,U,V ,W,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + O >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + O >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + O >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + O >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + O >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + O + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + O + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + O + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && O + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + O >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + O >= 0 && B + -1*L >= 0 && O >= 0 && -1*L + O >= 0 && -1*L >= 0 && S >= 11] f59(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) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,S,Z,U,V,W ,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && I + O >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && -1 + H + O >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -1 + E + O >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && D + O >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && C + O >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && -1 + O + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 1 + O + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && -1 + O + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && O + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 1 + -1*B + O >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && B + O >= 0 && B + -1*L >= 0 && O >= 0 && -1*L + O >= 0 && -1*L >= 0 && 10 >= S] f63(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) -> f26(A,B,1 + C,D,E,F,G,H,I,L,K,L,M,N,O,P,Q,R,S,T ,1 + U,V,W,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && 10 + I + -1*S >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && 9 + H + -1*S >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && 9 + E + -1*S >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && 10 + D + -1*S >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && 10 + C + -1*S >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 9 + -1*S + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 11 + -1*S + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && 9 + -1*S + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 10 + -1*S + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 11 + -1*B + -1*S >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && 10 + B + -1*S >= 0 && B + -1*L >= 0 && 10 + -1*S >= 0 && 10 + -1*L + -1*S >= 0 && -1*L >= 0 && O >= 0] f63(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) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U ,V,W,X ,Y) [-1 + H + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + E + I >= 0 && D + I >= 0 && C + I >= 0 && -1 + I + X >= 0 && -1 + I + W >= 0 && 1 + I + -1*W >= 0 && I + U >= 0 && B + I >= 0 && 1 + -1*B + I >= 0 && 10 + I + -1*S >= 0 && I + -1*L >= 0 && -1 + H >= 0 && -2 + E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -2 + H + X >= 0 && -2 + H + W >= 0 && H + -1*W >= 0 && -1 + H + U >= 0 && -1 + B + H >= 0 && -1*B + H >= 0 && 9 + H + -1*S >= 0 && -1 + H + -1*L >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -1 + C + E >= 0 && -1 + -1*C + E >= 0 && -2 + E + X >= 0 && -2 + E + W >= 0 && E + -1*W >= 0 && -1 + E + U >= 0 && -1 + E + -1*U >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && 9 + E + -1*S >= 0 && -1 + E + -1*L >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + D + X >= 0 && -1 + D + W >= 0 && 1 + D + -1*W >= 0 && D + U >= 0 && -1 + B + D >= 0 && 1 + -1*B + D >= 0 && 10 + D + -1*S >= 0 && D + -1*L >= 0 && C >= 0 && -1 + C + X >= 0 && -1 + C + W >= 0 && 1 + C + -1*W >= 0 && C + U >= 0 && C + -1*U >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && 10 + C + -1*S >= 0 && C + -1*L >= 0 && -1 + X >= 0 && -2 + W + X >= 0 && -1*W + X >= 0 && -1 + U + X >= 0 && -1 + B + X >= 0 && -1*B + X >= 0 && 9 + -1*S + X >= 0 && -1 + -1*L + X >= 0 && 1 + -1*W >= 0 && 1 + U + -1*W >= 0 && 1 + B + -1*W >= 0 && 2 + -1*B + -1*W >= 0 && 11 + -1*S + -1*W >= 0 && 1 + -1*L + -1*W >= 0 && -1 + W >= 0 && -1 + U + W >= 0 && -1 + B + W >= 0 && -1*B + W >= 0 && 9 + -1*S + W >= 0 && -1 + -1*L + W >= 0 && U >= 0 && B + U >= 0 && 1 + -1*B + U >= 0 && 10 + -1*S + U >= 0 && -1*L + U >= 0 && 1 + -1*B >= 0 && 11 + -1*B + -1*S >= 0 && 1 + -1*B + -1*L >= 0 && B >= 0 && 10 + B + -1*S >= 0 && B + -1*L >= 0 && 10 + -1*S >= 0 && 10 + -1*L + -1*S >= 0 && -1*L >= 0 && 0 >= 1 + O] Signature: {(f0,25);(f20,25);(f26,25);(f33,25);(f39,25);(f52,25);(f59,25);(f63,25);(f68,25);(f71,25)} Rule Graph: [0->{3,4,5},1->{3,4,5},2->{3,4,5},3->{6,7,8,9},4->{6,7,8,9},5->{6,7,8,9},6->{6,7,8,9},7->{10,11,12,13} ,8->{10,11,12,13},9->{14,15},10->{10},11->{11},12->{17},13->{18,19,20,21},14->{16},15->{16},16->{16},17->{14 ,15},18->{6,7,8,9},19->{6,7,8,9},20->{22,23,24,25,26,27},21->{22,23,24,25,26,27},22->{6,7,8,9},23->{28,29} ,24->{28,29},25->{28,29},26->{14,15},27->{14,15},28->{30,31},29->{30,31},30->{6,7,8,9},31->{6,7,8,9}] + Applied Processor: CloseWith False + Details: () NO