(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)
(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) -> Com_1(f37(A, N1, C, D, L1, F, G, H, I, J, K, J1, M, N, O, P, Q, R, S, T, U, V, W, X, H1, 20, I1, I1, J1, K1, K1, L1, M1)) [ I1 >= 1 /\ M1 >= 21 ]
  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) -> Com_1(f37(A, N1, C, D, M1, F, G, H, I, J, K, K1, M, N, O, P, Q, R, S, T, U, V, W, X, H1, I1, J1, J1, K1, L1, L1, M1, I1)) [ J1 >= 1 /\ 20 >= I1 /\ I1 >= 5 ]
  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) -> Com_1(f37(A, N1, C, D, L1, F, G, H, I, J, K, J1, M, N, O, P, Q, R, S, T, U, V, W, X, H1, 5, I1, I1, J1, K1, K1, L1, M1)) [ I1 >= 1 /\ 4 >= M1 ]
  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) -> Com_1(f94(A, B, C, D, L1, F, G, H, I, J, K, 1, M, N, O, P, Q, R, S, T, U, V, W, X, H1, H1, I1, I1, J1, K1, K1, L1, G1)) [ 0 >= I1 ]
  f37(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) -> Com_1(f94(A, 0, 0, D, E, F, G, H, I, J, K, 1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ B1 - 1 >= 0 /\ B = 0 ]
  f37(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) -> Com_1(f41(A, B, B, H1, 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)) [ B1 - 1 >= 0 /\ B >= 1 ]
  f37(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) -> Com_1(f41(A, B, B, H1, 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)) [ B1 - 1 >= 0 /\ 0 >= B + 1 ]
  f94(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) -> Com_1(f94(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)) [ -L + 1 >= 0 /\ L - 1 >= 0 ]
  f41(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) -> Com_1(f48(A, B, C, D, H1, I1, G, H, I, J, K, L, D, N, O, P, Q, R, S, T, U, V, W, H1, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ D >= 1 ]
  f41(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) -> Com_1(f48(A, B, C, D, H1, I1, G, H, I, J, K, L, D, N, O, P, Q, R, S, T, U, V, W, H1, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ 0 >= D + 1 ]
  f41(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) -> Com_1(f94(A, B, C, 0, E, F, G, H, I, J, K, 1, 0, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ D = 0 ]
  f48(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) -> Com_1(f89(A, B, C, D, E - 1, -1, G, H, I, J, K, L, M, N, O, P, Q, R, -1, 0, 0, 0, 0, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ F + 1 = 0 ]
  f48(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) -> Com_1(f61(A, B, C, D, E, -1, I1, H, I, J, K, L, M, N, O, P, Q, R, -1, 0, 0, H1, H1, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ H1 >= 1 /\ F + 1 = 0 ]
  f48(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) -> Com_1(f61(A, B, C, D, E, -1, I1, H, I, J, K, L, M, N, O, P, Q, R, -1, 0, 0, H1, H1, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ 0 >= H1 + 1 /\ F + 1 = 0 ]
  f48(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) -> Com_1(f94(A, B, C, D, E, F, G, H, I, J, K, 1, M, N, O, P, Q, R, F, H1, H1, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ H1 >= 1 ]
  f48(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) -> Com_1(f94(A, B, C, D, E, F, G, H, I, J, K, 1, M, N, O, P, Q, R, F, H1, H1, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ 0 >= H1 + 1 ]
  f48(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) -> Com_1(f89(A, B, C, D, E - 1, F, G, H, I, J, K, L, M, N, O, P, Q, R, F, 0, 0, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ 0 >= F + 2 ]
  f48(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) -> Com_1(f89(A, B, C, D, E - 1, F, G, H, I, J, K, L, M, N, O, P, Q, R, F, 0, 0, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ F >= 0 ]
  f89(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) -> Com_1(f94(A, B, C, D, E, F, G, H, I, J, K, 1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ S - F >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ -T >= 0 /\ T >= 0 /\ 0 >= E ]
  f89(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) -> Com_1(f48(A, B, C, D, E, H1, 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)) [ S - F >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ -T >= 0 /\ T >= 0 /\ E >= 1 ]
  f61(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) -> Com_1(f89(A, B, C, D, E - 1, F, 0, 0, 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)) [ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ G = 0 ]
  f61(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) -> Com_1(f66(A, B, C, D, E, F, G, G, 0, H1, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ G >= 1 ]
  f61(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) -> Com_1(f66(A, B, C, D, E, F, G, G, 0, H1, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ 0 >= G + 1 ]
  f66(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) -> Com_1(f77(A, B, C, D, E, F, G, H, I, J, K, L, M, J, 0, 0, H1, H1, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ H1 >= 1 ]
  f66(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) -> Com_1(f77(A, B, C, D, E, F, G, H, I, J, K, L, M, J, 0, 0, H1, H1, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ 0 >= H1 + 1 ]
  f66(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) -> Com_1(f80(A, B, C, D, E, F, G, H, I, J, K, L, M, J, 0, 0, 0, 0, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 ]
  f66(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) -> Com_1(f84(A, B, C, D, E, F, G, H, I, J, K, L, M, J, H1, H1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ H1 >= 1 ]
  f66(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) -> Com_1(f84(A, B, C, D, E, F, G, H, I, J, K, L, M, J, H1, H1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ 0 >= H1 + 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) -> Com_1(f80(A, B, C, D, E, F, G, H, I, J, 0, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ P - F - 1 >= 0 /\ -P - F - 1 >= 0 /\ O - F - 1 >= 0 /\ -O - F - 1 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ P + F + 1 >= 0 /\ -P + F + 1 >= 0 /\ O + F + 1 >= 0 /\ -O + F + 1 >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ O + B1 - 1 >= 0 /\ -O + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -S - 1 >= 0 /\ P - S - 1 >= 0 /\ -P - S - 1 >= 0 /\ O - S - 1 >= 0 /\ -O - S - 1 >= 0 /\ S + 1 >= 0 /\ P + S + 1 >= 0 /\ -P + S + 1 >= 0 /\ O + S + 1 >= 0 /\ -O + S + 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ -O >= 0 /\ O >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ K = 0 ]
  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) -> Com_1(f78(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)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ P - F - 1 >= 0 /\ -P - F - 1 >= 0 /\ O - F - 1 >= 0 /\ -O - F - 1 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ P + F + 1 >= 0 /\ -P + F + 1 >= 0 /\ O + F + 1 >= 0 /\ -O + F + 1 >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ O + B1 - 1 >= 0 /\ -O + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -S - 1 >= 0 /\ P - S - 1 >= 0 /\ -P - S - 1 >= 0 /\ O - S - 1 >= 0 /\ -O - S - 1 >= 0 /\ S + 1 >= 0 /\ P + S + 1 >= 0 /\ -P + S + 1 >= 0 /\ O + S + 1 >= 0 /\ -O + S + 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ -O >= 0 /\ O >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ K >= 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) -> Com_1(f78(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)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ P - F - 1 >= 0 /\ -P - F - 1 >= 0 /\ O - F - 1 >= 0 /\ -O - F - 1 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ P + F + 1 >= 0 /\ -P + F + 1 >= 0 /\ O + F + 1 >= 0 /\ -O + F + 1 >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ O + B1 - 1 >= 0 /\ -O + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -S - 1 >= 0 /\ P - S - 1 >= 0 /\ -P - S - 1 >= 0 /\ O - S - 1 >= 0 /\ -O - S - 1 >= 0 /\ S + 1 >= 0 /\ P + S + 1 >= 0 /\ -P + S + 1 >= 0 /\ O + S + 1 >= 0 /\ -O + S + 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ -O >= 0 /\ O >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ 0 >= K + 1 ]
  f80(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) -> Com_1(f84(A, B, C, D, E, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I + 1 >= 0 /\ F - I + 2 >= 0 /\ -F - I >= 0 /\ B1 - I >= 0 /\ U - I + 1 >= 0 /\ -U - I + 1 >= 0 /\ T - I + 1 >= 0 /\ -T - I + 1 >= 0 /\ S - I + 2 >= 0 /\ -S - I >= 0 /\ P - I + 1 >= 0 /\ -P - I + 1 >= 0 /\ O - I + 1 >= 0 /\ -O - I + 1 >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ P - F - 1 >= 0 /\ -P - F - 1 >= 0 /\ O - F - 1 >= 0 /\ -O - F - 1 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ P + F + 1 >= 0 /\ -P + F + 1 >= 0 /\ O + F + 1 >= 0 /\ -O + F + 1 >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ O + B1 - 1 >= 0 /\ -O + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -S - 1 >= 0 /\ P - S - 1 >= 0 /\ -P - S - 1 >= 0 /\ O - S - 1 >= 0 /\ -O - S - 1 >= 0 /\ S + 1 >= 0 /\ P + S + 1 >= 0 /\ -P + S + 1 >= 0 /\ O + S + 1 >= 0 /\ -O + S + 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ -O >= 0 /\ O >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ I = 0 ]
  f80(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) -> Com_1(f84(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)) [ -I + 1 >= 0 /\ F - I + 2 >= 0 /\ -F - I >= 0 /\ B1 - I >= 0 /\ U - I + 1 >= 0 /\ -U - I + 1 >= 0 /\ T - I + 1 >= 0 /\ -T - I + 1 >= 0 /\ S - I + 2 >= 0 /\ -S - I >= 0 /\ P - I + 1 >= 0 /\ -P - I + 1 >= 0 /\ O - I + 1 >= 0 /\ -O - I + 1 >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ P - F - 1 >= 0 /\ -P - F - 1 >= 0 /\ O - F - 1 >= 0 /\ -O - F - 1 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ P + F + 1 >= 0 /\ -P + F + 1 >= 0 /\ O + F + 1 >= 0 /\ -O + F + 1 >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ O + B1 - 1 >= 0 /\ -O + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -S - 1 >= 0 /\ P - S - 1 >= 0 /\ -P - S - 1 >= 0 /\ O - S - 1 >= 0 /\ -O - S - 1 >= 0 /\ S + 1 >= 0 /\ P + S + 1 >= 0 /\ -P + S + 1 >= 0 /\ O + S + 1 >= 0 /\ -O + S + 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ -O >= 0 /\ O >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ I >= 1 ]
  f84(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) -> Com_1(f89(A, B, C, D, E - 1, 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)) [ -I + 1 >= 0 /\ F - I + 2 >= 0 /\ -F - I >= 0 /\ B1 - I >= 0 /\ U - I + 1 >= 0 /\ -U - I + 1 >= 0 /\ T - I + 1 >= 0 /\ -T - I + 1 >= 0 /\ S - I + 2 >= 0 /\ -S - I >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ I >= 1 ]
  f84(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) -> Com_1(f89(A, B, C, D, E - 1, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I + 1 >= 0 /\ F - I + 2 >= 0 /\ -F - I >= 0 /\ B1 - I >= 0 /\ U - I + 1 >= 0 /\ -U - I + 1 >= 0 /\ T - I + 1 >= 0 /\ -T - I + 1 >= 0 /\ S - I + 2 >= 0 /\ -S - I >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ -S - 1 >= 0 /\ S + 1 >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ I = 0 ]
  f78(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) -> Com_1(f80(A, B, C, D, E, F, G, H, 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ P - F - 1 >= 0 /\ -P - F - 1 >= 0 /\ O - F - 1 >= 0 /\ -O - F - 1 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ P + F + 1 >= 0 /\ -P + F + 1 >= 0 /\ O + F + 1 >= 0 /\ -O + F + 1 >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ O + B1 - 1 >= 0 /\ -O + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -S - 1 >= 0 /\ P - S - 1 >= 0 /\ -P - S - 1 >= 0 /\ O - S - 1 >= 0 /\ -O - S - 1 >= 0 /\ S + 1 >= 0 /\ P + S + 1 >= 0 /\ -P + S + 1 >= 0 /\ O + S + 1 >= 0 /\ -O + S + 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ -O >= 0 /\ O >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ A >= 1 ]
  f78(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) -> Com_1(f80(A, B, C, D, E, F, G, H, 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ P - F - 1 >= 0 /\ -P - F - 1 >= 0 /\ O - F - 1 >= 0 /\ -O - F - 1 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ P + F + 1 >= 0 /\ -P + F + 1 >= 0 /\ O + F + 1 >= 0 /\ -O + F + 1 >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ O + B1 - 1 >= 0 /\ -O + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -S - 1 >= 0 /\ P - S - 1 >= 0 /\ -P - S - 1 >= 0 /\ O - S - 1 >= 0 /\ -O - S - 1 >= 0 /\ S + 1 >= 0 /\ P + S + 1 >= 0 /\ -P + S + 1 >= 0 /\ O + S + 1 >= 0 /\ -O + S + 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ -O >= 0 /\ O >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ 0 >= A + 1 ]
  f78(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) -> Com_1(f80(0, 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)) [ -I >= 0 /\ F - I + 1 >= 0 /\ -F - I - 1 >= 0 /\ B1 - I - 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ S - I + 1 >= 0 /\ -S - I - 1 >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ I >= 0 /\ F + I + 1 >= 0 /\ -F + I - 1 >= 0 /\ B1 + I - 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ S + I + 1 >= 0 /\ -S + I - 1 >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ -F - 1 >= 0 /\ B1 - F - 2 >= 0 /\ U - F - 1 >= 0 /\ -U - F - 1 >= 0 /\ T - F - 1 >= 0 /\ -T - F - 1 >= 0 /\ S - F >= 0 /\ -S - F - 2 >= 0 /\ P - F - 1 >= 0 /\ -P - F - 1 >= 0 /\ O - F - 1 >= 0 /\ -O - F - 1 >= 0 /\ F + 1 >= 0 /\ B1 + F >= 0 /\ U + F + 1 >= 0 /\ -U + F + 1 >= 0 /\ T + F + 1 >= 0 /\ -T + F + 1 >= 0 /\ S + F + 2 >= 0 /\ -S + F >= 0 /\ P + F + 1 >= 0 /\ -P + F + 1 >= 0 /\ O + F + 1 >= 0 /\ -O + F + 1 >= 0 /\ M - D >= 0 /\ -M + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ B1 - 1 >= 0 /\ U + B1 - 1 >= 0 /\ -U + B1 - 1 >= 0 /\ T + B1 - 1 >= 0 /\ -T + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 - 2 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ O + B1 - 1 >= 0 /\ -O + B1 - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ S - U + 1 >= 0 /\ -S - U - 1 >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ S + U + 1 >= 0 /\ -S + U - 1 >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ -T >= 0 /\ S - T + 1 >= 0 /\ -S - T - 1 >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ T >= 0 /\ S + T + 1 >= 0 /\ -S + T - 1 >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ -S - 1 >= 0 /\ P - S - 1 >= 0 /\ -P - S - 1 >= 0 /\ O - S - 1 >= 0 /\ -O - S - 1 >= 0 /\ S + 1 >= 0 /\ P + S + 1 >= 0 /\ -P + S + 1 >= 0 /\ O + S + 1 >= 0 /\ -O + S + 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ -O >= 0 /\ O >= 0 /\ J - N >= 0 /\ -J + N >= 0 /\ A = 0 ]
)