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