YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f10(S1,0,C,L1,0,F,G,H,I,J,K,L,M,N,O,P,Q1,X1,A2,Z1,U,V,Y1,B2,C2,Z,R1,B1,M1,N1,O1,P1,D2,H1,I1,T1,K1) [0 >= U1 && 0 >= V1 && 0 >= L1 && 0 >= W1] (1,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f1(2,B,C,L1,E,F,G,H,I,J,K,L,M,N,O,P,L1,O1,P1,O1,U,V,O1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,N1,M1) [L1 >= 2] (1,1) 2. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(H,R,0,L1,R,F,G,H,I,J,K,L,M,N,O,P,N1,O1,R1,M1,U,V,P1,S1,T1,Q1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) [-2 + Q >= 0 (?,1) && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && L1 >= 2 && R >= 1 && Q1 >= L1 && H >= L1 && C = 0] 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(H,R,0,L1,R,F,G,H,I,J,K,L,M,N,O,P,N1,O1,R1,M1,U,V,P1,S1,T1,Q1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) [-2 + Q >= 0 (?,1) && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && L1 >= 2 && 0 >= 1 + R && Q1 >= L1 && H >= L1 && C = 0] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f1(1 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,L1,S,N1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) [-2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] (?,1) 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && N1 >= 1 && P1 >= 1] 6. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && N1 >= 1 && 0 >= 1 + P1] 7. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && 0 >= 1 + N1 && P1 >= 1] 8. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && 0 >= 1 + N1 && 0 >= 1 + P1] 9. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && N1 >= 1 && P1 >= 1] 10. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && N1 >= 1 && 0 >= 1 + P1] 11. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && 0 >= 1 + N1 && P1 >= 1] 12. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && 0 >= 1 + N1 && 0 >= 1 + P1] 13. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,1 + H1,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,E,H1,0,E,0,E,E,H1,I1,J1,K1) [A + -1*H >= 0 (?,1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && N1 >= 2 && E >= 1 && L1 >= 2 && H >= 0 && B = 0] 14. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,1 + H1,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,E,H1,0,E,0,E,E,H1,I1,J1,K1) [A + -1*H >= 0 (?,1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && N1 >= 2 && 0 >= 1 + E && L1 >= 2 && H >= 0 && B = 0] 15. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && 0 >= 1 + N1 && C1 = 0] 16. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && N1 >= 1 && C1 = 0] 17. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && 0 >= 1 + N1 && C1 = 0] 18. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && N1 >= 1 && C1 = 0] 19. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && 0 >= 1 + N1 && C1 = 0] 20. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && N1 >= 1 && C1 = 0] 21. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && 0 >= 1 + N1 && C1 = 0] 22. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && N1 >= 1 && C1 = 0] 23. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f10(A,B,C,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,S1,Z,R1,B1,M1,N1,O1,P1,T1,H1,I1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && L1 >= 2 && H1 >= 0 && C1 = A1] Signature: {(f1,37);(f10,37);(f16,37);(f8,37);(f9,37)} Flow Graph: [0->{},1->{2,3,4},2->{5,6,7,8,9,10,11,12,13,14},3->{5,6,7,8,9,10,11,12,13,14},4->{2,3,4},5->{5,6,7,8,9,10 ,11,12,13,14},6->{5,6,7,8,9,10,11,12,13,14},7->{5,6,7,8,9,10,11,12,13,14},8->{5,6,7,8,9,10,11,12,13,14} ,9->{5,6,7,8,9,10,11,12,13,14},10->{5,6,7,8,9,10,11,12,13,14},11->{5,6,7,8,9,10,11,12,13,14},12->{5,6,7,8,9 ,10,11,12,13,14},13->{15,16,17,18,19,20,21,22,23},14->{15,16,17,18,19,20,21,22,23},15->{15,16,17,18,19,20,21 ,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23} ,19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19,20,21,22,23},21->{15,16,17,18,19,20,21,22,23},22->{15 ,16,17,18,19,20,21,22,23},23->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,13) ,(2,14) ,(3,13) ,(3,14) ,(5,14) ,(6,14) ,(7,13) ,(8,13) ,(9,14) ,(10,14) ,(11,13) ,(12,13) ,(13,21) ,(13,23) ,(14,22) ,(14,23) ,(21,22) ,(21,23) ,(22,21) ,(22,23)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f10(S1,0,C,L1,0,F,G,H,I,J,K,L,M,N,O,P,Q1,X1,A2,Z1,U,V,Y1,B2,C2,Z,R1,B1,M1,N1,O1,P1,D2,H1,I1,T1,K1) [0 >= U1 && 0 >= V1 && 0 >= L1 && 0 >= W1] (1,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f1(2,B,C,L1,E,F,G,H,I,J,K,L,M,N,O,P,L1,O1,P1,O1,U,V,O1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,N1,M1) [L1 >= 2] (1,1) 2. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(H,R,0,L1,R,F,G,H,I,J,K,L,M,N,O,P,N1,O1,R1,M1,U,V,P1,S1,T1,Q1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) [-2 + Q >= 0 (?,1) && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && L1 >= 2 && R >= 1 && Q1 >= L1 && H >= L1 && C = 0] 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(H,R,0,L1,R,F,G,H,I,J,K,L,M,N,O,P,N1,O1,R1,M1,U,V,P1,S1,T1,Q1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) [-2 + Q >= 0 (?,1) && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && L1 >= 2 && 0 >= 1 + R && Q1 >= L1 && H >= L1 && C = 0] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f1(1 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,L1,S,N1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) [-2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] (?,1) 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && N1 >= 1 && P1 >= 1] 6. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && N1 >= 1 && 0 >= 1 + P1] 7. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && 0 >= 1 + N1 && P1 >= 1] 8. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && 0 >= 1 + N1 && 0 >= 1 + P1] 9. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && N1 >= 1 && P1 >= 1] 10. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && N1 >= 1 && 0 >= 1 + P1] 11. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && 0 >= 1 + N1 && P1 >= 1] 12. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*H >= 0 (?,1) ,J1,K1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && 0 >= 1 + N1 && 0 >= 1 + P1] 13. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,1 + H1,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,E,H1,0,E,0,E,E,H1,I1,J1,K1) [A + -1*H >= 0 (?,1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && N1 >= 2 && E >= 1 && L1 >= 2 && H >= 0 && B = 0] 14. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,1 + H1,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,E,H1,0,E,0,E,E,H1,I1,J1,K1) [A + -1*H >= 0 (?,1) && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && N1 >= 2 && 0 >= 1 + E && L1 >= 2 && H >= 0 && B = 0] 15. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && 0 >= 1 + N1 && C1 = 0] 16. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && N1 >= 1 && C1 = 0] 17. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && 0 >= 1 + N1 && C1 = 0] 18. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && N1 >= 1 && C1 = 0] 19. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && 0 >= 1 + N1 && C1 = 0] 20. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && N1 >= 1 && C1 = 0] 21. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && 0 >= 1 + N1 && C1 = 0] 22. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && N1 >= 1 && C1 = 0] 23. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f10(A,B,C,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,S1,Z,R1,B1,M1,N1,O1,P1,T1,H1,I1,J1,K1) [A + -1*H >= 0 (?,1) && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && L1 >= 2 && H1 >= 0 && C1 = A1] Signature: {(f1,37);(f10,37);(f16,37);(f8,37);(f9,37)} Flow Graph: [0->{},1->{2,3,4},2->{5,6,7,8,9,10,11,12},3->{5,6,7,8,9,10,11,12},4->{2,3,4},5->{5,6,7,8,9,10,11,12,13} ,6->{5,6,7,8,9,10,11,12,13},7->{5,6,7,8,9,10,11,12,14},8->{5,6,7,8,9,10,11,12,14},9->{5,6,7,8,9,10,11,12,13} ,10->{5,6,7,8,9,10,11,12,13},11->{5,6,7,8,9,10,11,12,14},12->{5,6,7,8,9,10,11,12,14},13->{15,16,17,18,19,20 ,22},14->{15,16,17,18,19,20,21},15->{15,16,17,18,19,20,21,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16 ,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23},19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19 ,20,21,22,23},21->{15,16,17,18,19,20,21},22->{15,16,17,18,19,20,22},23->{}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f10(S1,0,C ,L1,0,F,G,H,I,J,K,L,M,N,O,P,Q1,X1,A2,Z1,U,V,Y1,B2,C2,Z,R1,B1,M1,N1,O1,P1,D2,H1,I1,T1 ,K1) [0 >= U1 && 0 >= V1 && 0 >= L1 && 0 >= W1] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f1(2,B,C,L1,E ,F,G,H,I,J,K,L,M,N,O,P,L1,O1,P1,O1,U,V,O1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,N1 ,M1) [L1 >= 2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(H,R,0,L1 ,R,F,G,H,I,J,K,L,M,N,O,P,N1,O1,R1,M1,U,V,P1,S1,T1,Q1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [-2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && L1 >= 2 && R >= 1 && Q1 >= L1 && H >= L1 && C = 0] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(H,R,0,L1 ,R,F,G,H,I,J,K,L,M,N,O,P,N1,O1,R1,M1,U,V,P1,S1,T1,Q1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [-2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && L1 >= 2 && 0 >= 1 + R && Q1 >= L1 && H >= L1 && C = 0] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f1(1 + A,B,C ,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,L1,S,N1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [-2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && N1 >= 1 && P1 >= 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && N1 >= 1 && 0 >= 1 + P1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && 0 >= 1 + N1 && P1 >= 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && 0 >= 1 + N1 && 0 >= 1 + P1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && N1 >= 1 && P1 >= 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && N1 >= 1 && 0 >= 1 + P1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && 0 >= 1 + N1 && P1 >= 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && 0 >= 1 + N1 && 0 >= 1 + P1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,1 + H1 ,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,E,H1,0,E,0,E,E,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && N1 >= 2 && E >= 1 && L1 >= 2 && H >= 0 && B = 0] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,1 + H1 ,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,E,H1,0,E,0,E,E,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && N1 >= 2 && 0 >= 1 + E && L1 >= 2 && H >= 0 && B = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && 0 >= 1 + N1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && N1 >= 1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && 0 >= 1 + N1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && N1 >= 1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && 0 >= 1 + N1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && N1 >= 1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && 0 >= 1 + N1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && N1 >= 1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f10(A,B,C,L1 ,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,S1,Z,R1,B1,M1,N1,O1,P1,T1,H1,I1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && L1 >= 2 && H1 >= 0 && C1 = A1] Signature: {(f1,37);(f10,37);(f16,37);(f8,37);(f9,37)} Rule Graph: [0->{},1->{2,3,4},2->{5,6,7,8,9,10,11,12},3->{5,6,7,8,9,10,11,12},4->{2,3,4},5->{5,6,7,8,9,10,11,12,13} ,6->{5,6,7,8,9,10,11,12,13},7->{5,6,7,8,9,10,11,12,14},8->{5,6,7,8,9,10,11,12,14},9->{5,6,7,8,9,10,11,12,13} ,10->{5,6,7,8,9,10,11,12,13},11->{5,6,7,8,9,10,11,12,14},12->{5,6,7,8,9,10,11,12,14},13->{15,16,17,18,19,20 ,22},14->{15,16,17,18,19,20,21},15->{15,16,17,18,19,20,21,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16 ,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23},19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19 ,20,21,22,23},21->{15,16,17,18,19,20,21},22->{15,16,17,18,19,20,22},23->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] | +- p:[4] c: [4] | +- p:[5,6,7,8,9,10,11,12] c: [12] | | | `- p:[5,6,7,8,9,10,11] c: [11] | | | `- p:[5,6,7,8,9,10] c: [10] | | | `- p:[5,6,7,8,9] c: [9] | | | `- p:[5,6,7,8] c: [8] | | | `- p:[5,6,7] c: [7] | | | `- p:[5,6] c: [6] | | | `- p:[5] c: [5] | `- p:[15,16,17,18,19,20,21,22] c: [22] | `- p:[15,16,17,18,19,20,21] c: [21] | `- p:[15,16,17,18,19,20] c: [20] | `- p:[15,16,17,18,19] c: [19] | `- p:[15,16,17,18] c: [18] | `- p:[15,16,17] c: [17] | `- p:[15,16] c: [16] | `- p:[15] c: [15] * Step 4: CloseWith YES + Considered Problem: (Rules: f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f10(S1,0,C ,L1,0,F,G,H,I,J,K,L,M,N,O,P,Q1,X1,A2,Z1,U,V,Y1,B2,C2,Z,R1,B1,M1,N1,O1,P1,D2,H1,I1,T1 ,K1) [0 >= U1 && 0 >= V1 && 0 >= L1 && 0 >= W1] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f1(2,B,C,L1,E ,F,G,H,I,J,K,L,M,N,O,P,L1,O1,P1,O1,U,V,O1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,N1 ,M1) [L1 >= 2] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(H,R,0,L1 ,R,F,G,H,I,J,K,L,M,N,O,P,N1,O1,R1,M1,U,V,P1,S1,T1,Q1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [-2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && L1 >= 2 && R >= 1 && Q1 >= L1 && H >= L1 && C = 0] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(H,R,0,L1 ,R,F,G,H,I,J,K,L,M,N,O,P,N1,O1,R1,M1,U,V,P1,S1,T1,Q1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [-2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && L1 >= 2 && 0 >= 1 + R && Q1 >= L1 && H >= L1 && C = 0] f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f1(1 + A,B,C ,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,L1,S,N1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [-2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && N1 >= 1 && P1 >= 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && N1 >= 1 && 0 >= 1 + P1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && 0 >= 1 + N1 && P1 >= 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && M1 >= 1 && 0 >= 1 + N1 && 0 >= 1 + P1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && N1 >= 1 && P1 >= 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && N1 >= 1 && 0 >= 1 + P1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && 0 >= 1 + N1 && P1 >= 1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f16(A,B,1 + C ,L1,N1,O1,G,-1 + H,I,J,K,L,B,P1,1 + C,-1 + H,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && H >= 0 && L1 >= 2 && 0 >= 1 + M1 && 0 >= 1 + N1 && 0 >= 1 + P1] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,1 + H1 ,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,E,H1,0,E,0,E,E,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && N1 >= 2 && E >= 1 && L1 >= 2 && H >= 0 && B = 0] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,1 + H1 ,L1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,E,H1,0,E,0,E,E,H1,I1,J1 ,K1) [A + -1*H >= 0 && -2 + C + H >= 0 && -2 + D >= 0 && -2 + C + D >= 0 && -4 + D + Z >= 0 && -4 + A + D >= 0 && C >= 0 && -2 + C + Z >= 0 && -2 + A + C >= 0 && -2 + Z >= 0 && -4 + A + Z >= 0 && -2 + A >= 0 && N1 >= 2 && 0 >= 1 + E && L1 >= 2 && H >= 0 && B = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && 0 >= 1 + N1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && N1 >= 1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && 0 >= 1 + N1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && N1 >= 1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && 0 >= 1 + N1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && N1 >= 1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && P1 >= 1 + A1 && H1 >= 0 && L1 >= 2 && N1 >= 1 + P1 && 0 >= 1 + N1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f8(A,0,C,L1 ,N1,O1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,0,N1,0,N1,A1,-1 + H1,-1 + H1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && A1 >= 1 + P1 && H1 >= 0 && L1 >= 2 && P1 >= 1 + N1 && N1 >= 1 && C1 = 0] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1) -> f10(A,B,C,L1 ,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,S1,Z,R1,B1,M1,N1,O1,P1,T1,H1,I1,J1 ,K1) [A + -1*H >= 0 && H >= 0 && -2 + D + H >= 0 && E1 + H >= 0 && -1*E1 + H >= 0 && C1 + H >= 0 && -1*C1 + H >= 0 && -2 + H + Z >= 0 && B + H >= 0 && -1*B + H >= 0 && -2 + A + H >= 0 && -2 + D >= 0 && -2 + D + E1 >= 0 && -2 + D + -1*E1 >= 0 && -2 + C1 + D >= 0 && -2 + -1*C1 + D >= 0 && -4 + D + Z >= 0 && -2 + B + D >= 0 && -2 + -1*B + D >= 0 && -4 + A + D >= 0 && -1 + C + -1*H1 >= 0 && B1 + -1*H1 >= 0 && A1 + -1*G1 >= 0 && -1*A1 + G1 >= 0 && -1*E1 >= 0 && C1 + -1*E1 >= 0 && -1*C1 + -1*E1 >= 0 && -2 + -1*E1 + Z >= 0 && B + -1*E1 >= 0 && -1*B + -1*E1 >= 0 && -2 + A + -1*E1 >= 0 && E1 >= 0 && C1 + E1 >= 0 && -1*C1 + E1 >= 0 && -2 + E1 + Z >= 0 && B + E1 >= 0 && -1*B + E1 >= 0 && -2 + A + E1 >= 0 && 1 + B1 + -1*C >= 0 && -1 + -1*B1 + C >= 0 && -1*C1 >= 0 && -2 + -1*C1 + Z >= 0 && B + -1*C1 >= 0 && -1*B + -1*C1 >= 0 && -2 + A + -1*C1 >= 0 && C1 >= 0 && -2 + C1 + Z >= 0 && B + C1 >= 0 && -1*B + C1 >= 0 && -2 + A + C1 >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -2 + -1*B + Z >= 0 && -4 + A + Z >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && L1 >= 2 && H1 >= 0 && C1 = A1] Signature: {(f1,37);(f10,37);(f16,37);(f8,37);(f9,37)} Rule Graph: [0->{},1->{2,3,4},2->{5,6,7,8,9,10,11,12},3->{5,6,7,8,9,10,11,12},4->{2,3,4},5->{5,6,7,8,9,10,11,12,13} ,6->{5,6,7,8,9,10,11,12,13},7->{5,6,7,8,9,10,11,12,14},8->{5,6,7,8,9,10,11,12,14},9->{5,6,7,8,9,10,11,12,13} ,10->{5,6,7,8,9,10,11,12,13},11->{5,6,7,8,9,10,11,12,14},12->{5,6,7,8,9,10,11,12,14},13->{15,16,17,18,19,20 ,22},14->{15,16,17,18,19,20,21},15->{15,16,17,18,19,20,21,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16 ,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23},19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19 ,20,21,22,23},21->{15,16,17,18,19,20,21},22->{15,16,17,18,19,20,22},23->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] | +- p:[4] c: [4] | +- p:[5,6,7,8,9,10,11,12] c: [12] | | | `- p:[5,6,7,8,9,10,11] c: [11] | | | `- p:[5,6,7,8,9,10] c: [10] | | | `- p:[5,6,7,8,9] c: [9] | | | `- p:[5,6,7,8] c: [8] | | | `- p:[5,6,7] c: [7] | | | `- p:[5,6] c: [6] | | | `- p:[5] c: [5] | `- p:[15,16,17,18,19,20,21,22] c: [22] | `- p:[15,16,17,18,19,20,21] c: [21] | `- p:[15,16,17,18,19,20] c: [20] | `- p:[15,16,17,18,19] c: [19] | `- p:[15,16,17,18] c: [18] | `- p:[15,16,17] c: [17] | `- p:[15,16] c: [16] | `- p:[15] c: [15]) + Applied Processor: CloseWith True + Details: () YES