(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)
(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) -> Com_1(f20(C1, B, C, A1, Z, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, 0, V, 1, B1, C1)) [ V >= 4 /\ A1 >= 0 /\ B1 >= 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) -> Com_1(f20(C1, B, C, A1, Z, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, 0, V, 1, B1, C1)) [ 2 >= V /\ A1 >= 0 /\ B1 >= 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) -> Com_1(f20(C1, B, C, A1, Z, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, 0, 3, 1, B1, C1)) [ A1 >= 0 /\ B1 >= 1 /\ V = 3 ]
  f20(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) -> Com_1(f26(A, 0, D, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ -I >= 0 /\ D - I >= 0 /\ X - I - 1 >= 0 /\ W - I - 1 >= 0 /\ -W - I + 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ I >= 0 /\ D + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ -U + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ -U - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ -U + W - 1 >= 0 /\ -U >= 0 /\ U >= 0 /\ D >= 1 /\ 0 >= A ]
  f20(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) -> Com_1(f26(A, 1, D, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ -I >= 0 /\ D - I >= 0 /\ X - I - 1 >= 0 /\ W - I - 1 >= 0 /\ -W - I + 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ I >= 0 /\ D + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ -U + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ -U - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ -U + W - 1 >= 0 /\ -U >= 0 /\ U >= 0 /\ 0 >= D /\ 0 >= A ]
  f20(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) -> Com_1(f26(A, 1, D, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ -I >= 0 /\ D - I >= 0 /\ X - I - 1 >= 0 /\ W - I - 1 >= 0 /\ -W - I + 1 >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ I >= 0 /\ D + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ -U + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ -U - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ -U + W - 1 >= 0 /\ -U >= 0 /\ U >= 0 /\ A >= 1 ]
  f26(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) -> Com_1(f26(A, B, C + 1, D, E, Z, A1, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ E >= C + 1 /\ 0 >= Z /\ A1 >= 1 ]
  f26(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) -> Com_1(f33(A, B, C, D, E, Z, A1, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ E >= C + 1 /\ 0 >= Z /\ 0 >= A1 ]
  f26(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) -> Com_1(f33(A, B, C, D, E, Z, A1, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ Z >= 1 /\ E >= C + 1 ]
  f26(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) -> Com_1(f68(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)) [ I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ C >= E ]
  f33(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) -> Com_1(f33(A, B, C, D, E, F, G, H, I + 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ I >= H /\ J >= 0 ]
  f33(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) -> Com_1(f33(A, B, C, D, E, F, G, H, I + 1, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ I >= H /\ 0 >= J + 2 ]
  f33(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) -> Com_1(f39(A, B, C, D, E, F, G, H, I, -1, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ I >= H /\ J + 1 = 0 ]
  f33(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) -> Com_1(f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ H >= I + 1 ]
  f68(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) -> Com_1(f71(1, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ U >= 1 ]
  f68(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) -> Com_1(f71(0, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ 0 >= U ]
  f71(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) -> Com_1(f71(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)) [ I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ A + I >= 0 /\ -A + I + 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ A + D >= 0 /\ -A + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ A + X - 1 >= 0 /\ -A + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ A - W + 1 >= 0 /\ -A - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ A + W - 1 >= 0 /\ -A + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ A + U >= 0 /\ -A + U >= 0 /\ -B + 1 >= 0 /\ A - B + 1 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 1 >= 0 /\ -A + 1 >= 0 /\ A >= 0 ]
  f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y) -> Com_1(f68(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)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ I >= H ]
  f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y) -> Com_1(f26(A, B, C + 1, D, E, F, G, H, I, J, Z, Z, A1, N, O, B1, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ B1 >= 1 /\ A1 >= 1 /\ H >= I + 1 /\ 0 >= Z ]
  f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y) -> Com_1(f26(A, B, C + 1, D, E, F, G, H, I, J, Z, Z, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ H >= I + 1 /\ Z >= 1 ]
  f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y) -> Com_1(f52(A, B, C, D, E, F, G, H, I, J, Z, Z, A1, C1, C1, B1, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ 0 >= B1 /\ A1 >= 1 /\ H >= I + 1 /\ 0 >= Z ]
  f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y) -> Com_1(f52(A, B, C, D, E, F, G, H, I, J, Z, Z, A1, B1, B1, P, Q, R, S, T, U, V, W, X, Y)) [ I >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -B + 1 >= 0 /\ B >= 0 /\ 0 >= A1 /\ H >= I + 1 /\ 0 >= Z ]
  f52(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) -> Com_1(f26(A, B, C + 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ -L + B >= 0 /\ -L >= 0 /\ 0 >= O + 1 ]
  f52(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) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 3, 1, Z, T, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ -L + B >= 0 /\ -L >= 0 /\ O >= 0 /\ Q = 3 ]
  f52(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) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, Z, T, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ -L + B >= 0 /\ -L >= 0 /\ O >= 0 /\ Q >= 4 ]
  f52(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) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, Z, T, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ -L + B >= 0 /\ -L >= 0 /\ O >= 0 /\ 2 >= Q ]
  f52(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) -> Com_1(f68(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 3, Z, S, T, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ -L + B >= 0 /\ -L >= 0 /\ O >= 0 /\ Z >= 2 /\ Q = 3 ]
  f52(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) -> Com_1(f68(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 3, Z, S, T, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ -L + B >= 0 /\ -L >= 0 /\ O >= 0 /\ 0 >= Z /\ Q = 3 ]
  f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y) -> Com_1(f63(A, B, C, D, E, F, G, H, I, J, K, L, M, N, Z, P, Q, R, 10, Z, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ O + I >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ O + H - 1 >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ O + E - 1 >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ O + D >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ O + C >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ O + X - 1 >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ O - W + 1 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ O + W - 1 >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ O + U >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ O - B + 1 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ O + B >= 0 /\ -L + B >= 0 /\ O >= 0 /\ -L + O >= 0 /\ -L >= 0 /\ S >= 11 ]
  f59(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y) -> Com_1(f63(A, B, C, D, E, F, G, H, I, J, K, L, M, N, Z, P, Q, R, S, Z, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ O + I >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ O + H - 1 >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ O + E - 1 >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ O + D >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ O + C >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ O + X - 1 >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ O - W + 1 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ O + W - 1 >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ O + U >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ O - B + 1 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ O + B >= 0 /\ -L + B >= 0 /\ O >= 0 /\ -L + O >= 0 /\ -L >= 0 /\ 10 >= S ]
  f63(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) -> Com_1(f26(A, B, C + 1, D, E, F, G, H, I, L, K, L, M, N, O, P, Q, R, S, T, U + 1, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ -S + I + 10 >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ -S + H + 9 >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ -S + E + 9 >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ -S + D + 10 >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ -S + C + 10 >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -S + X + 9 >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ -S - W + 11 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ -S + W + 9 >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -S + U + 10 >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ -S - B + 11 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ -S + B + 10 >= 0 /\ -L + B >= 0 /\ -S + 10 >= 0 /\ -L - S + 10 >= 0 /\ -L >= 0 /\ O >= 0 ]
  f63(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) -> Com_1(f26(A, B, C + 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y)) [ H - I - 1 >= 0 /\ I >= 0 /\ H + I - 1 >= 0 /\ E + I - 1 >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ X + I - 1 >= 0 /\ W + I - 1 >= 0 /\ -W + I + 1 >= 0 /\ U + I >= 0 /\ B + I >= 0 /\ -B + I + 1 >= 0 /\ -S + I + 10 >= 0 /\ -L + I >= 0 /\ H - 1 >= 0 /\ E + H - 2 >= 0 /\ D + H - 1 >= 0 /\ C + H - 1 >= 0 /\ X + H - 2 >= 0 /\ W + H - 2 >= 0 /\ -W + H >= 0 /\ U + H - 1 >= 0 /\ B + H - 1 >= 0 /\ -B + H >= 0 /\ -S + H + 9 >= 0 /\ -L + H - 1 >= 0 /\ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ X + E - 2 >= 0 /\ W + E - 2 >= 0 /\ -W + E >= 0 /\ U + E - 1 >= 0 /\ -U + E - 1 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ -S + E + 9 >= 0 /\ -L + E - 1 >= 0 /\ C - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ X + D - 1 >= 0 /\ W + D - 1 >= 0 /\ -W + D + 1 >= 0 /\ U + D >= 0 /\ B + D - 1 >= 0 /\ -B + D + 1 >= 0 /\ -S + D + 10 >= 0 /\ -L + D >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ W + C - 1 >= 0 /\ -W + C + 1 >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ B + C - 1 >= 0 /\ -B + C + 1 >= 0 /\ -S + C + 10 >= 0 /\ -L + C >= 0 /\ X - 1 >= 0 /\ W + X - 2 >= 0 /\ -W + X >= 0 /\ U + X - 1 >= 0 /\ B + X - 1 >= 0 /\ -B + X >= 0 /\ -S + X + 9 >= 0 /\ -L + X - 1 >= 0 /\ -W + 1 >= 0 /\ U - W + 1 >= 0 /\ B - W + 1 >= 0 /\ -B - W + 2 >= 0 /\ -S - W + 11 >= 0 /\ -L - W + 1 >= 0 /\ W - 1 >= 0 /\ U + W - 1 >= 0 /\ B + W - 1 >= 0 /\ -B + W >= 0 /\ -S + W + 9 >= 0 /\ -L + W - 1 >= 0 /\ U >= 0 /\ B + U >= 0 /\ -B + U + 1 >= 0 /\ -S + U + 10 >= 0 /\ -L + U >= 0 /\ -B + 1 >= 0 /\ -S - B + 11 >= 0 /\ -L - B + 1 >= 0 /\ B >= 0 /\ -S + B + 10 >= 0 /\ -L + B >= 0 /\ -S + 10 >= 0 /\ -L - S + 10 >= 0 /\ -L >= 0 /\ 0 >= O + 1 ]
)