(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f19))
(VAR A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1 C1 D1 E1 F1 G1 H1 I1 J1 K1 L1 M1 N1 O1 P1 Q1 R1 S1 T1 U1 V1 W1 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)
(RULES
  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, 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) -> Com_1(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, 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)) [ 0 >= Z2 ]
  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, 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) -> Com_1(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, 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)) [ E1 = A2 ]
  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, 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) -> Com_1(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, 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)) [ Y2 >= 2 /\ E1 = A2 ]
  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, 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) -> Com_1(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, 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)) [ Q1 - R1 >= 0 /\ -Q1 + R1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ C >= 1 /\ Q1 = 0 /\ R1 = 0 /\ A = 1 ]
  f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, 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, S2, T2, U2, V2, W2) -> Com_1(f20(1, B, Y2 - 1, D, E, F, G, H, I, 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, 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, Y2 - 1, A3, B3, X2, Z2, V2, W2)) [ Q1 - R1 >= 0 /\ -Q1 + R1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ C >= 1 /\ Y2 >= 2 /\ Q1 = 0 /\ R1 = 0 /\ A = 1 ]
  f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, 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, S2, T2, U2, V2, W2) -> Com_1(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, 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)) [ Q1 - R1 >= 0 /\ -Q1 + R1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 0 >= C /\ Q1 = R1 /\ A = 1 ]
  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, 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) -> Com_1(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, 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)) [ -M2 + 2 >= 0 /\ C1 - M2 >= 0 /\ B - M2 >= 0 /\ M2 - 2 >= 0 /\ C1 + M2 - 4 >= 0 /\ B + M2 - 4 >= 0 /\ D1 - F1 >= 0 /\ -D1 + F1 >= 0 /\ C1 - 2 >= 0 /\ B + C1 - 4 >= 0 /\ -B + C1 >= 0 /\ B - 2 >= 0 /\ F3 >= A /\ B3 >= A /\ B >= C1 /\ A >= 2 /\ H >= A /\ H >= 0 /\ B >= 0 /\ D = 0 ]
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, 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, S2, T2, U2, V2, W2) -> Com_1(f1(A, B + 1, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, E1, Y2, E1, G1, H1, 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, S2, T2, U2, V2, W2)) [ -M2 + 2 >= 0 /\ C1 - M2 >= 0 /\ B - M2 >= 0 /\ M2 - 2 >= 0 /\ C1 + M2 - 4 >= 0 /\ B + M2 - 4 >= 0 /\ D1 - F1 >= 0 /\ -D1 + F1 >= 0 /\ C1 - 2 >= 0 /\ B + C1 - 4 >= 0 /\ -B + C1 >= 0 /\ B - 2 >= 0 /\ B >= 0 /\ C1 >= B + 1 ]
  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, 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) -> Com_1(f11(A, B, C, J1 + 1, E, F, G, H, 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, 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)) [ -M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ D - M2 + 2 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ D + M2 - 2 >= 0 /\ A + M2 - 4 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ D + C2 - 2 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ D + Z1 - 2 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 + R1 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ A - 2 >= 0 /\ Z2 >= 0 /\ Y2 >= 0 /\ A >= 2 /\ C >= 1 /\ H >= 0 /\ Q1 = 0 ]
  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, 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) -> Com_1(f18(A, B, C - 1, D + 1, E, F, G, H - 1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, D + 1, H - 1, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, 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)) [ -M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ D - M2 + 2 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ D + M2 - 2 >= 0 /\ A + M2 - 4 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ D + C2 - 2 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ D + Z1 - 2 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 + R1 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ A - 2 >= 0 /\ A >= 2 /\ V >= 1 /\ H >= 0 /\ C = V ]
  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, 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) -> Com_1(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, 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)) [ -M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ D - M2 + 2 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ D + M2 - 2 >= 0 /\ A + M2 - 4 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ D + C2 - 2 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ D + Z1 - 2 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 + R1 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ 0 >= C ]
  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, 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) -> Com_1(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, 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)) [ H >= 0 /\ M2 + H - 2 >= 0 /\ -M2 + H + 2 >= 0 /\ I2 + H >= 0 /\ H2 + H + 1 >= 0 /\ -H2 + H - 1 >= 0 /\ G2 + H >= 0 /\ C2 + H - 2 >= 0 /\ Z1 + H - 2 >= 0 /\ R1 + H >= 0 /\ -R1 + H >= 0 /\ Q1 + H >= 0 /\ -Q1 + H >= 0 /\ O1 + H >= 0 /\ -O1 + H >= 0 /\ N1 + H >= 0 /\ -N1 + H >= 0 /\ M1 + H >= 0 /\ -M1 + H >= 0 /\ L1 + H >= 0 /\ -L1 + H >= 0 /\ I1 + H >= 0 /\ -I1 + H >= 0 /\ H1 + H >= 0 /\ -H1 + H >= 0 /\ C + H - 1 >= 0 /\ A + H - 2 >= 0 /\ -M2 + 2 >= 0 /\ I2 - M2 + 2 >= 0 /\ H2 - M2 + 3 >= 0 /\ -H2 - M2 + 1 >= 0 /\ G2 - M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ R1 - M2 + 2 >= 0 /\ -R1 - M2 + 2 >= 0 /\ Q1 - M2 + 2 >= 0 /\ -Q1 - M2 + 2 >= 0 /\ O1 - M2 + 2 >= 0 /\ -O1 - M2 + 2 >= 0 /\ N1 - M2 + 2 >= 0 /\ -N1 - M2 + 2 >= 0 /\ M1 - M2 + 2 >= 0 /\ -M1 - M2 + 2 >= 0 /\ L1 - M2 + 2 >= 0 /\ -L1 - M2 + 2 >= 0 /\ I1 - M2 + 2 >= 0 /\ -I1 - M2 + 2 >= 0 /\ H1 - M2 + 2 >= 0 /\ -H1 - M2 + 2 >= 0 /\ C - M2 + 1 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ I2 + M2 - 2 >= 0 /\ H2 + M2 - 1 >= 0 /\ -H2 + M2 - 3 >= 0 /\ G2 + M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ R1 + M2 - 2 >= 0 /\ -R1 + M2 - 2 >= 0 /\ Q1 + M2 - 2 >= 0 /\ -Q1 + M2 - 2 >= 0 /\ O1 + M2 - 2 >= 0 /\ -O1 + M2 - 2 >= 0 /\ N1 + M2 - 2 >= 0 /\ -N1 + M2 - 2 >= 0 /\ M1 + M2 - 2 >= 0 /\ -M1 + M2 - 2 >= 0 /\ L1 + M2 - 2 >= 0 /\ -L1 + M2 - 2 >= 0 /\ I1 + M2 - 2 >= 0 /\ -I1 + M2 - 2 >= 0 /\ H1 + M2 - 2 >= 0 /\ -H1 + M2 - 2 >= 0 /\ C + M2 - 3 >= 0 /\ A + M2 - 4 >= 0 /\ I2 >= 0 /\ H2 + I2 + 1 >= 0 /\ -H2 + I2 - 1 >= 0 /\ G2 + I2 >= 0 /\ C2 + I2 - 2 >= 0 /\ Z1 + I2 - 2 >= 0 /\ R1 + I2 >= 0 /\ -R1 + I2 >= 0 /\ Q1 + I2 >= 0 /\ -Q1 + I2 >= 0 /\ O1 + I2 >= 0 /\ -O1 + I2 >= 0 /\ N1 + I2 >= 0 /\ -N1 + I2 >= 0 /\ M1 + I2 >= 0 /\ -M1 + I2 >= 0 /\ L1 + I2 >= 0 /\ -L1 + I2 >= 0 /\ I1 + I2 >= 0 /\ -I1 + I2 >= 0 /\ H1 + I2 >= 0 /\ -H1 + I2 >= 0 /\ C + I2 - 1 >= 0 /\ A + I2 - 2 >= 0 /\ -H2 - 1 >= 0 /\ G2 - H2 - 1 >= 0 /\ C2 - H2 - 3 >= 0 /\ Z1 - H2 - 3 >= 0 /\ R1 - H2 - 1 >= 0 /\ -R1 - H2 - 1 >= 0 /\ Q1 - H2 - 1 >= 0 /\ -Q1 - H2 - 1 >= 0 /\ O1 - H2 - 1 >= 0 /\ -O1 - H2 - 1 >= 0 /\ N1 - H2 - 1 >= 0 /\ -N1 - H2 - 1 >= 0 /\ M1 - H2 - 1 >= 0 /\ -M1 - H2 - 1 >= 0 /\ L1 - H2 - 1 >= 0 /\ -L1 - H2 - 1 >= 0 /\ I1 - H2 - 1 >= 0 /\ -I1 - H2 - 1 >= 0 /\ H1 - H2 - 1 >= 0 /\ -H1 - H2 - 1 >= 0 /\ C - H2 - 2 >= 0 /\ A - H2 - 3 >= 0 /\ H2 + 1 >= 0 /\ G2 + H2 + 1 >= 0 /\ C2 + H2 - 1 >= 0 /\ Z1 + H2 - 1 >= 0 /\ R1 + H2 + 1 >= 0 /\ -R1 + H2 + 1 >= 0 /\ Q1 + H2 + 1 >= 0 /\ -Q1 + H2 + 1 >= 0 /\ O1 + H2 + 1 >= 0 /\ -O1 + H2 + 1 >= 0 /\ N1 + H2 + 1 >= 0 /\ -N1 + H2 + 1 >= 0 /\ M1 + H2 + 1 >= 0 /\ -M1 + H2 + 1 >= 0 /\ L1 + H2 + 1 >= 0 /\ -L1 + H2 + 1 >= 0 /\ I1 + H2 + 1 >= 0 /\ -I1 + H2 + 1 >= 0 /\ H1 + H2 + 1 >= 0 /\ -H1 + H2 + 1 >= 0 /\ C + H2 >= 0 /\ A + H2 - 1 >= 0 /\ G2 >= 0 /\ C2 + G2 - 2 >= 0 /\ Z1 + G2 - 2 >= 0 /\ R1 + G2 >= 0 /\ -R1 + G2 >= 0 /\ Q1 + G2 >= 0 /\ -Q1 + G2 >= 0 /\ O1 + G2 >= 0 /\ -O1 + G2 >= 0 /\ N1 + G2 >= 0 /\ -N1 + G2 >= 0 /\ M1 + G2 >= 0 /\ -M1 + G2 >= 0 /\ L1 + G2 >= 0 /\ -L1 + G2 >= 0 /\ I1 + G2 >= 0 /\ -I1 + G2 >= 0 /\ H1 + G2 >= 0 /\ -H1 + G2 >= 0 /\ C + G2 - 1 >= 0 /\ A + G2 - 2 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ R1 + C2 - 2 >= 0 /\ -R1 + C2 - 2 >= 0 /\ Q1 + C2 - 2 >= 0 /\ -Q1 + C2 - 2 >= 0 /\ O1 + C2 - 2 >= 0 /\ -O1 + C2 - 2 >= 0 /\ N1 + C2 - 2 >= 0 /\ -N1 + C2 - 2 >= 0 /\ M1 + C2 - 2 >= 0 /\ -M1 + C2 - 2 >= 0 /\ L1 + C2 - 2 >= 0 /\ -L1 + C2 - 2 >= 0 /\ I1 + C2 - 2 >= 0 /\ -I1 + C2 - 2 >= 0 /\ H1 + C2 - 2 >= 0 /\ -H1 + C2 - 2 >= 0 /\ C + C2 - 3 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ R1 + Z1 - 2 >= 0 /\ -R1 + Z1 - 2 >= 0 /\ Q1 + Z1 - 2 >= 0 /\ -Q1 + Z1 - 2 >= 0 /\ O1 + Z1 - 2 >= 0 /\ -O1 + Z1 - 2 >= 0 /\ N1 + Z1 - 2 >= 0 /\ -N1 + Z1 - 2 >= 0 /\ M1 + Z1 - 2 >= 0 /\ -M1 + Z1 - 2 >= 0 /\ L1 + Z1 - 2 >= 0 /\ -L1 + Z1 - 2 >= 0 /\ I1 + Z1 - 2 >= 0 /\ -I1 + Z1 - 2 >= 0 /\ H1 + Z1 - 2 >= 0 /\ -H1 + Z1 - 2 >= 0 /\ C + Z1 - 3 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ -R1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 - R1 >= 0 /\ O1 - R1 >= 0 /\ -O1 - R1 >= 0 /\ N1 - R1 >= 0 /\ -N1 - R1 >= 0 /\ M1 - R1 >= 0 /\ -M1 - R1 >= 0 /\ L1 - R1 >= 0 /\ -L1 - R1 >= 0 /\ I1 - R1 >= 0 /\ -I1 - R1 >= 0 /\ H1 - R1 >= 0 /\ -H1 - R1 >= 0 /\ C - R1 - 1 >= 0 /\ A - R1 - 2 >= 0 /\ R1 >= 0 /\ Q1 + R1 >= 0 /\ -Q1 + R1 >= 0 /\ O1 + R1 >= 0 /\ -O1 + R1 >= 0 /\ N1 + R1 >= 0 /\ -N1 + R1 >= 0 /\ M1 + R1 >= 0 /\ -M1 + R1 >= 0 /\ L1 + R1 >= 0 /\ -L1 + R1 >= 0 /\ I1 + R1 >= 0 /\ -I1 + R1 >= 0 /\ H1 + R1 >= 0 /\ -H1 + R1 >= 0 /\ C + R1 - 1 >= 0 /\ A + R1 - 2 >= 0 /\ -Q1 >= 0 /\ O1 - Q1 >= 0 /\ -O1 - Q1 >= 0 /\ N1 - Q1 >= 0 /\ -N1 - Q1 >= 0 /\ M1 - Q1 >= 0 /\ -M1 - Q1 >= 0 /\ L1 - Q1 >= 0 /\ -L1 - Q1 >= 0 /\ I1 - Q1 >= 0 /\ -I1 - Q1 >= 0 /\ H1 - Q1 >= 0 /\ -H1 - Q1 >= 0 /\ C - Q1 - 1 >= 0 /\ A - Q1 - 2 >= 0 /\ Q1 >= 0 /\ O1 + Q1 >= 0 /\ -O1 + Q1 >= 0 /\ N1 + Q1 >= 0 /\ -N1 + Q1 >= 0 /\ M1 + Q1 >= 0 /\ -M1 + Q1 >= 0 /\ L1 + Q1 >= 0 /\ -L1 + Q1 >= 0 /\ I1 + Q1 >= 0 /\ -I1 + Q1 >= 0 /\ H1 + Q1 >= 0 /\ -H1 + Q1 >= 0 /\ C + Q1 - 1 >= 0 /\ A + Q1 - 2 >= 0 /\ -O1 >= 0 /\ N1 - O1 >= 0 /\ -N1 - O1 >= 0 /\ M1 - O1 >= 0 /\ -M1 - O1 >= 0 /\ L1 - O1 >= 0 /\ -L1 - O1 >= 0 /\ I1 - O1 >= 0 /\ -I1 - O1 >= 0 /\ H1 - O1 >= 0 /\ -H1 - O1 >= 0 /\ C - O1 - 1 >= 0 /\ A - O1 - 2 >= 0 /\ O1 >= 0 /\ N1 + O1 >= 0 /\ -N1 + O1 >= 0 /\ M1 + O1 >= 0 /\ -M1 + O1 >= 0 /\ L1 + O1 >= 0 /\ -L1 + O1 >= 0 /\ I1 + O1 >= 0 /\ -I1 + O1 >= 0 /\ H1 + O1 >= 0 /\ -H1 + O1 >= 0 /\ C + O1 - 1 >= 0 /\ A + O1 - 2 >= 0 /\ -N1 >= 0 /\ M1 - N1 >= 0 /\ -M1 - N1 >= 0 /\ L1 - N1 >= 0 /\ -L1 - N1 >= 0 /\ I1 - N1 >= 0 /\ -I1 - N1 >= 0 /\ H1 - N1 >= 0 /\ -H1 - N1 >= 0 /\ C - N1 - 1 >= 0 /\ A - N1 - 2 >= 0 /\ N1 >= 0 /\ M1 + N1 >= 0 /\ -M1 + N1 >= 0 /\ L1 + N1 >= 0 /\ -L1 + N1 >= 0 /\ I1 + N1 >= 0 /\ -I1 + N1 >= 0 /\ H1 + N1 >= 0 /\ -H1 + N1 >= 0 /\ C + N1 - 1 >= 0 /\ A + N1 - 2 >= 0 /\ G1 - D + 1 >= 0 /\ -J1 + D - 1 >= 0 /\ -G1 + D - 1 >= 0 /\ -M1 >= 0 /\ L1 - M1 >= 0 /\ -L1 - M1 >= 0 /\ I1 - M1 >= 0 /\ -I1 - M1 >= 0 /\ H1 - M1 >= 0 /\ -H1 - M1 >= 0 /\ C - M1 - 1 >= 0 /\ A - M1 - 2 >= 0 /\ M1 >= 0 /\ L1 + M1 >= 0 /\ -L1 + M1 >= 0 /\ I1 + M1 >= 0 /\ -I1 + M1 >= 0 /\ H1 + M1 >= 0 /\ -H1 + M1 >= 0 /\ C + M1 - 1 >= 0 /\ A + M1 - 2 >= 0 /\ -L1 >= 0 /\ I1 - L1 >= 0 /\ -I1 - L1 >= 0 /\ H1 - L1 >= 0 /\ -H1 - L1 >= 0 /\ C - L1 - 1 >= 0 /\ A - L1 - 2 >= 0 /\ L1 >= 0 /\ I1 + L1 >= 0 /\ -I1 + L1 >= 0 /\ H1 + L1 >= 0 /\ -H1 + L1 >= 0 /\ C + L1 - 1 >= 0 /\ A + L1 - 2 >= 0 /\ G1 - J1 >= 0 /\ -I1 >= 0 /\ H1 - I1 >= 0 /\ -H1 - I1 >= 0 /\ C - I1 - 1 >= 0 /\ A - I1 - 2 >= 0 /\ I1 >= 0 /\ H1 + I1 >= 0 /\ -H1 + I1 >= 0 /\ C + I1 - 1 >= 0 /\ A + I1 - 2 >= 0 /\ -H1 >= 0 /\ C - H1 - 1 >= 0 /\ A - H1 - 2 >= 0 /\ H1 >= 0 /\ C + H1 - 1 >= 0 /\ A + H1 - 2 >= 0 /\ C - 1 >= 0 /\ A + C - 3 >= 0 /\ A - 2 >= 0 /\ J1 >= 0 /\ L1 = I1 ]
  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, 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) -> Com_1(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, J1 - 1, K1, 0, R1, 0, R1, P1, 0, R1, J1 - 1, 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)) [ H >= 0 /\ M2 + H - 2 >= 0 /\ -M2 + H + 2 >= 0 /\ I2 + H >= 0 /\ H2 + H + 1 >= 0 /\ -H2 + H - 1 >= 0 /\ G2 + H >= 0 /\ C2 + H - 2 >= 0 /\ Z1 + H - 2 >= 0 /\ R1 + H >= 0 /\ -R1 + H >= 0 /\ Q1 + H >= 0 /\ -Q1 + H >= 0 /\ O1 + H >= 0 /\ -O1 + H >= 0 /\ N1 + H >= 0 /\ -N1 + H >= 0 /\ M1 + H >= 0 /\ -M1 + H >= 0 /\ L1 + H >= 0 /\ -L1 + H >= 0 /\ I1 + H >= 0 /\ -I1 + H >= 0 /\ H1 + H >= 0 /\ -H1 + H >= 0 /\ C + H - 1 >= 0 /\ A + H - 2 >= 0 /\ -M2 + 2 >= 0 /\ I2 - M2 + 2 >= 0 /\ H2 - M2 + 3 >= 0 /\ -H2 - M2 + 1 >= 0 /\ G2 - M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ R1 - M2 + 2 >= 0 /\ -R1 - M2 + 2 >= 0 /\ Q1 - M2 + 2 >= 0 /\ -Q1 - M2 + 2 >= 0 /\ O1 - M2 + 2 >= 0 /\ -O1 - M2 + 2 >= 0 /\ N1 - M2 + 2 >= 0 /\ -N1 - M2 + 2 >= 0 /\ M1 - M2 + 2 >= 0 /\ -M1 - M2 + 2 >= 0 /\ L1 - M2 + 2 >= 0 /\ -L1 - M2 + 2 >= 0 /\ I1 - M2 + 2 >= 0 /\ -I1 - M2 + 2 >= 0 /\ H1 - M2 + 2 >= 0 /\ -H1 - M2 + 2 >= 0 /\ C - M2 + 1 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ I2 + M2 - 2 >= 0 /\ H2 + M2 - 1 >= 0 /\ -H2 + M2 - 3 >= 0 /\ G2 + M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ R1 + M2 - 2 >= 0 /\ -R1 + M2 - 2 >= 0 /\ Q1 + M2 - 2 >= 0 /\ -Q1 + M2 - 2 >= 0 /\ O1 + M2 - 2 >= 0 /\ -O1 + M2 - 2 >= 0 /\ N1 + M2 - 2 >= 0 /\ -N1 + M2 - 2 >= 0 /\ M1 + M2 - 2 >= 0 /\ -M1 + M2 - 2 >= 0 /\ L1 + M2 - 2 >= 0 /\ -L1 + M2 - 2 >= 0 /\ I1 + M2 - 2 >= 0 /\ -I1 + M2 - 2 >= 0 /\ H1 + M2 - 2 >= 0 /\ -H1 + M2 - 2 >= 0 /\ C + M2 - 3 >= 0 /\ A + M2 - 4 >= 0 /\ I2 >= 0 /\ H2 + I2 + 1 >= 0 /\ -H2 + I2 - 1 >= 0 /\ G2 + I2 >= 0 /\ C2 + I2 - 2 >= 0 /\ Z1 + I2 - 2 >= 0 /\ R1 + I2 >= 0 /\ -R1 + I2 >= 0 /\ Q1 + I2 >= 0 /\ -Q1 + I2 >= 0 /\ O1 + I2 >= 0 /\ -O1 + I2 >= 0 /\ N1 + I2 >= 0 /\ -N1 + I2 >= 0 /\ M1 + I2 >= 0 /\ -M1 + I2 >= 0 /\ L1 + I2 >= 0 /\ -L1 + I2 >= 0 /\ I1 + I2 >= 0 /\ -I1 + I2 >= 0 /\ H1 + I2 >= 0 /\ -H1 + I2 >= 0 /\ C + I2 - 1 >= 0 /\ A + I2 - 2 >= 0 /\ -H2 - 1 >= 0 /\ G2 - H2 - 1 >= 0 /\ C2 - H2 - 3 >= 0 /\ Z1 - H2 - 3 >= 0 /\ R1 - H2 - 1 >= 0 /\ -R1 - H2 - 1 >= 0 /\ Q1 - H2 - 1 >= 0 /\ -Q1 - H2 - 1 >= 0 /\ O1 - H2 - 1 >= 0 /\ -O1 - H2 - 1 >= 0 /\ N1 - H2 - 1 >= 0 /\ -N1 - H2 - 1 >= 0 /\ M1 - H2 - 1 >= 0 /\ -M1 - H2 - 1 >= 0 /\ L1 - H2 - 1 >= 0 /\ -L1 - H2 - 1 >= 0 /\ I1 - H2 - 1 >= 0 /\ -I1 - H2 - 1 >= 0 /\ H1 - H2 - 1 >= 0 /\ -H1 - H2 - 1 >= 0 /\ C - H2 - 2 >= 0 /\ A - H2 - 3 >= 0 /\ H2 + 1 >= 0 /\ G2 + H2 + 1 >= 0 /\ C2 + H2 - 1 >= 0 /\ Z1 + H2 - 1 >= 0 /\ R1 + H2 + 1 >= 0 /\ -R1 + H2 + 1 >= 0 /\ Q1 + H2 + 1 >= 0 /\ -Q1 + H2 + 1 >= 0 /\ O1 + H2 + 1 >= 0 /\ -O1 + H2 + 1 >= 0 /\ N1 + H2 + 1 >= 0 /\ -N1 + H2 + 1 >= 0 /\ M1 + H2 + 1 >= 0 /\ -M1 + H2 + 1 >= 0 /\ L1 + H2 + 1 >= 0 /\ -L1 + H2 + 1 >= 0 /\ I1 + H2 + 1 >= 0 /\ -I1 + H2 + 1 >= 0 /\ H1 + H2 + 1 >= 0 /\ -H1 + H2 + 1 >= 0 /\ C + H2 >= 0 /\ A + H2 - 1 >= 0 /\ G2 >= 0 /\ C2 + G2 - 2 >= 0 /\ Z1 + G2 - 2 >= 0 /\ R1 + G2 >= 0 /\ -R1 + G2 >= 0 /\ Q1 + G2 >= 0 /\ -Q1 + G2 >= 0 /\ O1 + G2 >= 0 /\ -O1 + G2 >= 0 /\ N1 + G2 >= 0 /\ -N1 + G2 >= 0 /\ M1 + G2 >= 0 /\ -M1 + G2 >= 0 /\ L1 + G2 >= 0 /\ -L1 + G2 >= 0 /\ I1 + G2 >= 0 /\ -I1 + G2 >= 0 /\ H1 + G2 >= 0 /\ -H1 + G2 >= 0 /\ C + G2 - 1 >= 0 /\ A + G2 - 2 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ R1 + C2 - 2 >= 0 /\ -R1 + C2 - 2 >= 0 /\ Q1 + C2 - 2 >= 0 /\ -Q1 + C2 - 2 >= 0 /\ O1 + C2 - 2 >= 0 /\ -O1 + C2 - 2 >= 0 /\ N1 + C2 - 2 >= 0 /\ -N1 + C2 - 2 >= 0 /\ M1 + C2 - 2 >= 0 /\ -M1 + C2 - 2 >= 0 /\ L1 + C2 - 2 >= 0 /\ -L1 + C2 - 2 >= 0 /\ I1 + C2 - 2 >= 0 /\ -I1 + C2 - 2 >= 0 /\ H1 + C2 - 2 >= 0 /\ -H1 + C2 - 2 >= 0 /\ C + C2 - 3 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ R1 + Z1 - 2 >= 0 /\ -R1 + Z1 - 2 >= 0 /\ Q1 + Z1 - 2 >= 0 /\ -Q1 + Z1 - 2 >= 0 /\ O1 + Z1 - 2 >= 0 /\ -O1 + Z1 - 2 >= 0 /\ N1 + Z1 - 2 >= 0 /\ -N1 + Z1 - 2 >= 0 /\ M1 + Z1 - 2 >= 0 /\ -M1 + Z1 - 2 >= 0 /\ L1 + Z1 - 2 >= 0 /\ -L1 + Z1 - 2 >= 0 /\ I1 + Z1 - 2 >= 0 /\ -I1 + Z1 - 2 >= 0 /\ H1 + Z1 - 2 >= 0 /\ -H1 + Z1 - 2 >= 0 /\ C + Z1 - 3 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ -R1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 - R1 >= 0 /\ O1 - R1 >= 0 /\ -O1 - R1 >= 0 /\ N1 - R1 >= 0 /\ -N1 - R1 >= 0 /\ M1 - R1 >= 0 /\ -M1 - R1 >= 0 /\ L1 - R1 >= 0 /\ -L1 - R1 >= 0 /\ I1 - R1 >= 0 /\ -I1 - R1 >= 0 /\ H1 - R1 >= 0 /\ -H1 - R1 >= 0 /\ C - R1 - 1 >= 0 /\ A - R1 - 2 >= 0 /\ R1 >= 0 /\ Q1 + R1 >= 0 /\ -Q1 + R1 >= 0 /\ O1 + R1 >= 0 /\ -O1 + R1 >= 0 /\ N1 + R1 >= 0 /\ -N1 + R1 >= 0 /\ M1 + R1 >= 0 /\ -M1 + R1 >= 0 /\ L1 + R1 >= 0 /\ -L1 + R1 >= 0 /\ I1 + R1 >= 0 /\ -I1 + R1 >= 0 /\ H1 + R1 >= 0 /\ -H1 + R1 >= 0 /\ C + R1 - 1 >= 0 /\ A + R1 - 2 >= 0 /\ -Q1 >= 0 /\ O1 - Q1 >= 0 /\ -O1 - Q1 >= 0 /\ N1 - Q1 >= 0 /\ -N1 - Q1 >= 0 /\ M1 - Q1 >= 0 /\ -M1 - Q1 >= 0 /\ L1 - Q1 >= 0 /\ -L1 - Q1 >= 0 /\ I1 - Q1 >= 0 /\ -I1 - Q1 >= 0 /\ H1 - Q1 >= 0 /\ -H1 - Q1 >= 0 /\ C - Q1 - 1 >= 0 /\ A - Q1 - 2 >= 0 /\ Q1 >= 0 /\ O1 + Q1 >= 0 /\ -O1 + Q1 >= 0 /\ N1 + Q1 >= 0 /\ -N1 + Q1 >= 0 /\ M1 + Q1 >= 0 /\ -M1 + Q1 >= 0 /\ L1 + Q1 >= 0 /\ -L1 + Q1 >= 0 /\ I1 + Q1 >= 0 /\ -I1 + Q1 >= 0 /\ H1 + Q1 >= 0 /\ -H1 + Q1 >= 0 /\ C + Q1 - 1 >= 0 /\ A + Q1 - 2 >= 0 /\ -O1 >= 0 /\ N1 - O1 >= 0 /\ -N1 - O1 >= 0 /\ M1 - O1 >= 0 /\ -M1 - O1 >= 0 /\ L1 - O1 >= 0 /\ -L1 - O1 >= 0 /\ I1 - O1 >= 0 /\ -I1 - O1 >= 0 /\ H1 - O1 >= 0 /\ -H1 - O1 >= 0 /\ C - O1 - 1 >= 0 /\ A - O1 - 2 >= 0 /\ O1 >= 0 /\ N1 + O1 >= 0 /\ -N1 + O1 >= 0 /\ M1 + O1 >= 0 /\ -M1 + O1 >= 0 /\ L1 + O1 >= 0 /\ -L1 + O1 >= 0 /\ I1 + O1 >= 0 /\ -I1 + O1 >= 0 /\ H1 + O1 >= 0 /\ -H1 + O1 >= 0 /\ C + O1 - 1 >= 0 /\ A + O1 - 2 >= 0 /\ -N1 >= 0 /\ M1 - N1 >= 0 /\ -M1 - N1 >= 0 /\ L1 - N1 >= 0 /\ -L1 - N1 >= 0 /\ I1 - N1 >= 0 /\ -I1 - N1 >= 0 /\ H1 - N1 >= 0 /\ -H1 - N1 >= 0 /\ C - N1 - 1 >= 0 /\ A - N1 - 2 >= 0 /\ N1 >= 0 /\ M1 + N1 >= 0 /\ -M1 + N1 >= 0 /\ L1 + N1 >= 0 /\ -L1 + N1 >= 0 /\ I1 + N1 >= 0 /\ -I1 + N1 >= 0 /\ H1 + N1 >= 0 /\ -H1 + N1 >= 0 /\ C + N1 - 1 >= 0 /\ A + N1 - 2 >= 0 /\ G1 - D + 1 >= 0 /\ -J1 + D - 1 >= 0 /\ -G1 + D - 1 >= 0 /\ -M1 >= 0 /\ L1 - M1 >= 0 /\ -L1 - M1 >= 0 /\ I1 - M1 >= 0 /\ -I1 - M1 >= 0 /\ H1 - M1 >= 0 /\ -H1 - M1 >= 0 /\ C - M1 - 1 >= 0 /\ A - M1 - 2 >= 0 /\ M1 >= 0 /\ L1 + M1 >= 0 /\ -L1 + M1 >= 0 /\ I1 + M1 >= 0 /\ -I1 + M1 >= 0 /\ H1 + M1 >= 0 /\ -H1 + M1 >= 0 /\ C + M1 - 1 >= 0 /\ A + M1 - 2 >= 0 /\ -L1 >= 0 /\ I1 - L1 >= 0 /\ -I1 - L1 >= 0 /\ H1 - L1 >= 0 /\ -H1 - L1 >= 0 /\ C - L1 - 1 >= 0 /\ A - L1 - 2 >= 0 /\ L1 >= 0 /\ I1 + L1 >= 0 /\ -I1 + L1 >= 0 /\ H1 + L1 >= 0 /\ -H1 + L1 >= 0 /\ C + L1 - 1 >= 0 /\ A + L1 - 2 >= 0 /\ G1 - J1 >= 0 /\ -I1 >= 0 /\ H1 - I1 >= 0 /\ -H1 - I1 >= 0 /\ C - I1 - 1 >= 0 /\ A - I1 - 2 >= 0 /\ I1 >= 0 /\ H1 + I1 >= 0 /\ -H1 + I1 >= 0 /\ C + I1 - 1 >= 0 /\ A + I1 - 2 >= 0 /\ -H1 >= 0 /\ C - H1 - 1 >= 0 /\ A - H1 - 2 >= 0 /\ H1 >= 0 /\ C + H1 - 1 >= 0 /\ A + H1 - 2 >= 0 /\ C - 1 >= 0 /\ A + C - 3 >= 0 /\ A - 2 >= 0 /\ A >= 2 /\ J1 >= 0 /\ C >= 1 /\ Q1 = 0 /\ R1 = O1 /\ N1 = 0 /\ M1 = O1 /\ L1 = 0 ]
  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, 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) -> Com_1(f13(A, B, C, U1 + 1, E, F, G, H, I, 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, 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)) [ -M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ -C - M2 + 2 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ -C + M2 - 2 >= 0 /\ A + M2 - 4 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ -C + C2 - 2 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ -C + Z1 - 2 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 + R1 >= 0 /\ -C >= 0 /\ A - C - 2 >= 0 /\ A - 2 >= 0 /\ Y2 >= 0 /\ A >= 2 /\ 0 >= C /\ D >= 0 /\ H >= 0 /\ Q1 = 0 ]
  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, 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) -> Com_1(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, 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)) [ -M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ -C - M2 + 2 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ -C + M2 - 2 >= 0 /\ A + M2 - 4 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ -C + C2 - 2 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ -C + Z1 - 2 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 + R1 >= 0 /\ -C >= 0 /\ A - C - 2 >= 0 /\ A - 2 >= 0 /\ A >= 2 /\ D >= 0 /\ 0 >= Y /\ H >= 0 ]
  f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, 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) -> Com_1(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, 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)) [ H >= 0 /\ M2 + H - 2 >= 0 /\ -M2 + H + 2 >= 0 /\ K2 + H + 1 >= 0 /\ -K2 + H - 1 >= 0 /\ J2 + H >= 0 /\ C2 + H - 2 >= 0 /\ Z1 + H - 2 >= 0 /\ R1 + H >= 0 /\ -R1 + H >= 0 /\ Q1 + H >= 0 /\ -Q1 + H >= 0 /\ O1 + H >= 0 /\ -O1 + H >= 0 /\ N1 + H >= 0 /\ -N1 + H >= 0 /\ M1 + H >= 0 /\ -M1 + H >= 0 /\ L1 + H >= 0 /\ -L1 + H >= 0 /\ I1 + H >= 0 /\ -I1 + H >= 0 /\ H1 + H >= 0 /\ -H1 + H >= 0 /\ -C + H >= 0 /\ A + H - 2 >= 0 /\ -M2 + 2 >= 0 /\ K2 - M2 + 3 >= 0 /\ -K2 - M2 + 1 >= 0 /\ J2 - M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ R1 - M2 + 2 >= 0 /\ -R1 - M2 + 2 >= 0 /\ Q1 - M2 + 2 >= 0 /\ -Q1 - M2 + 2 >= 0 /\ O1 - M2 + 2 >= 0 /\ -O1 - M2 + 2 >= 0 /\ N1 - M2 + 2 >= 0 /\ -N1 - M2 + 2 >= 0 /\ M1 - M2 + 2 >= 0 /\ -M1 - M2 + 2 >= 0 /\ L1 - M2 + 2 >= 0 /\ -L1 - M2 + 2 >= 0 /\ I1 - M2 + 2 >= 0 /\ -I1 - M2 + 2 >= 0 /\ H1 - M2 + 2 >= 0 /\ -H1 - M2 + 2 >= 0 /\ -C - M2 + 2 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ K2 + M2 - 1 >= 0 /\ -K2 + M2 - 3 >= 0 /\ J2 + M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ R1 + M2 - 2 >= 0 /\ -R1 + M2 - 2 >= 0 /\ Q1 + M2 - 2 >= 0 /\ -Q1 + M2 - 2 >= 0 /\ O1 + M2 - 2 >= 0 /\ -O1 + M2 - 2 >= 0 /\ N1 + M2 - 2 >= 0 /\ -N1 + M2 - 2 >= 0 /\ M1 + M2 - 2 >= 0 /\ -M1 + M2 - 2 >= 0 /\ L1 + M2 - 2 >= 0 /\ -L1 + M2 - 2 >= 0 /\ I1 + M2 - 2 >= 0 /\ -I1 + M2 - 2 >= 0 /\ H1 + M2 - 2 >= 0 /\ -H1 + M2 - 2 >= 0 /\ -C + M2 - 2 >= 0 /\ A + M2 - 4 >= 0 /\ -K2 - 1 >= 0 /\ J2 - K2 - 1 >= 0 /\ C2 - K2 - 3 >= 0 /\ Z1 - K2 - 3 >= 0 /\ R1 - K2 - 1 >= 0 /\ -R1 - K2 - 1 >= 0 /\ Q1 - K2 - 1 >= 0 /\ -Q1 - K2 - 1 >= 0 /\ O1 - K2 - 1 >= 0 /\ -O1 - K2 - 1 >= 0 /\ N1 - K2 - 1 >= 0 /\ -N1 - K2 - 1 >= 0 /\ M1 - K2 - 1 >= 0 /\ -M1 - K2 - 1 >= 0 /\ L1 - K2 - 1 >= 0 /\ -L1 - K2 - 1 >= 0 /\ I1 - K2 - 1 >= 0 /\ -I1 - K2 - 1 >= 0 /\ H1 - K2 - 1 >= 0 /\ -H1 - K2 - 1 >= 0 /\ -C - K2 - 1 >= 0 /\ A - K2 - 3 >= 0 /\ K2 + 1 >= 0 /\ J2 + K2 + 1 >= 0 /\ C2 + K2 - 1 >= 0 /\ Z1 + K2 - 1 >= 0 /\ R1 + K2 + 1 >= 0 /\ -R1 + K2 + 1 >= 0 /\ Q1 + K2 + 1 >= 0 /\ -Q1 + K2 + 1 >= 0 /\ O1 + K2 + 1 >= 0 /\ -O1 + K2 + 1 >= 0 /\ N1 + K2 + 1 >= 0 /\ -N1 + K2 + 1 >= 0 /\ M1 + K2 + 1 >= 0 /\ -M1 + K2 + 1 >= 0 /\ L1 + K2 + 1 >= 0 /\ -L1 + K2 + 1 >= 0 /\ I1 + K2 + 1 >= 0 /\ -I1 + K2 + 1 >= 0 /\ H1 + K2 + 1 >= 0 /\ -H1 + K2 + 1 >= 0 /\ -C + K2 + 1 >= 0 /\ A + K2 - 1 >= 0 /\ J2 >= 0 /\ C2 + J2 - 2 >= 0 /\ Z1 + J2 - 2 >= 0 /\ R1 + J2 >= 0 /\ -R1 + J2 >= 0 /\ Q1 + J2 >= 0 /\ -Q1 + J2 >= 0 /\ O1 + J2 >= 0 /\ -O1 + J2 >= 0 /\ N1 + J2 >= 0 /\ -N1 + J2 >= 0 /\ M1 + J2 >= 0 /\ -M1 + J2 >= 0 /\ L1 + J2 >= 0 /\ -L1 + J2 >= 0 /\ I1 + J2 >= 0 /\ -I1 + J2 >= 0 /\ H1 + J2 >= 0 /\ -H1 + J2 >= 0 /\ -C + J2 >= 0 /\ A + J2 - 2 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ R1 + C2 - 2 >= 0 /\ -R1 + C2 - 2 >= 0 /\ Q1 + C2 - 2 >= 0 /\ -Q1 + C2 - 2 >= 0 /\ O1 + C2 - 2 >= 0 /\ -O1 + C2 - 2 >= 0 /\ N1 + C2 - 2 >= 0 /\ -N1 + C2 - 2 >= 0 /\ M1 + C2 - 2 >= 0 /\ -M1 + C2 - 2 >= 0 /\ L1 + C2 - 2 >= 0 /\ -L1 + C2 - 2 >= 0 /\ I1 + C2 - 2 >= 0 /\ -I1 + C2 - 2 >= 0 /\ H1 + C2 - 2 >= 0 /\ -H1 + C2 - 2 >= 0 /\ -C + C2 - 2 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ R1 + Z1 - 2 >= 0 /\ -R1 + Z1 - 2 >= 0 /\ Q1 + Z1 - 2 >= 0 /\ -Q1 + Z1 - 2 >= 0 /\ O1 + Z1 - 2 >= 0 /\ -O1 + Z1 - 2 >= 0 /\ N1 + Z1 - 2 >= 0 /\ -N1 + Z1 - 2 >= 0 /\ M1 + Z1 - 2 >= 0 /\ -M1 + Z1 - 2 >= 0 /\ L1 + Z1 - 2 >= 0 /\ -L1 + Z1 - 2 >= 0 /\ I1 + Z1 - 2 >= 0 /\ -I1 + Z1 - 2 >= 0 /\ H1 + Z1 - 2 >= 0 /\ -H1 + Z1 - 2 >= 0 /\ -C + Z1 - 2 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ T1 - U1 >= 0 /\ D - U1 - 1 >= 0 /\ D - T1 - 1 >= 0 /\ -D + T1 + 1 >= 0 /\ -R1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 - R1 >= 0 /\ O1 - R1 >= 0 /\ -O1 - R1 >= 0 /\ N1 - R1 >= 0 /\ -N1 - R1 >= 0 /\ M1 - R1 >= 0 /\ -M1 - R1 >= 0 /\ L1 - R1 >= 0 /\ -L1 - R1 >= 0 /\ I1 - R1 >= 0 /\ -I1 - R1 >= 0 /\ H1 - R1 >= 0 /\ -H1 - R1 >= 0 /\ -C - R1 >= 0 /\ A - R1 - 2 >= 0 /\ R1 >= 0 /\ Q1 + R1 >= 0 /\ -Q1 + R1 >= 0 /\ O1 + R1 >= 0 /\ -O1 + R1 >= 0 /\ N1 + R1 >= 0 /\ -N1 + R1 >= 0 /\ M1 + R1 >= 0 /\ -M1 + R1 >= 0 /\ L1 + R1 >= 0 /\ -L1 + R1 >= 0 /\ I1 + R1 >= 0 /\ -I1 + R1 >= 0 /\ H1 + R1 >= 0 /\ -H1 + R1 >= 0 /\ -C + R1 >= 0 /\ A + R1 - 2 >= 0 /\ -Q1 >= 0 /\ O1 - Q1 >= 0 /\ -O1 - Q1 >= 0 /\ N1 - Q1 >= 0 /\ -N1 - Q1 >= 0 /\ M1 - Q1 >= 0 /\ -M1 - Q1 >= 0 /\ L1 - Q1 >= 0 /\ -L1 - Q1 >= 0 /\ I1 - Q1 >= 0 /\ -I1 - Q1 >= 0 /\ H1 - Q1 >= 0 /\ -H1 - Q1 >= 0 /\ -C - Q1 >= 0 /\ A - Q1 - 2 >= 0 /\ Q1 >= 0 /\ O1 + Q1 >= 0 /\ -O1 + Q1 >= 0 /\ N1 + Q1 >= 0 /\ -N1 + Q1 >= 0 /\ M1 + Q1 >= 0 /\ -M1 + Q1 >= 0 /\ L1 + Q1 >= 0 /\ -L1 + Q1 >= 0 /\ I1 + Q1 >= 0 /\ -I1 + Q1 >= 0 /\ H1 + Q1 >= 0 /\ -H1 + Q1 >= 0 /\ -C + Q1 >= 0 /\ A + Q1 - 2 >= 0 /\ -O1 >= 0 /\ N1 - O1 >= 0 /\ -N1 - O1 >= 0 /\ M1 - O1 >= 0 /\ -M1 - O1 >= 0 /\ L1 - O1 >= 0 /\ -L1 - O1 >= 0 /\ I1 - O1 >= 0 /\ -I1 - O1 >= 0 /\ H1 - O1 >= 0 /\ -H1 - O1 >= 0 /\ -C - O1 >= 0 /\ A - O1 - 2 >= 0 /\ O1 >= 0 /\ N1 + O1 >= 0 /\ -N1 + O1 >= 0 /\ M1 + O1 >= 0 /\ -M1 + O1 >= 0 /\ L1 + O1 >= 0 /\ -L1 + O1 >= 0 /\ I1 + O1 >= 0 /\ -I1 + O1 >= 0 /\ H1 + O1 >= 0 /\ -H1 + O1 >= 0 /\ -C + O1 >= 0 /\ A + O1 - 2 >= 0 /\ -N1 >= 0 /\ M1 - N1 >= 0 /\ -M1 - N1 >= 0 /\ L1 - N1 >= 0 /\ -L1 - N1 >= 0 /\ I1 - N1 >= 0 /\ -I1 - N1 >= 0 /\ H1 - N1 >= 0 /\ -H1 - N1 >= 0 /\ -C - N1 >= 0 /\ A - N1 - 2 >= 0 /\ N1 >= 0 /\ M1 + N1 >= 0 /\ -M1 + N1 >= 0 /\ L1 + N1 >= 0 /\ -L1 + N1 >= 0 /\ I1 + N1 >= 0 /\ -I1 + N1 >= 0 /\ H1 + N1 >= 0 /\ -H1 + N1 >= 0 /\ -C + N1 >= 0 /\ A + N1 - 2 >= 0 /\ -M1 >= 0 /\ L1 - M1 >= 0 /\ -L1 - M1 >= 0 /\ I1 - M1 >= 0 /\ -I1 - M1 >= 0 /\ H1 - M1 >= 0 /\ -H1 - M1 >= 0 /\ -C - M1 >= 0 /\ A - M1 - 2 >= 0 /\ M1 >= 0 /\ L1 + M1 >= 0 /\ -L1 + M1 >= 0 /\ I1 + M1 >= 0 /\ -I1 + M1 >= 0 /\ H1 + M1 >= 0 /\ -H1 + M1 >= 0 /\ -C + M1 >= 0 /\ A + M1 - 2 >= 0 /\ -L1 >= 0 /\ I1 - L1 >= 0 /\ -I1 - L1 >= 0 /\ H1 - L1 >= 0 /\ -H1 - L1 >= 0 /\ -C - L1 >= 0 /\ A - L1 - 2 >= 0 /\ L1 >= 0 /\ I1 + L1 >= 0 /\ -I1 + L1 >= 0 /\ H1 + L1 >= 0 /\ -H1 + L1 >= 0 /\ -C + L1 >= 0 /\ A + L1 - 2 >= 0 /\ -I1 >= 0 /\ H1 - I1 >= 0 /\ -H1 - I1 >= 0 /\ -C - I1 >= 0 /\ A - I1 - 2 >= 0 /\ I1 >= 0 /\ H1 + I1 >= 0 /\ -H1 + I1 >= 0 /\ -C + I1 >= 0 /\ A + I1 - 2 >= 0 /\ -H1 >= 0 /\ -C - H1 >= 0 /\ A - H1 - 2 >= 0 /\ H1 >= 0 /\ -C + H1 >= 0 /\ A + H1 - 2 >= 0 /\ -C >= 0 /\ A - C - 2 >= 0 /\ A - 2 >= 0 /\ U1 >= 0 /\ L1 = I1 ]
  f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, 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) -> Com_1(f13(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, I1, I1, J1, K1, 0, R1, 0, R1, P1, 0, R1, S1, T1, U1 - 1, V1, U1 - 1, 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)) [ H >= 0 /\ M2 + H - 2 >= 0 /\ -M2 + H + 2 >= 0 /\ K2 + H + 1 >= 0 /\ -K2 + H - 1 >= 0 /\ J2 + H >= 0 /\ C2 + H - 2 >= 0 /\ Z1 + H - 2 >= 0 /\ R1 + H >= 0 /\ -R1 + H >= 0 /\ Q1 + H >= 0 /\ -Q1 + H >= 0 /\ O1 + H >= 0 /\ -O1 + H >= 0 /\ N1 + H >= 0 /\ -N1 + H >= 0 /\ M1 + H >= 0 /\ -M1 + H >= 0 /\ L1 + H >= 0 /\ -L1 + H >= 0 /\ I1 + H >= 0 /\ -I1 + H >= 0 /\ H1 + H >= 0 /\ -H1 + H >= 0 /\ -C + H >= 0 /\ A + H - 2 >= 0 /\ -M2 + 2 >= 0 /\ K2 - M2 + 3 >= 0 /\ -K2 - M2 + 1 >= 0 /\ J2 - M2 + 2 >= 0 /\ C2 - M2 >= 0 /\ Z1 - M2 >= 0 /\ R1 - M2 + 2 >= 0 /\ -R1 - M2 + 2 >= 0 /\ Q1 - M2 + 2 >= 0 /\ -Q1 - M2 + 2 >= 0 /\ O1 - M2 + 2 >= 0 /\ -O1 - M2 + 2 >= 0 /\ N1 - M2 + 2 >= 0 /\ -N1 - M2 + 2 >= 0 /\ M1 - M2 + 2 >= 0 /\ -M1 - M2 + 2 >= 0 /\ L1 - M2 + 2 >= 0 /\ -L1 - M2 + 2 >= 0 /\ I1 - M2 + 2 >= 0 /\ -I1 - M2 + 2 >= 0 /\ H1 - M2 + 2 >= 0 /\ -H1 - M2 + 2 >= 0 /\ -C - M2 + 2 >= 0 /\ A - M2 >= 0 /\ M2 - 2 >= 0 /\ K2 + M2 - 1 >= 0 /\ -K2 + M2 - 3 >= 0 /\ J2 + M2 - 2 >= 0 /\ C2 + M2 - 4 >= 0 /\ Z1 + M2 - 4 >= 0 /\ R1 + M2 - 2 >= 0 /\ -R1 + M2 - 2 >= 0 /\ Q1 + M2 - 2 >= 0 /\ -Q1 + M2 - 2 >= 0 /\ O1 + M2 - 2 >= 0 /\ -O1 + M2 - 2 >= 0 /\ N1 + M2 - 2 >= 0 /\ -N1 + M2 - 2 >= 0 /\ M1 + M2 - 2 >= 0 /\ -M1 + M2 - 2 >= 0 /\ L1 + M2 - 2 >= 0 /\ -L1 + M2 - 2 >= 0 /\ I1 + M2 - 2 >= 0 /\ -I1 + M2 - 2 >= 0 /\ H1 + M2 - 2 >= 0 /\ -H1 + M2 - 2 >= 0 /\ -C + M2 - 2 >= 0 /\ A + M2 - 4 >= 0 /\ -K2 - 1 >= 0 /\ J2 - K2 - 1 >= 0 /\ C2 - K2 - 3 >= 0 /\ Z1 - K2 - 3 >= 0 /\ R1 - K2 - 1 >= 0 /\ -R1 - K2 - 1 >= 0 /\ Q1 - K2 - 1 >= 0 /\ -Q1 - K2 - 1 >= 0 /\ O1 - K2 - 1 >= 0 /\ -O1 - K2 - 1 >= 0 /\ N1 - K2 - 1 >= 0 /\ -N1 - K2 - 1 >= 0 /\ M1 - K2 - 1 >= 0 /\ -M1 - K2 - 1 >= 0 /\ L1 - K2 - 1 >= 0 /\ -L1 - K2 - 1 >= 0 /\ I1 - K2 - 1 >= 0 /\ -I1 - K2 - 1 >= 0 /\ H1 - K2 - 1 >= 0 /\ -H1 - K2 - 1 >= 0 /\ -C - K2 - 1 >= 0 /\ A - K2 - 3 >= 0 /\ K2 + 1 >= 0 /\ J2 + K2 + 1 >= 0 /\ C2 + K2 - 1 >= 0 /\ Z1 + K2 - 1 >= 0 /\ R1 + K2 + 1 >= 0 /\ -R1 + K2 + 1 >= 0 /\ Q1 + K2 + 1 >= 0 /\ -Q1 + K2 + 1 >= 0 /\ O1 + K2 + 1 >= 0 /\ -O1 + K2 + 1 >= 0 /\ N1 + K2 + 1 >= 0 /\ -N1 + K2 + 1 >= 0 /\ M1 + K2 + 1 >= 0 /\ -M1 + K2 + 1 >= 0 /\ L1 + K2 + 1 >= 0 /\ -L1 + K2 + 1 >= 0 /\ I1 + K2 + 1 >= 0 /\ -I1 + K2 + 1 >= 0 /\ H1 + K2 + 1 >= 0 /\ -H1 + K2 + 1 >= 0 /\ -C + K2 + 1 >= 0 /\ A + K2 - 1 >= 0 /\ J2 >= 0 /\ C2 + J2 - 2 >= 0 /\ Z1 + J2 - 2 >= 0 /\ R1 + J2 >= 0 /\ -R1 + J2 >= 0 /\ Q1 + J2 >= 0 /\ -Q1 + J2 >= 0 /\ O1 + J2 >= 0 /\ -O1 + J2 >= 0 /\ N1 + J2 >= 0 /\ -N1 + J2 >= 0 /\ M1 + J2 >= 0 /\ -M1 + J2 >= 0 /\ L1 + J2 >= 0 /\ -L1 + J2 >= 0 /\ I1 + J2 >= 0 /\ -I1 + J2 >= 0 /\ H1 + J2 >= 0 /\ -H1 + J2 >= 0 /\ -C + J2 >= 0 /\ A + J2 - 2 >= 0 /\ C2 - 2 >= 0 /\ Z1 + C2 - 4 >= 0 /\ R1 + C2 - 2 >= 0 /\ -R1 + C2 - 2 >= 0 /\ Q1 + C2 - 2 >= 0 /\ -Q1 + C2 - 2 >= 0 /\ O1 + C2 - 2 >= 0 /\ -O1 + C2 - 2 >= 0 /\ N1 + C2 - 2 >= 0 /\ -N1 + C2 - 2 >= 0 /\ M1 + C2 - 2 >= 0 /\ -M1 + C2 - 2 >= 0 /\ L1 + C2 - 2 >= 0 /\ -L1 + C2 - 2 >= 0 /\ I1 + C2 - 2 >= 0 /\ -I1 + C2 - 2 >= 0 /\ H1 + C2 - 2 >= 0 /\ -H1 + C2 - 2 >= 0 /\ -C + C2 - 2 >= 0 /\ A + C2 - 4 >= 0 /\ -A + C2 >= 0 /\ Z1 - 2 >= 0 /\ R1 + Z1 - 2 >= 0 /\ -R1 + Z1 - 2 >= 0 /\ Q1 + Z1 - 2 >= 0 /\ -Q1 + Z1 - 2 >= 0 /\ O1 + Z1 - 2 >= 0 /\ -O1 + Z1 - 2 >= 0 /\ N1 + Z1 - 2 >= 0 /\ -N1 + Z1 - 2 >= 0 /\ M1 + Z1 - 2 >= 0 /\ -M1 + Z1 - 2 >= 0 /\ L1 + Z1 - 2 >= 0 /\ -L1 + Z1 - 2 >= 0 /\ I1 + Z1 - 2 >= 0 /\ -I1 + Z1 - 2 >= 0 /\ H1 + Z1 - 2 >= 0 /\ -H1 + Z1 - 2 >= 0 /\ -C + Z1 - 2 >= 0 /\ A + Z1 - 4 >= 0 /\ -A + Z1 >= 0 /\ T1 - U1 >= 0 /\ D - U1 - 1 >= 0 /\ D - T1 - 1 >= 0 /\ -D + T1 + 1 >= 0 /\ -R1 >= 0 /\ Q1 - R1 >= 0 /\ -Q1 - R1 >= 0 /\ O1 - R1 >= 0 /\ -O1 - R1 >= 0 /\ N1 - R1 >= 0 /\ -N1 - R1 >= 0 /\ M1 - R1 >= 0 /\ -M1 - R1 >= 0 /\ L1 - R1 >= 0 /\ -L1 - R1 >= 0 /\ I1 - R1 >= 0 /\ -I1 - R1 >= 0 /\ H1 - R1 >= 0 /\ -H1 - R1 >= 0 /\ -C - R1 >= 0 /\ A - R1 - 2 >= 0 /\ R1 >= 0 /\ Q1 + R1 >= 0 /\ -Q1 + R1 >= 0 /\ O1 + R1 >= 0 /\ -O1 + R1 >= 0 /\ N1 + R1 >= 0 /\ -N1 + R1 >= 0 /\ M1 + R1 >= 0 /\ -M1 + R1 >= 0 /\ L1 + R1 >= 0 /\ -L1 + R1 >= 0 /\ I1 + R1 >= 0 /\ -I1 + R1 >= 0 /\ H1 + R1 >= 0 /\ -H1 + R1 >= 0 /\ -C + R1 >= 0 /\ A + R1 - 2 >= 0 /\ -Q1 >= 0 /\ O1 - Q1 >= 0 /\ -O1 - Q1 >= 0 /\ N1 - Q1 >= 0 /\ -N1 - Q1 >= 0 /\ M1 - Q1 >= 0 /\ -M1 - Q1 >= 0 /\ L1 - Q1 >= 0 /\ -L1 - Q1 >= 0 /\ I1 - Q1 >= 0 /\ -I1 - Q1 >= 0 /\ H1 - Q1 >= 0 /\ -H1 - Q1 >= 0 /\ -C - Q1 >= 0 /\ A - Q1 - 2 >= 0 /\ Q1 >= 0 /\ O1 + Q1 >= 0 /\ -O1 + Q1 >= 0 /\ N1 + Q1 >= 0 /\ -N1 + Q1 >= 0 /\ M1 + Q1 >= 0 /\ -M1 + Q1 >= 0 /\ L1 + Q1 >= 0 /\ -L1 + Q1 >= 0 /\ I1 + Q1 >= 0 /\ -I1 + Q1 >= 0 /\ H1 + Q1 >= 0 /\ -H1 + Q1 >= 0 /\ -C + Q1 >= 0 /\ A + Q1 - 2 >= 0 /\ -O1 >= 0 /\ N1 - O1 >= 0 /\ -N1 - O1 >= 0 /\ M1 - O1 >= 0 /\ -M1 - O1 >= 0 /\ L1 - O1 >= 0 /\ -L1 - O1 >= 0 /\ I1 - O1 >= 0 /\ -I1 - O1 >= 0 /\ H1 - O1 >= 0 /\ -H1 - O1 >= 0 /\ -C - O1 >= 0 /\ A - O1 - 2 >= 0 /\ O1 >= 0 /\ N1 + O1 >= 0 /\ -N1 + O1 >= 0 /\ M1 + O1 >= 0 /\ -M1 + O1 >= 0 /\ L1 + O1 >= 0 /\ -L1 + O1 >= 0 /\ I1 + O1 >= 0 /\ -I1 + O1 >= 0 /\ H1 + O1 >= 0 /\ -H1 + O1 >= 0 /\ -C + O1 >= 0 /\ A + O1 - 2 >= 0 /\ -N1 >= 0 /\ M1 - N1 >= 0 /\ -M1 - N1 >= 0 /\ L1 - N1 >= 0 /\ -L1 - N1 >= 0 /\ I1 - N1 >= 0 /\ -I1 - N1 >= 0 /\ H1 - N1 >= 0 /\ -H1 - N1 >= 0 /\ -C - N1 >= 0 /\ A - N1 - 2 >= 0 /\ N1 >= 0 /\ M1 + N1 >= 0 /\ -M1 + N1 >= 0 /\ L1 + N1 >= 0 /\ -L1 + N1 >= 0 /\ I1 + N1 >= 0 /\ -I1 + N1 >= 0 /\ H1 + N1 >= 0 /\ -H1 + N1 >= 0 /\ -C + N1 >= 0 /\ A + N1 - 2 >= 0 /\ -M1 >= 0 /\ L1 - M1 >= 0 /\ -L1 - M1 >= 0 /\ I1 - M1 >= 0 /\ -I1 - M1 >= 0 /\ H1 - M1 >= 0 /\ -H1 - M1 >= 0 /\ -C - M1 >= 0 /\ A - M1 - 2 >= 0 /\ M1 >= 0 /\ L1 + M1 >= 0 /\ -L1 + M1 >= 0 /\ I1 + M1 >= 0 /\ -I1 + M1 >= 0 /\ H1 + M1 >= 0 /\ -H1 + M1 >= 0 /\ -C + M1 >= 0 /\ A + M1 - 2 >= 0 /\ -L1 >= 0 /\ I1 - L1 >= 0 /\ -I1 - L1 >= 0 /\ H1 - L1 >= 0 /\ -H1 - L1 >= 0 /\ -C - L1 >= 0 /\ A - L1 - 2 >= 0 /\ L1 >= 0 /\ I1 + L1 >= 0 /\ -I1 + L1 >= 0 /\ H1 + L1 >= 0 /\ -H1 + L1 >= 0 /\ -C + L1 >= 0 /\ A + L1 - 2 >= 0 /\ -I1 >= 0 /\ H1 - I1 >= 0 /\ -H1 - I1 >= 0 /\ -C - I1 >= 0 /\ A - I1 - 2 >= 0 /\ I1 >= 0 /\ H1 + I1 >= 0 /\ -H1 + I1 >= 0 /\ -C + I1 >= 0 /\ A + I1 - 2 >= 0 /\ -H1 >= 0 /\ -C - H1 >= 0 /\ A - H1 - 2 >= 0 /\ H1 >= 0 /\ -C + H1 >= 0 /\ A + H1 - 2 >= 0 /\ -C >= 0 /\ A - C - 2 >= 0 /\ A - 2 >= 0 /\ A >= 2 /\ U1 >= 0 /\ 0 >= C /\ Q1 = 0 /\ R1 = O1 /\ N1 = 0 /\ M1 = O1 /\ L1 = 0 ]
)