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