(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)
(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) -> Com_1(f36(A, 40, 0, 40, 0, 1, 0, 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)) [ 0 >= A + 1 ]
  f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1) -> Com_1(f36(A, 40, 0, 40, 0, 1, 0, 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)) [ A >= 1 ]
  f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1) -> Com_1(f17(1, 40, 0, 40, 0, 1, 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)) [ A = 0 ]
  f17(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) -> Com_1(f23(A, B, C, D, E, F, G, H, G1, 0, H1, 0, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1)) [ H >= 0 /\ G + H >= 0 /\ -G + H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ E + H >= 0 /\ -E + H >= 0 /\ D + H - 40 >= 0 /\ -D + H + 40 >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B + H - 40 >= 0 /\ -B + H + 40 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ E - G >= 0 /\ -E - G >= 0 /\ D - G - 40 >= 0 /\ -D - G + 40 >= 0 /\ C - G >= 0 /\ -C - G >= 0 /\ B - G - 40 >= 0 /\ -B - G + 40 >= 0 /\ A - G - 1 >= 0 /\ -A - G + 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ E + G >= 0 /\ -E + G >= 0 /\ D + G - 40 >= 0 /\ -D + G + 40 >= 0 /\ C + G >= 0 /\ -C + G >= 0 /\ B + G - 40 >= 0 /\ -B + G + 40 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ A - E - 1 >= 0 /\ -A - E + 1 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ A + E - 1 >= 0 /\ -A + E + 1 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ A - D + 39 >= 0 /\ -A - D + 41 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ A + D - 41 >= 0 /\ -A + D - 39 >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ A - C - 1 >= 0 /\ -A - C + 1 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 40 >= 0 /\ A - B + 39 >= 0 /\ -A - B + 41 >= 0 /\ B - 40 >= 0 /\ A + B - 41 >= 0 /\ -A + B - 39 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 255 >= H ]
  f23(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) -> Com_1(f23(A, B, C, D, E, F, G, H, I, J, G1, L + 1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1)) [ H >= 0 /\ G + H >= 0 /\ -G + H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ E + H >= 0 /\ -E + H >= 0 /\ D + H - 40 >= 0 /\ -D + H + 40 >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B + H - 40 >= 0 /\ -B + H + 40 >= 0 /\ L + H >= 0 /\ J + H >= 0 /\ -J + H >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ E - G >= 0 /\ -E - G >= 0 /\ D - G - 40 >= 0 /\ -D - G + 40 >= 0 /\ C - G >= 0 /\ -C - G >= 0 /\ B - G - 40 >= 0 /\ -B - G + 40 >= 0 /\ L - G >= 0 /\ J - G >= 0 /\ -J - G >= 0 /\ A - G - 1 >= 0 /\ -A - G + 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ E + G >= 0 /\ -E + G >= 0 /\ D + G - 40 >= 0 /\ -D + G + 40 >= 0 /\ C + G >= 0 /\ -C + G >= 0 /\ B + G - 40 >= 0 /\ -B + G + 40 >= 0 /\ L + G >= 0 /\ J + G >= 0 /\ -J + G >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ L - F + 1 >= 0 /\ J - F + 1 >= 0 /\ -J - F + 1 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ L + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F - 1 >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ L - E >= 0 /\ J - E >= 0 /\ -J - E >= 0 /\ A - E - 1 >= 0 /\ -A - E + 1 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ L + E >= 0 /\ J + E >= 0 /\ -J + E >= 0 /\ A + E - 1 >= 0 /\ -A + E + 1 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ L - D + 40 >= 0 /\ J - D + 40 >= 0 /\ -J - D + 40 >= 0 /\ A - D + 39 >= 0 /\ -A - D + 41 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ L + D - 40 >= 0 /\ J + D - 40 >= 0 /\ -J + D - 40 >= 0 /\ A + D - 41 >= 0 /\ -A + D - 39 >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ L - C >= 0 /\ J - C >= 0 /\ -J - C >= 0 /\ A - C - 1 >= 0 /\ -A - C + 1 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ L + C >= 0 /\ J + C >= 0 /\ -J + C >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 40 >= 0 /\ L - B + 40 >= 0 /\ J - B + 40 >= 0 /\ -J - B + 40 >= 0 /\ A - B + 39 >= 0 /\ -A - B + 41 >= 0 /\ B - 40 >= 0 /\ L + B - 40 >= 0 /\ J + B - 40 >= 0 /\ -J + B - 40 >= 0 /\ A + B - 41 >= 0 /\ -A + B - 39 >= 0 /\ L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L - 1 >= 0 /\ -A + L + 1 >= 0 /\ -J >= 0 /\ A - J - 1 >= 0 /\ -A - J + 1 >= 0 /\ J >= 0 /\ A + J - 1 >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 7 >= L ]
  f36(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) -> Com_1(f42(A, B, C, D, E, F, G1, 1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1)) [ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ E - G >= 0 /\ -E - G >= 0 /\ D - G - 40 >= 0 /\ -D - G + 40 >= 0 /\ C - G >= 0 /\ -C - G >= 0 /\ B - G - 40 >= 0 /\ -B - G + 40 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ E + G >= 0 /\ -E + G >= 0 /\ D + G - 40 >= 0 /\ -D + G + 40 >= 0 /\ C + G >= 0 /\ -C + G >= 0 /\ B + G - 40 >= 0 /\ -B + G + 40 >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ -B + 40 >= 0 /\ B - 40 >= 0 ]
  f42(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1) -> Com_1(f42(A, B, C, D, E, F, G1, H + 1, I, J, K, L, H1, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1)) [ H - 1 >= 0 /\ F + H - 2 >= 0 /\ -F + H >= 0 /\ E + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 41 >= 0 /\ -D + H + 39 >= 0 /\ C + H - 1 >= 0 /\ -C + H - 1 >= 0 /\ B + H - 41 >= 0 /\ -B + H + 39 >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ -B + 40 >= 0 /\ B - 40 >= 0 /\ F >= 0 /\ D >= H ]
  f56(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) -> Com_1(f85(A, B, C, D, E, F, G, H, I, J, K, L, M, O, O, O, B + 2, 0, 1, O, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ E1 - G >= 0 /\ O - G >= 0 /\ -E1 + G >= 0 /\ -O + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ O - E1 >= 0 /\ -O + E1 >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ -B + 40 >= 0 /\ B - 40 >= 0 /\ 0 >= A + 1 ]
  f56(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) -> Com_1(f85(A, B, C, D, E, F, G, H, I, J, K, L, M, O, O, O, B + 2, 0, 1, O, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ E1 - G >= 0 /\ O - G >= 0 /\ -E1 + G >= 0 /\ -O + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ O - E1 >= 0 /\ -O + E1 >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ -B + 40 >= 0 /\ B - 40 >= 0 /\ A >= 1 ]
  f56(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) -> Com_1(f66(1, B, C, D, E, F, G, H, I, J, K, L, M, O, O, O, B + 2, 0, 1, O, 0, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ E1 - G >= 0 /\ O - G >= 0 /\ -E1 + G >= 0 /\ -O + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ O - E1 >= 0 /\ -O + E1 >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ -B + 40 >= 0 /\ B - 40 >= 0 /\ A = 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) -> Com_1(f72(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, G1, 0, H1, 0, Z, A1, B1, C1, D1, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ U + H - 41 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ S + H - 42 >= 0 /\ -S + H - 40 >= 0 /\ R + H - 41 >= 0 /\ -R + H - 41 >= 0 /\ Q + H - 83 >= 0 /\ -Q + H + 1 >= 0 /\ A + H - 42 >= 0 /\ -A + H - 40 >= 0 /\ E1 - G >= 0 /\ T - G >= 0 /\ P - G >= 0 /\ O - G >= 0 /\ N - G >= 0 /\ -E1 + G >= 0 /\ -T + G >= 0 /\ -P + G >= 0 /\ -O + G >= 0 /\ -N + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ U - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ S - F >= 0 /\ -S - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -R - F + 1 >= 0 /\ Q - F - 41 >= 0 /\ -Q - F + 43 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ U + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ S + F - 2 >= 0 /\ -S + F >= 0 /\ R + F - 1 >= 0 /\ -R + F - 1 >= 0 /\ Q + F - 43 >= 0 /\ -Q + F + 41 >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ U - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ S - E - 1 >= 0 /\ -S - E + 1 >= 0 /\ R - E >= 0 /\ -R - E >= 0 /\ Q - E - 42 >= 0 /\ -Q - E + 42 >= 0 /\ A - E - 1 >= 0 /\ -A - E + 1 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ U + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ S + E - 1 >= 0 /\ -S + E + 1 >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E - 42 >= 0 /\ -Q + E + 42 >= 0 /\ A + E - 1 >= 0 /\ -A + E + 1 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ U - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ S - D + 39 >= 0 /\ -S - D + 41 >= 0 /\ R - D + 40 >= 0 /\ -R - D + 40 >= 0 /\ Q - D - 2 >= 0 /\ -Q - D + 82 >= 0 /\ A - D + 39 >= 0 /\ -A - D + 41 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ U + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ S + D - 41 >= 0 /\ -S + D - 39 >= 0 /\ R + D - 40 >= 0 /\ -R + D - 40 >= 0 /\ Q + D - 82 >= 0 /\ -Q + D + 2 >= 0 /\ A + D - 41 >= 0 /\ -A + D - 39 >= 0 /\ T - E1 >= 0 /\ P - E1 >= 0 /\ O - E1 >= 0 /\ N - E1 >= 0 /\ -T + E1 >= 0 /\ -P + E1 >= 0 /\ -O + E1 >= 0 /\ -N + E1 >= 0 /\ -C >= 0 /\ U - C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ S - C - 1 >= 0 /\ -S - C + 1 >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C - 42 >= 0 /\ -Q - C + 42 >= 0 /\ A - C - 1 >= 0 /\ -A - C + 1 >= 0 /\ C >= 0 /\ U + C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ S + C - 1 >= 0 /\ -S + C + 1 >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C - 42 >= 0 /\ -Q + C + 42 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ U >= 0 /\ B + U - 40 >= 0 /\ -B + U + 40 >= 0 /\ S + U - 1 >= 0 /\ -S + U + 1 >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U - 42 >= 0 /\ -Q + U + 42 >= 0 /\ A + U - 1 >= 0 /\ -A + U + 1 >= 0 /\ P - T >= 0 /\ O - T >= 0 /\ N - T >= 0 /\ -P + T >= 0 /\ -O + T >= 0 /\ -N + T >= 0 /\ -B + 40 >= 0 /\ S - B + 39 >= 0 /\ -S - B + 41 >= 0 /\ R - B + 40 >= 0 /\ -R - B + 40 >= 0 /\ Q - B - 2 >= 0 /\ -Q - B + 82 >= 0 /\ A - B + 39 >= 0 /\ -A - B + 41 >= 0 /\ B - 40 >= 0 /\ S + B - 41 >= 0 /\ -S + B - 39 >= 0 /\ R + B - 40 >= 0 /\ -R + B - 40 >= 0 /\ Q + B - 82 >= 0 /\ -Q + B + 2 >= 0 /\ A + B - 41 >= 0 /\ -A + B - 39 >= 0 /\ -S + 1 >= 0 /\ R - S + 1 >= 0 /\ -R - S + 1 >= 0 /\ Q - S - 41 >= 0 /\ -Q - S + 43 >= 0 /\ A - S >= 0 /\ -A - S + 2 >= 0 /\ S - 1 >= 0 /\ R + S - 1 >= 0 /\ -R + S - 1 >= 0 /\ Q + S - 43 >= 0 /\ -Q + S + 41 >= 0 /\ A + S - 2 >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R - 42 >= 0 /\ -Q - R + 42 >= 0 /\ A - R - 1 >= 0 /\ -A - R + 1 >= 0 /\ R >= 0 /\ Q + R - 42 >= 0 /\ -Q + R + 42 >= 0 /\ A + R - 1 >= 0 /\ -A + R + 1 >= 0 /\ -Q + 42 >= 0 /\ A - Q + 41 >= 0 /\ -A - Q + 43 >= 0 /\ Q - 42 >= 0 /\ A + Q - 43 >= 0 /\ -A + Q - 41 >= 0 /\ O - P >= 0 /\ N - P >= 0 /\ -O + P >= 0 /\ -N + P >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 255 >= U ]
  f72(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) -> Com_1(f72(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, G1, Y + 1, Z, A1, B1, C1, D1, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ Y + H - 41 >= 0 /\ W + H - 41 >= 0 /\ -W + H - 41 >= 0 /\ U + H - 41 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ S + H - 42 >= 0 /\ -S + H - 40 >= 0 /\ R + H - 41 >= 0 /\ -R + H - 41 >= 0 /\ Q + H - 83 >= 0 /\ -Q + H + 1 >= 0 /\ A + H - 42 >= 0 /\ -A + H - 40 >= 0 /\ E1 - G >= 0 /\ T - G >= 0 /\ P - G >= 0 /\ O - G >= 0 /\ N - G >= 0 /\ -E1 + G >= 0 /\ -T + G >= 0 /\ -P + G >= 0 /\ -O + G >= 0 /\ -N + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ Y - F + 1 >= 0 /\ W - F + 1 >= 0 /\ -W - F + 1 >= 0 /\ U - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ S - F >= 0 /\ -S - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -R - F + 1 >= 0 /\ Q - F - 41 >= 0 /\ -Q - F + 43 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ Y + F - 1 >= 0 /\ W + F - 1 >= 0 /\ -W + F - 1 >= 0 /\ U + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ S + F - 2 >= 0 /\ -S + F >= 0 /\ R + F - 1 >= 0 /\ -R + F - 1 >= 0 /\ Q + F - 43 >= 0 /\ -Q + F + 41 >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ Y - E >= 0 /\ W - E >= 0 /\ -W - E >= 0 /\ U - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ S - E - 1 >= 0 /\ -S - E + 1 >= 0 /\ R - E >= 0 /\ -R - E >= 0 /\ Q - E - 42 >= 0 /\ -Q - E + 42 >= 0 /\ A - E - 1 >= 0 /\ -A - E + 1 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ Y + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ U + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ S + E - 1 >= 0 /\ -S + E + 1 >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E - 42 >= 0 /\ -Q + E + 42 >= 0 /\ A + E - 1 >= 0 /\ -A + E + 1 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ Y - D + 40 >= 0 /\ W - D + 40 >= 0 /\ -W - D + 40 >= 0 /\ U - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ S - D + 39 >= 0 /\ -S - D + 41 >= 0 /\ R - D + 40 >= 0 /\ -R - D + 40 >= 0 /\ Q - D - 2 >= 0 /\ -Q - D + 82 >= 0 /\ A - D + 39 >= 0 /\ -A - D + 41 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ Y + D - 40 >= 0 /\ W + D - 40 >= 0 /\ -W + D - 40 >= 0 /\ U + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ S + D - 41 >= 0 /\ -S + D - 39 >= 0 /\ R + D - 40 >= 0 /\ -R + D - 40 >= 0 /\ Q + D - 82 >= 0 /\ -Q + D + 2 >= 0 /\ A + D - 41 >= 0 /\ -A + D - 39 >= 0 /\ T - E1 >= 0 /\ P - E1 >= 0 /\ O - E1 >= 0 /\ N - E1 >= 0 /\ -T + E1 >= 0 /\ -P + E1 >= 0 /\ -O + E1 >= 0 /\ -N + E1 >= 0 /\ -C >= 0 /\ Y - C >= 0 /\ W - C >= 0 /\ -W - C >= 0 /\ U - C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ S - C - 1 >= 0 /\ -S - C + 1 >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C - 42 >= 0 /\ -Q - C + 42 >= 0 /\ A - C - 1 >= 0 /\ -A - C + 1 >= 0 /\ C >= 0 /\ Y + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ U + C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ S + C - 1 >= 0 /\ -S + C + 1 >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C - 42 >= 0 /\ -Q + C + 42 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ U + Y >= 0 /\ B + Y - 40 >= 0 /\ -B + Y + 40 >= 0 /\ S + Y - 1 >= 0 /\ -S + Y + 1 >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y - 42 >= 0 /\ -Q + Y + 42 >= 0 /\ A + Y - 1 >= 0 /\ -A + Y + 1 >= 0 /\ -W >= 0 /\ U - W >= 0 /\ B - W - 40 >= 0 /\ -B - W + 40 >= 0 /\ S - W - 1 >= 0 /\ -S - W + 1 >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W - 42 >= 0 /\ -Q - W + 42 >= 0 /\ A - W - 1 >= 0 /\ -A - W + 1 >= 0 /\ W >= 0 /\ U + W >= 0 /\ B + W - 40 >= 0 /\ -B + W + 40 >= 0 /\ S + W - 1 >= 0 /\ -S + W + 1 >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W - 42 >= 0 /\ -Q + W + 42 >= 0 /\ A + W - 1 >= 0 /\ -A + W + 1 >= 0 /\ U >= 0 /\ B + U - 40 >= 0 /\ -B + U + 40 >= 0 /\ S + U - 1 >= 0 /\ -S + U + 1 >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U - 42 >= 0 /\ -Q + U + 42 >= 0 /\ A + U - 1 >= 0 /\ -A + U + 1 >= 0 /\ P - T >= 0 /\ O - T >= 0 /\ N - T >= 0 /\ -P + T >= 0 /\ -O + T >= 0 /\ -N + T >= 0 /\ -B + 40 >= 0 /\ S - B + 39 >= 0 /\ -S - B + 41 >= 0 /\ R - B + 40 >= 0 /\ -R - B + 40 >= 0 /\ Q - B - 2 >= 0 /\ -Q - B + 82 >= 0 /\ A - B + 39 >= 0 /\ -A - B + 41 >= 0 /\ B - 40 >= 0 /\ S + B - 41 >= 0 /\ -S + B - 39 >= 0 /\ R + B - 40 >= 0 /\ -R + B - 40 >= 0 /\ Q + B - 82 >= 0 /\ -Q + B + 2 >= 0 /\ A + B - 41 >= 0 /\ -A + B - 39 >= 0 /\ -S + 1 >= 0 /\ R - S + 1 >= 0 /\ -R - S + 1 >= 0 /\ Q - S - 41 >= 0 /\ -Q - S + 43 >= 0 /\ A - S >= 0 /\ -A - S + 2 >= 0 /\ S - 1 >= 0 /\ R + S - 1 >= 0 /\ -R + S - 1 >= 0 /\ Q + S - 43 >= 0 /\ -Q + S + 41 >= 0 /\ A + S - 2 >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R - 42 >= 0 /\ -Q - R + 42 >= 0 /\ A - R - 1 >= 0 /\ -A - R + 1 >= 0 /\ R >= 0 /\ Q + R - 42 >= 0 /\ -Q + R + 42 >= 0 /\ A + R - 1 >= 0 /\ -A + R + 1 >= 0 /\ -Q + 42 >= 0 /\ A - Q + 41 >= 0 /\ -A - Q + 43 >= 0 /\ Q - 42 >= 0 /\ A + Q - 43 >= 0 /\ -A + Q - 41 >= 0 /\ O - P >= 0 /\ N - P >= 0 /\ -O + P >= 0 /\ -N + P >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 7 >= Y ]
  f85(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) -> Com_1(f91(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, G1, 1, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ S + H - 42 >= 0 /\ -S + H - 40 >= 0 /\ R + H - 41 >= 0 /\ -R + H - 41 >= 0 /\ Q + H - 83 >= 0 /\ -Q + H + 1 >= 0 /\ E1 - G >= 0 /\ T - G >= 0 /\ P - G >= 0 /\ O - G >= 0 /\ N - G >= 0 /\ -E1 + G >= 0 /\ -T + G >= 0 /\ -P + G >= 0 /\ -O + G >= 0 /\ -N + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ S - F >= 0 /\ -S - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -R - F + 1 >= 0 /\ Q - F - 41 >= 0 /\ -Q - F + 43 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ S + F - 2 >= 0 /\ -S + F >= 0 /\ R + F - 1 >= 0 /\ -R + F - 1 >= 0 /\ Q + F - 43 >= 0 /\ -Q + F + 41 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ S - E - 1 >= 0 /\ -S - E + 1 >= 0 /\ R - E >= 0 /\ -R - E >= 0 /\ Q - E - 42 >= 0 /\ -Q - E + 42 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ S + E - 1 >= 0 /\ -S + E + 1 >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E - 42 >= 0 /\ -Q + E + 42 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ S - D + 39 >= 0 /\ -S - D + 41 >= 0 /\ R - D + 40 >= 0 /\ -R - D + 40 >= 0 /\ Q - D - 2 >= 0 /\ -Q - D + 82 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ S + D - 41 >= 0 /\ -S + D - 39 >= 0 /\ R + D - 40 >= 0 /\ -R + D - 40 >= 0 /\ Q + D - 82 >= 0 /\ -Q + D + 2 >= 0 /\ T - E1 >= 0 /\ P - E1 >= 0 /\ O - E1 >= 0 /\ N - E1 >= 0 /\ -T + E1 >= 0 /\ -P + E1 >= 0 /\ -O + E1 >= 0 /\ -N + E1 >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ S - C - 1 >= 0 /\ -S - C + 1 >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C - 42 >= 0 /\ -Q - C + 42 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ S + C - 1 >= 0 /\ -S + C + 1 >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C - 42 >= 0 /\ -Q + C + 42 >= 0 /\ P - T >= 0 /\ O - T >= 0 /\ N - T >= 0 /\ -P + T >= 0 /\ -O + T >= 0 /\ -N + T >= 0 /\ -B + 40 >= 0 /\ S - B + 39 >= 0 /\ -S - B + 41 >= 0 /\ R - B + 40 >= 0 /\ -R - B + 40 >= 0 /\ Q - B - 2 >= 0 /\ -Q - B + 82 >= 0 /\ B - 40 >= 0 /\ S + B - 41 >= 0 /\ -S + B - 39 >= 0 /\ R + B - 40 >= 0 /\ -R + B - 40 >= 0 /\ Q + B - 82 >= 0 /\ -Q + B + 2 >= 0 /\ -S + 1 >= 0 /\ R - S + 1 >= 0 /\ -R - S + 1 >= 0 /\ Q - S - 41 >= 0 /\ -Q - S + 43 >= 0 /\ S - 1 >= 0 /\ R + S - 1 >= 0 /\ -R + S - 1 >= 0 /\ Q + S - 43 >= 0 /\ -Q + S + 41 >= 0 /\ -R >= 0 /\ Q - R - 42 >= 0 /\ -Q - R + 42 >= 0 /\ R >= 0 /\ Q + R - 42 >= 0 /\ -Q + R + 42 >= 0 /\ -Q + 42 >= 0 /\ Q - 42 >= 0 /\ O - P >= 0 /\ N - P >= 0 /\ -O + P >= 0 /\ -N + P >= 0 /\ N - O >= 0 /\ -N + O >= 0 ]
  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, F1) -> Com_1(f91(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, G1, U + 1, V, W, X, Y, H1, A1, B1, C1, D1, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ U + H - 42 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ S + H - 42 >= 0 /\ -S + H - 40 >= 0 /\ R + H - 41 >= 0 /\ -R + H - 41 >= 0 /\ Q + H - 83 >= 0 /\ -Q + H + 1 >= 0 /\ E1 - G >= 0 /\ P - G >= 0 /\ O - G >= 0 /\ N - G >= 0 /\ -E1 + G >= 0 /\ -P + G >= 0 /\ -O + G >= 0 /\ -N + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ U - F >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ S - F >= 0 /\ -S - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -R - F + 1 >= 0 /\ Q - F - 41 >= 0 /\ -Q - F + 43 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ U + F - 2 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ S + F - 2 >= 0 /\ -S + F >= 0 /\ R + F - 1 >= 0 /\ -R + F - 1 >= 0 /\ Q + F - 43 >= 0 /\ -Q + F + 41 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ U - E - 1 >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ S - E - 1 >= 0 /\ -S - E + 1 >= 0 /\ R - E >= 0 /\ -R - E >= 0 /\ Q - E - 42 >= 0 /\ -Q - E + 42 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ U + E - 1 >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ S + E - 1 >= 0 /\ -S + E + 1 >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E - 42 >= 0 /\ -Q + E + 42 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ U - D + 39 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ S - D + 39 >= 0 /\ -S - D + 41 >= 0 /\ R - D + 40 >= 0 /\ -R - D + 40 >= 0 /\ Q - D - 2 >= 0 /\ -Q - D + 82 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ U + D - 41 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ S + D - 41 >= 0 /\ -S + D - 39 >= 0 /\ R + D - 40 >= 0 /\ -R + D - 40 >= 0 /\ Q + D - 82 >= 0 /\ -Q + D + 2 >= 0 /\ P - E1 >= 0 /\ O - E1 >= 0 /\ N - E1 >= 0 /\ -P + E1 >= 0 /\ -O + E1 >= 0 /\ -N + E1 >= 0 /\ -C >= 0 /\ U - C - 1 >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ S - C - 1 >= 0 /\ -S - C + 1 >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C - 42 >= 0 /\ -Q - C + 42 >= 0 /\ C >= 0 /\ U + C - 1 >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ S + C - 1 >= 0 /\ -S + C + 1 >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C - 42 >= 0 /\ -Q + C + 42 >= 0 /\ U - 1 >= 0 /\ B + U - 41 >= 0 /\ -B + U + 39 >= 0 /\ S + U - 2 >= 0 /\ -S + U >= 0 /\ R + U - 1 >= 0 /\ -R + U - 1 >= 0 /\ Q + U - 43 >= 0 /\ -Q + U + 41 >= 0 /\ -B + 40 >= 0 /\ S - B + 39 >= 0 /\ -S - B + 41 >= 0 /\ R - B + 40 >= 0 /\ -R - B + 40 >= 0 /\ Q - B - 2 >= 0 /\ -Q - B + 82 >= 0 /\ B - 40 >= 0 /\ S + B - 41 >= 0 /\ -S + B - 39 >= 0 /\ R + B - 40 >= 0 /\ -R + B - 40 >= 0 /\ Q + B - 82 >= 0 /\ -Q + B + 2 >= 0 /\ -S + 1 >= 0 /\ R - S + 1 >= 0 /\ -R - S + 1 >= 0 /\ Q - S - 41 >= 0 /\ -Q - S + 43 >= 0 /\ S - 1 >= 0 /\ R + S - 1 >= 0 /\ -R + S - 1 >= 0 /\ Q + S - 43 >= 0 /\ -Q + S + 41 >= 0 /\ -R >= 0 /\ Q - R - 42 >= 0 /\ -Q - R + 42 >= 0 /\ R >= 0 /\ Q + R - 42 >= 0 /\ -Q + R + 42 >= 0 /\ -Q + 42 >= 0 /\ Q - 42 >= 0 /\ O - P >= 0 /\ N - P >= 0 /\ -O + P >= 0 /\ -N + P >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ S >= 0 /\ Q >= U ]
  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, F1) -> Com_1(f106(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, T, T, T, D1, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ U + H - 42 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ S + H - 42 >= 0 /\ -S + H - 40 >= 0 /\ R + H - 41 >= 0 /\ -R + H - 41 >= 0 /\ Q + H - 83 >= 0 /\ -Q + H + 1 >= 0 /\ E1 - G >= 0 /\ P - G >= 0 /\ O - G >= 0 /\ N - G >= 0 /\ -E1 + G >= 0 /\ -P + G >= 0 /\ -O + G >= 0 /\ -N + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ U - F >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ S - F >= 0 /\ -S - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -R - F + 1 >= 0 /\ Q - F - 41 >= 0 /\ -Q - F + 43 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ U + F - 2 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ S + F - 2 >= 0 /\ -S + F >= 0 /\ R + F - 1 >= 0 /\ -R + F - 1 >= 0 /\ Q + F - 43 >= 0 /\ -Q + F + 41 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ U - E - 1 >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ S - E - 1 >= 0 /\ -S - E + 1 >= 0 /\ R - E >= 0 /\ -R - E >= 0 /\ Q - E - 42 >= 0 /\ -Q - E + 42 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ U + E - 1 >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ S + E - 1 >= 0 /\ -S + E + 1 >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E - 42 >= 0 /\ -Q + E + 42 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ U - D + 39 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ S - D + 39 >= 0 /\ -S - D + 41 >= 0 /\ R - D + 40 >= 0 /\ -R - D + 40 >= 0 /\ Q - D - 2 >= 0 /\ -Q - D + 82 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ U + D - 41 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ S + D - 41 >= 0 /\ -S + D - 39 >= 0 /\ R + D - 40 >= 0 /\ -R + D - 40 >= 0 /\ Q + D - 82 >= 0 /\ -Q + D + 2 >= 0 /\ P - E1 >= 0 /\ O - E1 >= 0 /\ N - E1 >= 0 /\ -P + E1 >= 0 /\ -O + E1 >= 0 /\ -N + E1 >= 0 /\ -C >= 0 /\ U - C - 1 >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ S - C - 1 >= 0 /\ -S - C + 1 >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C - 42 >= 0 /\ -Q - C + 42 >= 0 /\ C >= 0 /\ U + C - 1 >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ S + C - 1 >= 0 /\ -S + C + 1 >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C - 42 >= 0 /\ -Q + C + 42 >= 0 /\ U - 1 >= 0 /\ B + U - 41 >= 0 /\ -B + U + 39 >= 0 /\ S + U - 2 >= 0 /\ -S + U >= 0 /\ R + U - 1 >= 0 /\ -R + U - 1 >= 0 /\ Q + U - 43 >= 0 /\ -Q + U + 41 >= 0 /\ -B + 40 >= 0 /\ S - B + 39 >= 0 /\ -S - B + 41 >= 0 /\ R - B + 40 >= 0 /\ -R - B + 40 >= 0 /\ Q - B - 2 >= 0 /\ -Q - B + 82 >= 0 /\ B - 40 >= 0 /\ S + B - 41 >= 0 /\ -S + B - 39 >= 0 /\ R + B - 40 >= 0 /\ -R + B - 40 >= 0 /\ Q + B - 82 >= 0 /\ -Q + B + 2 >= 0 /\ -S + 1 >= 0 /\ R - S + 1 >= 0 /\ -R - S + 1 >= 0 /\ Q - S - 41 >= 0 /\ -Q - S + 43 >= 0 /\ S - 1 >= 0 /\ R + S - 1 >= 0 /\ -R + S - 1 >= 0 /\ Q + S - 43 >= 0 /\ -Q + S + 41 >= 0 /\ -R >= 0 /\ Q - R - 42 >= 0 /\ -Q - R + 42 >= 0 /\ R >= 0 /\ Q + R - 42 >= 0 /\ -Q + R + 42 >= 0 /\ -Q + 42 >= 0 /\ Q - 42 >= 0 /\ O - P >= 0 /\ N - P >= 0 /\ -O + P >= 0 /\ -N + P >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ S >= 0 /\ U >= Q + 1 ]
  f72(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) -> Com_1(f66(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U + 1, V, W, X, Y, Z, A1, B1, C1, X, E1, F1)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ Y + H - 41 >= 0 /\ W + H - 41 >= 0 /\ -W + H - 41 >= 0 /\ U + H - 41 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ S + H - 42 >= 0 /\ -S + H - 40 >= 0 /\ R + H - 41 >= 0 /\ -R + H - 41 >= 0 /\ Q + H - 83 >= 0 /\ -Q + H + 1 >= 0 /\ A + H - 42 >= 0 /\ -A + H - 40 >= 0 /\ E1 - G >= 0 /\ T - G >= 0 /\ P - G >= 0 /\ O - G >= 0 /\ N - G >= 0 /\ -E1 + G >= 0 /\ -T + G >= 0 /\ -P + G >= 0 /\ -O + G >= 0 /\ -N + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ Y - F + 1 >= 0 /\ W - F + 1 >= 0 /\ -W - F + 1 >= 0 /\ U - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ S - F >= 0 /\ -S - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -R - F + 1 >= 0 /\ Q - F - 41 >= 0 /\ -Q - F + 43 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ Y + F - 1 >= 0 /\ W + F - 1 >= 0 /\ -W + F - 1 >= 0 /\ U + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ S + F - 2 >= 0 /\ -S + F >= 0 /\ R + F - 1 >= 0 /\ -R + F - 1 >= 0 /\ Q + F - 43 >= 0 /\ -Q + F + 41 >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ Y - E >= 0 /\ W - E >= 0 /\ -W - E >= 0 /\ U - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ S - E - 1 >= 0 /\ -S - E + 1 >= 0 /\ R - E >= 0 /\ -R - E >= 0 /\ Q - E - 42 >= 0 /\ -Q - E + 42 >= 0 /\ A - E - 1 >= 0 /\ -A - E + 1 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ Y + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ U + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ S + E - 1 >= 0 /\ -S + E + 1 >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E - 42 >= 0 /\ -Q + E + 42 >= 0 /\ A + E - 1 >= 0 /\ -A + E + 1 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ Y - D + 40 >= 0 /\ W - D + 40 >= 0 /\ -W - D + 40 >= 0 /\ U - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ S - D + 39 >= 0 /\ -S - D + 41 >= 0 /\ R - D + 40 >= 0 /\ -R - D + 40 >= 0 /\ Q - D - 2 >= 0 /\ -Q - D + 82 >= 0 /\ A - D + 39 >= 0 /\ -A - D + 41 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ Y + D - 40 >= 0 /\ W + D - 40 >= 0 /\ -W + D - 40 >= 0 /\ U + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ S + D - 41 >= 0 /\ -S + D - 39 >= 0 /\ R + D - 40 >= 0 /\ -R + D - 40 >= 0 /\ Q + D - 82 >= 0 /\ -Q + D + 2 >= 0 /\ A + D - 41 >= 0 /\ -A + D - 39 >= 0 /\ T - E1 >= 0 /\ P - E1 >= 0 /\ O - E1 >= 0 /\ N - E1 >= 0 /\ -T + E1 >= 0 /\ -P + E1 >= 0 /\ -O + E1 >= 0 /\ -N + E1 >= 0 /\ -C >= 0 /\ Y - C >= 0 /\ W - C >= 0 /\ -W - C >= 0 /\ U - C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ S - C - 1 >= 0 /\ -S - C + 1 >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C - 42 >= 0 /\ -Q - C + 42 >= 0 /\ A - C - 1 >= 0 /\ -A - C + 1 >= 0 /\ C >= 0 /\ Y + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ U + C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ S + C - 1 >= 0 /\ -S + C + 1 >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C - 42 >= 0 /\ -Q + C + 42 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ U + Y >= 0 /\ B + Y - 40 >= 0 /\ -B + Y + 40 >= 0 /\ S + Y - 1 >= 0 /\ -S + Y + 1 >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y - 42 >= 0 /\ -Q + Y + 42 >= 0 /\ A + Y - 1 >= 0 /\ -A + Y + 1 >= 0 /\ -W >= 0 /\ U - W >= 0 /\ B - W - 40 >= 0 /\ -B - W + 40 >= 0 /\ S - W - 1 >= 0 /\ -S - W + 1 >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W - 42 >= 0 /\ -Q - W + 42 >= 0 /\ A - W - 1 >= 0 /\ -A - W + 1 >= 0 /\ W >= 0 /\ U + W >= 0 /\ B + W - 40 >= 0 /\ -B + W + 40 >= 0 /\ S + W - 1 >= 0 /\ -S + W + 1 >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W - 42 >= 0 /\ -Q + W + 42 >= 0 /\ A + W - 1 >= 0 /\ -A + W + 1 >= 0 /\ U >= 0 /\ B + U - 40 >= 0 /\ -B + U + 40 >= 0 /\ S + U - 1 >= 0 /\ -S + U + 1 >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U - 42 >= 0 /\ -Q + U + 42 >= 0 /\ A + U - 1 >= 0 /\ -A + U + 1 >= 0 /\ P - T >= 0 /\ O - T >= 0 /\ N - T >= 0 /\ -P + T >= 0 /\ -O + T >= 0 /\ -N + T >= 0 /\ -B + 40 >= 0 /\ S - B + 39 >= 0 /\ -S - B + 41 >= 0 /\ R - B + 40 >= 0 /\ -R - B + 40 >= 0 /\ Q - B - 2 >= 0 /\ -Q - B + 82 >= 0 /\ A - B + 39 >= 0 /\ -A - B + 41 >= 0 /\ B - 40 >= 0 /\ S + B - 41 >= 0 /\ -S + B - 39 >= 0 /\ R + B - 40 >= 0 /\ -R + B - 40 >= 0 /\ Q + B - 82 >= 0 /\ -Q + B + 2 >= 0 /\ A + B - 41 >= 0 /\ -A + B - 39 >= 0 /\ -S + 1 >= 0 /\ R - S + 1 >= 0 /\ -R - S + 1 >= 0 /\ Q - S - 41 >= 0 /\ -Q - S + 43 >= 0 /\ A - S >= 0 /\ -A - S + 2 >= 0 /\ S - 1 >= 0 /\ R + S - 1 >= 0 /\ -R + S - 1 >= 0 /\ Q + S - 43 >= 0 /\ -Q + S + 41 >= 0 /\ A + S - 2 >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R - 42 >= 0 /\ -Q - R + 42 >= 0 /\ A - R - 1 >= 0 /\ -A - R + 1 >= 0 /\ R >= 0 /\ Q + R - 42 >= 0 /\ -Q + R + 42 >= 0 /\ A + R - 1 >= 0 /\ -A + R + 1 >= 0 /\ -Q + 42 >= 0 /\ A - Q + 41 >= 0 /\ -A - Q + 43 >= 0 /\ Q - 42 >= 0 /\ A + Q - 43 >= 0 /\ -A + Q - 41 >= 0 /\ O - P >= 0 /\ N - P >= 0 /\ -O + P >= 0 /\ -N + P >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ Y >= 8 ]
  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) -> Com_1(f85(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)) [ H - 41 >= 0 /\ F + H - 42 >= 0 /\ -F + H - 40 >= 0 /\ E + H - 41 >= 0 /\ -E + H - 41 >= 0 /\ D + H - 81 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 41 >= 0 /\ -C + H - 41 >= 0 /\ U + H - 41 >= 0 /\ B + H - 81 >= 0 /\ -B + H - 1 >= 0 /\ S + H - 42 >= 0 /\ -S + H - 40 >= 0 /\ R + H - 41 >= 0 /\ -R + H - 41 >= 0 /\ Q + H - 83 >= 0 /\ -Q + H + 1 >= 0 /\ A + H - 42 >= 0 /\ -A + H - 40 >= 0 /\ E1 - G >= 0 /\ T - G >= 0 /\ P - G >= 0 /\ O - G >= 0 /\ N - G >= 0 /\ -E1 + G >= 0 /\ -T + G >= 0 /\ -P + G >= 0 /\ -O + G >= 0 /\ -N + G >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ U - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ S - F >= 0 /\ -S - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -R - F + 1 >= 0 /\ Q - F - 41 >= 0 /\ -Q - F + 43 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ U + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ S + F - 2 >= 0 /\ -S + F >= 0 /\ R + F - 1 >= 0 /\ -R + F - 1 >= 0 /\ Q + F - 43 >= 0 /\ -Q + F + 41 >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ U - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ S - E - 1 >= 0 /\ -S - E + 1 >= 0 /\ R - E >= 0 /\ -R - E >= 0 /\ Q - E - 42 >= 0 /\ -Q - E + 42 >= 0 /\ A - E - 1 >= 0 /\ -A - E + 1 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ U + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ S + E - 1 >= 0 /\ -S + E + 1 >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E - 42 >= 0 /\ -Q + E + 42 >= 0 /\ A + E - 1 >= 0 /\ -A + E + 1 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ U - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ S - D + 39 >= 0 /\ -S - D + 41 >= 0 /\ R - D + 40 >= 0 /\ -R - D + 40 >= 0 /\ Q - D - 2 >= 0 /\ -Q - D + 82 >= 0 /\ A - D + 39 >= 0 /\ -A - D + 41 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ U + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ S + D - 41 >= 0 /\ -S + D - 39 >= 0 /\ R + D - 40 >= 0 /\ -R + D - 40 >= 0 /\ Q + D - 82 >= 0 /\ -Q + D + 2 >= 0 /\ A + D - 41 >= 0 /\ -A + D - 39 >= 0 /\ T - E1 >= 0 /\ P - E1 >= 0 /\ O - E1 >= 0 /\ N - E1 >= 0 /\ -T + E1 >= 0 /\ -P + E1 >= 0 /\ -O + E1 >= 0 /\ -N + E1 >= 0 /\ -C >= 0 /\ U - C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ S - C - 1 >= 0 /\ -S - C + 1 >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C - 42 >= 0 /\ -Q - C + 42 >= 0 /\ A - C - 1 >= 0 /\ -A - C + 1 >= 0 /\ C >= 0 /\ U + C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ S + C - 1 >= 0 /\ -S + C + 1 >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C - 42 >= 0 /\ -Q + C + 42 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ U >= 0 /\ B + U - 40 >= 0 /\ -B + U + 40 >= 0 /\ S + U - 1 >= 0 /\ -S + U + 1 >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U - 42 >= 0 /\ -Q + U + 42 >= 0 /\ A + U - 1 >= 0 /\ -A + U + 1 >= 0 /\ P - T >= 0 /\ O - T >= 0 /\ N - T >= 0 /\ -P + T >= 0 /\ -O + T >= 0 /\ -N + T >= 0 /\ -B + 40 >= 0 /\ S - B + 39 >= 0 /\ -S - B + 41 >= 0 /\ R - B + 40 >= 0 /\ -R - B + 40 >= 0 /\ Q - B - 2 >= 0 /\ -Q - B + 82 >= 0 /\ A - B + 39 >= 0 /\ -A - B + 41 >= 0 /\ B - 40 >= 0 /\ S + B - 41 >= 0 /\ -S + B - 39 >= 0 /\ R + B - 40 >= 0 /\ -R + B - 40 >= 0 /\ Q + B - 82 >= 0 /\ -Q + B + 2 >= 0 /\ A + B - 41 >= 0 /\ -A + B - 39 >= 0 /\ -S + 1 >= 0 /\ R - S + 1 >= 0 /\ -R - S + 1 >= 0 /\ Q - S - 41 >= 0 /\ -Q - S + 43 >= 0 /\ A - S >= 0 /\ -A - S + 2 >= 0 /\ S - 1 >= 0 /\ R + S - 1 >= 0 /\ -R + S - 1 >= 0 /\ Q + S - 43 >= 0 /\ -Q + S + 41 >= 0 /\ A + S - 2 >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R - 42 >= 0 /\ -Q - R + 42 >= 0 /\ A - R - 1 >= 0 /\ -A - R + 1 >= 0 /\ R >= 0 /\ Q + R - 42 >= 0 /\ -Q + R + 42 >= 0 /\ A + R - 1 >= 0 /\ -A + R + 1 >= 0 /\ -Q + 42 >= 0 /\ A - Q + 41 >= 0 /\ -A - Q + 43 >= 0 /\ Q - 42 >= 0 /\ A + Q - 43 >= 0 /\ -A + Q - 41 >= 0 /\ O - P >= 0 /\ N - P >= 0 /\ -O + P >= 0 /\ -N + P >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ U >= 256 ]
  f42(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1) -> Com_1(f56(A, B, C, D, E, F, G, H, I, J, K, L, M, N, G, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, G, F1)) [ H - 1 >= 0 /\ F + H - 2 >= 0 /\ -F + H >= 0 /\ E + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 41 >= 0 /\ -D + H + 39 >= 0 /\ C + H - 1 >= 0 /\ -C + H - 1 >= 0 /\ B + H - 41 >= 0 /\ -B + H + 39 >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ -B + 40 >= 0 /\ B - 40 >= 0 /\ F >= 0 /\ H >= D + 1 ]
  f23(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) -> Com_1(f17(A, B, C, D, E, F, G, H + 1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, K)) [ H >= 0 /\ G + H >= 0 /\ -G + H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ E + H >= 0 /\ -E + H >= 0 /\ D + H - 40 >= 0 /\ -D + H + 40 >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B + H - 40 >= 0 /\ -B + H + 40 >= 0 /\ L + H >= 0 /\ J + H >= 0 /\ -J + H >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ E - G >= 0 /\ -E - G >= 0 /\ D - G - 40 >= 0 /\ -D - G + 40 >= 0 /\ C - G >= 0 /\ -C - G >= 0 /\ B - G - 40 >= 0 /\ -B - G + 40 >= 0 /\ L - G >= 0 /\ J - G >= 0 /\ -J - G >= 0 /\ A - G - 1 >= 0 /\ -A - G + 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ E + G >= 0 /\ -E + G >= 0 /\ D + G - 40 >= 0 /\ -D + G + 40 >= 0 /\ C + G >= 0 /\ -C + G >= 0 /\ B + G - 40 >= 0 /\ -B + G + 40 >= 0 /\ L + G >= 0 /\ J + G >= 0 /\ -J + G >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ L - F + 1 >= 0 /\ J - F + 1 >= 0 /\ -J - F + 1 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ L + F - 1 >= 0 /\ J + F - 1 >= 0 /\ -J + F - 1 >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ L - E >= 0 /\ J - E >= 0 /\ -J - E >= 0 /\ A - E - 1 >= 0 /\ -A - E + 1 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ L + E >= 0 /\ J + E >= 0 /\ -J + E >= 0 /\ A + E - 1 >= 0 /\ -A + E + 1 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ L - D + 40 >= 0 /\ J - D + 40 >= 0 /\ -J - D + 40 >= 0 /\ A - D + 39 >= 0 /\ -A - D + 41 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ L + D - 40 >= 0 /\ J + D - 40 >= 0 /\ -J + D - 40 >= 0 /\ A + D - 41 >= 0 /\ -A + D - 39 >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ L - C >= 0 /\ J - C >= 0 /\ -J - C >= 0 /\ A - C - 1 >= 0 /\ -A - C + 1 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ L + C >= 0 /\ J + C >= 0 /\ -J + C >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 40 >= 0 /\ L - B + 40 >= 0 /\ J - B + 40 >= 0 /\ -J - B + 40 >= 0 /\ A - B + 39 >= 0 /\ -A - B + 41 >= 0 /\ B - 40 >= 0 /\ L + B - 40 >= 0 /\ J + B - 40 >= 0 /\ -J + B - 40 >= 0 /\ A + B - 41 >= 0 /\ -A + B - 39 >= 0 /\ L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L - 1 >= 0 /\ -A + L + 1 >= 0 /\ -J >= 0 /\ A - J - 1 >= 0 /\ -A - J + 1 >= 0 /\ J >= 0 /\ A + J - 1 >= 0 /\ -A + J + 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ L >= 8 ]
  f17(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) -> Com_1(f36(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)) [ H >= 0 /\ G + H >= 0 /\ -G + H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ E + H >= 0 /\ -E + H >= 0 /\ D + H - 40 >= 0 /\ -D + H + 40 >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B + H - 40 >= 0 /\ -B + H + 40 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ E - G >= 0 /\ -E - G >= 0 /\ D - G - 40 >= 0 /\ -D - G + 40 >= 0 /\ C - G >= 0 /\ -C - G >= 0 /\ B - G - 40 >= 0 /\ -B - G + 40 >= 0 /\ A - G - 1 >= 0 /\ -A - G + 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ E + G >= 0 /\ -E + G >= 0 /\ D + G - 40 >= 0 /\ -D + G + 40 >= 0 /\ C + G >= 0 /\ -C + G >= 0 /\ B + G - 40 >= 0 /\ -B + G + 40 >= 0 /\ A + G - 1 >= 0 /\ -A + G + 1 >= 0 /\ -F + 1 >= 0 /\ E - F + 1 >= 0 /\ -E - F + 1 >= 0 /\ D - F - 39 >= 0 /\ -D - F + 41 >= 0 /\ C - F + 1 >= 0 /\ -C - F + 1 >= 0 /\ B - F - 39 >= 0 /\ -B - F + 41 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ -E + F - 1 >= 0 /\ D + F - 41 >= 0 /\ -D + F + 39 >= 0 /\ C + F - 1 >= 0 /\ -C + F - 1 >= 0 /\ B + F - 41 >= 0 /\ -B + F + 39 >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E >= 0 /\ D - E - 40 >= 0 /\ -D - E + 40 >= 0 /\ C - E >= 0 /\ -C - E >= 0 /\ B - E - 40 >= 0 /\ -B - E + 40 >= 0 /\ A - E - 1 >= 0 /\ -A - E + 1 >= 0 /\ E >= 0 /\ D + E - 40 >= 0 /\ -D + E + 40 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 40 >= 0 /\ -B + E + 40 >= 0 /\ A + E - 1 >= 0 /\ -A + E + 1 >= 0 /\ -D + 40 >= 0 /\ C - D + 40 >= 0 /\ -C - D + 40 >= 0 /\ B - D >= 0 /\ -B - D + 80 >= 0 /\ A - D + 39 >= 0 /\ -A - D + 41 >= 0 /\ D - 40 >= 0 /\ C + D - 40 >= 0 /\ -C + D - 40 >= 0 /\ B + D - 80 >= 0 /\ -B + D >= 0 /\ A + D - 41 >= 0 /\ -A + D - 39 >= 0 /\ -C >= 0 /\ B - C - 40 >= 0 /\ -B - C + 40 >= 0 /\ A - C - 1 >= 0 /\ -A - C + 1 >= 0 /\ C >= 0 /\ B + C - 40 >= 0 /\ -B + C + 40 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ -B + 40 >= 0 /\ A - B + 39 >= 0 /\ -A - B + 41 >= 0 /\ B - 40 >= 0 /\ A + B - 41 >= 0 /\ -A + B - 39 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ H >= 256 ]
)