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