(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)
(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) -> Com_1(f34(A, K1, H1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, I1, W, X, F1, 20, G1, G1, H1, I1, J1)) [ G1 >= 1 /\ J1 >= 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) -> Com_1(f34(A, K1, I1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, J1, W, X, F1, G1, H1, H1, I1, J1, G1)) [ H1 >= 1 /\ 20 >= G1 /\ G1 >= 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) -> Com_1(f34(A, K1, H1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, I1, W, X, F1, 5, G1, G1, H1, I1, J1)) [ G1 >= 1 /\ 4 >= J1 ]
  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) -> Com_1(f91(A, B, 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, I1, W, X, F1, F1, G1, G1, H1, I1, E1)) [ 0 >= G1 ]
  f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f91(A, 0, 1, 0, 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)) [ B1 - 1 >= 0 /\ B = 0 ]
  f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f39(A, B, 1, B, F1, 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)) [ B1 - 1 >= 0 /\ B >= 1 ]
  f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f39(A, B, 1, B, F1, 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)) [ B1 - 1 >= 0 /\ 0 >= B + 1 ]
  f91(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) -> Com_1(f91(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)) [ -C + 1 >= 0 /\ C - 1 >= 0 ]
  f39(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) -> Com_1(f91(A, B, 1, D, 0, 0, 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)) [ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ B1 - 1 >= 0 /\ E = 0 ]
  f39(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) -> Com_1(f44(A, B, C, D, E, E, 10, F1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ B1 - 1 >= 0 /\ E >= 1 ]
  f39(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) -> Com_1(f44(A, B, C, D, E, E, 10, F1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ B1 - 1 >= 0 /\ 0 >= E + 1 ]
  f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f91(A, B, 1, D, E, F, G, H, I, J, K, L, M, H, O, P, Q, R, S, T, U, V, F1, F1, Y, Z, A1, B1, C1, D1, E1)) [ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ B1 - 1 >= 0 /\ F1 >= 1 ]
  f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f91(A, B, 1, D, E, F, G, H, I, J, K, L, M, H, O, P, Q, R, S, T, U, V, F1, F1, Y, Z, A1, B1, C1, D1, E1)) [ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ B1 - 1 >= 0 /\ 0 >= F1 + 1 ]
  f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f44(A, B, C, D, E, F, G, F1, I, J, K, L, M, H, O, P, Q, R, S, T, U, 0, 0, 0, Y, Z, A1, B1, C1, D1, E1)) [ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ B1 - 1 >= 0 /\ V = 0 ]
  f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f51(A, B, C, D, E, F, G, H, I, J, K, L, M, H, O, P, Q, R, S, T, U, V, 0, 0, Y, Z, A1, B1, C1, D1, E1)) [ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ B1 - 1 >= 0 /\ V >= 1 ]
  f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f51(A, B, C, D, E, F, G, H, I, J, K, L, M, H, O, P, Q, R, S, T, U, V, 0, 0, Y, Z, A1, B1, C1, D1, E1)) [ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ B1 - 1 >= 0 /\ 0 >= V + 1 ]
  f51(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) -> Com_1(f44(A, B, C, D, E, F, G, F1, I, J, K, L, M, -1, O, P, Q, R, S, 0, 0, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ N + 1 = 0 ]
  f51(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) -> Com_1(f59(A, B, C, D, E, F, G, H, G1, J, K, L, M, -1, O, P, Q, R, S, F1, F1, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ F1 >= 1 /\ N + 1 = 0 ]
  f51(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) -> Com_1(f59(A, B, C, D, E, F, G, H, G1, J, K, L, M, -1, O, P, Q, R, S, F1, F1, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ 0 >= F1 + 1 /\ N + 1 = 0 ]
  f51(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) -> Com_1(f44(A, B, C, D, E, F, G, F1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ 0 >= N + 2 ]
  f51(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) -> Com_1(f44(A, B, C, D, E, F, G, F1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ N >= 0 ]
  f59(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) -> Com_1(f44(A, B, C, D, E, F, G, F1, 0, 0, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ -N - 1 >= 0 /\ N + 1 >= 0 /\ I = 0 ]
  f59(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) -> Com_1(f64(A, B, C, D, E, F, G, H, I, I, 0, F1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ -N - 1 >= 0 /\ N + 1 >= 0 /\ I >= 1 ]
  f59(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) -> Com_1(f64(A, B, C, D, E, F, G, H, I, I, 0, F1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ -N - 1 >= 0 /\ N + 1 >= 0 /\ 0 >= I + 1 ]
  f64(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) -> Com_1(f75(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, 0, 0, F1, F1, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ F1 >= 1 ]
  f64(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) -> Com_1(f75(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, 0, 0, F1, F1, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= F1 + 1 ]
  f64(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) -> Com_1(f78(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, 0, 0, 0, 0, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 ]
  f64(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) -> Com_1(f82(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, F1, F1, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ F1 >= 1 ]
  f64(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) -> Com_1(f82(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, F1, F1, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= F1 + 1 ]
  f75(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f78(A, B, C, D, E, F, G, H, I, J, K, L, 0, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ Q + B1 - 1 >= 0 /\ -Q + B1 - 1 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ M = 0 ]
  f75(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f76(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)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ Q + B1 - 1 >= 0 /\ -Q + B1 - 1 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ M >= 1 ]
  f75(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1) -> Com_1(f76(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)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ Q + B1 - 1 >= 0 /\ -Q + B1 - 1 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= M + 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) -> Com_1(f82(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)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 2 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 11 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 2 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ Q + B1 - 1 >= 0 /\ -Q + B1 - 1 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X + 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X + 1 >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W + 1 >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W + 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q + 1 >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q + 1 >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P + 1 >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P + 1 >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 2 >= 0 /\ -K + 1 >= 0 /\ K >= 0 /\ K = 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) -> Com_1(f82(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)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 2 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 11 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 2 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ Q + B1 - 1 >= 0 /\ -Q + B1 - 1 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X + 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X + 1 >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W + 1 >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W + 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q + 1 >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q + 1 >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P + 1 >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P + 1 >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 2 >= 0 /\ -K + 1 >= 0 /\ K >= 0 /\ K >= 1 ]
  f82(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) -> Com_1(f44(A, B, C, D, E, F, G, F1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 2 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 11 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 2 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X + 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X + 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W + 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W + 1 >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 2 >= 0 /\ -K + 1 >= 0 /\ K >= 0 /\ K >= 1 ]
  f82(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) -> Com_1(f44(A, B, C, D, E, F, G, F1, I, J, 0, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 2 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 11 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 2 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X + 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X + 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W + 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W + 1 >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 2 >= 0 /\ -K + 1 >= 0 /\ K >= 0 /\ K = 0 ]
  f76(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) -> Com_1(f78(A, B, C, D, E, F, G, H, I, J, 1, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ Q + B1 - 1 >= 0 /\ -Q + B1 - 1 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ A >= 1 ]
  f76(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) -> Com_1(f78(A, B, C, D, E, F, G, H, I, J, 1, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ Q + B1 - 1 >= 0 /\ -Q + B1 - 1 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= A + 1 ]
  f76(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) -> Com_1(f78(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)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ C - H - 2 >= 0 /\ -C - H >= 0 /\ B1 - H - 2 >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ C + H >= 0 /\ -C + H + 2 >= 0 /\ B1 + H >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ C - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ B1 - G + 9 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ C + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ B1 + G - 11 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ -C + 1 >= 0 /\ B1 - C >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ C - 1 >= 0 /\ B1 + C - 2 >= 0 /\ X + C - 1 >= 0 /\ -X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ P + C - 1 >= 0 /\ -P + C - 1 >= 0 /\ N + C >= 0 /\ -N + C - 2 >= 0 /\ K + C - 1 >= 0 /\ -K + C - 1 >= 0 /\ B1 - 1 >= 0 /\ X + B1 - 1 >= 0 /\ -X + B1 - 1 >= 0 /\ W + B1 - 1 >= 0 /\ -W + B1 - 1 >= 0 /\ Q + B1 - 1 >= 0 /\ -Q + B1 - 1 >= 0 /\ P + B1 - 1 >= 0 /\ -P + B1 - 1 >= 0 /\ N + B1 >= 0 /\ -N + B1 - 2 >= 0 /\ K + B1 - 1 >= 0 /\ -K + B1 - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ A = 0 ]
)