(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (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) (RULES f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f34(A, P2, C, D, E, F, G, H, I, J, 0, L, M, N, O, P, Q, 0, 0, T, 0, 0, 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, 0, 0, L2, M2, 0, P2, N2, O2, 0)) [ M2 >= 1 ] f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f34(A, N2, C, D, E, F, G, H, I, J, 0, L, M, N, O, P, Q, 0, 0, T, 0, 0, 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, 0, 0, L2, M2, 0, N2, I2, J2, K2)) [ 0 >= M2 ] f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f65(A, B, C, D, E, F, M2, H, I, J, K, L, M, N, O, P, Q, R, 0, T, U, 0, 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, L2, M2, C2, D2, E2, F2, G2, H2, I2, J2, K2)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= B ] f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f44(A, B - 1, L2, M2, N2, F, G, H, I, J, K, L, M, N, O, P, 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)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ M2 >= 1 /\ B >= 1 /\ L2 >= 1 ] f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f44(A, B - 1, L2, M2, N2, F, G, H, I, J, K, L, M, N, O, P, 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)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= M2 /\ B >= 1 /\ L2 >= 1 ] f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f34(A, B - 1, L2, D, E, F, G, H, I, J, K, L, M, N, O, P, 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)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ B >= 1 /\ 0 >= L2 ] f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f100(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, T, U, 0, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, M2, S1, T1, U1, V1, W1, L2, M2, Z1, A2, B2, C2, D2, E2, F2, G2, H2, I2, J2, K2)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= G ] f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f75(A, B, C, D, E, L2, G - 1, M2, N2, J, K, L, M, N, O, P, 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)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ G >= 1 /\ M2 >= 1 ] f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f75(A, B, C, D, E, L2, G - 1, M2, N2, J, K, L, M, N, O, P, 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)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ G >= 1 /\ 0 >= M2 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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, C, A2, B2, C2, D2, E2, F2, G2, H2, I2, J2, K2)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ C - G2 - 1 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ C + G2 - 1 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ C - D2 - 1 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ C + D2 - 1 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ C - C2 - 1 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ C + C2 - 1 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ C - 1 >= 0 /\ V + C - 1 >= 0 /\ -V + C - 1 >= 0 /\ U + C - 1 >= 0 /\ -U + C - 1 >= 0 /\ B + C - 1 >= 0 /\ S + C - 1 >= 0 /\ -S + C - 1 >= 0 /\ R + C - 1 >= 0 /\ -R + C - 1 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ B >= 0 /\ S + B >= 0 /\ -S + B >= 0 /\ R + B >= 0 /\ -R + B >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ E >= 1 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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, C, A2, B2, C2, D2, E2, F2, G2, H2, I2, J2, K2)) [ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ C - G2 - 1 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ C + G2 - 1 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ C - D2 - 1 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ C + D2 - 1 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ C - C2 - 1 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ C + C2 - 1 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ C - 1 >= 0 /\ V + C - 1 >= 0 /\ -V + C - 1 >= 0 /\ U + C - 1 >= 0 /\ -U + C - 1 >= 0 /\ B + C - 1 >= 0 /\ S + C - 1 >= 0 /\ -S + C - 1 >= 0 /\ R + C - 1 >= 0 /\ -R + C - 1 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ B >= 0 /\ S + B >= 0 /\ -S + B >= 0 /\ R + B >= 0 /\ -R + B >= 0 /\ K + B >= 0 /\ -K + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= E ] f100(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f100(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, T, U, 0, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1 - 1, S1, L2, M2, N2, L2, X1, Y1, Z1, A2, B2, C2, D2, E2, F2, G2, H2, I2, J2, K2)) [ -G >= 0 /\ G2 - G >= 0 /\ -G2 - G >= 0 /\ D2 - G >= 0 /\ -D2 - G >= 0 /\ C2 - G >= 0 /\ -C2 - G >= 0 /\ V - G >= 0 /\ -V - G >= 0 /\ U - G >= 0 /\ -U - G >= 0 /\ -B - G >= 0 /\ S - G >= 0 /\ -S - G >= 0 /\ R - G >= 0 /\ -R - G >= 0 /\ K - G >= 0 /\ -K - G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ R1 >= 1 ] f100(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f130(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, T, U, 0, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, L2, T1, U1, V1, W1, X1, Y1, Z1, A2, B2, C2, D2, E2, F2, G2, H2, I2, J2, K2)) [ -G >= 0 /\ G2 - G >= 0 /\ -G2 - G >= 0 /\ D2 - G >= 0 /\ -D2 - G >= 0 /\ C2 - G >= 0 /\ -C2 - G >= 0 /\ V - G >= 0 /\ -V - G >= 0 /\ U - G >= 0 /\ -U - G >= 0 /\ -B - G >= 0 /\ S - G >= 0 /\ -S - G >= 0 /\ R - G >= 0 /\ -R - G >= 0 /\ K - G >= 0 /\ -K - G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= R1 ] f75(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f79(L2, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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)) [ G >= 0 /\ G2 + G >= 0 /\ -G2 + G >= 0 /\ D2 + G >= 0 /\ -D2 + G >= 0 /\ C2 + G >= 0 /\ -C2 + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ -B + G >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ K + G >= 0 /\ -K + G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ I >= 1 ] f75(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f79(L2, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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)) [ G >= 0 /\ G2 + G >= 0 /\ -G2 + G >= 0 /\ D2 + G >= 0 /\ -D2 + G >= 0 /\ C2 + G >= 0 /\ -C2 + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ -B + G >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ K + G >= 0 /\ -K + G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= I ] f79(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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)) [ G >= 0 /\ G2 + G >= 0 /\ -G2 + G >= 0 /\ D2 + G >= 0 /\ -D2 + G >= 0 /\ C2 + G >= 0 /\ -C2 + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ -B + G >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ K + G >= 0 /\ -K + G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ A >= 1 ] f79(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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)) [ G >= 0 /\ G2 + G >= 0 /\ -G2 + G >= 0 /\ D2 + G >= 0 /\ -D2 + G >= 0 /\ C2 + G >= 0 /\ -C2 + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ -B + G >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ K + G >= 0 /\ -K + G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= A ] f130(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f130(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, T, U, 0, L2, L2 - 1, Y, Z, A1, O2, C1, D1, E1, 0, G1, H1, I1, J1, K1, M2, N2, P2, P2, 0, 0, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2, C2, D2, E2, F2, G2, H2, I2, J2, K2)) [ -G >= 0 /\ G2 - G >= 0 /\ -G2 - G >= 0 /\ D2 - G >= 0 /\ -D2 - G >= 0 /\ C2 - G >= 0 /\ -C2 - G >= 0 /\ -R1 - G >= 0 /\ V - G >= 0 /\ -V - G >= 0 /\ U - G >= 0 /\ -U - G >= 0 /\ -B - G >= 0 /\ S - G >= 0 /\ -S - G >= 0 /\ R - G >= 0 /\ -R - G >= 0 /\ K - G >= 0 /\ -K - G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ -R1 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ -R1 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ -R1 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ -R1 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ -R1 - C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ -R1 + C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -R1 >= 0 /\ V - R1 >= 0 /\ -V - R1 >= 0 /\ U - R1 >= 0 /\ -U - R1 >= 0 /\ -B - R1 >= 0 /\ S - R1 >= 0 /\ -S - R1 >= 0 /\ R - R1 >= 0 /\ -R - R1 >= 0 /\ K - R1 >= 0 /\ -K - R1 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ L2 >= 1 /\ M2 >= 1 ] f130(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f130(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, T, U, 0, L2, L2 - 1, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, M2, N2, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2, C2, D2, E2, F2, G2, H2, I2, J2, K2)) [ -G >= 0 /\ G2 - G >= 0 /\ -G2 - G >= 0 /\ D2 - G >= 0 /\ -D2 - G >= 0 /\ C2 - G >= 0 /\ -C2 - G >= 0 /\ -R1 - G >= 0 /\ V - G >= 0 /\ -V - G >= 0 /\ U - G >= 0 /\ -U - G >= 0 /\ -B - G >= 0 /\ S - G >= 0 /\ -S - G >= 0 /\ R - G >= 0 /\ -R - G >= 0 /\ K - G >= 0 /\ -K - G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ -R1 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ -R1 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ -R1 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ -R1 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ -R1 - C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ -R1 + C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -R1 >= 0 /\ V - R1 >= 0 /\ -V - R1 >= 0 /\ U - R1 >= 0 /\ -U - R1 >= 0 /\ -B - R1 >= 0 /\ S - R1 >= 0 /\ -S - R1 >= 0 /\ R - R1 >= 0 /\ -R - R1 >= 0 /\ K - R1 >= 0 /\ -K - R1 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ L2 >= 1 /\ 0 >= M2 ] f130(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f191(A, B, C, D, E, F, G, H, I, N2, K, L, M, N, O, P, Q, R, 0, T, U, 0, L2, L2, M2, N2, 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)) [ -G >= 0 /\ G2 - G >= 0 /\ -G2 - G >= 0 /\ D2 - G >= 0 /\ -D2 - G >= 0 /\ C2 - G >= 0 /\ -C2 - G >= 0 /\ -R1 - G >= 0 /\ V - G >= 0 /\ -V - G >= 0 /\ U - G >= 0 /\ -U - G >= 0 /\ -B - G >= 0 /\ S - G >= 0 /\ -S - G >= 0 /\ R - G >= 0 /\ -R - G >= 0 /\ K - G >= 0 /\ -K - G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ -R1 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ -R1 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ -R1 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ -R1 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ -R1 - C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ -R1 + C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -R1 >= 0 /\ V - R1 >= 0 /\ -V - R1 >= 0 /\ U - R1 >= 0 /\ -U - R1 >= 0 /\ -B - R1 >= 0 /\ S - R1 >= 0 /\ -S - R1 >= 0 /\ R - R1 >= 0 /\ -R - R1 >= 0 /\ K - R1 >= 0 /\ -K - R1 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= L2 ] f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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)) [ G >= 0 /\ G2 + G >= 0 /\ -G2 + G >= 0 /\ D2 + G >= 0 /\ -D2 + G >= 0 /\ C2 + G >= 0 /\ -C2 + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ -B + G >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ K + G >= 0 /\ -K + G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ F >= 1 ] f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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)) [ G >= 0 /\ G2 + G >= 0 /\ -G2 + G >= 0 /\ D2 + G >= 0 /\ -D2 + G >= 0 /\ C2 + G >= 0 /\ -C2 + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ -B + G >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ K + G >= 0 /\ -K + G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -K + D2 >= 0 /\ -C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -K - C2 >= 0 /\ C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -K + C2 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ -K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -K + R >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= F ] f191(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f216(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, L2, 1, 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)) [ -G >= 0 /\ G2 - G >= 0 /\ -G2 - G >= 0 /\ D2 - G >= 0 /\ -D2 - G >= 0 /\ C2 - G >= 0 /\ -C2 - G >= 0 /\ -R1 - G >= 0 /\ -X - G >= 0 /\ V - G >= 0 /\ -V - G >= 0 /\ U - G >= 0 /\ -U - G >= 0 /\ -B - G >= 0 /\ S - G >= 0 /\ -S - G >= 0 /\ R - G >= 0 /\ -R - G >= 0 /\ K - G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ -R1 - G2 >= 0 /\ -X - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ -R1 + G2 >= 0 /\ -X + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ -R1 - D2 >= 0 /\ -X - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ -R1 + D2 >= 0 /\ -X + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -C2 >= 0 /\ -R1 - C2 >= 0 /\ -X - C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ C2 >= 0 /\ -R1 + C2 >= 0 /\ -X + C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -R1 >= 0 /\ -X - R1 >= 0 /\ V - R1 >= 0 /\ -V - R1 >= 0 /\ U - R1 >= 0 /\ -U - R1 >= 0 /\ -B - R1 >= 0 /\ S - R1 >= 0 /\ -S - R1 >= 0 /\ R - R1 >= 0 /\ -R - R1 >= 0 /\ K - R1 >= 0 /\ -X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ -B - X >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ K - X >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ K >= 0 /\ 1 >= R /\ 0 >= J ] f191(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f191(A, B, C, D, E, F, G, H, I, J - 1, 1, 0, L2, 0, 0, 2, L2, 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)) [ -G >= 0 /\ G2 - G >= 0 /\ -G2 - G >= 0 /\ D2 - G >= 0 /\ -D2 - G >= 0 /\ C2 - G >= 0 /\ -C2 - G >= 0 /\ -R1 - G >= 0 /\ -X - G >= 0 /\ V - G >= 0 /\ -V - G >= 0 /\ U - G >= 0 /\ -U - G >= 0 /\ -B - G >= 0 /\ S - G >= 0 /\ -S - G >= 0 /\ R - G >= 0 /\ -R - G >= 0 /\ K - G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ -R1 - G2 >= 0 /\ -X - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 >= 0 /\ -U - G2 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ -R1 + G2 >= 0 /\ -X + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 >= 0 /\ -U + G2 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ -R1 - D2 >= 0 /\ -X - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 >= 0 /\ -U - D2 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ -R1 + D2 >= 0 /\ -X + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 >= 0 /\ -U + D2 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -C2 >= 0 /\ -R1 - C2 >= 0 /\ -X - C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 >= 0 /\ -U - C2 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ C2 >= 0 /\ -R1 + C2 >= 0 /\ -X + C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 >= 0 /\ -U + C2 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -R1 >= 0 /\ -X - R1 >= 0 /\ V - R1 >= 0 /\ -V - R1 >= 0 /\ U - R1 >= 0 /\ -U - R1 >= 0 /\ -B - R1 >= 0 /\ S - R1 >= 0 /\ -S - R1 >= 0 /\ R - R1 >= 0 /\ -R - R1 >= 0 /\ K - R1 >= 0 /\ -X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ -B - X >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ K - X >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ K - U >= 0 /\ U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ K + U >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ K >= 0 /\ J >= 1 ] f216(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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) -> Com_1(f216(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 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)) [ -G >= 0 /\ G2 - G >= 0 /\ -G2 - G >= 0 /\ D2 - G >= 0 /\ -D2 - G >= 0 /\ C2 - G >= 0 /\ -C2 - G >= 0 /\ -R1 - G >= 0 /\ -X - G >= 0 /\ V - G >= 0 /\ -V - G >= 0 /\ U - G - 1 >= 0 /\ -U - G + 1 >= 0 /\ -B - G >= 0 /\ S - G >= 0 /\ -S - G >= 0 /\ R - G >= 0 /\ -R - G >= 0 /\ K - G >= 0 /\ -J - G >= 0 /\ -G2 >= 0 /\ D2 - G2 >= 0 /\ -D2 - G2 >= 0 /\ C2 - G2 >= 0 /\ -C2 - G2 >= 0 /\ -R1 - G2 >= 0 /\ -X - G2 >= 0 /\ V - G2 >= 0 /\ -V - G2 >= 0 /\ U - G2 - 1 >= 0 /\ -U - G2 + 1 >= 0 /\ -B - G2 >= 0 /\ S - G2 >= 0 /\ -S - G2 >= 0 /\ R - G2 >= 0 /\ -R - G2 >= 0 /\ K - G2 >= 0 /\ -J - G2 >= 0 /\ G2 >= 0 /\ D2 + G2 >= 0 /\ -D2 + G2 >= 0 /\ C2 + G2 >= 0 /\ -C2 + G2 >= 0 /\ -R1 + G2 >= 0 /\ -X + G2 >= 0 /\ V + G2 >= 0 /\ -V + G2 >= 0 /\ U + G2 - 1 >= 0 /\ -U + G2 + 1 >= 0 /\ -B + G2 >= 0 /\ S + G2 >= 0 /\ -S + G2 >= 0 /\ R + G2 >= 0 /\ -R + G2 >= 0 /\ K + G2 >= 0 /\ -J + G2 >= 0 /\ -D2 >= 0 /\ C2 - D2 >= 0 /\ -C2 - D2 >= 0 /\ -R1 - D2 >= 0 /\ -X - D2 >= 0 /\ V - D2 >= 0 /\ -V - D2 >= 0 /\ U - D2 - 1 >= 0 /\ -U - D2 + 1 >= 0 /\ -B - D2 >= 0 /\ S - D2 >= 0 /\ -S - D2 >= 0 /\ R - D2 >= 0 /\ -R - D2 >= 0 /\ K - D2 >= 0 /\ -J - D2 >= 0 /\ D2 >= 0 /\ C2 + D2 >= 0 /\ -C2 + D2 >= 0 /\ -R1 + D2 >= 0 /\ -X + D2 >= 0 /\ V + D2 >= 0 /\ -V + D2 >= 0 /\ U + D2 - 1 >= 0 /\ -U + D2 + 1 >= 0 /\ -B + D2 >= 0 /\ S + D2 >= 0 /\ -S + D2 >= 0 /\ R + D2 >= 0 /\ -R + D2 >= 0 /\ K + D2 >= 0 /\ -J + D2 >= 0 /\ -C2 >= 0 /\ -R1 - C2 >= 0 /\ -X - C2 >= 0 /\ V - C2 >= 0 /\ -V - C2 >= 0 /\ U - C2 - 1 >= 0 /\ -U - C2 + 1 >= 0 /\ -B - C2 >= 0 /\ S - C2 >= 0 /\ -S - C2 >= 0 /\ R - C2 >= 0 /\ -R - C2 >= 0 /\ K - C2 >= 0 /\ -J - C2 >= 0 /\ C2 >= 0 /\ -R1 + C2 >= 0 /\ -X + C2 >= 0 /\ V + C2 >= 0 /\ -V + C2 >= 0 /\ U + C2 - 1 >= 0 /\ -U + C2 + 1 >= 0 /\ -B + C2 >= 0 /\ S + C2 >= 0 /\ -S + C2 >= 0 /\ R + C2 >= 0 /\ -R + C2 >= 0 /\ K + C2 >= 0 /\ -J + C2 >= 0 /\ -R1 >= 0 /\ -X - R1 >= 0 /\ V - R1 >= 0 /\ -V - R1 >= 0 /\ U - R1 - 1 >= 0 /\ -U - R1 + 1 >= 0 /\ -B - R1 >= 0 /\ S - R1 >= 0 /\ -S - R1 >= 0 /\ R - R1 >= 0 /\ -R - R1 >= 0 /\ K - R1 >= 0 /\ -J - R1 >= 0 /\ -X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X - 1 >= 0 /\ -U - X + 1 >= 0 /\ -B - X >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ K - X >= 0 /\ -J - X >= 0 /\ -V >= 0 /\ U - V - 1 >= 0 /\ -U - V + 1 >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ K - V >= 0 /\ -J - V >= 0 /\ V >= 0 /\ U + V - 1 >= 0 /\ -U + V + 1 >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ K + V >= 0 /\ -J + V >= 0 /\ -U + 1 >= 0 /\ -B - U + 1 >= 0 /\ S - U + 1 >= 0 /\ -S - U + 1 >= 0 /\ R - U + 1 >= 0 /\ -R - U + 1 >= 0 /\ K - U + 1 >= 0 /\ -J - U + 1 >= 0 /\ U - 1 >= 0 /\ -B + U - 1 >= 0 /\ S + U - 1 >= 0 /\ -S + U - 1 >= 0 /\ R + U - 1 >= 0 /\ -R + U - 1 >= 0 /\ K + U - 1 >= 0 /\ -J + U - 1 >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ K - B >= 0 /\ -J - B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ K - S >= 0 /\ -J - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ K + S >= 0 /\ -J + S >= 0 /\ -R >= 0 /\ K - R >= 0 /\ -J - R >= 0 /\ R >= 0 /\ K + R >= 0 /\ -J + R >= 0 /\ K >= 0 /\ -J + K >= 0 /\ -J >= 0 ] )