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