(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1 C1 D1 E1 F1 G1) (RULES f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f34(A, M1, J1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, K1, W, X, Y, Z, H1, 20, I1, I1, J1, K1, L1)) [ I1 >= 1 /\ L1 >= 21 ] f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f34(A, M1, K1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, L1, W, X, Y, Z, H1, I1, J1, J1, K1, L1, I1)) [ J1 >= 1 /\ 20 >= I1 /\ I1 >= 5 ] f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f34(A, M1, J1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, K1, W, X, Y, Z, H1, 5, I1, I1, J1, K1, L1)) [ I1 >= 1 /\ 4 >= L1 ] f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f96(A, B, 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, K1, W, X, Y, Z, H1, H1, I1, I1, J1, K1, G1)) [ 0 >= I1 ] f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f96(A, 0, 1, 0, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ D1 - 1 >= 0 /\ B = 0 ] f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f39(A, B, 1, B, H1, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ D1 - 1 >= 0 /\ B >= 1 ] f34(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f39(A, B, 1, B, H1, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ D1 - 1 >= 0 /\ 0 >= B + 1 ] f96(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f96(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -C + 1 >= 0 /\ C - 1 >= 0 ] f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f96(A, B, 1, D, 0, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ C + D1 - 2 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ C - 1 >= 0 /\ E = 0 ] f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, E, 10, H1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ C + D1 - 2 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ C - 1 >= 0 /\ E >= 1 ] f39(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, E, 10, H1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ C + D1 - 2 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ C - 1 >= 0 /\ 0 >= E + 1 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f96(A, B, 1, D, E, F, G, H, I, J, K, L, M, H, O, P, Q, R, S, T, U, V, H1, H1, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ H1 >= 1 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f96(A, B, 1, D, E, F, G, H, I, J, K, L, M, H, O, P, Q, R, S, T, U, V, H1, H1, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ 0 >= H1 + 1 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, 0, D, E, F, G, H1, I, J, K, L, M, H, O, P, Q, R, S, T, U, 0, 0, 0, I1, I1, A1, B1, C1, D1, E1, F1, G1)) [ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ I1 >= 1 /\ V = 0 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, 0, D, E, F, G, H1, I, J, K, L, M, H, O, P, Q, R, S, T, U, 0, 0, 0, I1, I1, A1, B1, C1, D1, E1, F1, G1)) [ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ 0 >= I1 + 1 /\ V = 0 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, F, G, H1, I, J, K, L, M, H, O, P, Q, R, S, T, U, 0, 0, 0, 0, 0, A1, B1, C1, D1, E1, F1, G1)) [ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ V = 0 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f56(A, B, C, D, E, F, G, H, I, J, K, L, M, H, O, P, Q, R, S, T, U, V, 0, 0, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ V >= 1 ] f44(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f56(A, B, C, D, E, F, G, H, I, J, K, L, M, H, O, P, Q, R, S, T, U, V, 0, 0, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ -C + 1 >= 0 /\ 0 >= V + 1 ] f56(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, F, G, H1, I, J, K, L, M, -1, O, P, Q, R, S, 0, 0, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ N + 1 = 0 ] f56(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f64(A, B, C, D, E, F, G, H, I1, J, K, L, M, -1, O, P, Q, R, S, H1, H1, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ H1 >= 1 /\ N + 1 = 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, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f64(A, B, C, D, E, F, G, H, I1, J, K, L, M, -1, O, P, Q, R, S, H1, H1, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ 0 >= H1 + 1 /\ N + 1 = 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, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, F, G, H1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ 0 >= N + 2 ] f56(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, F, G, H1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ N - H >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ -W >= 0 /\ W >= 0 /\ N >= 0 ] f64(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, F, G, H1, 0, 0, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ -N - 1 >= 0 /\ N + 1 >= 0 /\ I = 0 ] f64(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f69(A, B, C, D, E, F, G, H, I, I, 0, H1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ -N - 1 >= 0 /\ N + 1 >= 0 /\ I >= 1 ] f64(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f69(A, B, C, D, E, F, G, H, I, I, 0, H1, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ -N - 1 >= 0 /\ N + 1 >= 0 /\ 0 >= I + 1 ] f69(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, 0, 0, H1, H1, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ H1 >= 1 ] f69(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, 0, 0, H1, H1, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= H1 + 1 ] f69(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f83(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, 0, 0, 0, 0, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 ] f69(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f87(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, H1, H1, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ H1 >= 1 ] f69(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f87(A, B, C, D, E, F, G, H, I, J, K, L, M, N, L, H1, H1, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= H1 + 1 ] f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f83(A, B, C, D, E, F, G, H, I, J, K, L, 0, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ Q + D1 - 1 >= 0 /\ -Q + D1 - 1 >= 0 /\ P + D1 - 1 >= 0 /\ -P + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ M = 0 ] f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ Q + D1 - 1 >= 0 /\ -Q + D1 - 1 >= 0 /\ P + D1 - 1 >= 0 /\ -P + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ M >= 1 ] f80(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ Q + D1 - 1 >= 0 /\ -Q + D1 - 1 >= 0 /\ P + D1 - 1 >= 0 /\ -P + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= M + 1 ] f83(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f87(A, B, C, D, E, F, G, H, I, J, 0, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 2 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ Q + D1 - 1 >= 0 /\ -Q + D1 - 1 >= 0 /\ P + D1 - 1 >= 0 /\ -P + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 2 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X + 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X + 1 >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W + 1 >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W + 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q + 1 >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q + 1 >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P + 1 >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P + 1 >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 2 >= 0 /\ -K + 1 >= 0 /\ K >= 0 /\ K = 0 ] f83(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f87(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 2 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ Q + D1 - 1 >= 0 /\ -Q + D1 - 1 >= 0 /\ P + D1 - 1 >= 0 /\ -P + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 2 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X + 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X + 1 >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W + 1 >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W + 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q + 1 >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q + 1 >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P + 1 >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P + 1 >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 2 >= 0 /\ -K + 1 >= 0 /\ K >= 0 /\ K >= 1 ] f87(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, F, G, H1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 2 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 2 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X + 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X + 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W + 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W + 1 >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 2 >= 0 /\ -K + 1 >= 0 /\ K >= 0 /\ K >= 1 ] f87(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f44(A, B, C, D, E, F, G, H1, I, J, 0, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 2 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 11 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 9 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 2 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X + 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X + 1 >= 0 /\ -W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W + 1 >= 0 /\ W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W + 1 >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 2 >= 0 /\ -K + 1 >= 0 /\ K >= 0 /\ K = 0 ] f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f83(A, B, C, D, E, F, G, H, I, J, 1, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ Q + D1 - 1 >= 0 /\ -Q + D1 - 1 >= 0 /\ P + D1 - 1 >= 0 /\ -P + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ A >= 1 ] f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f83(A, B, C, D, E, F, G, H, I, J, 1, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ Q + D1 - 1 >= 0 /\ -Q + D1 - 1 >= 0 /\ P + D1 - 1 >= 0 /\ -P + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ 0 >= A + 1 ] f81(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1) -> Com_1(f83(0, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1)) [ J - I >= 0 /\ -J + I >= 0 /\ -H - 1 >= 0 /\ G - H - 11 >= 0 /\ -G - H + 9 >= 0 /\ D1 - H - 2 >= 0 /\ -C - H >= 0 /\ X - H - 1 >= 0 /\ -X - H - 1 >= 0 /\ W - H - 1 >= 0 /\ -W - H - 1 >= 0 /\ Q - H - 1 >= 0 /\ -Q - H - 1 >= 0 /\ P - H - 1 >= 0 /\ -P - H - 1 >= 0 /\ N - H >= 0 /\ -N - H - 2 >= 0 /\ K - H - 1 >= 0 /\ -K - H - 1 >= 0 /\ H + 1 >= 0 /\ G + H - 9 >= 0 /\ -G + H + 11 >= 0 /\ D1 + H >= 0 /\ -C + H + 2 >= 0 /\ X + H + 1 >= 0 /\ -X + H + 1 >= 0 /\ W + H + 1 >= 0 /\ -W + H + 1 >= 0 /\ Q + H + 1 >= 0 /\ -Q + H + 1 >= 0 /\ P + H + 1 >= 0 /\ -P + H + 1 >= 0 /\ N + H + 2 >= 0 /\ -N + H >= 0 /\ K + H + 1 >= 0 /\ -K + H + 1 >= 0 /\ -G + 10 >= 0 /\ D1 - G + 9 >= 0 /\ -C - G + 11 >= 0 /\ X - G + 10 >= 0 /\ -X - G + 10 >= 0 /\ W - G + 10 >= 0 /\ -W - G + 10 >= 0 /\ Q - G + 10 >= 0 /\ -Q - G + 10 >= 0 /\ P - G + 10 >= 0 /\ -P - G + 10 >= 0 /\ N - G + 11 >= 0 /\ -N - G + 9 >= 0 /\ K - G + 10 >= 0 /\ -K - G + 10 >= 0 /\ G - 10 >= 0 /\ D1 + G - 11 >= 0 /\ -C + G - 9 >= 0 /\ X + G - 10 >= 0 /\ -X + G - 10 >= 0 /\ W + G - 10 >= 0 /\ -W + G - 10 >= 0 /\ Q + G - 10 >= 0 /\ -Q + G - 10 >= 0 /\ P + G - 10 >= 0 /\ -P + G - 10 >= 0 /\ N + G - 9 >= 0 /\ -N + G - 11 >= 0 /\ K + G - 10 >= 0 /\ -K + G - 10 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ B - D >= 0 /\ -B + D >= 0 /\ D1 - 1 >= 0 /\ -C + D1 >= 0 /\ X + D1 - 1 >= 0 /\ -X + D1 - 1 >= 0 /\ W + D1 - 1 >= 0 /\ -W + D1 - 1 >= 0 /\ Q + D1 - 1 >= 0 /\ -Q + D1 - 1 >= 0 /\ P + D1 - 1 >= 0 /\ -P + D1 - 1 >= 0 /\ N + D1 >= 0 /\ -N + D1 - 2 >= 0 /\ K + D1 - 1 >= 0 /\ -K + D1 - 1 >= 0 /\ -C + 1 >= 0 /\ X - C + 1 >= 0 /\ -X - C + 1 >= 0 /\ W - C + 1 >= 0 /\ -W - C + 1 >= 0 /\ Q - C + 1 >= 0 /\ -Q - C + 1 >= 0 /\ P - C + 1 >= 0 /\ -P - C + 1 >= 0 /\ N - C + 2 >= 0 /\ -N - C >= 0 /\ K - C + 1 >= 0 /\ -K - C + 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ N - X + 1 >= 0 /\ -N - X - 1 >= 0 /\ K - X >= 0 /\ -K - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ N + X + 1 >= 0 /\ -N + X - 1 >= 0 /\ K + X >= 0 /\ -K + X >= 0 /\ -W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ N - W + 1 >= 0 /\ -N - W - 1 >= 0 /\ K - W >= 0 /\ -K - W >= 0 /\ W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ N + W + 1 >= 0 /\ -N + W - 1 >= 0 /\ K + W >= 0 /\ -K + W >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ N - Q + 1 >= 0 /\ -N - Q - 1 >= 0 /\ K - Q >= 0 /\ -K - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ N + Q + 1 >= 0 /\ -N + Q - 1 >= 0 /\ K + Q >= 0 /\ -K + Q >= 0 /\ -P >= 0 /\ N - P + 1 >= 0 /\ -N - P - 1 >= 0 /\ K - P >= 0 /\ -K - P >= 0 /\ P >= 0 /\ N + P + 1 >= 0 /\ -N + P - 1 >= 0 /\ K + P >= 0 /\ -K + P >= 0 /\ L - O >= 0 /\ -L + O >= 0 /\ -N - 1 >= 0 /\ K - N - 1 >= 0 /\ -K - N - 1 >= 0 /\ N + 1 >= 0 /\ K + N + 1 >= 0 /\ -K + N + 1 >= 0 /\ -K >= 0 /\ K >= 0 /\ A = 0 ] )