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