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