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