NO * Step 1: TrivialSCCs NO + Considered Problem: Rules: 0. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f20(Z2,Y2,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,E3,A1,B1,G3,H3,F3,I3,G1,M3,D3,J1,K1,C3,A3,B3,X2 [0 >= Z2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,L3,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,J3,K3,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 1. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f16(1,Y2,Z2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B3,A1,B1,X2,C3,E3,D3,G1,H1,I1,J1,K1,L1,M1,N1,O1 [E1 = A2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,F3,E1,E1,S1,T1,U1,V1,W1,X1,Y1,Z1,H3,I3,C2,D2,A3,A3,G2,H2,I2,J2,K2,G3,M2,N2,J3,P2,Q2,R2,S2,T2,U2,V2,W2) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f1(Y2,2,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,Y2,E1,B3,E1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[Y2 >= 2 && E1 = A2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,E1,B2,C2,D2,Z2,F2,G2,H2,I2,J2,K2,X2,2,C3,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 3. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(1,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I3,G3,J1,K1,E3,X2,C3,D3,H3 [Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && Q1 = 0 && R1 = 0 && A = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,Y2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,-1,0,Z2,A3,T2,U2,B3,Y2) 4. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(1,B,-1 + Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,F3,H3,J1,K1,G3,C3,D3 [Q1 + -1*R1 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,E3,I3,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,Z2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,-1,-1 + Y2,A3,B3,X2,Z2,V2 && -1*Q1 + R1 >= 0 ,W2) && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && Y2 >= 2 && Q1 = 0 && R1 = 0 && A = 1] 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f16(1,B,Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= C && Q1 = R1 && A = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,Q1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,E2,Z2,Z2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 6. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f18(A,Y2,Z2,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,X2,C3,E3,D3,G1,H1,I1,J1,K1,L1,M1,N1,O1 [2 + -1*M2 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,I3,D1,D1,S1,T1,U1,V1,W1,X1,Y2,B3,G3,H3,H,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C1 + -1*M2 >= 0 && B + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C1 + M2 >= 0 && -4 + B + M2 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + F1 >= 0 && -2 + C1 >= 0 && -4 + B + C1 >= 0 && -1*B + C1 >= 0 && -2 + B >= 0 && F3 >= A && B3 >= A && B >= C1 && A >= 2 && H >= A && H >= 0 && B >= 0 && D = 0] 7. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,E1,Y2,E1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [2 + -1*M2 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C1 + -1*M2 >= 0 && B + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C1 + M2 >= 0 && -4 + B + M2 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + F1 >= 0 && -2 + C1 >= 0 && -4 + B + C1 >= 0 && -1*B + C1 >= 0 && -2 + B >= 0 && B >= 0 && C1 >= 1 + B] 8. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f11(A,B,C,1 + J1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,J1,R1,R1,J1,K1,0,R1,0,R1 [2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,Z2,-1,Y2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && Z2 >= 0 && Y2 >= 0 && A >= 2 && C >= 1 && H >= 0 && Q1 = 0] 9. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f18(A,B,-1 + C,1 + D,E,F,G,-1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,1 + D,-1 + H,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2 && C2 + -1*M2 >= 0 ,S2,T2,U2,V2,W2) && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && A >= 2 && V >= 1 && H >= 0 && C = V] 10. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f27(A,B,C,Z2,E,F,G,Y2,I,J,K,L,M,N,O,P,Q,R,S,Z2,Y2,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && H >= 0 && 0 >= C] 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f20(Y2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,E3,C3,J1,K1,X2,Z2,A3,B3,D3[H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && H + I2 >= 0 && 1 + H + H2 >= 0 && -1 + H + -1*H2 >= 0 && G2 + H >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1 + C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 2 + I2 + -1*M2 >= 0 && 3 + H2 + -1*M2 >= 0 && 1 + -1*H2 + -1*M2 >= 0 && 2 + G2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 1 + C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -2 + I2 + M2 >= 0 && -1 + H2 + M2 >= 0 && -3 + -1*H2 + M2 >= 0 && -2 + G2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -3 + C + M2 >= 0 && -4 + A + M2 >= 0 && I2 >= 0 && 1 + H2 + I2 >= 0 && -1 + -1*H2 + I2 >= 0 && G2 + I2 >= 0 && -2 + C2 + I2 >= 0 && -2 + I2 + Z1 >= 0 && I2 + R1 >= 0 && I2 + -1*R1 >= 0 && I2 + Q1 >= 0 && I2 + -1*Q1 >= 0 && I2 + O1 >= 0 && I2 + -1*O1 >= 0 && I2 + N1 >= 0 && I2 + -1*N1 >= 0 && I2 + M1 >= 0 && I2 + -1*M1 >= 0 && I2 + L1 >= 0 && I2 + -1*L1 >= 0 && I1 + I2 >= 0 && -1*I1 + I2 >= 0 && H1 + I2 >= 0 && -1*H1 + I2 >= 0 && -1 + C + I2 >= 0 && -2 + A + I2 >= 0 && -1 + -1*H2 >= 0 && -1 + G2 + -1*H2 >= 0 && -3 + C2 + -1*H2 >= 0 && -3 + -1*H2 + Z1 >= 0 && -1 + -1*H2 + R1 >= 0 && -1 + -1*H2 + -1*R1 >= 0 && -1 + -1*H2 + Q1 >= 0 && -1 + -1*H2 + -1*Q1 >= 0 && -1 + -1*H2 + O1 >= 0 && -1 + -1*H2 + -1*O1 >= 0 && -1 + -1*H2 + N1 >= 0 && -1 + -1*H2 + -1*N1 >= 0 && -1 + -1*H2 + M1 >= 0 && -1 + -1*H2 + -1*M1 >= 0 && -1 + -1*H2 + L1 >= 0 && -1 + -1*H2 + -1*L1 >= 0 && -1 + -1*H2 + I1 >= 0 && -1 + -1*H2 + -1*I1 >= 0 && -1 + H1 + -1*H2 >= 0 && -1 + -1*H1 + -1*H2 >= 0 && -2 + C + -1*H2 >= 0 && -3 + A + -1*H2 >= 0 && 1 + H2 >= 0 && 1 + G2 + H2 >= 0 && -1 + C2 + H2 >= 0 && -1 + H2 + Z1 >= 0 && 1 + H2 + R1 >= 0 && 1 + H2 + -1*R1 >= 0 && 1 + H2 + Q1 >= 0 && 1 + H2 + -1*Q1 >= 0 && 1 + H2 + O1 >= 0 && 1 + H2 + -1*O1 >= 0 && 1 + H2 + N1 >= 0 && 1 + H2 + -1*N1 >= 0 && 1 + H2 + M1 >= 0 && 1 + H2 + -1*M1 >= 0 && 1 + H2 + L1 >= 0 && 1 + H2 + -1*L1 >= 0 && 1 + H2 + I1 >= 0 && 1 + H2 + -1*I1 >= 0 && 1 + H1 + H2 >= 0 && 1 + -1*H1 + H2 >= 0 && C + H2 >= 0 && -1 + A + H2 >= 0 && G2 >= 0 && -2 + C2 + G2 >= 0 && -2 + G2 + Z1 >= 0 && G2 + R1 >= 0 && G2 + -1*R1 >= 0 && G2 + Q1 >= 0 && G2 + -1*Q1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && G2 + N1 >= 0 && G2 + -1*N1 >= 0 && G2 + M1 >= 0 && G2 + -1*M1 >= 0 && G2 + L1 >= 0 && G2 + -1*L1 >= 0 && G2 + I1 >= 0 && G2 + -1*I1 >= 0 && G2 + H1 >= 0 && G2 + -1*H1 >= 0 && -1 + C + G2 >= 0 && -2 + A + G2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -3 + C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -3 + C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1 + C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1 + C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1 + C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1 + C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1 + C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1 + C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1 + C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1 + C + N1 >= 0 && -2 + A + N1 >= 0 && 1 + -1*D + G1 >= 0 && -1 + D + -1*J1 >= 0 && -1 + D + -1*G1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1 + C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1 + C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1 + C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1 + C + L1 >= 0 && -2 + A + L1 >= 0 && G1 + -1*J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1 + C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1 + C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1 + C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1 + C + H1 >= 0 && -2 + A + H1 >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && -2 + A >= 0 && J1 >= 0 && L1 = I1] 12. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I1,I1,-1 + J1,K1,0,R1,0,R1 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,-1 + J1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && H + I2 >= 0 && 1 + H + H2 >= 0 && -1 + H + -1*H2 >= 0 && G2 + H >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1 + C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 2 + I2 + -1*M2 >= 0 && 3 + H2 + -1*M2 >= 0 && 1 + -1*H2 + -1*M2 >= 0 && 2 + G2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 1 + C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -2 + I2 + M2 >= 0 && -1 + H2 + M2 >= 0 && -3 + -1*H2 + M2 >= 0 && -2 + G2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -3 + C + M2 >= 0 && -4 + A + M2 >= 0 && I2 >= 0 && 1 + H2 + I2 >= 0 && -1 + -1*H2 + I2 >= 0 && G2 + I2 >= 0 && -2 + C2 + I2 >= 0 && -2 + I2 + Z1 >= 0 && I2 + R1 >= 0 && I2 + -1*R1 >= 0 && I2 + Q1 >= 0 && I2 + -1*Q1 >= 0 && I2 + O1 >= 0 && I2 + -1*O1 >= 0 && I2 + N1 >= 0 && I2 + -1*N1 >= 0 && I2 + M1 >= 0 && I2 + -1*M1 >= 0 && I2 + L1 >= 0 && I2 + -1*L1 >= 0 && I1 + I2 >= 0 && -1*I1 + I2 >= 0 && H1 + I2 >= 0 && -1*H1 + I2 >= 0 && -1 + C + I2 >= 0 && -2 + A + I2 >= 0 && -1 + -1*H2 >= 0 && -1 + G2 + -1*H2 >= 0 && -3 + C2 + -1*H2 >= 0 && -3 + -1*H2 + Z1 >= 0 && -1 + -1*H2 + R1 >= 0 && -1 + -1*H2 + -1*R1 >= 0 && -1 + -1*H2 + Q1 >= 0 && -1 + -1*H2 + -1*Q1 >= 0 && -1 + -1*H2 + O1 >= 0 && -1 + -1*H2 + -1*O1 >= 0 && -1 + -1*H2 + N1 >= 0 && -1 + -1*H2 + -1*N1 >= 0 && -1 + -1*H2 + M1 >= 0 && -1 + -1*H2 + -1*M1 >= 0 && -1 + -1*H2 + L1 >= 0 && -1 + -1*H2 + -1*L1 >= 0 && -1 + -1*H2 + I1 >= 0 && -1 + -1*H2 + -1*I1 >= 0 && -1 + H1 + -1*H2 >= 0 && -1 + -1*H1 + -1*H2 >= 0 && -2 + C + -1*H2 >= 0 && -3 + A + -1*H2 >= 0 && 1 + H2 >= 0 && 1 + G2 + H2 >= 0 && -1 + C2 + H2 >= 0 && -1 + H2 + Z1 >= 0 && 1 + H2 + R1 >= 0 && 1 + H2 + -1*R1 >= 0 && 1 + H2 + Q1 >= 0 && 1 + H2 + -1*Q1 >= 0 && 1 + H2 + O1 >= 0 && 1 + H2 + -1*O1 >= 0 && 1 + H2 + N1 >= 0 && 1 + H2 + -1*N1 >= 0 && 1 + H2 + M1 >= 0 && 1 + H2 + -1*M1 >= 0 && 1 + H2 + L1 >= 0 && 1 + H2 + -1*L1 >= 0 && 1 + H2 + I1 >= 0 && 1 + H2 + -1*I1 >= 0 && 1 + H1 + H2 >= 0 && 1 + -1*H1 + H2 >= 0 && C + H2 >= 0 && -1 + A + H2 >= 0 && G2 >= 0 && -2 + C2 + G2 >= 0 && -2 + G2 + Z1 >= 0 && G2 + R1 >= 0 && G2 + -1*R1 >= 0 && G2 + Q1 >= 0 && G2 + -1*Q1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && G2 + N1 >= 0 && G2 + -1*N1 >= 0 && G2 + M1 >= 0 && G2 + -1*M1 >= 0 && G2 + L1 >= 0 && G2 + -1*L1 >= 0 && G2 + I1 >= 0 && G2 + -1*I1 >= 0 && G2 + H1 >= 0 && G2 + -1*H1 >= 0 && -1 + C + G2 >= 0 && -2 + A + G2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -3 + C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -3 + C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1 + C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1 + C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1 + C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1 + C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1 + C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1 + C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1 + C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1 + C + N1 >= 0 && -2 + A + N1 >= 0 && 1 + -1*D + G1 >= 0 && -1 + D + -1*J1 >= 0 && -1 + D + -1*G1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1 + C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1 + C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1 + C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1 + C + L1 >= 0 && -2 + A + L1 >= 0 && G1 + -1*J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1 + C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1 + C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1 + C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1 + C + H1 >= 0 && -2 + A + H1 >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && -2 + A >= 0 && A >= 2 && J1 >= 0 && C >= 1 && Q1 = 0 && R1 = O1 && N1 = 0 && M1 = O1 && L1 = 0] 13. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,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,1 + U1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,R1,R1,J1,K1,0,R1,0,R1 [2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,S1,U1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,Y2,-1,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && Y2 >= 0 && A >= 2 && 0 >= C && D >= 0 && H >= 0 && Q1 = 0] 14. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f18(A,B,Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z2,D,H,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && A >= 2 && D >= 0 && 0 >= Y && H >= 0] 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 -> f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,D3,X2,J1,K1,B3,Y2,Z2,A3,C3 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && 1 + H + K2 >= 0 && -1 + H + -1*K2 >= 0 && H + J2 >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1*C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 3 + K2 + -1*M2 >= 0 && 1 + -1*K2 + -1*M2 >= 0 && 2 + J2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -1 + K2 + M2 >= 0 && -3 + -1*K2 + M2 >= 0 && -2 + J2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -1 + -1*K2 >= 0 && -1 + J2 + -1*K2 >= 0 && -3 + C2 + -1*K2 >= 0 && -3 + -1*K2 + Z1 >= 0 && -1 + -1*K2 + R1 >= 0 && -1 + -1*K2 + -1*R1 >= 0 && -1 + -1*K2 + Q1 >= 0 && -1 + -1*K2 + -1*Q1 >= 0 && -1 + -1*K2 + O1 >= 0 && -1 + -1*K2 + -1*O1 >= 0 && -1 + -1*K2 + N1 >= 0 && -1 + -1*K2 + -1*N1 >= 0 && -1 + -1*K2 + M1 >= 0 && -1 + -1*K2 + -1*M1 >= 0 && -1 + -1*K2 + L1 >= 0 && -1 + -1*K2 + -1*L1 >= 0 && -1 + I1 + -1*K2 >= 0 && -1 + -1*I1 + -1*K2 >= 0 && -1 + H1 + -1*K2 >= 0 && -1 + -1*H1 + -1*K2 >= 0 && -1 + -1*C + -1*K2 >= 0 && -3 + A + -1*K2 >= 0 && 1 + K2 >= 0 && 1 + J2 + K2 >= 0 && -1 + C2 + K2 >= 0 && -1 + K2 + Z1 >= 0 && 1 + K2 + R1 >= 0 && 1 + K2 + -1*R1 >= 0 && 1 + K2 + Q1 >= 0 && 1 + K2 + -1*Q1 >= 0 && 1 + K2 + O1 >= 0 && 1 + K2 + -1*O1 >= 0 && 1 + K2 + N1 >= 0 && 1 + K2 + -1*N1 >= 0 && 1 + K2 + M1 >= 0 && 1 + K2 + -1*M1 >= 0 && 1 + K2 + L1 >= 0 && 1 + K2 + -1*L1 >= 0 && 1 + I1 + K2 >= 0 && 1 + -1*I1 + K2 >= 0 && 1 + H1 + K2 >= 0 && 1 + -1*H1 + K2 >= 0 && 1 + -1*C + K2 >= 0 && -1 + A + K2 >= 0 && J2 >= 0 && -2 + C2 + J2 >= 0 && -2 + J2 + Z1 >= 0 && J2 + R1 >= 0 && J2 + -1*R1 >= 0 && J2 + Q1 >= 0 && J2 + -1*Q1 >= 0 && J2 + O1 >= 0 && J2 + -1*O1 >= 0 && J2 + N1 >= 0 && J2 + -1*N1 >= 0 && J2 + M1 >= 0 && J2 + -1*M1 >= 0 && J2 + L1 >= 0 && J2 + -1*L1 >= 0 && I1 + J2 >= 0 && -1*I1 + J2 >= 0 && H1 + J2 >= 0 && -1*H1 + J2 >= 0 && -1*C + J2 >= 0 && -2 + A + J2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && T1 + -1*U1 >= 0 && -1 + D + -1*U1 >= 0 && -1 + D + -1*T1 >= 0 && 1 + -1*D + T1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1*C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1*C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1*C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1*C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1*C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1*C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1*C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1*C + N1 >= 0 && -2 + A + N1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1*C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1*C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1*C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1*C + L1 >= 0 && -2 + A + L1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1*C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1*C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1*C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1*C + H1 >= 0 && -2 + A + H1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && U1 >= 0 && L1 = I1] 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,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I1,I1,J1,K1,0,R1,0,R1,P1,0 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,R1,S1,T1,-1 + U1,V1,-1 + U1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && 1 + H + K2 >= 0 && -1 + H + -1*K2 >= 0 && H + J2 >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1*C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 3 + K2 + -1*M2 >= 0 && 1 + -1*K2 + -1*M2 >= 0 && 2 + J2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -1 + K2 + M2 >= 0 && -3 + -1*K2 + M2 >= 0 && -2 + J2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -1 + -1*K2 >= 0 && -1 + J2 + -1*K2 >= 0 && -3 + C2 + -1*K2 >= 0 && -3 + -1*K2 + Z1 >= 0 && -1 + -1*K2 + R1 >= 0 && -1 + -1*K2 + -1*R1 >= 0 && -1 + -1*K2 + Q1 >= 0 && -1 + -1*K2 + -1*Q1 >= 0 && -1 + -1*K2 + O1 >= 0 && -1 + -1*K2 + -1*O1 >= 0 && -1 + -1*K2 + N1 >= 0 && -1 + -1*K2 + -1*N1 >= 0 && -1 + -1*K2 + M1 >= 0 && -1 + -1*K2 + -1*M1 >= 0 && -1 + -1*K2 + L1 >= 0 && -1 + -1*K2 + -1*L1 >= 0 && -1 + I1 + -1*K2 >= 0 && -1 + -1*I1 + -1*K2 >= 0 && -1 + H1 + -1*K2 >= 0 && -1 + -1*H1 + -1*K2 >= 0 && -1 + -1*C + -1*K2 >= 0 && -3 + A + -1*K2 >= 0 && 1 + K2 >= 0 && 1 + J2 + K2 >= 0 && -1 + C2 + K2 >= 0 && -1 + K2 + Z1 >= 0 && 1 + K2 + R1 >= 0 && 1 + K2 + -1*R1 >= 0 && 1 + K2 + Q1 >= 0 && 1 + K2 + -1*Q1 >= 0 && 1 + K2 + O1 >= 0 && 1 + K2 + -1*O1 >= 0 && 1 + K2 + N1 >= 0 && 1 + K2 + -1*N1 >= 0 && 1 + K2 + M1 >= 0 && 1 + K2 + -1*M1 >= 0 && 1 + K2 + L1 >= 0 && 1 + K2 + -1*L1 >= 0 && 1 + I1 + K2 >= 0 && 1 + -1*I1 + K2 >= 0 && 1 + H1 + K2 >= 0 && 1 + -1*H1 + K2 >= 0 && 1 + -1*C + K2 >= 0 && -1 + A + K2 >= 0 && J2 >= 0 && -2 + C2 + J2 >= 0 && -2 + J2 + Z1 >= 0 && J2 + R1 >= 0 && J2 + -1*R1 >= 0 && J2 + Q1 >= 0 && J2 + -1*Q1 >= 0 && J2 + O1 >= 0 && J2 + -1*O1 >= 0 && J2 + N1 >= 0 && J2 + -1*N1 >= 0 && J2 + M1 >= 0 && J2 + -1*M1 >= 0 && J2 + L1 >= 0 && J2 + -1*L1 >= 0 && I1 + J2 >= 0 && -1*I1 + J2 >= 0 && H1 + J2 >= 0 && -1*H1 + J2 >= 0 && -1*C + J2 >= 0 && -2 + A + J2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && T1 + -1*U1 >= 0 && -1 + D + -1*U1 >= 0 && -1 + D + -1*T1 >= 0 && 1 + -1*D + T1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1*C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1*C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1*C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1*C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1*C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1*C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1*C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1*C + N1 >= 0 && -2 + A + N1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1*C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1*C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1*C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1*C + L1 >= 0 && -2 + A + L1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1*C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1*C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1*C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1*C + H1 >= 0 && -2 + A + H1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && A >= 2 && U1 >= 0 && 0 >= C && Q1 = 0 && R1 = O1 && N1 = 0 && M1 = O1 && L1 = 0] Signature: {(f1,75);(f11,75);(f13,75);(f16,75);(f18,75);(f19,75);(f20,75);(f27,75)} Flow Graph: [0->{},1->{3,4,5},2->{6,7},3->{},4->{},5->{3,4,5},6->{8,9,10},7->{6,7},8->{11,12},9->{8,9,10},10->{13,14} ,11->{},12->{11,12},13->{15,16},14->{8,9,10},15->{},16->{15,16}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths NO + Considered Problem: Rules: 0. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f20(Z2,Y2,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,E3,A1,B1,G3,H3,F3,I3,G1,M3,D3,J1,K1,C3,A3,B3,X2 [0 >= Z2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,L3,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,J3,K3,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 1. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f16(1,Y2,Z2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B3,A1,B1,X2,C3,E3,D3,G1,H1,I1,J1,K1,L1,M1,N1,O1 [E1 = A2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,F3,E1,E1,S1,T1,U1,V1,W1,X1,Y1,Z1,H3,I3,C2,D2,A3,A3,G2,H2,I2,J2,K2,G3,M2,N2,J3,P2,Q2,R2,S2,T2,U2,V2,W2) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f1(Y2,2,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,Y2,E1,B3,E1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[Y2 >= 2 && E1 = A2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,E1,B2,C2,D2,Z2,F2,G2,H2,I2,J2,K2,X2,2,C3,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 3. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(1,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I3,G3,J1,K1,E3,X2,C3,D3,H3 [Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && Q1 = 0 && R1 = 0 && A = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,Y2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,-1,0,Z2,A3,T2,U2,B3,Y2) 4. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(1,B,-1 + Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,F3,H3,J1,K1,G3,C3,D3 [Q1 + -1*R1 >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,E3,I3,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,Z2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,-1,-1 + Y2,A3,B3,X2,Z2,V2 && -1*Q1 + R1 >= 0 ,W2) && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && Y2 >= 2 && Q1 = 0 && R1 = 0 && A = 1] 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f16(1,B,Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= C && Q1 = R1 && A = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,Q1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,E2,Z2,Z2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 6. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f18(A,Y2,Z2,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,X2,C3,E3,D3,G1,H1,I1,J1,K1,L1,M1,N1,O1 [2 + -1*M2 >= 0 (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,I3,D1,D1,S1,T1,U1,V1,W1,X1,Y2,B3,G3,H3,H,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C1 + -1*M2 >= 0 && B + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C1 + M2 >= 0 && -4 + B + M2 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + F1 >= 0 && -2 + C1 >= 0 && -4 + B + C1 >= 0 && -1*B + C1 >= 0 && -2 + B >= 0 && F3 >= A && B3 >= A && B >= C1 && A >= 2 && H >= A && H >= 0 && B >= 0 && D = 0] 7. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,E1,Y2,E1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [2 + -1*M2 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C1 + -1*M2 >= 0 && B + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C1 + M2 >= 0 && -4 + B + M2 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + F1 >= 0 && -2 + C1 >= 0 && -4 + B + C1 >= 0 && -1*B + C1 >= 0 && -2 + B >= 0 && B >= 0 && C1 >= 1 + B] 8. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f11(A,B,C,1 + J1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,J1,R1,R1,J1,K1,0,R1,0,R1 [2 + -1*M2 >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,Z2,-1,Y2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && Z2 >= 0 && Y2 >= 0 && A >= 2 && C >= 1 && H >= 0 && Q1 = 0] 9. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f18(A,B,-1 + C,1 + D,E,F,G,-1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,1 + D,-1 + H,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2 && C2 + -1*M2 >= 0 ,S2,T2,U2,V2,W2) && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && A >= 2 && V >= 1 && H >= 0 && C = V] 10. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f27(A,B,C,Z2,E,F,G,Y2,I,J,K,L,M,N,O,P,Q,R,S,Z2,Y2,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && H >= 0 && 0 >= C] 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f20(Y2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,E3,C3,J1,K1,X2,Z2,A3,B3,D3[H >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && H + I2 >= 0 && 1 + H + H2 >= 0 && -1 + H + -1*H2 >= 0 && G2 + H >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1 + C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 2 + I2 + -1*M2 >= 0 && 3 + H2 + -1*M2 >= 0 && 1 + -1*H2 + -1*M2 >= 0 && 2 + G2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 1 + C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -2 + I2 + M2 >= 0 && -1 + H2 + M2 >= 0 && -3 + -1*H2 + M2 >= 0 && -2 + G2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -3 + C + M2 >= 0 && -4 + A + M2 >= 0 && I2 >= 0 && 1 + H2 + I2 >= 0 && -1 + -1*H2 + I2 >= 0 && G2 + I2 >= 0 && -2 + C2 + I2 >= 0 && -2 + I2 + Z1 >= 0 && I2 + R1 >= 0 && I2 + -1*R1 >= 0 && I2 + Q1 >= 0 && I2 + -1*Q1 >= 0 && I2 + O1 >= 0 && I2 + -1*O1 >= 0 && I2 + N1 >= 0 && I2 + -1*N1 >= 0 && I2 + M1 >= 0 && I2 + -1*M1 >= 0 && I2 + L1 >= 0 && I2 + -1*L1 >= 0 && I1 + I2 >= 0 && -1*I1 + I2 >= 0 && H1 + I2 >= 0 && -1*H1 + I2 >= 0 && -1 + C + I2 >= 0 && -2 + A + I2 >= 0 && -1 + -1*H2 >= 0 && -1 + G2 + -1*H2 >= 0 && -3 + C2 + -1*H2 >= 0 && -3 + -1*H2 + Z1 >= 0 && -1 + -1*H2 + R1 >= 0 && -1 + -1*H2 + -1*R1 >= 0 && -1 + -1*H2 + Q1 >= 0 && -1 + -1*H2 + -1*Q1 >= 0 && -1 + -1*H2 + O1 >= 0 && -1 + -1*H2 + -1*O1 >= 0 && -1 + -1*H2 + N1 >= 0 && -1 + -1*H2 + -1*N1 >= 0 && -1 + -1*H2 + M1 >= 0 && -1 + -1*H2 + -1*M1 >= 0 && -1 + -1*H2 + L1 >= 0 && -1 + -1*H2 + -1*L1 >= 0 && -1 + -1*H2 + I1 >= 0 && -1 + -1*H2 + -1*I1 >= 0 && -1 + H1 + -1*H2 >= 0 && -1 + -1*H1 + -1*H2 >= 0 && -2 + C + -1*H2 >= 0 && -3 + A + -1*H2 >= 0 && 1 + H2 >= 0 && 1 + G2 + H2 >= 0 && -1 + C2 + H2 >= 0 && -1 + H2 + Z1 >= 0 && 1 + H2 + R1 >= 0 && 1 + H2 + -1*R1 >= 0 && 1 + H2 + Q1 >= 0 && 1 + H2 + -1*Q1 >= 0 && 1 + H2 + O1 >= 0 && 1 + H2 + -1*O1 >= 0 && 1 + H2 + N1 >= 0 && 1 + H2 + -1*N1 >= 0 && 1 + H2 + M1 >= 0 && 1 + H2 + -1*M1 >= 0 && 1 + H2 + L1 >= 0 && 1 + H2 + -1*L1 >= 0 && 1 + H2 + I1 >= 0 && 1 + H2 + -1*I1 >= 0 && 1 + H1 + H2 >= 0 && 1 + -1*H1 + H2 >= 0 && C + H2 >= 0 && -1 + A + H2 >= 0 && G2 >= 0 && -2 + C2 + G2 >= 0 && -2 + G2 + Z1 >= 0 && G2 + R1 >= 0 && G2 + -1*R1 >= 0 && G2 + Q1 >= 0 && G2 + -1*Q1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && G2 + N1 >= 0 && G2 + -1*N1 >= 0 && G2 + M1 >= 0 && G2 + -1*M1 >= 0 && G2 + L1 >= 0 && G2 + -1*L1 >= 0 && G2 + I1 >= 0 && G2 + -1*I1 >= 0 && G2 + H1 >= 0 && G2 + -1*H1 >= 0 && -1 + C + G2 >= 0 && -2 + A + G2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -3 + C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -3 + C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1 + C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1 + C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1 + C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1 + C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1 + C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1 + C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1 + C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1 + C + N1 >= 0 && -2 + A + N1 >= 0 && 1 + -1*D + G1 >= 0 && -1 + D + -1*J1 >= 0 && -1 + D + -1*G1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1 + C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1 + C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1 + C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1 + C + L1 >= 0 && -2 + A + L1 >= 0 && G1 + -1*J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1 + C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1 + C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1 + C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1 + C + H1 >= 0 && -2 + A + H1 >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && -2 + A >= 0 && J1 >= 0 && L1 = I1] 12. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I1,I1,-1 + J1,K1,0,R1,0,R1 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,-1 + J1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && H + I2 >= 0 && 1 + H + H2 >= 0 && -1 + H + -1*H2 >= 0 && G2 + H >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1 + C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 2 + I2 + -1*M2 >= 0 && 3 + H2 + -1*M2 >= 0 && 1 + -1*H2 + -1*M2 >= 0 && 2 + G2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 1 + C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -2 + I2 + M2 >= 0 && -1 + H2 + M2 >= 0 && -3 + -1*H2 + M2 >= 0 && -2 + G2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -3 + C + M2 >= 0 && -4 + A + M2 >= 0 && I2 >= 0 && 1 + H2 + I2 >= 0 && -1 + -1*H2 + I2 >= 0 && G2 + I2 >= 0 && -2 + C2 + I2 >= 0 && -2 + I2 + Z1 >= 0 && I2 + R1 >= 0 && I2 + -1*R1 >= 0 && I2 + Q1 >= 0 && I2 + -1*Q1 >= 0 && I2 + O1 >= 0 && I2 + -1*O1 >= 0 && I2 + N1 >= 0 && I2 + -1*N1 >= 0 && I2 + M1 >= 0 && I2 + -1*M1 >= 0 && I2 + L1 >= 0 && I2 + -1*L1 >= 0 && I1 + I2 >= 0 && -1*I1 + I2 >= 0 && H1 + I2 >= 0 && -1*H1 + I2 >= 0 && -1 + C + I2 >= 0 && -2 + A + I2 >= 0 && -1 + -1*H2 >= 0 && -1 + G2 + -1*H2 >= 0 && -3 + C2 + -1*H2 >= 0 && -3 + -1*H2 + Z1 >= 0 && -1 + -1*H2 + R1 >= 0 && -1 + -1*H2 + -1*R1 >= 0 && -1 + -1*H2 + Q1 >= 0 && -1 + -1*H2 + -1*Q1 >= 0 && -1 + -1*H2 + O1 >= 0 && -1 + -1*H2 + -1*O1 >= 0 && -1 + -1*H2 + N1 >= 0 && -1 + -1*H2 + -1*N1 >= 0 && -1 + -1*H2 + M1 >= 0 && -1 + -1*H2 + -1*M1 >= 0 && -1 + -1*H2 + L1 >= 0 && -1 + -1*H2 + -1*L1 >= 0 && -1 + -1*H2 + I1 >= 0 && -1 + -1*H2 + -1*I1 >= 0 && -1 + H1 + -1*H2 >= 0 && -1 + -1*H1 + -1*H2 >= 0 && -2 + C + -1*H2 >= 0 && -3 + A + -1*H2 >= 0 && 1 + H2 >= 0 && 1 + G2 + H2 >= 0 && -1 + C2 + H2 >= 0 && -1 + H2 + Z1 >= 0 && 1 + H2 + R1 >= 0 && 1 + H2 + -1*R1 >= 0 && 1 + H2 + Q1 >= 0 && 1 + H2 + -1*Q1 >= 0 && 1 + H2 + O1 >= 0 && 1 + H2 + -1*O1 >= 0 && 1 + H2 + N1 >= 0 && 1 + H2 + -1*N1 >= 0 && 1 + H2 + M1 >= 0 && 1 + H2 + -1*M1 >= 0 && 1 + H2 + L1 >= 0 && 1 + H2 + -1*L1 >= 0 && 1 + H2 + I1 >= 0 && 1 + H2 + -1*I1 >= 0 && 1 + H1 + H2 >= 0 && 1 + -1*H1 + H2 >= 0 && C + H2 >= 0 && -1 + A + H2 >= 0 && G2 >= 0 && -2 + C2 + G2 >= 0 && -2 + G2 + Z1 >= 0 && G2 + R1 >= 0 && G2 + -1*R1 >= 0 && G2 + Q1 >= 0 && G2 + -1*Q1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && G2 + N1 >= 0 && G2 + -1*N1 >= 0 && G2 + M1 >= 0 && G2 + -1*M1 >= 0 && G2 + L1 >= 0 && G2 + -1*L1 >= 0 && G2 + I1 >= 0 && G2 + -1*I1 >= 0 && G2 + H1 >= 0 && G2 + -1*H1 >= 0 && -1 + C + G2 >= 0 && -2 + A + G2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -3 + C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -3 + C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1 + C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1 + C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1 + C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1 + C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1 + C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1 + C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1 + C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1 + C + N1 >= 0 && -2 + A + N1 >= 0 && 1 + -1*D + G1 >= 0 && -1 + D + -1*J1 >= 0 && -1 + D + -1*G1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1 + C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1 + C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1 + C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1 + C + L1 >= 0 && -2 + A + L1 >= 0 && G1 + -1*J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1 + C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1 + C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1 + C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1 + C + H1 >= 0 && -2 + A + H1 >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && -2 + A >= 0 && A >= 2 && J1 >= 0 && C >= 1 && Q1 = 0 && R1 = O1 && N1 = 0 && M1 = O1 && L1 = 0] 13. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,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,1 + U1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,R1,R1,J1,K1,0,R1,0,R1 [2 + -1*M2 >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,S1,U1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,Y2,-1,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && Y2 >= 0 && A >= 2 && 0 >= C && D >= 0 && H >= 0 && Q1 = 0] 14. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f18(A,B,Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z2,D,H,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && A >= 2 && D >= 0 && 0 >= Y && H >= 0] 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 -> f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,D3,X2,J1,K1,B3,Y2,Z2,A3,C3 [H >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && 1 + H + K2 >= 0 && -1 + H + -1*K2 >= 0 && H + J2 >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1*C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 3 + K2 + -1*M2 >= 0 && 1 + -1*K2 + -1*M2 >= 0 && 2 + J2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -1 + K2 + M2 >= 0 && -3 + -1*K2 + M2 >= 0 && -2 + J2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -1 + -1*K2 >= 0 && -1 + J2 + -1*K2 >= 0 && -3 + C2 + -1*K2 >= 0 && -3 + -1*K2 + Z1 >= 0 && -1 + -1*K2 + R1 >= 0 && -1 + -1*K2 + -1*R1 >= 0 && -1 + -1*K2 + Q1 >= 0 && -1 + -1*K2 + -1*Q1 >= 0 && -1 + -1*K2 + O1 >= 0 && -1 + -1*K2 + -1*O1 >= 0 && -1 + -1*K2 + N1 >= 0 && -1 + -1*K2 + -1*N1 >= 0 && -1 + -1*K2 + M1 >= 0 && -1 + -1*K2 + -1*M1 >= 0 && -1 + -1*K2 + L1 >= 0 && -1 + -1*K2 + -1*L1 >= 0 && -1 + I1 + -1*K2 >= 0 && -1 + -1*I1 + -1*K2 >= 0 && -1 + H1 + -1*K2 >= 0 && -1 + -1*H1 + -1*K2 >= 0 && -1 + -1*C + -1*K2 >= 0 && -3 + A + -1*K2 >= 0 && 1 + K2 >= 0 && 1 + J2 + K2 >= 0 && -1 + C2 + K2 >= 0 && -1 + K2 + Z1 >= 0 && 1 + K2 + R1 >= 0 && 1 + K2 + -1*R1 >= 0 && 1 + K2 + Q1 >= 0 && 1 + K2 + -1*Q1 >= 0 && 1 + K2 + O1 >= 0 && 1 + K2 + -1*O1 >= 0 && 1 + K2 + N1 >= 0 && 1 + K2 + -1*N1 >= 0 && 1 + K2 + M1 >= 0 && 1 + K2 + -1*M1 >= 0 && 1 + K2 + L1 >= 0 && 1 + K2 + -1*L1 >= 0 && 1 + I1 + K2 >= 0 && 1 + -1*I1 + K2 >= 0 && 1 + H1 + K2 >= 0 && 1 + -1*H1 + K2 >= 0 && 1 + -1*C + K2 >= 0 && -1 + A + K2 >= 0 && J2 >= 0 && -2 + C2 + J2 >= 0 && -2 + J2 + Z1 >= 0 && J2 + R1 >= 0 && J2 + -1*R1 >= 0 && J2 + Q1 >= 0 && J2 + -1*Q1 >= 0 && J2 + O1 >= 0 && J2 + -1*O1 >= 0 && J2 + N1 >= 0 && J2 + -1*N1 >= 0 && J2 + M1 >= 0 && J2 + -1*M1 >= 0 && J2 + L1 >= 0 && J2 + -1*L1 >= 0 && I1 + J2 >= 0 && -1*I1 + J2 >= 0 && H1 + J2 >= 0 && -1*H1 + J2 >= 0 && -1*C + J2 >= 0 && -2 + A + J2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && T1 + -1*U1 >= 0 && -1 + D + -1*U1 >= 0 && -1 + D + -1*T1 >= 0 && 1 + -1*D + T1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1*C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1*C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1*C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1*C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1*C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1*C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1*C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1*C + N1 >= 0 && -2 + A + N1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1*C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1*C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1*C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1*C + L1 >= 0 && -2 + A + L1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1*C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1*C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1*C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1*C + H1 >= 0 && -2 + A + H1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && U1 >= 0 && L1 = I1] 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,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I1,I1,J1,K1,0,R1,0,R1,P1,0 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,R1,S1,T1,-1 + U1,V1,-1 + U1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && 1 + H + K2 >= 0 && -1 + H + -1*K2 >= 0 && H + J2 >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1*C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 3 + K2 + -1*M2 >= 0 && 1 + -1*K2 + -1*M2 >= 0 && 2 + J2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -1 + K2 + M2 >= 0 && -3 + -1*K2 + M2 >= 0 && -2 + J2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -1 + -1*K2 >= 0 && -1 + J2 + -1*K2 >= 0 && -3 + C2 + -1*K2 >= 0 && -3 + -1*K2 + Z1 >= 0 && -1 + -1*K2 + R1 >= 0 && -1 + -1*K2 + -1*R1 >= 0 && -1 + -1*K2 + Q1 >= 0 && -1 + -1*K2 + -1*Q1 >= 0 && -1 + -1*K2 + O1 >= 0 && -1 + -1*K2 + -1*O1 >= 0 && -1 + -1*K2 + N1 >= 0 && -1 + -1*K2 + -1*N1 >= 0 && -1 + -1*K2 + M1 >= 0 && -1 + -1*K2 + -1*M1 >= 0 && -1 + -1*K2 + L1 >= 0 && -1 + -1*K2 + -1*L1 >= 0 && -1 + I1 + -1*K2 >= 0 && -1 + -1*I1 + -1*K2 >= 0 && -1 + H1 + -1*K2 >= 0 && -1 + -1*H1 + -1*K2 >= 0 && -1 + -1*C + -1*K2 >= 0 && -3 + A + -1*K2 >= 0 && 1 + K2 >= 0 && 1 + J2 + K2 >= 0 && -1 + C2 + K2 >= 0 && -1 + K2 + Z1 >= 0 && 1 + K2 + R1 >= 0 && 1 + K2 + -1*R1 >= 0 && 1 + K2 + Q1 >= 0 && 1 + K2 + -1*Q1 >= 0 && 1 + K2 + O1 >= 0 && 1 + K2 + -1*O1 >= 0 && 1 + K2 + N1 >= 0 && 1 + K2 + -1*N1 >= 0 && 1 + K2 + M1 >= 0 && 1 + K2 + -1*M1 >= 0 && 1 + K2 + L1 >= 0 && 1 + K2 + -1*L1 >= 0 && 1 + I1 + K2 >= 0 && 1 + -1*I1 + K2 >= 0 && 1 + H1 + K2 >= 0 && 1 + -1*H1 + K2 >= 0 && 1 + -1*C + K2 >= 0 && -1 + A + K2 >= 0 && J2 >= 0 && -2 + C2 + J2 >= 0 && -2 + J2 + Z1 >= 0 && J2 + R1 >= 0 && J2 + -1*R1 >= 0 && J2 + Q1 >= 0 && J2 + -1*Q1 >= 0 && J2 + O1 >= 0 && J2 + -1*O1 >= 0 && J2 + N1 >= 0 && J2 + -1*N1 >= 0 && J2 + M1 >= 0 && J2 + -1*M1 >= 0 && J2 + L1 >= 0 && J2 + -1*L1 >= 0 && I1 + J2 >= 0 && -1*I1 + J2 >= 0 && H1 + J2 >= 0 && -1*H1 + J2 >= 0 && -1*C + J2 >= 0 && -2 + A + J2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && T1 + -1*U1 >= 0 && -1 + D + -1*U1 >= 0 && -1 + D + -1*T1 >= 0 && 1 + -1*D + T1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1*C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1*C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1*C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1*C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1*C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1*C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1*C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1*C + N1 >= 0 && -2 + A + N1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1*C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1*C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1*C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1*C + L1 >= 0 && -2 + A + L1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1*C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1*C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1*C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1*C + H1 >= 0 && -2 + A + H1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && A >= 2 && U1 >= 0 && 0 >= C && Q1 = 0 && R1 = O1 && N1 = 0 && M1 = O1 && L1 = 0] Signature: {(f1,75);(f11,75);(f13,75);(f16,75);(f18,75);(f19,75);(f20,75);(f27,75)} Flow Graph: [0->{},1->{3,4,5},2->{6,7},3->{},4->{},5->{3,4,5},6->{8,9,10},7->{6,7},8->{11,12},9->{8,9,10},10->{13,14} ,11->{},12->{11,12},13->{15,16},14->{8,9,10},15->{},16->{15,16}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,9)] * Step 3: Looptree NO + Considered Problem: Rules: 0. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f20(Z2,Y2,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,E3,A1,B1,G3,H3,F3,I3,G1,M3,D3,J1,K1,C3,A3,B3,X2 [0 >= Z2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,L3,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,J3,K3,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 1. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f16(1,Y2,Z2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B3,A1,B1,X2,C3,E3,D3,G1,H1,I1,J1,K1,L1,M1,N1,O1 [E1 = A2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,F3,E1,E1,S1,T1,U1,V1,W1,X1,Y1,Z1,H3,I3,C2,D2,A3,A3,G2,H2,I2,J2,K2,G3,M2,N2,J3,P2,Q2,R2,S2,T2,U2,V2,W2) 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f1(Y2,2,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,Y2,E1,B3,E1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[Y2 >= 2 && E1 = A2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,E1,B2,C2,D2,Z2,F2,G2,H2,I2,J2,K2,X2,2,C3,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 3. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(1,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I3,G3,J1,K1,E3,X2,C3,D3,H3 [Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && Q1 = 0 && R1 = 0 && A = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,Y2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,-1,0,Z2,A3,T2,U2,B3,Y2) 4. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(1,B,-1 + Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,F3,H3,J1,K1,G3,C3,D3 [Q1 + -1*R1 >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,E3,I3,0,0,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,Z2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,-1,-1 + Y2,A3,B3,X2,Z2,V2 && -1*Q1 + R1 >= 0 ,W2) && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && Y2 >= 2 && Q1 = 0 && R1 = 0 && A = 1] 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f16(1,B,Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= C && Q1 = R1 && A = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,Q1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,E2,Z2,Z2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) 6. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f18(A,Y2,Z2,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,A3,A1,B1,X2,C3,E3,D3,G1,H1,I1,J1,K1,L1,M1,N1,O1 [2 + -1*M2 >= 0 (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,I3,D1,D1,S1,T1,U1,V1,W1,X1,Y2,B3,G3,H3,H,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C1 + -1*M2 >= 0 && B + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C1 + M2 >= 0 && -4 + B + M2 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + F1 >= 0 && -2 + C1 >= 0 && -4 + B + C1 >= 0 && -1*B + C1 >= 0 && -2 + B >= 0 && F3 >= A && B3 >= A && B >= C1 && A >= 2 && H >= A && H >= 0 && B >= 0 && D = 0] 7. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,E1,Y2,E1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [2 + -1*M2 >= 0 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C1 + -1*M2 >= 0 && B + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C1 + M2 >= 0 && -4 + B + M2 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + F1 >= 0 && -2 + C1 >= 0 && -4 + B + C1 >= 0 && -1*B + C1 >= 0 && -2 + B >= 0 && B >= 0 && C1 >= 1 + B] 8. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f11(A,B,C,1 + J1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,J1,R1,R1,J1,K1,0,R1,0,R1 [2 + -1*M2 >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,Z2,-1,Y2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && Z2 >= 0 && Y2 >= 0 && A >= 2 && C >= 1 && H >= 0 && Q1 = 0] 9. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f18(A,B,-1 + C,1 + D,E,F,G,-1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,1 + D,-1 + H,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2 && C2 + -1*M2 >= 0 ,S2,T2,U2,V2,W2) && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && A >= 2 && V >= 1 && H >= 0 && C = V] 10. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f27(A,B,C,Z2,E,F,G,Y2,I,J,K,L,M,N,O,P,Q,R,S,Z2,Y2,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + D + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + D + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + D >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + D + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && D >= 0 && -2 + A + D >= 0 && -2 + A >= 0 && H >= 0 && 0 >= C] 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f20(Y2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,E3,C3,J1,K1,X2,Z2,A3,B3,D3[H >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && H + I2 >= 0 && 1 + H + H2 >= 0 && -1 + H + -1*H2 >= 0 && G2 + H >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1 + C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 2 + I2 + -1*M2 >= 0 && 3 + H2 + -1*M2 >= 0 && 1 + -1*H2 + -1*M2 >= 0 && 2 + G2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 1 + C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -2 + I2 + M2 >= 0 && -1 + H2 + M2 >= 0 && -3 + -1*H2 + M2 >= 0 && -2 + G2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -3 + C + M2 >= 0 && -4 + A + M2 >= 0 && I2 >= 0 && 1 + H2 + I2 >= 0 && -1 + -1*H2 + I2 >= 0 && G2 + I2 >= 0 && -2 + C2 + I2 >= 0 && -2 + I2 + Z1 >= 0 && I2 + R1 >= 0 && I2 + -1*R1 >= 0 && I2 + Q1 >= 0 && I2 + -1*Q1 >= 0 && I2 + O1 >= 0 && I2 + -1*O1 >= 0 && I2 + N1 >= 0 && I2 + -1*N1 >= 0 && I2 + M1 >= 0 && I2 + -1*M1 >= 0 && I2 + L1 >= 0 && I2 + -1*L1 >= 0 && I1 + I2 >= 0 && -1*I1 + I2 >= 0 && H1 + I2 >= 0 && -1*H1 + I2 >= 0 && -1 + C + I2 >= 0 && -2 + A + I2 >= 0 && -1 + -1*H2 >= 0 && -1 + G2 + -1*H2 >= 0 && -3 + C2 + -1*H2 >= 0 && -3 + -1*H2 + Z1 >= 0 && -1 + -1*H2 + R1 >= 0 && -1 + -1*H2 + -1*R1 >= 0 && -1 + -1*H2 + Q1 >= 0 && -1 + -1*H2 + -1*Q1 >= 0 && -1 + -1*H2 + O1 >= 0 && -1 + -1*H2 + -1*O1 >= 0 && -1 + -1*H2 + N1 >= 0 && -1 + -1*H2 + -1*N1 >= 0 && -1 + -1*H2 + M1 >= 0 && -1 + -1*H2 + -1*M1 >= 0 && -1 + -1*H2 + L1 >= 0 && -1 + -1*H2 + -1*L1 >= 0 && -1 + -1*H2 + I1 >= 0 && -1 + -1*H2 + -1*I1 >= 0 && -1 + H1 + -1*H2 >= 0 && -1 + -1*H1 + -1*H2 >= 0 && -2 + C + -1*H2 >= 0 && -3 + A + -1*H2 >= 0 && 1 + H2 >= 0 && 1 + G2 + H2 >= 0 && -1 + C2 + H2 >= 0 && -1 + H2 + Z1 >= 0 && 1 + H2 + R1 >= 0 && 1 + H2 + -1*R1 >= 0 && 1 + H2 + Q1 >= 0 && 1 + H2 + -1*Q1 >= 0 && 1 + H2 + O1 >= 0 && 1 + H2 + -1*O1 >= 0 && 1 + H2 + N1 >= 0 && 1 + H2 + -1*N1 >= 0 && 1 + H2 + M1 >= 0 && 1 + H2 + -1*M1 >= 0 && 1 + H2 + L1 >= 0 && 1 + H2 + -1*L1 >= 0 && 1 + H2 + I1 >= 0 && 1 + H2 + -1*I1 >= 0 && 1 + H1 + H2 >= 0 && 1 + -1*H1 + H2 >= 0 && C + H2 >= 0 && -1 + A + H2 >= 0 && G2 >= 0 && -2 + C2 + G2 >= 0 && -2 + G2 + Z1 >= 0 && G2 + R1 >= 0 && G2 + -1*R1 >= 0 && G2 + Q1 >= 0 && G2 + -1*Q1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && G2 + N1 >= 0 && G2 + -1*N1 >= 0 && G2 + M1 >= 0 && G2 + -1*M1 >= 0 && G2 + L1 >= 0 && G2 + -1*L1 >= 0 && G2 + I1 >= 0 && G2 + -1*I1 >= 0 && G2 + H1 >= 0 && G2 + -1*H1 >= 0 && -1 + C + G2 >= 0 && -2 + A + G2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -3 + C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -3 + C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1 + C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1 + C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1 + C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1 + C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1 + C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1 + C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1 + C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1 + C + N1 >= 0 && -2 + A + N1 >= 0 && 1 + -1*D + G1 >= 0 && -1 + D + -1*J1 >= 0 && -1 + D + -1*G1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1 + C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1 + C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1 + C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1 + C + L1 >= 0 && -2 + A + L1 >= 0 && G1 + -1*J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1 + C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1 + C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1 + C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1 + C + H1 >= 0 && -2 + A + H1 >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && -2 + A >= 0 && J1 >= 0 && L1 = I1] 12. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I1,I1,-1 + J1,K1,0,R1,0,R1 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,-1 + J1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && H + I2 >= 0 && 1 + H + H2 >= 0 && -1 + H + -1*H2 >= 0 && G2 + H >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1 + C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 2 + I2 + -1*M2 >= 0 && 3 + H2 + -1*M2 >= 0 && 1 + -1*H2 + -1*M2 >= 0 && 2 + G2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 1 + C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -2 + I2 + M2 >= 0 && -1 + H2 + M2 >= 0 && -3 + -1*H2 + M2 >= 0 && -2 + G2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -3 + C + M2 >= 0 && -4 + A + M2 >= 0 && I2 >= 0 && 1 + H2 + I2 >= 0 && -1 + -1*H2 + I2 >= 0 && G2 + I2 >= 0 && -2 + C2 + I2 >= 0 && -2 + I2 + Z1 >= 0 && I2 + R1 >= 0 && I2 + -1*R1 >= 0 && I2 + Q1 >= 0 && I2 + -1*Q1 >= 0 && I2 + O1 >= 0 && I2 + -1*O1 >= 0 && I2 + N1 >= 0 && I2 + -1*N1 >= 0 && I2 + M1 >= 0 && I2 + -1*M1 >= 0 && I2 + L1 >= 0 && I2 + -1*L1 >= 0 && I1 + I2 >= 0 && -1*I1 + I2 >= 0 && H1 + I2 >= 0 && -1*H1 + I2 >= 0 && -1 + C + I2 >= 0 && -2 + A + I2 >= 0 && -1 + -1*H2 >= 0 && -1 + G2 + -1*H2 >= 0 && -3 + C2 + -1*H2 >= 0 && -3 + -1*H2 + Z1 >= 0 && -1 + -1*H2 + R1 >= 0 && -1 + -1*H2 + -1*R1 >= 0 && -1 + -1*H2 + Q1 >= 0 && -1 + -1*H2 + -1*Q1 >= 0 && -1 + -1*H2 + O1 >= 0 && -1 + -1*H2 + -1*O1 >= 0 && -1 + -1*H2 + N1 >= 0 && -1 + -1*H2 + -1*N1 >= 0 && -1 + -1*H2 + M1 >= 0 && -1 + -1*H2 + -1*M1 >= 0 && -1 + -1*H2 + L1 >= 0 && -1 + -1*H2 + -1*L1 >= 0 && -1 + -1*H2 + I1 >= 0 && -1 + -1*H2 + -1*I1 >= 0 && -1 + H1 + -1*H2 >= 0 && -1 + -1*H1 + -1*H2 >= 0 && -2 + C + -1*H2 >= 0 && -3 + A + -1*H2 >= 0 && 1 + H2 >= 0 && 1 + G2 + H2 >= 0 && -1 + C2 + H2 >= 0 && -1 + H2 + Z1 >= 0 && 1 + H2 + R1 >= 0 && 1 + H2 + -1*R1 >= 0 && 1 + H2 + Q1 >= 0 && 1 + H2 + -1*Q1 >= 0 && 1 + H2 + O1 >= 0 && 1 + H2 + -1*O1 >= 0 && 1 + H2 + N1 >= 0 && 1 + H2 + -1*N1 >= 0 && 1 + H2 + M1 >= 0 && 1 + H2 + -1*M1 >= 0 && 1 + H2 + L1 >= 0 && 1 + H2 + -1*L1 >= 0 && 1 + H2 + I1 >= 0 && 1 + H2 + -1*I1 >= 0 && 1 + H1 + H2 >= 0 && 1 + -1*H1 + H2 >= 0 && C + H2 >= 0 && -1 + A + H2 >= 0 && G2 >= 0 && -2 + C2 + G2 >= 0 && -2 + G2 + Z1 >= 0 && G2 + R1 >= 0 && G2 + -1*R1 >= 0 && G2 + Q1 >= 0 && G2 + -1*Q1 >= 0 && G2 + O1 >= 0 && G2 + -1*O1 >= 0 && G2 + N1 >= 0 && G2 + -1*N1 >= 0 && G2 + M1 >= 0 && G2 + -1*M1 >= 0 && G2 + L1 >= 0 && G2 + -1*L1 >= 0 && G2 + I1 >= 0 && G2 + -1*I1 >= 0 && G2 + H1 >= 0 && G2 + -1*H1 >= 0 && -1 + C + G2 >= 0 && -2 + A + G2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -3 + C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -3 + C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1 + C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1 + C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1 + C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1 + C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1 + C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1 + C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1 + C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1 + C + N1 >= 0 && -2 + A + N1 >= 0 && 1 + -1*D + G1 >= 0 && -1 + D + -1*J1 >= 0 && -1 + D + -1*G1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1 + C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1 + C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1 + C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1 + C + L1 >= 0 && -2 + A + L1 >= 0 && G1 + -1*J1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1 + C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1 + C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1 + C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1 + C + H1 >= 0 && -2 + A + H1 >= 0 && -1 + C >= 0 && -3 + A + C >= 0 && -2 + A >= 0 && A >= 2 && J1 >= 0 && C >= 1 && Q1 = 0 && R1 = O1 && N1 = 0 && M1 = O1 && L1 = 0] 13. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,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,1 + U1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,R1,R1,J1,K1,0,R1,0,R1 [2 + -1*M2 >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,P1,0,R1,S1,U1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,Y2,-1,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && Y2 >= 0 && A >= 2 && 0 >= C && D >= 0 && H >= 0 && Q1 = 0] 14. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,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 -> f18(A,B,Y2,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z2,D,H,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 [2 + -1*M2 >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + R1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && A >= 2 && D >= 0 && 0 >= Y && H >= 0] 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 -> f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,D3,X2,J1,K1,B3,Y2,Z2,A3,C3 [H >= 0 (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && 1 + H + K2 >= 0 && -1 + H + -1*K2 >= 0 && H + J2 >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1*C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 3 + K2 + -1*M2 >= 0 && 1 + -1*K2 + -1*M2 >= 0 && 2 + J2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -1 + K2 + M2 >= 0 && -3 + -1*K2 + M2 >= 0 && -2 + J2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -1 + -1*K2 >= 0 && -1 + J2 + -1*K2 >= 0 && -3 + C2 + -1*K2 >= 0 && -3 + -1*K2 + Z1 >= 0 && -1 + -1*K2 + R1 >= 0 && -1 + -1*K2 + -1*R1 >= 0 && -1 + -1*K2 + Q1 >= 0 && -1 + -1*K2 + -1*Q1 >= 0 && -1 + -1*K2 + O1 >= 0 && -1 + -1*K2 + -1*O1 >= 0 && -1 + -1*K2 + N1 >= 0 && -1 + -1*K2 + -1*N1 >= 0 && -1 + -1*K2 + M1 >= 0 && -1 + -1*K2 + -1*M1 >= 0 && -1 + -1*K2 + L1 >= 0 && -1 + -1*K2 + -1*L1 >= 0 && -1 + I1 + -1*K2 >= 0 && -1 + -1*I1 + -1*K2 >= 0 && -1 + H1 + -1*K2 >= 0 && -1 + -1*H1 + -1*K2 >= 0 && -1 + -1*C + -1*K2 >= 0 && -3 + A + -1*K2 >= 0 && 1 + K2 >= 0 && 1 + J2 + K2 >= 0 && -1 + C2 + K2 >= 0 && -1 + K2 + Z1 >= 0 && 1 + K2 + R1 >= 0 && 1 + K2 + -1*R1 >= 0 && 1 + K2 + Q1 >= 0 && 1 + K2 + -1*Q1 >= 0 && 1 + K2 + O1 >= 0 && 1 + K2 + -1*O1 >= 0 && 1 + K2 + N1 >= 0 && 1 + K2 + -1*N1 >= 0 && 1 + K2 + M1 >= 0 && 1 + K2 + -1*M1 >= 0 && 1 + K2 + L1 >= 0 && 1 + K2 + -1*L1 >= 0 && 1 + I1 + K2 >= 0 && 1 + -1*I1 + K2 >= 0 && 1 + H1 + K2 >= 0 && 1 + -1*H1 + K2 >= 0 && 1 + -1*C + K2 >= 0 && -1 + A + K2 >= 0 && J2 >= 0 && -2 + C2 + J2 >= 0 && -2 + J2 + Z1 >= 0 && J2 + R1 >= 0 && J2 + -1*R1 >= 0 && J2 + Q1 >= 0 && J2 + -1*Q1 >= 0 && J2 + O1 >= 0 && J2 + -1*O1 >= 0 && J2 + N1 >= 0 && J2 + -1*N1 >= 0 && J2 + M1 >= 0 && J2 + -1*M1 >= 0 && J2 + L1 >= 0 && J2 + -1*L1 >= 0 && I1 + J2 >= 0 && -1*I1 + J2 >= 0 && H1 + J2 >= 0 && -1*H1 + J2 >= 0 && -1*C + J2 >= 0 && -2 + A + J2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && T1 + -1*U1 >= 0 && -1 + D + -1*U1 >= 0 && -1 + D + -1*T1 >= 0 && 1 + -1*D + T1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1*C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1*C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1*C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1*C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1*C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1*C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1*C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1*C + N1 >= 0 && -2 + A + N1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1*C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1*C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1*C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1*C + L1 >= 0 && -2 + A + L1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1*C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1*C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1*C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1*C + H1 >= 0 && -2 + A + H1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && U1 >= 0 && L1 = I1] 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,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,I1,I1,J1,K1,0,R1,0,R1,P1,0 [H >= 0 (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) ,R1,S1,T1,-1 + U1,V1,-1 + U1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2) && -2 + H + M2 >= 0 && 2 + H + -1*M2 >= 0 && 1 + H + K2 >= 0 && -1 + H + -1*K2 >= 0 && H + J2 >= 0 && -2 + C2 + H >= 0 && -2 + H + Z1 >= 0 && H + R1 >= 0 && H + -1*R1 >= 0 && H + Q1 >= 0 && H + -1*Q1 >= 0 && H + O1 >= 0 && H + -1*O1 >= 0 && H + N1 >= 0 && H + -1*N1 >= 0 && H + M1 >= 0 && H + -1*M1 >= 0 && H + L1 >= 0 && H + -1*L1 >= 0 && H + I1 >= 0 && H + -1*I1 >= 0 && H + H1 >= 0 && H + -1*H1 >= 0 && -1*C + H >= 0 && -2 + A + H >= 0 && 2 + -1*M2 >= 0 && 3 + K2 + -1*M2 >= 0 && 1 + -1*K2 + -1*M2 >= 0 && 2 + J2 + -1*M2 >= 0 && C2 + -1*M2 >= 0 && -1*M2 + Z1 >= 0 && 2 + -1*M2 + R1 >= 0 && 2 + -1*M2 + -1*R1 >= 0 && 2 + -1*M2 + Q1 >= 0 && 2 + -1*M2 + -1*Q1 >= 0 && 2 + -1*M2 + O1 >= 0 && 2 + -1*M2 + -1*O1 >= 0 && 2 + -1*M2 + N1 >= 0 && 2 + -1*M2 + -1*N1 >= 0 && 2 + M1 + -1*M2 >= 0 && 2 + -1*M1 + -1*M2 >= 0 && 2 + L1 + -1*M2 >= 0 && 2 + -1*L1 + -1*M2 >= 0 && 2 + I1 + -1*M2 >= 0 && 2 + -1*I1 + -1*M2 >= 0 && 2 + H1 + -1*M2 >= 0 && 2 + -1*H1 + -1*M2 >= 0 && 2 + -1*C + -1*M2 >= 0 && A + -1*M2 >= 0 && -2 + M2 >= 0 && -1 + K2 + M2 >= 0 && -3 + -1*K2 + M2 >= 0 && -2 + J2 + M2 >= 0 && -4 + C2 + M2 >= 0 && -4 + M2 + Z1 >= 0 && -2 + M2 + R1 >= 0 && -2 + M2 + -1*R1 >= 0 && -2 + M2 + Q1 >= 0 && -2 + M2 + -1*Q1 >= 0 && -2 + M2 + O1 >= 0 && -2 + M2 + -1*O1 >= 0 && -2 + M2 + N1 >= 0 && -2 + M2 + -1*N1 >= 0 && -2 + M1 + M2 >= 0 && -2 + -1*M1 + M2 >= 0 && -2 + L1 + M2 >= 0 && -2 + -1*L1 + M2 >= 0 && -2 + I1 + M2 >= 0 && -2 + -1*I1 + M2 >= 0 && -2 + H1 + M2 >= 0 && -2 + -1*H1 + M2 >= 0 && -2 + -1*C + M2 >= 0 && -4 + A + M2 >= 0 && -1 + -1*K2 >= 0 && -1 + J2 + -1*K2 >= 0 && -3 + C2 + -1*K2 >= 0 && -3 + -1*K2 + Z1 >= 0 && -1 + -1*K2 + R1 >= 0 && -1 + -1*K2 + -1*R1 >= 0 && -1 + -1*K2 + Q1 >= 0 && -1 + -1*K2 + -1*Q1 >= 0 && -1 + -1*K2 + O1 >= 0 && -1 + -1*K2 + -1*O1 >= 0 && -1 + -1*K2 + N1 >= 0 && -1 + -1*K2 + -1*N1 >= 0 && -1 + -1*K2 + M1 >= 0 && -1 + -1*K2 + -1*M1 >= 0 && -1 + -1*K2 + L1 >= 0 && -1 + -1*K2 + -1*L1 >= 0 && -1 + I1 + -1*K2 >= 0 && -1 + -1*I1 + -1*K2 >= 0 && -1 + H1 + -1*K2 >= 0 && -1 + -1*H1 + -1*K2 >= 0 && -1 + -1*C + -1*K2 >= 0 && -3 + A + -1*K2 >= 0 && 1 + K2 >= 0 && 1 + J2 + K2 >= 0 && -1 + C2 + K2 >= 0 && -1 + K2 + Z1 >= 0 && 1 + K2 + R1 >= 0 && 1 + K2 + -1*R1 >= 0 && 1 + K2 + Q1 >= 0 && 1 + K2 + -1*Q1 >= 0 && 1 + K2 + O1 >= 0 && 1 + K2 + -1*O1 >= 0 && 1 + K2 + N1 >= 0 && 1 + K2 + -1*N1 >= 0 && 1 + K2 + M1 >= 0 && 1 + K2 + -1*M1 >= 0 && 1 + K2 + L1 >= 0 && 1 + K2 + -1*L1 >= 0 && 1 + I1 + K2 >= 0 && 1 + -1*I1 + K2 >= 0 && 1 + H1 + K2 >= 0 && 1 + -1*H1 + K2 >= 0 && 1 + -1*C + K2 >= 0 && -1 + A + K2 >= 0 && J2 >= 0 && -2 + C2 + J2 >= 0 && -2 + J2 + Z1 >= 0 && J2 + R1 >= 0 && J2 + -1*R1 >= 0 && J2 + Q1 >= 0 && J2 + -1*Q1 >= 0 && J2 + O1 >= 0 && J2 + -1*O1 >= 0 && J2 + N1 >= 0 && J2 + -1*N1 >= 0 && J2 + M1 >= 0 && J2 + -1*M1 >= 0 && J2 + L1 >= 0 && J2 + -1*L1 >= 0 && I1 + J2 >= 0 && -1*I1 + J2 >= 0 && H1 + J2 >= 0 && -1*H1 + J2 >= 0 && -1*C + J2 >= 0 && -2 + A + J2 >= 0 && -2 + C2 >= 0 && -4 + C2 + Z1 >= 0 && -2 + C2 + R1 >= 0 && -2 + C2 + -1*R1 >= 0 && -2 + C2 + Q1 >= 0 && -2 + C2 + -1*Q1 >= 0 && -2 + C2 + O1 >= 0 && -2 + C2 + -1*O1 >= 0 && -2 + C2 + N1 >= 0 && -2 + C2 + -1*N1 >= 0 && -2 + C2 + M1 >= 0 && -2 + C2 + -1*M1 >= 0 && -2 + C2 + L1 >= 0 && -2 + C2 + -1*L1 >= 0 && -2 + C2 + I1 >= 0 && -2 + C2 + -1*I1 >= 0 && -2 + C2 + H1 >= 0 && -2 + C2 + -1*H1 >= 0 && -2 + -1*C + C2 >= 0 && -4 + A + C2 >= 0 && -1*A + C2 >= 0 && -2 + Z1 >= 0 && -2 + R1 + Z1 >= 0 && -2 + -1*R1 + Z1 >= 0 && -2 + Q1 + Z1 >= 0 && -2 + -1*Q1 + Z1 >= 0 && -2 + O1 + Z1 >= 0 && -2 + -1*O1 + Z1 >= 0 && -2 + N1 + Z1 >= 0 && -2 + -1*N1 + Z1 >= 0 && -2 + M1 + Z1 >= 0 && -2 + -1*M1 + Z1 >= 0 && -2 + L1 + Z1 >= 0 && -2 + -1*L1 + Z1 >= 0 && -2 + I1 + Z1 >= 0 && -2 + -1*I1 + Z1 >= 0 && -2 + H1 + Z1 >= 0 && -2 + -1*H1 + Z1 >= 0 && -2 + -1*C + Z1 >= 0 && -4 + A + Z1 >= 0 && -1*A + Z1 >= 0 && T1 + -1*U1 >= 0 && -1 + D + -1*U1 >= 0 && -1 + D + -1*T1 >= 0 && 1 + -1*D + T1 >= 0 && -1*R1 >= 0 && Q1 + -1*R1 >= 0 && -1*Q1 + -1*R1 >= 0 && O1 + -1*R1 >= 0 && -1*O1 + -1*R1 >= 0 && N1 + -1*R1 >= 0 && -1*N1 + -1*R1 >= 0 && M1 + -1*R1 >= 0 && -1*M1 + -1*R1 >= 0 && L1 + -1*R1 >= 0 && -1*L1 + -1*R1 >= 0 && I1 + -1*R1 >= 0 && -1*I1 + -1*R1 >= 0 && H1 + -1*R1 >= 0 && -1*H1 + -1*R1 >= 0 && -1*C + -1*R1 >= 0 && -2 + A + -1*R1 >= 0 && R1 >= 0 && Q1 + R1 >= 0 && -1*Q1 + R1 >= 0 && O1 + R1 >= 0 && -1*O1 + R1 >= 0 && N1 + R1 >= 0 && -1*N1 + R1 >= 0 && M1 + R1 >= 0 && -1*M1 + R1 >= 0 && L1 + R1 >= 0 && -1*L1 + R1 >= 0 && I1 + R1 >= 0 && -1*I1 + R1 >= 0 && H1 + R1 >= 0 && -1*H1 + R1 >= 0 && -1*C + R1 >= 0 && -2 + A + R1 >= 0 && -1*Q1 >= 0 && O1 + -1*Q1 >= 0 && -1*O1 + -1*Q1 >= 0 && N1 + -1*Q1 >= 0 && -1*N1 + -1*Q1 >= 0 && M1 + -1*Q1 >= 0 && -1*M1 + -1*Q1 >= 0 && L1 + -1*Q1 >= 0 && -1*L1 + -1*Q1 >= 0 && I1 + -1*Q1 >= 0 && -1*I1 + -1*Q1 >= 0 && H1 + -1*Q1 >= 0 && -1*H1 + -1*Q1 >= 0 && -1*C + -1*Q1 >= 0 && -2 + A + -1*Q1 >= 0 && Q1 >= 0 && O1 + Q1 >= 0 && -1*O1 + Q1 >= 0 && N1 + Q1 >= 0 && -1*N1 + Q1 >= 0 && M1 + Q1 >= 0 && -1*M1 + Q1 >= 0 && L1 + Q1 >= 0 && -1*L1 + Q1 >= 0 && I1 + Q1 >= 0 && -1*I1 + Q1 >= 0 && H1 + Q1 >= 0 && -1*H1 + Q1 >= 0 && -1*C + Q1 >= 0 && -2 + A + Q1 >= 0 && -1*O1 >= 0 && N1 + -1*O1 >= 0 && -1*N1 + -1*O1 >= 0 && M1 + -1*O1 >= 0 && -1*M1 + -1*O1 >= 0 && L1 + -1*O1 >= 0 && -1*L1 + -1*O1 >= 0 && I1 + -1*O1 >= 0 && -1*I1 + -1*O1 >= 0 && H1 + -1*O1 >= 0 && -1*H1 + -1*O1 >= 0 && -1*C + -1*O1 >= 0 && -2 + A + -1*O1 >= 0 && O1 >= 0 && N1 + O1 >= 0 && -1*N1 + O1 >= 0 && M1 + O1 >= 0 && -1*M1 + O1 >= 0 && L1 + O1 >= 0 && -1*L1 + O1 >= 0 && I1 + O1 >= 0 && -1*I1 + O1 >= 0 && H1 + O1 >= 0 && -1*H1 + O1 >= 0 && -1*C + O1 >= 0 && -2 + A + O1 >= 0 && -1*N1 >= 0 && M1 + -1*N1 >= 0 && -1*M1 + -1*N1 >= 0 && L1 + -1*N1 >= 0 && -1*L1 + -1*N1 >= 0 && I1 + -1*N1 >= 0 && -1*I1 + -1*N1 >= 0 && H1 + -1*N1 >= 0 && -1*H1 + -1*N1 >= 0 && -1*C + -1*N1 >= 0 && -2 + A + -1*N1 >= 0 && N1 >= 0 && M1 + N1 >= 0 && -1*M1 + N1 >= 0 && L1 + N1 >= 0 && -1*L1 + N1 >= 0 && I1 + N1 >= 0 && -1*I1 + N1 >= 0 && H1 + N1 >= 0 && -1*H1 + N1 >= 0 && -1*C + N1 >= 0 && -2 + A + N1 >= 0 && -1*M1 >= 0 && L1 + -1*M1 >= 0 && -1*L1 + -1*M1 >= 0 && I1 + -1*M1 >= 0 && -1*I1 + -1*M1 >= 0 && H1 + -1*M1 >= 0 && -1*H1 + -1*M1 >= 0 && -1*C + -1*M1 >= 0 && -2 + A + -1*M1 >= 0 && M1 >= 0 && L1 + M1 >= 0 && -1*L1 + M1 >= 0 && I1 + M1 >= 0 && -1*I1 + M1 >= 0 && H1 + M1 >= 0 && -1*H1 + M1 >= 0 && -1*C + M1 >= 0 && -2 + A + M1 >= 0 && -1*L1 >= 0 && I1 + -1*L1 >= 0 && -1*I1 + -1*L1 >= 0 && H1 + -1*L1 >= 0 && -1*H1 + -1*L1 >= 0 && -1*C + -1*L1 >= 0 && -2 + A + -1*L1 >= 0 && L1 >= 0 && I1 + L1 >= 0 && -1*I1 + L1 >= 0 && H1 + L1 >= 0 && -1*H1 + L1 >= 0 && -1*C + L1 >= 0 && -2 + A + L1 >= 0 && -1*I1 >= 0 && H1 + -1*I1 >= 0 && -1*H1 + -1*I1 >= 0 && -1*C + -1*I1 >= 0 && -2 + A + -1*I1 >= 0 && I1 >= 0 && H1 + I1 >= 0 && -1*H1 + I1 >= 0 && -1*C + I1 >= 0 && -2 + A + I1 >= 0 && -1*H1 >= 0 && -1*C + -1*H1 >= 0 && -2 + A + -1*H1 >= 0 && H1 >= 0 && -1*C + H1 >= 0 && -2 + A + H1 >= 0 && -1*C >= 0 && -2 + A + -1*C >= 0 && -2 + A >= 0 && A >= 2 && U1 >= 0 && 0 >= C && Q1 = 0 && R1 = O1 && N1 = 0 && M1 = O1 && L1 = 0] Signature: {(f1,75);(f11,75);(f13,75);(f16,75);(f18,75);(f19,75);(f20,75);(f27,75)} Flow Graph: [0->{},1->{3,4,5},2->{6,7},3->{},4->{},5->{3,4,5},6->{8,9,10},7->{6,7},8->{11,12},9->{8,10},10->{13,14} ,11->{},12->{11,12},13->{15,16},14->{8,9,10},15->{},16->{15,16}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | +- p:[7] c: [7] | +- p:[9,14,10] c: [] | +- p:[16] c: [16] | +- p:[12] c: [12] | `- p:[5] c: [] NO