(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)
(RULES
  f135(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f136(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ 0 >= A + 1 ]
  f135(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f136(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ A >= 1 ]
  f136(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ 0 >= B + 1 ]
  f136(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ B >= 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) -> Com_1(f26(1, 1, 3, X, 1, 1, Y, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W))
  f26(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f29(A, B, C, D, E, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ E + H - 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ E - F >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ -E + F >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ E - 1 >= 0 /\ C + E - 4 >= 0 /\ -C + E + 2 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ A + E - 2 >= 0 /\ -A + E >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ D >= H + 1 ]
  f29(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f29(A, B, C, D, E, F, G, H, I + 1, X, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ E + I - 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ A + I - 1 >= 0 /\ -A + I + 1 >= 0 /\ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ E + H - 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ E - F >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 4 >= 0 /\ -C + E + 2 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ A + E - 2 >= 0 /\ -A + E >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ D >= I + 1 ]
  f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f41(A, B, C, D, E, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ D >= H + 1 ]
  f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_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)) [ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ A + I - 1 >= 0 /\ -A + I + 1 >= 0 /\ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 0 >= E + 1 /\ D >= I + 1 ]
  f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_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)) [ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ A + I - 1 >= 0 /\ -A + I + 1 >= 0 /\ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ E >= 1 /\ D >= I + 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) -> Com_1(f41(A, B, C, D, 1, F, G, H, I + 1, J, 1, L, M, N, O, P, Q, R, S, T, U, V, W)) [ D - I - 1 >= 0 /\ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ A + I - 1 >= 0 /\ -A + I + 1 >= 0 /\ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 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) -> Com_1(f41(A, B, C, D, 0, F, G, H, I + 1, J, 0, L, M, N, O, P, Q, R, S, T, U, V, W)) [ D - I - 1 >= 0 /\ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ A + I - 1 >= 0 /\ -A + I + 1 >= 0 /\ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 ]
  f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f41(A, B, C, D, 0, F, G, H, I + 1, J, 0, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ A + I - 1 >= 0 /\ -A + I + 1 >= 0 /\ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ D >= I + 1 /\ E = 0 ]
  f56(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, 0, M, N, O, P, Q, R, S, T, U, V, W)) [ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ D >= H + 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) -> Com_1(f62(A, B, C, D, E, F, G, H, I, J, K, L, L + 1, N, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ L + D - 1 >= 0 /\ -L + D - 1 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 /\ D >= L + 2 ]
  f62(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 2 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ M + H - 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ M - F >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ M - E >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ B + D - 3 >= 0 /\ -B + D - 1 >= 0 /\ M + D - 3 >= 0 /\ L + D - 2 >= 0 /\ -L + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ M - C + 2 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ M + C - 4 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ M - 1 >= 0 /\ L + M - 1 >= 0 /\ -L + M - 1 >= 0 /\ -A + M >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 /\ D >= M + 1 /\ 0 >= A + 1 ]
  f62(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 2 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ M + H - 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ M - F >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ M - E >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ B + D - 3 >= 0 /\ -B + D - 1 >= 0 /\ M + D - 3 >= 0 /\ L + D - 2 >= 0 /\ -L + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ M - C + 2 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ M + C - 4 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ M - 1 >= 0 /\ L + M - 1 >= 0 /\ -L + M - 1 >= 0 /\ -A + M >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 /\ D >= M + 1 /\ A >= 1 ]
  f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f62(1, B, C, D, E, F, G, H, I, J, K, L, M + 1, 1, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 2 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ M + H - 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ M - F >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ M - E >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ B + D - 3 >= 0 /\ -B + D - 1 >= 0 /\ M + D - 3 >= 0 /\ -M + D - 1 >= 0 /\ L + D - 2 >= 0 /\ -L + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ M - C + 2 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ M + C - 4 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ M - 1 >= 0 /\ L + M - 1 >= 0 /\ -L + M - 1 >= 0 /\ -A + M >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 /\ X >= Y + 1 ]
  f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f62(1, B, C, D, E, F, G, H, I, J, K, L, M + 1, 1, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 2 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ M + H - 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ M - F >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ M - E >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ B + D - 3 >= 0 /\ -B + D - 1 >= 0 /\ M + D - 3 >= 0 /\ -M + D - 1 >= 0 /\ L + D - 2 >= 0 /\ -L + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ M - C + 2 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ M + C - 4 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ M - 1 >= 0 /\ L + M - 1 >= 0 /\ -L + M - 1 >= 0 /\ -A + M >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 ]
  f65(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f62(0, B, C, D, E, F, G, H, I, J, K, L, M + 1, 0, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 2 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ M + H - 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ M - F >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ M - E >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ B + D - 3 >= 0 /\ -B + D - 1 >= 0 /\ M + D - 3 >= 0 /\ -M + D - 1 >= 0 /\ L + D - 2 >= 0 /\ -L + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ M - C + 2 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ M + C - 4 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ M - 1 >= 0 /\ L + M - 1 >= 0 /\ -L + M - 1 >= 0 /\ -A + M >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 ]
  f62(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f62(0, B, C, D, E, F, G, H, I, J, K, L, M + 1, 0, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 2 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ M + H - 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ M - F >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ M - E >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ B + D - 3 >= 0 /\ -B + D - 1 >= 0 /\ M + D - 3 >= 0 /\ L + D - 2 >= 0 /\ -L + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ M - C + 2 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ M + C - 4 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ M - 1 >= 0 /\ L + M - 1 >= 0 /\ -L + M - 1 >= 0 /\ -A + M >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 /\ D >= M + 1 /\ A = 0 ]
  f77(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, 0, P, Q, R, S, T, U, V, W)) [ H - I >= 0 /\ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ -D + H >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ D >= I + 1 ]
  f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f83(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, O + 1, Q, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 1 >= 0 /\ F + H - 2 >= 0 /\ -F + H >= 0 /\ -E + H >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ C + H - 4 >= 0 /\ -C + H + 2 >= 0 /\ -B + H >= 0 /\ O + H - 1 >= 0 /\ -O + H - 1 >= 0 /\ -A + H >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ -B + D >= 0 /\ O + D - 1 >= 0 /\ -O + D - 1 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 /\ D >= O + 2 ]
  f83(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f86(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ P + I - 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 2 >= 0 /\ F + H - 3 >= 0 /\ -F + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 4 >= 0 /\ -D + H >= 0 /\ C + H - 5 >= 0 /\ -C + H + 1 >= 0 /\ -B + H - 1 >= 0 /\ P + H - 3 >= 0 /\ O + H - 2 >= 0 /\ -O + H - 2 >= 0 /\ -A + H - 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ P - F >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ P - E >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ -B + D - 1 >= 0 /\ P + D - 3 >= 0 /\ O + D - 2 >= 0 /\ -O + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ P - C + 2 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ P + C - 4 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ P - B >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ P - 1 >= 0 /\ O + P - 1 >= 0 /\ -O + P - 1 >= 0 /\ -A + P >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 /\ D >= P + 1 /\ 0 >= B + 1 ]
  f83(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f86(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ P + I - 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 2 >= 0 /\ F + H - 3 >= 0 /\ -F + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 4 >= 0 /\ -D + H >= 0 /\ C + H - 5 >= 0 /\ -C + H + 1 >= 0 /\ -B + H - 1 >= 0 /\ P + H - 3 >= 0 /\ O + H - 2 >= 0 /\ -O + H - 2 >= 0 /\ -A + H - 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ P - F >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ P - E >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ -B + D - 1 >= 0 /\ P + D - 3 >= 0 /\ O + D - 2 >= 0 /\ -O + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ P - C + 2 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ P + C - 4 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ P - B >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ P - 1 >= 0 /\ O + P - 1 >= 0 /\ -O + P - 1 >= 0 /\ -A + P >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 /\ D >= P + 1 /\ B >= 1 ]
  f86(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f83(A, 1, C, D, E, F, G, H, I, J, K, L, M, N, O, P + 1, 1, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ P + I - 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 2 >= 0 /\ F + H - 3 >= 0 /\ -F + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 4 >= 0 /\ -D + H >= 0 /\ C + H - 5 >= 0 /\ -C + H + 1 >= 0 /\ -B + H - 1 >= 0 /\ P + H - 3 >= 0 /\ -P + H - 1 >= 0 /\ O + H - 2 >= 0 /\ -O + H - 2 >= 0 /\ -A + H - 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ P - F >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ P - E >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ -B + D - 1 >= 0 /\ P + D - 3 >= 0 /\ -P + D - 1 >= 0 /\ O + D - 2 >= 0 /\ -O + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ P - C + 2 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ P + C - 4 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ P - B >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ P - 1 >= 0 /\ O + P - 1 >= 0 /\ -O + P - 1 >= 0 /\ -A + P >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 /\ X >= Y + 1 ]
  f86(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f83(A, 1, C, D, E, F, G, H, I, J, K, L, M, N, O, P + 1, 1, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ P + I - 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 2 >= 0 /\ F + H - 3 >= 0 /\ -F + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 4 >= 0 /\ -D + H >= 0 /\ C + H - 5 >= 0 /\ -C + H + 1 >= 0 /\ -B + H - 1 >= 0 /\ P + H - 3 >= 0 /\ -P + H - 1 >= 0 /\ O + H - 2 >= 0 /\ -O + H - 2 >= 0 /\ -A + H - 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ P - F >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ P - E >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ -B + D - 1 >= 0 /\ P + D - 3 >= 0 /\ -P + D - 1 >= 0 /\ O + D - 2 >= 0 /\ -O + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ P - C + 2 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ P + C - 4 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ P - B >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ P - 1 >= 0 /\ O + P - 1 >= 0 /\ -O + P - 1 >= 0 /\ -A + P >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 ]
  f86(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f83(A, 0, C, D, E, F, G, H, I, J, K, L, M, N, O, P + 1, 0, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ P + I - 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 2 >= 0 /\ F + H - 3 >= 0 /\ -F + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 4 >= 0 /\ -D + H >= 0 /\ C + H - 5 >= 0 /\ -C + H + 1 >= 0 /\ -B + H - 1 >= 0 /\ P + H - 3 >= 0 /\ -P + H - 1 >= 0 /\ O + H - 2 >= 0 /\ -O + H - 2 >= 0 /\ -A + H - 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ P - F >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ P - E >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ -B + D - 1 >= 0 /\ P + D - 3 >= 0 /\ -P + D - 1 >= 0 /\ O + D - 2 >= 0 /\ -O + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ P - C + 2 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ P + C - 4 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ P - B >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ P - 1 >= 0 /\ O + P - 1 >= 0 /\ -O + P - 1 >= 0 /\ -A + P >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 ]
  f83(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f83(A, 0, C, D, E, F, G, H, I, J, K, L, M, N, O, P + 1, 0, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ P + I - 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 2 >= 0 /\ F + H - 3 >= 0 /\ -F + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 4 >= 0 /\ -D + H >= 0 /\ C + H - 5 >= 0 /\ -C + H + 1 >= 0 /\ -B + H - 1 >= 0 /\ P + H - 3 >= 0 /\ O + H - 2 >= 0 /\ -O + H - 2 >= 0 /\ -A + H - 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ P - F >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ P - E >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ -B + D - 1 >= 0 /\ P + D - 3 >= 0 /\ O + D - 2 >= 0 /\ -O + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ P - C + 2 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ P + C - 4 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ P - B >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ P - 1 >= 0 /\ O + P - 1 >= 0 /\ -O + P - 1 >= 0 /\ -A + P >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 /\ D >= P + 1 /\ B = 0 ]
  f98(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f101(A, B, C, D, E, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ C >= H + 1 ]
  f101(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f104(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, 0, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ C >= I + 1 ]
  f104(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f107(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ C >= R + 1 ]
  f107(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f110(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, 0, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ C >= S + 1 ]
  f110(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f113(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, 0, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ C >= T + 1 ]
  f113(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f117(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ U + I >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ U + H >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ U - F + 1 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ U - E + 1 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ U - C + 3 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ U + C - 3 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -B + U + 1 >= 0 /\ S + U >= 0 /\ R + U >= 0 /\ -A + U + 1 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ 0 >= F + 1 /\ C*T + U >= C*R + S + 1 /\ C >= U + 1 ]
  f113(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f117(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ U + I >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ U + H >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ U - F + 1 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ U - E + 1 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ U - C + 3 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ U + C - 3 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -B + U + 1 >= 0 /\ S + U >= 0 /\ R + U >= 0 /\ -A + U + 1 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ F >= 1 /\ C*T + U >= C*R + S + 1 /\ C >= U + 1 ]
  f113(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f113(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U + 1, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ U + I >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ U + H >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ U - F + 1 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ U - E + 1 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ U - C + 3 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ U + C - 3 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -B + U + 1 >= 0 /\ S + U >= 0 /\ R + U >= 0 /\ -A + U + 1 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ C*R + S >= C*T + U /\ C >= U + 1 ]
  f117(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f113(A, B, C, D, E, 1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U + 1, 1, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ U + I >= 0 /\ -U + I + 2 >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ U + H >= 0 /\ -U + H + 2 >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ U - F + 1 >= 0 /\ -U - F + 3 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ U - E + 1 >= 0 /\ -U - E + 3 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ U - C + 3 >= 0 /\ -U - C + 5 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ U + C - 3 >= 0 /\ -U + C - 1 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -U + 2 >= 0 /\ T - U + 2 >= 0 /\ -B - U + 3 >= 0 /\ S - U + 2 >= 0 /\ R - U + 2 >= 0 /\ -A - U + 3 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -B + U + 1 >= 0 /\ S + U >= 0 /\ R + U >= 0 /\ -A + U + 1 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ X >= Y + 1 ]
  f117(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f113(A, B, C, D, E, 1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U + 1, 1, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ U + I >= 0 /\ -U + I + 2 >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ U + H >= 0 /\ -U + H + 2 >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ U - F + 1 >= 0 /\ -U - F + 3 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ U - E + 1 >= 0 /\ -U - E + 3 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ U - C + 3 >= 0 /\ -U - C + 5 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ U + C - 3 >= 0 /\ -U + C - 1 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -U + 2 >= 0 /\ T - U + 2 >= 0 /\ -B - U + 3 >= 0 /\ S - U + 2 >= 0 /\ R - U + 2 >= 0 /\ -A - U + 3 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -B + U + 1 >= 0 /\ S + U >= 0 /\ R + U >= 0 /\ -A + U + 1 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 ]
  f117(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f113(A, B, C, D, E, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U + 1, 0, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ U + I >= 0 /\ -U + I + 2 >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ U + H >= 0 /\ -U + H + 2 >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ U - F + 1 >= 0 /\ -U - F + 3 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ U - E + 1 >= 0 /\ -U - E + 3 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ U - C + 3 >= 0 /\ -U - C + 5 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ U + C - 3 >= 0 /\ -U + C - 1 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -U + 2 >= 0 /\ T - U + 2 >= 0 /\ -B - U + 3 >= 0 /\ S - U + 2 >= 0 /\ R - U + 2 >= 0 /\ -A - U + 3 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -B + U + 1 >= 0 /\ S + U >= 0 /\ R + U >= 0 /\ -A + U + 1 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 ]
  f113(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f113(A, B, C, D, E, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U + 1, 0, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ U + I >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ U + H >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ U - F + 1 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ U - E + 1 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ U - C + 3 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ U + C - 3 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -B + U + 1 >= 0 /\ S + U >= 0 /\ R + U >= 0 /\ -A + U + 1 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ C*T + U >= C*R + S + 1 /\ C >= U + 1 /\ F = 0 ]
  f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f146(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 0)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ 0 >= F + 1 ]
  f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f146(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 0)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ F >= 1 ]
  f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f146(A, B, C, D, E, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 1)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ F = 0 ]
  f136(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f146(A, 0, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 1)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ B = 0 ]
  f135(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f146(0, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 1)) [ I >= 0 /\ H + I - 3 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H - 3 >= 0 /\ -F + H - 2 >= 0 /\ -E + H - 2 >= 0 /\ C + H - 6 >= 0 /\ -C + H >= 0 /\ -B + H - 2 >= 0 /\ -A + H - 2 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ A = 0 ]
  f113(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f110(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T + 1, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ U + I >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ U + H >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ U - F + 1 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ U - E + 1 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ U - C + 3 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ U + C - 3 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -B + U + 1 >= 0 /\ S + U >= 0 /\ R + U >= 0 /\ -A + U + 1 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ U >= C ]
  f110(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f107(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S + 1, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ T + I >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ T + H >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ T - F + 1 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ T - E + 1 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ T - C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ T + C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ T >= 0 /\ -B + T + 1 >= 0 /\ S + T >= 0 /\ R + T >= 0 /\ -A + T + 1 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ T >= C ]
  f107(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f104(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R + 1, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ S + I >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ S + H >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ S - F + 1 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ S - E + 1 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ S - C + 3 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ S + C - 3 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ S - B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -A + S + 1 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ S >= C ]
  f104(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f101(A, B, C, D, E, F, G, H, I + 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ R + I >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ R + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ R - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ R - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ R - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ R + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ R - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ R >= 0 /\ -A + R + 1 >= 0 /\ -A + 1 >= 0 /\ R >= C ]
  f101(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f98(A, B, C, D, E, F, G, H + 1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ I >= C ]
  f98(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f135(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ 0 >= E + 1 /\ H >= C ]
  f98(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f135(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ E >= 1 /\ H >= C ]
  f98(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f146(A, B, C, D, 0, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, 1)) [ I >= 0 /\ H + I >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ H >= C /\ E = 0 ]
  f83(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O + 1, P, Q, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 2 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ P + I - 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 2 >= 0 /\ F + H - 3 >= 0 /\ -F + H - 1 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 4 >= 0 /\ -D + H >= 0 /\ C + H - 5 >= 0 /\ -C + H + 1 >= 0 /\ -B + H - 1 >= 0 /\ P + H - 3 >= 0 /\ O + H - 2 >= 0 /\ -O + H - 2 >= 0 /\ -A + H - 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ P - F >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ P + F - 2 >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ P - E >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ -B + D - 1 >= 0 /\ P + D - 3 >= 0 /\ O + D - 2 >= 0 /\ -O + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ P - C + 2 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ P + C - 4 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ P - B >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ P - 1 >= 0 /\ O + P - 1 >= 0 /\ -O + P - 1 >= 0 /\ -A + P >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 /\ P >= D ]
  f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f77(A, B, C, D, E, F, G, H, I + 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I - 1 >= 0 /\ D - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ O + I >= 0 /\ -A + I + 1 >= 0 /\ H - 1 >= 0 /\ F + H - 2 >= 0 /\ -F + H >= 0 /\ -E + H >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ C + H - 4 >= 0 /\ -C + H + 2 >= 0 /\ -B + H >= 0 /\ O + H - 1 >= 0 /\ -O + H - 1 >= 0 /\ -A + H >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ O - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ O + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ O - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ -B + D >= 0 /\ O + D - 1 >= 0 /\ -O + D - 1 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ O - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ O + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ O - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ O >= 0 /\ -A + O + 1 >= 0 /\ -A + 1 >= 0 /\ O + 1 >= D ]
  f77(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f98(A, B, C, D, E, F, G, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H - I >= 0 /\ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ -B + I + 1 >= 0 /\ -A + I + 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ -D + H >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ -B + F >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ -A + 1 >= 0 /\ I >= D ]
  f62(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, L + 1, M, N, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 2 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ M + H - 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F - 1 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ M - F >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 3 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ M + F - 2 >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ M - E >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ -C + D + 1 >= 0 /\ B + D - 3 >= 0 /\ -B + D - 1 >= 0 /\ M + D - 3 >= 0 /\ L + D - 2 >= 0 /\ -L + D - 2 >= 0 /\ -A + D - 1 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ M - C + 2 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ M + C - 4 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ M - B >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 2 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ M - 1 >= 0 /\ L + M - 1 >= 0 /\ -L + M - 1 >= 0 /\ -A + M >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 /\ M >= D ]
  f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f56(A, B, C, D, E, F, G, H + 1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ L + H >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ L - F + 1 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ L + F - 1 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ L - E + 1 >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ L + D - 1 >= 0 /\ -L + D - 1 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ L - C + 3 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ L + C - 3 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ L - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ L + B - 1 >= 0 /\ -A + B >= 0 /\ L >= 0 /\ -A + L + 1 >= 0 /\ -A + 1 >= 0 /\ L + 1 >= D ]
  f56(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f77(A, B, C, D, E, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ H >= D ]
  f41(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, H + 1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ A + I - 1 >= 0 /\ -A + I + 1 >= 0 /\ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ I >= D ]
  f38(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f56(A, B, C, D, E, F, G, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ -E + F >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ H >= D ]
  f29(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f26(A, B, C, D, E, F, G, H + 1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ I >= 0 /\ H + I >= 0 /\ F + I - 1 >= 0 /\ -F + I + 1 >= 0 /\ E + I - 1 >= 0 /\ -E + I + 1 >= 0 /\ D + I - 1 >= 0 /\ C + I - 3 >= 0 /\ -C + I + 3 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ A + I - 1 >= 0 /\ -A + I + 1 >= 0 /\ D - H - 1 >= 0 /\ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ E + H - 1 >= 0 /\ -E + H + 1 >= 0 /\ D + H - 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ E - F >= 0 /\ -E - F + 2 >= 0 /\ D - F >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ -E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ D - E >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 4 >= 0 /\ -C + E + 2 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ A + E - 2 >= 0 /\ -A + E >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ -C + D + 2 >= 0 /\ B + D - 2 >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ I >= D ]
  f26(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W) -> Com_1(f38(A, B, C, D, E, F, G, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W)) [ H >= 0 /\ F + H - 1 >= 0 /\ -F + H + 1 >= 0 /\ E + H - 1 >= 0 /\ -E + H + 1 >= 0 /\ C + H - 3 >= 0 /\ -C + H + 3 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 1 >= 0 /\ A + H - 1 >= 0 /\ -A + H + 1 >= 0 /\ -F + 1 >= 0 /\ E - F >= 0 /\ -E - F + 2 >= 0 /\ C - F - 2 >= 0 /\ -C - F + 4 >= 0 /\ B - F >= 0 /\ -B - F + 2 >= 0 /\ A - F >= 0 /\ -A - F + 2 >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ -E + F >= 0 /\ C + F - 4 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 2 >= 0 /\ -B + F >= 0 /\ A + F - 2 >= 0 /\ -A + F >= 0 /\ -E + 1 >= 0 /\ C - E - 2 >= 0 /\ -C - E + 4 >= 0 /\ B - E >= 0 /\ -B - E + 2 >= 0 /\ A - E >= 0 /\ -A - E + 2 >= 0 /\ E - 1 >= 0 /\ C + E - 4 >= 0 /\ -C + E + 2 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ A + E - 2 >= 0 /\ -A + E >= 0 /\ -C + 3 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 4 >= 0 /\ C - 3 >= 0 /\ B + C - 4 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ -A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ H >= D ]
)