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,O1,P1,Q1 -> f0(A2,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3 [0 >= U2 && 0 >= Y1 && 0 >= V2] (1,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,X1,G2,O1,P1,E2,B2,S1,T1,U1,M2,L2) 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,O1,P1,Q1 -> f15(Y1,2,A2,C2,A2,F,G,H,I,Y1,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,X1,A2 [Y1 >= 2] (1,1) ,R1,S1,T1,U1,V1,W1) ,D2,P1,Q1,R1,S1,T1,U1,V1,W1) 2. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] 3. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] 4. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] 5. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] 6. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] 7. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] 8. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] 9. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] 10. f15(A,B,C,D,E,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,O1,P1,Q1 -> f15(A,1 + B,D,X1,D,Y1,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) ,R1,S1,T1,U1,V1,W1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 11. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] 12. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] 13. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] 14. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] 15. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] 16. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] 17. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] 18. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] 19. f13(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] 20. f13(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] 21. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] 22. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] 23. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] 24. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] 25. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] 26. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] 27. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] 28. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] 29. f10(A,B,C,D,E,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,O1,P1,Q1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1[I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && X1 >= 2 && K1 >= 0 && F1 = D1] Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49)} Flow Graph: [0->{},1->{2,3,4,5,6,7,8,9,10},2->{11,12,13,14,15,16,17,18,19,20},3->{11,12,13,14,15,16,17,18,19,20} ,4->{11,12,13,14,15,16,17,18,19,20},5->{11,12,13,14,15,16,17,18,19,20},6->{11,12,13,14,15,16,17,18,19,20} ,7->{11,12,13,14,15,16,17,18,19,20},8->{11,12,13,14,15,16,17,18,19,20},9->{11,12,13,14,15,16,17,18,19,20} ,10->{2,3,4,5,6,7,8,9,10},11->{11,12,13,14,15,16,17,18,19,20},12->{11,12,13,14,15,16,17,18,19,20},13->{11,12 ,13,14,15,16,17,18,19,20},14->{11,12,13,14,15,16,17,18,19,20},15->{11,12,13,14,15,16,17,18,19,20},16->{11,12 ,13,14,15,16,17,18,19,20},17->{11,12,13,14,15,16,17,18,19,20},18->{11,12,13,14,15,16,17,18,19,20},19->{21,22 ,23,24,25,26,27,28,29},20->{21,22,23,24,25,26,27,28,29},21->{21,22,23,24,25,26,27,28,29},22->{21,22,23,24,25 ,26,27,28,29},23->{21,22,23,24,25,26,27,28,29},24->{21,22,23,24,25,26,27,28,29},25->{21,22,23,24,25,26,27,28 ,29},26->{21,22,23,24,25,26,27,28,29},27->{21,22,23,24,25,26,27,28,29},28->{21,22,23,24,25,26,27,28,29} ,29->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,19) ,(2,20) ,(3,19) ,(3,20) ,(4,19) ,(4,20) ,(5,19) ,(5,20) ,(6,19) ,(6,20) ,(7,19) ,(7,20) ,(8,19) ,(8,20) ,(9,19) ,(9,20) ,(11,20) ,(12,20) ,(13,19) ,(14,19) ,(15,20) ,(16,20) ,(17,19) ,(18,19) ,(19,27) ,(19,29) ,(20,28) ,(20,29) ,(27,28) ,(27,29) ,(28,27) ,(28,29)] * 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,O1,P1,Q1 -> f0(A2,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3 [0 >= U2 && 0 >= Y1 && 0 >= V2] (1,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,X1,G2,O1,P1,E2,B2,S1,T1,U1,M2,L2) 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,O1,P1,Q1 -> f15(Y1,2,A2,C2,A2,F,G,H,I,Y1,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,X1,A2 [Y1 >= 2] (1,1) ,R1,S1,T1,U1,V1,W1) ,D2,P1,Q1,R1,S1,T1,U1,V1,W1) 2. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] 3. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] 4. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] 5. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] 6. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] 7. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] 8. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] 9. f15(A,B,C,D,E,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,O1,P1,Q1 -> f13(Y1,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [-2 + B >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,K1,L1,M1,F2,O1,P1,D2,J2,Z1,T2,M2,V1,W1) && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] 10. f15(A,B,C,D,E,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,O1,P1,Q1 -> f15(A,1 + B,D,X1,D,Y1,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) ,R1,S1,T1,U1,V1,W1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1) 11. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] 12. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] 13. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] 14. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] 15. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] 16. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] 17. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] 18. f13(A,B,C,D,E,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,O1,P1,Q1 -> f13(A,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1 [-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] 19. f13(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] 20. f13(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1[-2 + S1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,D2,S1,T1,U1,Z1,N2) && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] 21. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] 22. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] 23. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] 24. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] 25. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] 26. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] 27. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] 28. f10(A,B,C,D,E,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,O1,P1,Q1 -> f10(A,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1 [I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] 29. f10(A,B,C,D,E,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,O1,P1,Q1 -> f0(A,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1[I >= 0 (?,1) ,R1,S1,T1,U1,V1,W1) ,Q1,R1,S1,T1,U1,V1,W1) && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && X1 >= 2 && K1 >= 0 && F1 = D1] Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49)} Flow Graph: [0->{},1->{2,3,4,5,6,7,8,9,10},2->{11,12,13,14,15,16,17,18},3->{11,12,13,14,15,16,17,18},4->{11,12,13,14 ,15,16,17,18},5->{11,12,13,14,15,16,17,18},6->{11,12,13,14,15,16,17,18},7->{11,12,13,14,15,16,17,18},8->{11 ,12,13,14,15,16,17,18},9->{11,12,13,14,15,16,17,18},10->{2,3,4,5,6,7,8,9,10},11->{11,12,13,14,15,16,17,18 ,19},12->{11,12,13,14,15,16,17,18,19},13->{11,12,13,14,15,16,17,18,20},14->{11,12,13,14,15,16,17,18,20} ,15->{11,12,13,14,15,16,17,18,19},16->{11,12,13,14,15,16,17,18,19},17->{11,12,13,14,15,16,17,18,20},18->{11 ,12,13,14,15,16,17,18,20},19->{21,22,23,24,25,26,28},20->{21,22,23,24,25,26,27},21->{21,22,23,24,25,26,27,28 ,29},22->{21,22,23,24,25,26,27,28,29},23->{21,22,23,24,25,26,27,28,29},24->{21,22,23,24,25,26,27,28,29} ,25->{21,22,23,24,25,26,27,28,29},26->{21,22,23,24,25,26,27,28,29},27->{21,22,23,24,25,26,27},28->{21,22,23 ,24,25,26,28},29->{}] + 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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f0(A2 ,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3,K1,L1,X1 ,G2,O1,P1,E2,B2,S1,T1,U1,M2 ,L2) [0 >= U2 && 0 >= Y1 && 0 >= V2] 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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f15(Y1 ,2,A2,C2,A2,F,G,H,I,Y1,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,X1,A2,D2,P1,Q1,R1 ,S1,T1,U1,V1 ,W1) [Y1 >= 2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f15(A ,1 + B,D,X1,D,Y1,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && A >= 1 + B && B >= 0] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1,M1,N1,O1 ,P1,Q1,D2,S1,T1,U1,Z1 ,N2) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1,M1,N1,O1 ,P1,Q1,D2,S1,T1,U1,Z1 ,N2) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f0(A ,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && X1 >= 2 && K1 >= 0 && F1 = D1] Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49)} Rule Graph: [0->{},1->{2,3,4,5,6,7,8,9,10},2->{11,12,13,14,15,16,17,18},3->{11,12,13,14,15,16,17,18},4->{11,12,13,14 ,15,16,17,18},5->{11,12,13,14,15,16,17,18},6->{11,12,13,14,15,16,17,18},7->{11,12,13,14,15,16,17,18},8->{11 ,12,13,14,15,16,17,18},9->{11,12,13,14,15,16,17,18},10->{2,3,4,5,6,7,8,9,10},11->{11,12,13,14,15,16,17,18 ,19},12->{11,12,13,14,15,16,17,18,19},13->{11,12,13,14,15,16,17,18,20},14->{11,12,13,14,15,16,17,18,20} ,15->{11,12,13,14,15,16,17,18,19},16->{11,12,13,14,15,16,17,18,19},17->{11,12,13,14,15,16,17,18,20},18->{11 ,12,13,14,15,16,17,18,20},19->{21,22,23,24,25,26,28},20->{21,22,23,24,25,26,27},21->{21,22,23,24,25,26,27,28 ,29},22->{21,22,23,24,25,26,27,28,29},23->{21,22,23,24,25,26,27,28,29},24->{21,22,23,24,25,26,27,28,29} ,25->{21,22,23,24,25,26,27,28,29},26->{21,22,23,24,25,26,27,28,29},27->{21,22,23,24,25,26,27},28->{21,22,23 ,24,25,26,28},29->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29] | +- p:[10] c: [10] | +- p:[11,12,13,14,15,16,17,18] c: [18] | | | `- p:[11,12,13,14,15,16,17] c: [17] | | | `- p:[11,12,13,14,15,16] c: [16] | | | `- p:[11,12,13,14,15] c: [15] | | | `- p:[11,12,13,14] c: [14] | | | `- p:[11,12,13] c: [13] | | | `- p:[11,12] c: [12] | | | `- p:[11] c: [11] | `- p:[21,22,23,24,25,26,27,28] c: [28] | `- p:[21,22,23,24,25,26,27] c: [27] | `- p:[21,22,23,24,25,26] c: [26] | `- p:[21,22,23,24,25] c: [25] | `- p:[21,22,23,24] c: [24] | `- p:[21,22,23] c: [23] | `- p:[21,22] c: [22] | `- p:[21] c: [21] * 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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f0(A2 ,D2,C2,I2,H2,F,G,H,I,Y1,F2,0,J2,Z1,N2,O2,P2,Q2,R2,S2,T2,W2,X2,X,Y,K2,A1,B1,C1,C3,E1,B3,Y2,Z2,A3,D3,K1,L1,X1 ,G2,O1,P1,E2,B2,S1,T1,U1,M2 ,L2) [0 >= U2 && 0 >= Y1 && 0 >= V2] 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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f15(Y1 ,2,A2,C2,A2,F,G,H,I,Y1,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,X1,A2,D2,P1,Q1,R1 ,S1,T1,U1,V1 ,W1) [Y1 >= 2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && I2 >= 1] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && C >= 1 && 0 >= 1 + I2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && I2 >= 1] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && M2 >= 1 && 0 >= 1 + C && 0 >= 1 + I2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && I2 >= 1] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && C >= 1 && 0 >= 1 + I2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && I2 >= 1] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(Y1 ,C2,A2,H2,G2,F,G,H,I,X1,E2,I2,I2,K2,B2,0,N2,O2,P2,Q2,R2,S2,0,X,Y,C,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,F2 ,O1,P1,D2,J2,Z1,T2,M2,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && L2 >= 2 && Z1 >= L2 && X1 >= 2 && B >= A && B >= 0 && P1 >= 0 && 0 >= 1 + M2 && 0 >= 1 + C && 0 >= 1 + I2] f15(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f15(A ,1 + B,D,X1,D,Y1,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) [-2 + B >= 0 && -4 + B + J >= 0 && -2 + J >= 0 && A >= 1 + B && B >= 0] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && B2 >= 1] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && A2 >= 1 && 0 >= 1 + B2] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && B2 >= 1] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && Z1 >= 1 && 0 >= 1 + A2 && 0 >= 1 + B2] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && B2 >= 1] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && A2 >= 1 && 0 >= 1 + B2] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && B2 >= 1] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f13(A ,B,C,D,E,F,G,1 + H,-1 + I,X1,Y1,A2,A2,C2,D2,0,E2,F2,G2,H2,I2,J2,0,K2,Z,Z,B2,1 + H,-1 + I,D1,E1,F1,G1,H1,I1 ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1 ,W1) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && H >= 0 && I >= 0 && X1 >= 2 && 0 >= 1 + Z1 && 0 >= 1 + A2 && 0 >= 1 + B2] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1,M1,N1,O1 ,P1,Q1,D2,S1,T1,U1,Z1 ,N2) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && L >= 1 && Z = 0] f13(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,1 + K1,I,X1,Y1,L,A2,E2,F2,G2,H2,I2,J2,K2,B2,O2,P2,X,Y,C2,A1,B1,C1,L,K1,0,L,0,L,L,K1,L1,M1,N1,O1 ,P1,Q1,D2,S1,T1,U1,Z1 ,N2) [-2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + S1 + W >= 0 && -2 + S1 + -1*W >= 0 && -2 + P + S1 >= 0 && -2 + -1*P + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && P1 + W >= 0 && P1 + -1*W >= 0 && P + P1 >= 0 && -1*P + P1 >= 0 && -2 + J + P1 >= 0 && -1*W >= 0 && P + -1*W >= 0 && -1*P + -1*W >= 0 && -2 + J + -1*W >= 0 && W >= 0 && P + W >= 0 && -1*P + W >= 0 && -2 + J + W >= 0 && -1*P >= 0 && -2 + J + -1*P >= 0 && P >= 0 && -2 + J + P >= 0 && -2 + J >= 0 && Q2 >= 2 && X1 >= 2 && I >= 0 && H >= 0 && 0 >= 1 + L && Z = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && C2 >= 1 + D1 && K1 >= 0 && X1 >= 2 && Y1 >= 1 + C2 && 0 >= 1 + Y1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f10(A ,B,C,D,E,F,G,H,I,X1,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,A2,Y,Z,A1,B1,C1,D1,E1,0,Y1,0,Y1,D1,-1 + K1,-1 + K1,M1,N1,O1 ,P1,Q1,R1,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && D1 >= 1 + C2 && K1 >= 0 && X1 >= 2 && C2 >= 1 + Y1 && Y1 >= 1 && F1 = 0] f10(A,B,C,D,E,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,O1,P1,Q1 ,R1,S1,T1,U1,V1 ,W1) -> f0(A ,B,C,D,E,F,G,H,I,X1,Y1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,F2,E1,E2,A2,C2,D2,G2,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1 ,W1) [I >= 0 && -2 + I + S1 >= 0 && I + P1 >= 0 && H1 + I >= 0 && -1*H1 + I >= 0 && F1 + I >= 0 && -1*F1 + I >= 0 && -2 + I + J >= 0 && 1 + E1 + -1*H >= 0 && -1 + H + -1*K1 >= 0 && -1 + -1*E1 + H >= 0 && -2 + S1 >= 0 && -2 + P1 + S1 >= 0 && -2 + H1 + S1 >= 0 && -2 + -1*H1 + S1 >= 0 && -2 + F1 + S1 >= 0 && -2 + -1*F1 + S1 >= 0 && -4 + J + S1 >= 0 && P1 >= 0 && H1 + P1 >= 0 && -1*H1 + P1 >= 0 && F1 + P1 >= 0 && -1*F1 + P1 >= 0 && -2 + J + P1 >= 0 && E1 + -1*K1 >= 0 && D1 + -1*J1 >= 0 && -1*D1 + J1 >= 0 && -1*H1 >= 0 && F1 + -1*H1 >= 0 && -1*F1 + -1*H1 >= 0 && -2 + -1*H1 + J >= 0 && H1 >= 0 && F1 + H1 >= 0 && -1*F1 + H1 >= 0 && -2 + H1 + J >= 0 && -1*F1 >= 0 && -2 + -1*F1 + J >= 0 && F1 >= 0 && -2 + F1 + J >= 0 && -2 + J >= 0 && X1 >= 2 && K1 >= 0 && F1 = D1] Signature: {(f0,49);(f10,49);(f13,49);(f15,49);(f17,49)} Rule Graph: [0->{},1->{2,3,4,5,6,7,8,9,10},2->{11,12,13,14,15,16,17,18},3->{11,12,13,14,15,16,17,18},4->{11,12,13,14 ,15,16,17,18},5->{11,12,13,14,15,16,17,18},6->{11,12,13,14,15,16,17,18},7->{11,12,13,14,15,16,17,18},8->{11 ,12,13,14,15,16,17,18},9->{11,12,13,14,15,16,17,18},10->{2,3,4,5,6,7,8,9,10},11->{11,12,13,14,15,16,17,18 ,19},12->{11,12,13,14,15,16,17,18,19},13->{11,12,13,14,15,16,17,18,20},14->{11,12,13,14,15,16,17,18,20} ,15->{11,12,13,14,15,16,17,18,19},16->{11,12,13,14,15,16,17,18,19},17->{11,12,13,14,15,16,17,18,20},18->{11 ,12,13,14,15,16,17,18,20},19->{21,22,23,24,25,26,28},20->{21,22,23,24,25,26,27},21->{21,22,23,24,25,26,27,28 ,29},22->{21,22,23,24,25,26,27,28,29},23->{21,22,23,24,25,26,27,28,29},24->{21,22,23,24,25,26,27,28,29} ,25->{21,22,23,24,25,26,27,28,29},26->{21,22,23,24,25,26,27,28,29},27->{21,22,23,24,25,26,27},28->{21,22,23 ,24,25,26,28},29->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29] | +- p:[10] c: [10] | +- p:[11,12,13,14,15,16,17,18] c: [18] | | | `- p:[11,12,13,14,15,16,17] c: [17] | | | `- p:[11,12,13,14,15,16] c: [16] | | | `- p:[11,12,13,14,15] c: [15] | | | `- p:[11,12,13,14] c: [14] | | | `- p:[11,12,13] c: [13] | | | `- p:[11,12] c: [12] | | | `- p:[11] c: [11] | `- p:[21,22,23,24,25,26,27,28] c: [28] | `- p:[21,22,23,24,25,26,27] c: [27] | `- p:[21,22,23,24,25,26] c: [26] | `- p:[21,22,23,24,25] c: [25] | `- p:[21,22,23,24] c: [24] | `- p:[21,22,23] c: [23] | `- p:[21,22] c: [22] | `- p:[21] c: [21]) + Applied Processor: CloseWith True + Details: () YES