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