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