(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) (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) -> Com_1(f17(100, 10, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) 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) -> Com_1(f17(100, 0, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) f17(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f20(A, B, B, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ B >= 1 ] f17(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f45(A, 0, 0, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ B = 0 ] f45(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f57(A, B, C, D, E, F, 200, 10, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f45(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f57(A, B, C, D, E, F, 200, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f20(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f26(A, B, C, 10, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 101 >= 0 /\ -A + C + 99 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B - 1 >= 0 /\ A + B - 101 >= 0 /\ -A + B + 99 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f20(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f26(A, B, C, 0, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 101 >= 0 /\ -A + C + 99 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B - 1 >= 0 /\ A + B - 101 >= 0 /\ -A + B + 99 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f57(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f60(A, B, C, D, E, F, G, H, H, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ H >= 1 ] f57(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f85(A, B, C, D, E, F, G, 0, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ H = 0 ] f26(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f29(A, B, C, D, D, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -D + 10 >= 0 /\ C - D + 9 >= 0 /\ -C - D + 20 >= 0 /\ B - D + 9 >= 0 /\ -B - D + 20 >= 0 /\ A - D - 90 >= 0 /\ -A - D + 110 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ -C + D + 10 >= 0 /\ B + D - 1 >= 0 /\ -B + D + 10 >= 0 /\ A + D - 100 >= 0 /\ -A + D + 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 101 >= 0 /\ -A + C + 99 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B - 1 >= 0 /\ A + B - 101 >= 0 /\ -A + B + 99 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ D >= 1 ] f26(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f45(A, B, C, 0, 0, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -D + 10 >= 0 /\ C - D + 9 >= 0 /\ -C - D + 20 >= 0 /\ B - D + 9 >= 0 /\ -B - D + 20 >= 0 /\ A - D - 90 >= 0 /\ -A - D + 110 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ -C + D + 10 >= 0 /\ B + D - 1 >= 0 /\ -B + D + 10 >= 0 /\ A + D - 100 >= 0 /\ -A + D + 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 101 >= 0 /\ -A + C + 99 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B - 1 >= 0 /\ A + B - 101 >= 0 /\ -A + B + 99 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ D = 0 ] f85(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f97(A, B, C, D, E, F, G, H, I, J, K, L, 50, 10, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f85(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f97(A, B, C, D, E, F, G, H, I, J, K, L, 50, 0, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f60(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f66(A, B, C, D, E, F, G, H, I, 10, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I - 1 >= 0 /\ H + I - 2 >= 0 /\ -H + I >= 0 /\ G + I - 201 >= 0 /\ -G + I + 199 >= 0 /\ C + I - 1 >= 0 /\ -C + I + 9 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 9 >= 0 /\ A + I - 101 >= 0 /\ -A + I + 99 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H - 1 >= 0 /\ G + H - 201 >= 0 /\ -G + H + 199 >= 0 /\ C + H - 1 >= 0 /\ -C + H + 9 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 9 >= 0 /\ A + H - 101 >= 0 /\ -A + H + 99 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f60(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f66(A, B, C, D, E, F, G, H, I, 0, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I - 1 >= 0 /\ H + I - 2 >= 0 /\ -H + I >= 0 /\ G + I - 201 >= 0 /\ -G + I + 199 >= 0 /\ C + I - 1 >= 0 /\ -C + I + 9 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 9 >= 0 /\ A + I - 101 >= 0 /\ -A + I + 99 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H - 1 >= 0 /\ G + H - 201 >= 0 /\ -G + H + 199 >= 0 /\ C + H - 1 >= 0 /\ -C + H + 9 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 9 >= 0 /\ A + H - 101 >= 0 /\ -A + H + 99 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f29(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f45(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ F >= 0 /\ E + F - 1 >= 0 /\ -E + F + 10 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 10 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 10 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 10 >= 0 /\ A + F - 100 >= 0 /\ -A + F + 100 >= 0 /\ -E + 10 >= 0 /\ D - E >= 0 /\ -D - E + 20 >= 0 /\ C - E + 9 >= 0 /\ -C - E + 20 >= 0 /\ B - E + 9 >= 0 /\ -B - E + 20 >= 0 /\ A - E - 90 >= 0 /\ -A - E + 110 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ -D + E >= 0 /\ C + E - 2 >= 0 /\ -C + E + 9 >= 0 /\ B + E - 2 >= 0 /\ -B + E + 9 >= 0 /\ A + E - 101 >= 0 /\ -A + E + 99 >= 0 /\ -D + 10 >= 0 /\ C - D + 9 >= 0 /\ -C - D + 20 >= 0 /\ B - D + 9 >= 0 /\ -B - D + 20 >= 0 /\ A - D - 90 >= 0 /\ -A - D + 110 >= 0 /\ D - 1 >= 0 /\ C + D - 2 >= 0 /\ -C + D + 9 >= 0 /\ B + D - 2 >= 0 /\ -B + D + 9 >= 0 /\ A + D - 101 >= 0 /\ -A + D + 99 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 101 >= 0 /\ -A + C + 99 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B - 1 >= 0 /\ A + B - 101 >= 0 /\ -A + B + 99 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ F >= A ] f29(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f29(A, B, C, D, E, F + 1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ F >= 0 /\ E + F - 1 >= 0 /\ -E + F + 10 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 10 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 10 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 10 >= 0 /\ A + F - 100 >= 0 /\ -A + F + 100 >= 0 /\ -E + 10 >= 0 /\ D - E >= 0 /\ -D - E + 20 >= 0 /\ C - E + 9 >= 0 /\ -C - E + 20 >= 0 /\ B - E + 9 >= 0 /\ -B - E + 20 >= 0 /\ A - E - 90 >= 0 /\ -A - E + 110 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ -D + E >= 0 /\ C + E - 2 >= 0 /\ -C + E + 9 >= 0 /\ B + E - 2 >= 0 /\ -B + E + 9 >= 0 /\ A + E - 101 >= 0 /\ -A + E + 99 >= 0 /\ -D + 10 >= 0 /\ C - D + 9 >= 0 /\ -C - D + 20 >= 0 /\ B - D + 9 >= 0 /\ -B - D + 20 >= 0 /\ A - D - 90 >= 0 /\ -A - D + 110 >= 0 /\ D - 1 >= 0 /\ C + D - 2 >= 0 /\ -C + D + 9 >= 0 /\ B + D - 2 >= 0 /\ -B + D + 9 >= 0 /\ A + D - 101 >= 0 /\ -A + D + 99 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 101 >= 0 /\ -A + C + 99 >= 0 /\ -B + 10 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B - 1 >= 0 /\ A + B - 101 >= 0 /\ -A + B + 99 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ A >= F + 1 ] f97(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f100(A, B, C, D, E, F, G, H, I, J, K, L, M, N, N, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ N >= 1 ] f97(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f125(A, B, C, D, E, F, G, H, I, J, K, L, M, 0, 0, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ N = 0 ] f66(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f69(A, B, C, D, E, F, G, H, I, J, J, 0, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ J - I + 10 >= 0 /\ -J - I + 20 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I - 1 >= 0 /\ H + I - 2 >= 0 /\ -H + I >= 0 /\ G + I - 201 >= 0 /\ -G + I + 199 >= 0 /\ C + I - 1 >= 0 /\ -C + I + 9 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 9 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 9 >= 0 /\ A + I - 101 >= 0 /\ -A + I + 99 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ J - H + 10 >= 0 /\ -J - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H - 1 >= 0 /\ G + H - 201 >= 0 /\ -G + H + 199 >= 0 /\ C + H - 1 >= 0 /\ -C + H + 9 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 9 >= 0 /\ J + H - 1 >= 0 /\ -J + H + 9 >= 0 /\ A + H - 101 >= 0 /\ -A + H + 99 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ J - G + 200 >= 0 /\ -J - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ J + G - 200 >= 0 /\ -J + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ J - C + 10 >= 0 /\ -J - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ J + C >= 0 /\ -J + C + 10 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ J - B + 10 >= 0 /\ -J - B + 20 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ J + B >= 0 /\ -J + B + 10 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -J + 10 >= 0 /\ A - J - 90 >= 0 /\ -A - J + 110 >= 0 /\ J >= 0 /\ A + J - 100 >= 0 /\ -A + J + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ J >= 1 ] f66(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f85(A, B, C, D, E, F, G, H, I, 0, 0, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ J - I + 10 >= 0 /\ -J - I + 20 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I - 1 >= 0 /\ H + I - 2 >= 0 /\ -H + I >= 0 /\ G + I - 201 >= 0 /\ -G + I + 199 >= 0 /\ C + I - 1 >= 0 /\ -C + I + 9 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 9 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 9 >= 0 /\ A + I - 101 >= 0 /\ -A + I + 99 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ J - H + 10 >= 0 /\ -J - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H - 1 >= 0 /\ G + H - 201 >= 0 /\ -G + H + 199 >= 0 /\ C + H - 1 >= 0 /\ -C + H + 9 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 9 >= 0 /\ J + H - 1 >= 0 /\ -J + H + 9 >= 0 /\ A + H - 101 >= 0 /\ -A + H + 99 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ J - G + 200 >= 0 /\ -J - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ J + G - 200 >= 0 /\ -J + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ J - C + 10 >= 0 /\ -J - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ J + C >= 0 /\ -J + C + 10 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ J - B + 10 >= 0 /\ -J - B + 20 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ J + B >= 0 /\ -J + B + 10 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -J + 10 >= 0 /\ A - J - 90 >= 0 /\ -A - J + 110 >= 0 /\ J >= 0 /\ A + J - 100 >= 0 /\ -A + J + 100 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ J = 0 ] f125(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 20, 10, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f125(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 20, 0, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f100(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f106(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, 10, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ O - I + 9 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 9 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ O + I - 1 >= 0 /\ -O + I + 10 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ O - H + 9 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 9 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ O + H - 1 >= 0 /\ -O + H + 10 >= 0 /\ N + H - 1 >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ O - G + 199 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 199 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ O + G - 201 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 201 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ O - C + 9 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 9 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ O + C - 1 >= 0 /\ -O + C + 10 >= 0 /\ N + C - 1 >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ O - B + 9 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 9 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ O + B - 1 >= 0 /\ -O + B + 10 >= 0 /\ N + B - 1 >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O - 1 >= 0 /\ N + O - 2 >= 0 /\ -N + O >= 0 /\ M + O - 51 >= 0 /\ -M + O + 49 >= 0 /\ A + O - 101 >= 0 /\ -A + O + 99 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N - 1 >= 0 /\ M + N - 51 >= 0 /\ -M + N + 49 >= 0 /\ A + N - 101 >= 0 /\ -A + N + 99 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f100(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f106(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, 0, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ O - I + 9 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 9 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ O + I - 1 >= 0 /\ -O + I + 10 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ O - H + 9 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 9 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ O + H - 1 >= 0 /\ -O + H + 10 >= 0 /\ N + H - 1 >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ O - G + 199 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 199 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ O + G - 201 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 201 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ O - C + 9 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 9 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ O + C - 1 >= 0 /\ -O + C + 10 >= 0 /\ N + C - 1 >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ O - B + 9 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 9 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ O + B - 1 >= 0 /\ -O + B + 10 >= 0 /\ N + B - 1 >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O - 1 >= 0 /\ N + O - 2 >= 0 /\ -N + O >= 0 /\ M + O - 51 >= 0 /\ -M + O + 49 >= 0 /\ A + O - 101 >= 0 /\ -A + O + 99 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N - 1 >= 0 /\ M + N - 51 >= 0 /\ -M + N + 49 >= 0 /\ A + N - 101 >= 0 /\ -A + N + 99 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 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) -> Com_1(f85(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ L - I + 10 >= 0 /\ K - I + 9 >= 0 /\ -K - I + 20 >= 0 /\ J - I + 9 >= 0 /\ -J - I + 20 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I - 1 >= 0 /\ H + I - 2 >= 0 /\ -H + I >= 0 /\ G + I - 201 >= 0 /\ -G + I + 199 >= 0 /\ C + I - 1 >= 0 /\ -C + I + 9 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 9 >= 0 /\ L + I - 1 >= 0 /\ K + I - 2 >= 0 /\ -K + I + 9 >= 0 /\ J + I - 2 >= 0 /\ -J + I + 9 >= 0 /\ A + I - 101 >= 0 /\ -A + I + 99 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ L - H + 10 >= 0 /\ K - H + 9 >= 0 /\ -K - H + 20 >= 0 /\ J - H + 9 >= 0 /\ -J - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H - 1 >= 0 /\ G + H - 201 >= 0 /\ -G + H + 199 >= 0 /\ C + H - 1 >= 0 /\ -C + H + 9 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 9 >= 0 /\ L + H - 1 >= 0 /\ K + H - 2 >= 0 /\ -K + H + 9 >= 0 /\ J + H - 2 >= 0 /\ -J + H + 9 >= 0 /\ A + H - 101 >= 0 /\ -A + H + 99 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ L - G + 200 >= 0 /\ K - G + 199 >= 0 /\ -K - G + 210 >= 0 /\ J - G + 199 >= 0 /\ -J - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ L + G - 200 >= 0 /\ K + G - 201 >= 0 /\ -K + G - 190 >= 0 /\ J + G - 201 >= 0 /\ -J + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ L - C + 10 >= 0 /\ K - C + 9 >= 0 /\ -K - C + 20 >= 0 /\ J - C + 9 >= 0 /\ -J - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ L + C >= 0 /\ K + C - 1 >= 0 /\ -K + C + 10 >= 0 /\ J + C - 1 >= 0 /\ -J + C + 10 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ L - B + 10 >= 0 /\ K - B + 9 >= 0 /\ -K - B + 20 >= 0 /\ J - B + 9 >= 0 /\ -J - B + 20 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ L + B >= 0 /\ K + B - 1 >= 0 /\ -K + B + 10 >= 0 /\ J + B - 1 >= 0 /\ -J + B + 10 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ L >= 0 /\ K + L - 1 >= 0 /\ -K + L + 10 >= 0 /\ J + L - 1 >= 0 /\ -J + L + 10 >= 0 /\ A + L - 100 >= 0 /\ -A + L + 100 >= 0 /\ -K + 10 >= 0 /\ J - K >= 0 /\ -J - K + 20 >= 0 /\ A - K - 90 >= 0 /\ -A - K + 110 >= 0 /\ K - 1 >= 0 /\ J + K - 2 >= 0 /\ -J + K >= 0 /\ A + K - 101 >= 0 /\ -A + K + 99 >= 0 /\ -J + 10 >= 0 /\ A - J - 90 >= 0 /\ -A - J + 110 >= 0 /\ J - 1 >= 0 /\ A + J - 101 >= 0 /\ -A + J + 99 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ L >= G ] 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) -> Com_1(f69(A, B, C, D, E, F, G, H, I, J, K, L + 1, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ L - I + 10 >= 0 /\ K - I + 9 >= 0 /\ -K - I + 20 >= 0 /\ J - I + 9 >= 0 /\ -J - I + 20 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I - 1 >= 0 /\ H + I - 2 >= 0 /\ -H + I >= 0 /\ G + I - 201 >= 0 /\ -G + I + 199 >= 0 /\ C + I - 1 >= 0 /\ -C + I + 9 >= 0 /\ B + I - 1 >= 0 /\ -B + I + 9 >= 0 /\ L + I - 1 >= 0 /\ K + I - 2 >= 0 /\ -K + I + 9 >= 0 /\ J + I - 2 >= 0 /\ -J + I + 9 >= 0 /\ A + I - 101 >= 0 /\ -A + I + 99 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ L - H + 10 >= 0 /\ K - H + 9 >= 0 /\ -K - H + 20 >= 0 /\ J - H + 9 >= 0 /\ -J - H + 20 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H - 1 >= 0 /\ G + H - 201 >= 0 /\ -G + H + 199 >= 0 /\ C + H - 1 >= 0 /\ -C + H + 9 >= 0 /\ B + H - 1 >= 0 /\ -B + H + 9 >= 0 /\ L + H - 1 >= 0 /\ K + H - 2 >= 0 /\ -K + H + 9 >= 0 /\ J + H - 2 >= 0 /\ -J + H + 9 >= 0 /\ A + H - 101 >= 0 /\ -A + H + 99 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ L - G + 200 >= 0 /\ K - G + 199 >= 0 /\ -K - G + 210 >= 0 /\ J - G + 199 >= 0 /\ -J - G + 210 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ L + G - 200 >= 0 /\ K + G - 201 >= 0 /\ -K + G - 190 >= 0 /\ J + G - 201 >= 0 /\ -J + G - 190 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ L - C + 10 >= 0 /\ K - C + 9 >= 0 /\ -K - C + 20 >= 0 /\ J - C + 9 >= 0 /\ -J - C + 20 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ L + C >= 0 /\ K + C - 1 >= 0 /\ -K + C + 10 >= 0 /\ J + C - 1 >= 0 /\ -J + C + 10 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ L - B + 10 >= 0 /\ K - B + 9 >= 0 /\ -K - B + 20 >= 0 /\ J - B + 9 >= 0 /\ -J - B + 20 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ L + B >= 0 /\ K + B - 1 >= 0 /\ -K + B + 10 >= 0 /\ J + B - 1 >= 0 /\ -J + B + 10 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ L >= 0 /\ K + L - 1 >= 0 /\ -K + L + 10 >= 0 /\ J + L - 1 >= 0 /\ -J + L + 10 >= 0 /\ A + L - 100 >= 0 /\ -A + L + 100 >= 0 /\ -K + 10 >= 0 /\ J - K >= 0 /\ -J - K + 20 >= 0 /\ A - K - 90 >= 0 /\ -A - K + 110 >= 0 /\ K - 1 >= 0 /\ J + K - 2 >= 0 /\ -J + K >= 0 /\ A + K - 101 >= 0 /\ -A + K + 99 >= 0 /\ -J + 10 >= 0 /\ A - J - 90 >= 0 /\ -A - J + 110 >= 0 /\ J - 1 >= 0 /\ A + J - 101 >= 0 /\ -A + J + 99 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ G >= L + 1 ] f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f140(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, T, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ T - I + 10 >= 0 /\ -T - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ S - I - 10 >= 0 /\ -S - I + 30 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ T + I >= 0 /\ -T + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ S + I - 20 >= 0 /\ -S + I + 20 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ T - H + 10 >= 0 /\ -T - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ S - H - 10 >= 0 /\ -S - H + 30 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ T + H >= 0 /\ -T + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ S + H - 20 >= 0 /\ -S + H + 20 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ T - G + 200 >= 0 /\ -T - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ S - G + 180 >= 0 /\ -S - G + 220 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ T + G - 200 >= 0 /\ -T + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ S + G - 220 >= 0 /\ -S + G - 180 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ T - C + 10 >= 0 /\ -T - C + 20 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ S - C - 10 >= 0 /\ -S - C + 30 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ T + C >= 0 /\ -T + C + 10 >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C - 20 >= 0 /\ -S + C + 20 >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -T + 10 >= 0 /\ B - T + 10 >= 0 /\ -B - T + 20 >= 0 /\ S - T - 10 >= 0 /\ -S - T + 30 >= 0 /\ O - T + 10 >= 0 /\ -O - T + 20 >= 0 /\ N - T + 10 >= 0 /\ -N - T + 20 >= 0 /\ M - T - 40 >= 0 /\ -M - T + 60 >= 0 /\ A - T - 90 >= 0 /\ -A - T + 110 >= 0 /\ T >= 0 /\ B + T >= 0 /\ -B + T + 10 >= 0 /\ S + T - 20 >= 0 /\ -S + T + 20 >= 0 /\ O + T >= 0 /\ -O + T + 10 >= 0 /\ N + T >= 0 /\ -N + T + 10 >= 0 /\ M + T - 50 >= 0 /\ -M + T + 50 >= 0 /\ A + T - 100 >= 0 /\ -A + T + 100 >= 0 /\ -B + 10 >= 0 /\ S - B - 10 >= 0 /\ -S - B + 30 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ S + B - 20 >= 0 /\ -S + B + 20 >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -S + 20 >= 0 /\ O - S + 20 >= 0 /\ -O - S + 30 >= 0 /\ N - S + 20 >= 0 /\ -N - S + 30 >= 0 /\ M - S - 30 >= 0 /\ -M - S + 70 >= 0 /\ A - S - 80 >= 0 /\ -A - S + 120 >= 0 /\ S - 20 >= 0 /\ O + S - 20 >= 0 /\ -O + S - 10 >= 0 /\ N + S - 20 >= 0 /\ -N + S - 10 >= 0 /\ M + S - 70 >= 0 /\ -M + S + 30 >= 0 /\ A + S - 120 >= 0 /\ -A + S + 80 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ T >= 1 ] f137(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f166(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, 0, 0, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ T - I + 10 >= 0 /\ -T - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ S - I - 10 >= 0 /\ -S - I + 30 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ T + I >= 0 /\ -T + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ S + I - 20 >= 0 /\ -S + I + 20 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ T - H + 10 >= 0 /\ -T - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ S - H - 10 >= 0 /\ -S - H + 30 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ T + H >= 0 /\ -T + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ S + H - 20 >= 0 /\ -S + H + 20 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ T - G + 200 >= 0 /\ -T - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ S - G + 180 >= 0 /\ -S - G + 220 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ T + G - 200 >= 0 /\ -T + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ S + G - 220 >= 0 /\ -S + G - 180 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ T - C + 10 >= 0 /\ -T - C + 20 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ S - C - 10 >= 0 /\ -S - C + 30 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ T + C >= 0 /\ -T + C + 10 >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C - 20 >= 0 /\ -S + C + 20 >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -T + 10 >= 0 /\ B - T + 10 >= 0 /\ -B - T + 20 >= 0 /\ S - T - 10 >= 0 /\ -S - T + 30 >= 0 /\ O - T + 10 >= 0 /\ -O - T + 20 >= 0 /\ N - T + 10 >= 0 /\ -N - T + 20 >= 0 /\ M - T - 40 >= 0 /\ -M - T + 60 >= 0 /\ A - T - 90 >= 0 /\ -A - T + 110 >= 0 /\ T >= 0 /\ B + T >= 0 /\ -B + T + 10 >= 0 /\ S + T - 20 >= 0 /\ -S + T + 20 >= 0 /\ O + T >= 0 /\ -O + T + 10 >= 0 /\ N + T >= 0 /\ -N + T + 10 >= 0 /\ M + T - 50 >= 0 /\ -M + T + 50 >= 0 /\ A + T - 100 >= 0 /\ -A + T + 100 >= 0 /\ -B + 10 >= 0 /\ S - B - 10 >= 0 /\ -S - B + 30 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ S + B - 20 >= 0 /\ -S + B + 20 >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -S + 20 >= 0 /\ O - S + 20 >= 0 /\ -O - S + 30 >= 0 /\ N - S + 20 >= 0 /\ -N - S + 30 >= 0 /\ M - S - 30 >= 0 /\ -M - S + 70 >= 0 /\ A - S - 80 >= 0 /\ -A - S + 120 >= 0 /\ S - 20 >= 0 /\ O + S - 20 >= 0 /\ -O + S - 10 >= 0 /\ N + S - 20 >= 0 /\ -N + S - 10 >= 0 /\ M + S - 70 >= 0 /\ -M + S + 30 >= 0 /\ A + S - 120 >= 0 /\ -A + S + 80 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ T = 0 ] f106(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f109(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, P, 0, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ P - I + 10 >= 0 /\ -P - I + 20 >= 0 /\ O - I + 9 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 9 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ P + I >= 0 /\ -P + I + 10 >= 0 /\ O + I - 1 >= 0 /\ -O + I + 10 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ P - H + 10 >= 0 /\ -P - H + 20 >= 0 /\ O - H + 9 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 9 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ P + H >= 0 /\ -P + H + 10 >= 0 /\ O + H - 1 >= 0 /\ -O + H + 10 >= 0 /\ N + H - 1 >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ P - G + 200 >= 0 /\ -P - G + 210 >= 0 /\ O - G + 199 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 199 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ P + G - 200 >= 0 /\ -P + G - 190 >= 0 /\ O + G - 201 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 201 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ P - C + 10 >= 0 /\ -P - C + 20 >= 0 /\ O - C + 9 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 9 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ P + C >= 0 /\ -P + C + 10 >= 0 /\ O + C - 1 >= 0 /\ -O + C + 10 >= 0 /\ N + C - 1 >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ P - B + 10 >= 0 /\ -P - B + 20 >= 0 /\ O - B + 9 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 9 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ P + B >= 0 /\ -P + B + 10 >= 0 /\ O + B - 1 >= 0 /\ -O + B + 10 >= 0 /\ N + B - 1 >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -P + 10 >= 0 /\ O - P + 9 >= 0 /\ -O - P + 20 >= 0 /\ N - P + 9 >= 0 /\ -N - P + 20 >= 0 /\ M - P - 40 >= 0 /\ -M - P + 60 >= 0 /\ A - P - 90 >= 0 /\ -A - P + 110 >= 0 /\ P >= 0 /\ O + P - 1 >= 0 /\ -O + P + 10 >= 0 /\ N + P - 1 >= 0 /\ -N + P + 10 >= 0 /\ M + P - 50 >= 0 /\ -M + P + 50 >= 0 /\ A + P - 100 >= 0 /\ -A + P + 100 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O - 1 >= 0 /\ N + O - 2 >= 0 /\ -N + O >= 0 /\ M + O - 51 >= 0 /\ -M + O + 49 >= 0 /\ A + O - 101 >= 0 /\ -A + O + 99 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N - 1 >= 0 /\ M + N - 51 >= 0 /\ -M + N + 49 >= 0 /\ A + N - 101 >= 0 /\ -A + N + 99 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ P >= 1 ] f106(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f125(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, 0, 0, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ P - I + 10 >= 0 /\ -P - I + 20 >= 0 /\ O - I + 9 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 9 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ P + I >= 0 /\ -P + I + 10 >= 0 /\ O + I - 1 >= 0 /\ -O + I + 10 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ P - H + 10 >= 0 /\ -P - H + 20 >= 0 /\ O - H + 9 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 9 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ P + H >= 0 /\ -P + H + 10 >= 0 /\ O + H - 1 >= 0 /\ -O + H + 10 >= 0 /\ N + H - 1 >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ P - G + 200 >= 0 /\ -P - G + 210 >= 0 /\ O - G + 199 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 199 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ P + G - 200 >= 0 /\ -P + G - 190 >= 0 /\ O + G - 201 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 201 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ P - C + 10 >= 0 /\ -P - C + 20 >= 0 /\ O - C + 9 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 9 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ P + C >= 0 /\ -P + C + 10 >= 0 /\ O + C - 1 >= 0 /\ -O + C + 10 >= 0 /\ N + C - 1 >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ P - B + 10 >= 0 /\ -P - B + 20 >= 0 /\ O - B + 9 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 9 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ P + B >= 0 /\ -P + B + 10 >= 0 /\ O + B - 1 >= 0 /\ -O + B + 10 >= 0 /\ N + B - 1 >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -P + 10 >= 0 /\ O - P + 9 >= 0 /\ -O - P + 20 >= 0 /\ N - P + 9 >= 0 /\ -N - P + 20 >= 0 /\ M - P - 40 >= 0 /\ -M - P + 60 >= 0 /\ A - P - 90 >= 0 /\ -A - P + 110 >= 0 /\ P >= 0 /\ O + P - 1 >= 0 /\ -O + P + 10 >= 0 /\ N + P - 1 >= 0 /\ -N + P + 10 >= 0 /\ M + P - 50 >= 0 /\ -M + P + 50 >= 0 /\ A + P - 100 >= 0 /\ -A + P + 100 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O - 1 >= 0 /\ N + O - 2 >= 0 /\ -N + O >= 0 /\ M + O - 51 >= 0 /\ -M + O + 49 >= 0 /\ A + O - 101 >= 0 /\ -A + O + 99 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N - 1 >= 0 /\ M + N - 51 >= 0 /\ -M + N + 49 >= 0 /\ A + N - 101 >= 0 /\ -A + N + 99 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ P = 0 ] f140(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f146(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, 10, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ U - I + 9 >= 0 /\ -U - I + 20 >= 0 /\ T - I + 9 >= 0 /\ -T - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ S - I - 10 >= 0 /\ -S - I + 30 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ U + I - 1 >= 0 /\ -U + I + 10 >= 0 /\ T + I - 1 >= 0 /\ -T + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ S + I - 20 >= 0 /\ -S + I + 20 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ U - H + 9 >= 0 /\ -U - H + 20 >= 0 /\ T - H + 9 >= 0 /\ -T - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ S - H - 10 >= 0 /\ -S - H + 30 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ U + H - 1 >= 0 /\ -U + H + 10 >= 0 /\ T + H - 1 >= 0 /\ -T + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ S + H - 20 >= 0 /\ -S + H + 20 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ U - G + 199 >= 0 /\ -U - G + 210 >= 0 /\ T - G + 199 >= 0 /\ -T - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ S - G + 180 >= 0 /\ -S - G + 220 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ U + G - 201 >= 0 /\ -U + G - 190 >= 0 /\ T + G - 201 >= 0 /\ -T + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ S + G - 220 >= 0 /\ -S + G - 180 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ U - C + 9 >= 0 /\ -U - C + 20 >= 0 /\ T - C + 9 >= 0 /\ -T - C + 20 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ S - C - 10 >= 0 /\ -S - C + 30 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ U + C - 1 >= 0 /\ -U + C + 10 >= 0 /\ T + C - 1 >= 0 /\ -T + C + 10 >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C - 20 >= 0 /\ -S + C + 20 >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -U + 10 >= 0 /\ T - U >= 0 /\ -T - U + 20 >= 0 /\ B - U + 10 >= 0 /\ -B - U + 20 >= 0 /\ S - U - 10 >= 0 /\ -S - U + 30 >= 0 /\ O - U + 10 >= 0 /\ -O - U + 20 >= 0 /\ N - U + 10 >= 0 /\ -N - U + 20 >= 0 /\ M - U - 40 >= 0 /\ -M - U + 60 >= 0 /\ A - U - 90 >= 0 /\ -A - U + 110 >= 0 /\ U - 1 >= 0 /\ T + U - 2 >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ -B + U + 9 >= 0 /\ S + U - 21 >= 0 /\ -S + U + 19 >= 0 /\ O + U - 1 >= 0 /\ -O + U + 9 >= 0 /\ N + U - 1 >= 0 /\ -N + U + 9 >= 0 /\ M + U - 51 >= 0 /\ -M + U + 49 >= 0 /\ A + U - 101 >= 0 /\ -A + U + 99 >= 0 /\ -T + 10 >= 0 /\ B - T + 10 >= 0 /\ -B - T + 20 >= 0 /\ S - T - 10 >= 0 /\ -S - T + 30 >= 0 /\ O - T + 10 >= 0 /\ -O - T + 20 >= 0 /\ N - T + 10 >= 0 /\ -N - T + 20 >= 0 /\ M - T - 40 >= 0 /\ -M - T + 60 >= 0 /\ A - T - 90 >= 0 /\ -A - T + 110 >= 0 /\ T - 1 >= 0 /\ B + T - 1 >= 0 /\ -B + T + 9 >= 0 /\ S + T - 21 >= 0 /\ -S + T + 19 >= 0 /\ O + T - 1 >= 0 /\ -O + T + 9 >= 0 /\ N + T - 1 >= 0 /\ -N + T + 9 >= 0 /\ M + T - 51 >= 0 /\ -M + T + 49 >= 0 /\ A + T - 101 >= 0 /\ -A + T + 99 >= 0 /\ -B + 10 >= 0 /\ S - B - 10 >= 0 /\ -S - B + 30 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ S + B - 20 >= 0 /\ -S + B + 20 >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -S + 20 >= 0 /\ O - S + 20 >= 0 /\ -O - S + 30 >= 0 /\ N - S + 20 >= 0 /\ -N - S + 30 >= 0 /\ M - S - 30 >= 0 /\ -M - S + 70 >= 0 /\ A - S - 80 >= 0 /\ -A - S + 120 >= 0 /\ S - 20 >= 0 /\ O + S - 20 >= 0 /\ -O + S - 10 >= 0 /\ N + S - 20 >= 0 /\ -N + S - 10 >= 0 /\ M + S - 70 >= 0 /\ -M + S + 30 >= 0 /\ A + S - 120 >= 0 /\ -A + S + 80 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f140(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f146(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, 0, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ U - I + 9 >= 0 /\ -U - I + 20 >= 0 /\ T - I + 9 >= 0 /\ -T - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ S - I - 10 >= 0 /\ -S - I + 30 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ U + I - 1 >= 0 /\ -U + I + 10 >= 0 /\ T + I - 1 >= 0 /\ -T + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ S + I - 20 >= 0 /\ -S + I + 20 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ U - H + 9 >= 0 /\ -U - H + 20 >= 0 /\ T - H + 9 >= 0 /\ -T - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ S - H - 10 >= 0 /\ -S - H + 30 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ U + H - 1 >= 0 /\ -U + H + 10 >= 0 /\ T + H - 1 >= 0 /\ -T + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ S + H - 20 >= 0 /\ -S + H + 20 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ U - G + 199 >= 0 /\ -U - G + 210 >= 0 /\ T - G + 199 >= 0 /\ -T - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ S - G + 180 >= 0 /\ -S - G + 220 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ U + G - 201 >= 0 /\ -U + G - 190 >= 0 /\ T + G - 201 >= 0 /\ -T + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ S + G - 220 >= 0 /\ -S + G - 180 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ U - C + 9 >= 0 /\ -U - C + 20 >= 0 /\ T - C + 9 >= 0 /\ -T - C + 20 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ S - C - 10 >= 0 /\ -S - C + 30 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ U + C - 1 >= 0 /\ -U + C + 10 >= 0 /\ T + C - 1 >= 0 /\ -T + C + 10 >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C - 20 >= 0 /\ -S + C + 20 >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -U + 10 >= 0 /\ T - U >= 0 /\ -T - U + 20 >= 0 /\ B - U + 10 >= 0 /\ -B - U + 20 >= 0 /\ S - U - 10 >= 0 /\ -S - U + 30 >= 0 /\ O - U + 10 >= 0 /\ -O - U + 20 >= 0 /\ N - U + 10 >= 0 /\ -N - U + 20 >= 0 /\ M - U - 40 >= 0 /\ -M - U + 60 >= 0 /\ A - U - 90 >= 0 /\ -A - U + 110 >= 0 /\ U - 1 >= 0 /\ T + U - 2 >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ -B + U + 9 >= 0 /\ S + U - 21 >= 0 /\ -S + U + 19 >= 0 /\ O + U - 1 >= 0 /\ -O + U + 9 >= 0 /\ N + U - 1 >= 0 /\ -N + U + 9 >= 0 /\ M + U - 51 >= 0 /\ -M + U + 49 >= 0 /\ A + U - 101 >= 0 /\ -A + U + 99 >= 0 /\ -T + 10 >= 0 /\ B - T + 10 >= 0 /\ -B - T + 20 >= 0 /\ S - T - 10 >= 0 /\ -S - T + 30 >= 0 /\ O - T + 10 >= 0 /\ -O - T + 20 >= 0 /\ N - T + 10 >= 0 /\ -N - T + 20 >= 0 /\ M - T - 40 >= 0 /\ -M - T + 60 >= 0 /\ A - T - 90 >= 0 /\ -A - T + 110 >= 0 /\ T - 1 >= 0 /\ B + T - 1 >= 0 /\ -B + T + 9 >= 0 /\ S + T - 21 >= 0 /\ -S + T + 19 >= 0 /\ O + T - 1 >= 0 /\ -O + T + 9 >= 0 /\ N + T - 1 >= 0 /\ -N + T + 9 >= 0 /\ M + T - 51 >= 0 /\ -M + T + 49 >= 0 /\ A + T - 101 >= 0 /\ -A + T + 99 >= 0 /\ -B + 10 >= 0 /\ S - B - 10 >= 0 /\ -S - B + 30 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ S + B - 20 >= 0 /\ -S + B + 20 >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -S + 20 >= 0 /\ O - S + 20 >= 0 /\ -O - S + 30 >= 0 /\ N - S + 20 >= 0 /\ -N - S + 30 >= 0 /\ M - S - 30 >= 0 /\ -M - S + 70 >= 0 /\ A - S - 80 >= 0 /\ -A - S + 120 >= 0 /\ S - 20 >= 0 /\ O + S - 20 >= 0 /\ -O + S - 10 >= 0 /\ N + S - 20 >= 0 /\ -N + S - 10 >= 0 /\ M + S - 70 >= 0 /\ -M + S + 30 >= 0 /\ A + S - 120 >= 0 /\ -A + S + 80 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 ] f109(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f125(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ R - I + 10 >= 0 /\ Q - I + 9 >= 0 /\ -Q - I + 20 >= 0 /\ P - I + 9 >= 0 /\ -P - I + 20 >= 0 /\ O - I + 9 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 9 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ R + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I + 10 >= 0 /\ P + I - 1 >= 0 /\ -P + I + 10 >= 0 /\ O + I - 1 >= 0 /\ -O + I + 10 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ R - H + 10 >= 0 /\ Q - H + 9 >= 0 /\ -Q - H + 20 >= 0 /\ P - H + 9 >= 0 /\ -P - H + 20 >= 0 /\ O - H + 9 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 9 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ R + H >= 0 /\ Q + H - 1 >= 0 /\ -Q + H + 10 >= 0 /\ P + H - 1 >= 0 /\ -P + H + 10 >= 0 /\ O + H - 1 >= 0 /\ -O + H + 10 >= 0 /\ N + H - 1 >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ R - G + 200 >= 0 /\ Q - G + 199 >= 0 /\ -Q - G + 210 >= 0 /\ P - G + 199 >= 0 /\ -P - G + 210 >= 0 /\ O - G + 199 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 199 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ R + G - 200 >= 0 /\ Q + G - 201 >= 0 /\ -Q + G - 190 >= 0 /\ P + G - 201 >= 0 /\ -P + G - 190 >= 0 /\ O + G - 201 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 201 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ R - C + 10 >= 0 /\ Q - C + 9 >= 0 /\ -Q - C + 20 >= 0 /\ P - C + 9 >= 0 /\ -P - C + 20 >= 0 /\ O - C + 9 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 9 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ R + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C + 10 >= 0 /\ P + C - 1 >= 0 /\ -P + C + 10 >= 0 /\ O + C - 1 >= 0 /\ -O + C + 10 >= 0 /\ N + C - 1 >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ R - B + 10 >= 0 /\ Q - B + 9 >= 0 /\ -Q - B + 20 >= 0 /\ P - B + 9 >= 0 /\ -P - B + 20 >= 0 /\ O - B + 9 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 9 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ R + B >= 0 /\ Q + B - 1 >= 0 /\ -Q + B + 10 >= 0 /\ P + B - 1 >= 0 /\ -P + B + 10 >= 0 /\ O + B - 1 >= 0 /\ -O + B + 10 >= 0 /\ N + B - 1 >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ R >= 0 /\ Q + R - 1 >= 0 /\ -Q + R + 10 >= 0 /\ P + R - 1 >= 0 /\ -P + R + 10 >= 0 /\ O + R - 1 >= 0 /\ -O + R + 10 >= 0 /\ N + R - 1 >= 0 /\ -N + R + 10 >= 0 /\ M + R - 50 >= 0 /\ -M + R + 50 >= 0 /\ A + R - 100 >= 0 /\ -A + R + 100 >= 0 /\ -Q + 10 >= 0 /\ P - Q >= 0 /\ -P - Q + 20 >= 0 /\ O - Q + 9 >= 0 /\ -O - Q + 20 >= 0 /\ N - Q + 9 >= 0 /\ -N - Q + 20 >= 0 /\ M - Q - 40 >= 0 /\ -M - Q + 60 >= 0 /\ A - Q - 90 >= 0 /\ -A - Q + 110 >= 0 /\ Q - 1 >= 0 /\ P + Q - 2 >= 0 /\ -P + Q >= 0 /\ O + Q - 2 >= 0 /\ -O + Q + 9 >= 0 /\ N + Q - 2 >= 0 /\ -N + Q + 9 >= 0 /\ M + Q - 51 >= 0 /\ -M + Q + 49 >= 0 /\ A + Q - 101 >= 0 /\ -A + Q + 99 >= 0 /\ -P + 10 >= 0 /\ O - P + 9 >= 0 /\ -O - P + 20 >= 0 /\ N - P + 9 >= 0 /\ -N - P + 20 >= 0 /\ M - P - 40 >= 0 /\ -M - P + 60 >= 0 /\ A - P - 90 >= 0 /\ -A - P + 110 >= 0 /\ P - 1 >= 0 /\ O + P - 2 >= 0 /\ -O + P + 9 >= 0 /\ N + P - 2 >= 0 /\ -N + P + 9 >= 0 /\ M + P - 51 >= 0 /\ -M + P + 49 >= 0 /\ A + P - 101 >= 0 /\ -A + P + 99 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O - 1 >= 0 /\ N + O - 2 >= 0 /\ -N + O >= 0 /\ M + O - 51 >= 0 /\ -M + O + 49 >= 0 /\ A + O - 101 >= 0 /\ -A + O + 99 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N - 1 >= 0 /\ M + N - 51 >= 0 /\ -M + N + 49 >= 0 /\ A + N - 101 >= 0 /\ -A + N + 99 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ R >= M ] f109(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f109(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R + 1, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ R - I + 10 >= 0 /\ Q - I + 9 >= 0 /\ -Q - I + 20 >= 0 /\ P - I + 9 >= 0 /\ -P - I + 20 >= 0 /\ O - I + 9 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 9 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ R + I >= 0 /\ Q + I - 1 >= 0 /\ -Q + I + 10 >= 0 /\ P + I - 1 >= 0 /\ -P + I + 10 >= 0 /\ O + I - 1 >= 0 /\ -O + I + 10 >= 0 /\ N + I - 1 >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ R - H + 10 >= 0 /\ Q - H + 9 >= 0 /\ -Q - H + 20 >= 0 /\ P - H + 9 >= 0 /\ -P - H + 20 >= 0 /\ O - H + 9 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 9 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ R + H >= 0 /\ Q + H - 1 >= 0 /\ -Q + H + 10 >= 0 /\ P + H - 1 >= 0 /\ -P + H + 10 >= 0 /\ O + H - 1 >= 0 /\ -O + H + 10 >= 0 /\ N + H - 1 >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ R - G + 200 >= 0 /\ Q - G + 199 >= 0 /\ -Q - G + 210 >= 0 /\ P - G + 199 >= 0 /\ -P - G + 210 >= 0 /\ O - G + 199 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 199 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ R + G - 200 >= 0 /\ Q + G - 201 >= 0 /\ -Q + G - 190 >= 0 /\ P + G - 201 >= 0 /\ -P + G - 190 >= 0 /\ O + G - 201 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 201 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ R - C + 10 >= 0 /\ Q - C + 9 >= 0 /\ -Q - C + 20 >= 0 /\ P - C + 9 >= 0 /\ -P - C + 20 >= 0 /\ O - C + 9 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 9 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ R + C >= 0 /\ Q + C - 1 >= 0 /\ -Q + C + 10 >= 0 /\ P + C - 1 >= 0 /\ -P + C + 10 >= 0 /\ O + C - 1 >= 0 /\ -O + C + 10 >= 0 /\ N + C - 1 >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -B + 10 >= 0 /\ R - B + 10 >= 0 /\ Q - B + 9 >= 0 /\ -Q - B + 20 >= 0 /\ P - B + 9 >= 0 /\ -P - B + 20 >= 0 /\ O - B + 9 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 9 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ R + B >= 0 /\ Q + B - 1 >= 0 /\ -Q + B + 10 >= 0 /\ P + B - 1 >= 0 /\ -P + B + 10 >= 0 /\ O + B - 1 >= 0 /\ -O + B + 10 >= 0 /\ N + B - 1 >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ R >= 0 /\ Q + R - 1 >= 0 /\ -Q + R + 10 >= 0 /\ P + R - 1 >= 0 /\ -P + R + 10 >= 0 /\ O + R - 1 >= 0 /\ -O + R + 10 >= 0 /\ N + R - 1 >= 0 /\ -N + R + 10 >= 0 /\ M + R - 50 >= 0 /\ -M + R + 50 >= 0 /\ A + R - 100 >= 0 /\ -A + R + 100 >= 0 /\ -Q + 10 >= 0 /\ P - Q >= 0 /\ -P - Q + 20 >= 0 /\ O - Q + 9 >= 0 /\ -O - Q + 20 >= 0 /\ N - Q + 9 >= 0 /\ -N - Q + 20 >= 0 /\ M - Q - 40 >= 0 /\ -M - Q + 60 >= 0 /\ A - Q - 90 >= 0 /\ -A - Q + 110 >= 0 /\ Q - 1 >= 0 /\ P + Q - 2 >= 0 /\ -P + Q >= 0 /\ O + Q - 2 >= 0 /\ -O + Q + 9 >= 0 /\ N + Q - 2 >= 0 /\ -N + Q + 9 >= 0 /\ M + Q - 51 >= 0 /\ -M + Q + 49 >= 0 /\ A + Q - 101 >= 0 /\ -A + Q + 99 >= 0 /\ -P + 10 >= 0 /\ O - P + 9 >= 0 /\ -O - P + 20 >= 0 /\ N - P + 9 >= 0 /\ -N - P + 20 >= 0 /\ M - P - 40 >= 0 /\ -M - P + 60 >= 0 /\ A - P - 90 >= 0 /\ -A - P + 110 >= 0 /\ P - 1 >= 0 /\ O + P - 2 >= 0 /\ -O + P + 9 >= 0 /\ N + P - 2 >= 0 /\ -N + P + 9 >= 0 /\ M + P - 51 >= 0 /\ -M + P + 49 >= 0 /\ A + P - 101 >= 0 /\ -A + P + 99 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O - 1 >= 0 /\ N + O - 2 >= 0 /\ -N + O >= 0 /\ M + O - 51 >= 0 /\ -M + O + 49 >= 0 /\ A + O - 101 >= 0 /\ -A + O + 99 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N - 1 >= 0 /\ M + N - 51 >= 0 /\ -M + N + 49 >= 0 /\ A + N - 101 >= 0 /\ -A + N + 99 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ M >= R + 1 ] f146(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f149(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, V, 0)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ V - I + 10 >= 0 /\ -V - I + 20 >= 0 /\ U - I + 9 >= 0 /\ -U - I + 20 >= 0 /\ T - I + 9 >= 0 /\ -T - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ S - I - 10 >= 0 /\ -S - I + 30 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ V + I >= 0 /\ -V + I + 10 >= 0 /\ U + I - 1 >= 0 /\ -U + I + 10 >= 0 /\ T + I - 1 >= 0 /\ -T + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ S + I - 20 >= 0 /\ -S + I + 20 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ V - H + 10 >= 0 /\ -V - H + 20 >= 0 /\ U - H + 9 >= 0 /\ -U - H + 20 >= 0 /\ T - H + 9 >= 0 /\ -T - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ S - H - 10 >= 0 /\ -S - H + 30 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ V + H >= 0 /\ -V + H + 10 >= 0 /\ U + H - 1 >= 0 /\ -U + H + 10 >= 0 /\ T + H - 1 >= 0 /\ -T + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ S + H - 20 >= 0 /\ -S + H + 20 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ V - G + 200 >= 0 /\ -V - G + 210 >= 0 /\ U - G + 199 >= 0 /\ -U - G + 210 >= 0 /\ T - G + 199 >= 0 /\ -T - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ S - G + 180 >= 0 /\ -S - G + 220 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ V + G - 200 >= 0 /\ -V + G - 190 >= 0 /\ U + G - 201 >= 0 /\ -U + G - 190 >= 0 /\ T + G - 201 >= 0 /\ -T + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ S + G - 220 >= 0 /\ -S + G - 180 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ V - C + 10 >= 0 /\ -V - C + 20 >= 0 /\ U - C + 9 >= 0 /\ -U - C + 20 >= 0 /\ T - C + 9 >= 0 /\ -T - C + 20 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ S - C - 10 >= 0 /\ -S - C + 30 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ V + C >= 0 /\ -V + C + 10 >= 0 /\ U + C - 1 >= 0 /\ -U + C + 10 >= 0 /\ T + C - 1 >= 0 /\ -T + C + 10 >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C - 20 >= 0 /\ -S + C + 20 >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -V + 10 >= 0 /\ U - V + 9 >= 0 /\ -U - V + 20 >= 0 /\ T - V + 9 >= 0 /\ -T - V + 20 >= 0 /\ B - V + 10 >= 0 /\ -B - V + 20 >= 0 /\ S - V - 10 >= 0 /\ -S - V + 30 >= 0 /\ O - V + 10 >= 0 /\ -O - V + 20 >= 0 /\ N - V + 10 >= 0 /\ -N - V + 20 >= 0 /\ M - V - 40 >= 0 /\ -M - V + 60 >= 0 /\ A - V - 90 >= 0 /\ -A - V + 110 >= 0 /\ V >= 0 /\ U + V - 1 >= 0 /\ -U + V + 10 >= 0 /\ T + V - 1 >= 0 /\ -T + V + 10 >= 0 /\ B + V >= 0 /\ -B + V + 10 >= 0 /\ S + V - 20 >= 0 /\ -S + V + 20 >= 0 /\ O + V >= 0 /\ -O + V + 10 >= 0 /\ N + V >= 0 /\ -N + V + 10 >= 0 /\ M + V - 50 >= 0 /\ -M + V + 50 >= 0 /\ A + V - 100 >= 0 /\ -A + V + 100 >= 0 /\ -U + 10 >= 0 /\ T - U >= 0 /\ -T - U + 20 >= 0 /\ B - U + 10 >= 0 /\ -B - U + 20 >= 0 /\ S - U - 10 >= 0 /\ -S - U + 30 >= 0 /\ O - U + 10 >= 0 /\ -O - U + 20 >= 0 /\ N - U + 10 >= 0 /\ -N - U + 20 >= 0 /\ M - U - 40 >= 0 /\ -M - U + 60 >= 0 /\ A - U - 90 >= 0 /\ -A - U + 110 >= 0 /\ U - 1 >= 0 /\ T + U - 2 >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ -B + U + 9 >= 0 /\ S + U - 21 >= 0 /\ -S + U + 19 >= 0 /\ O + U - 1 >= 0 /\ -O + U + 9 >= 0 /\ N + U - 1 >= 0 /\ -N + U + 9 >= 0 /\ M + U - 51 >= 0 /\ -M + U + 49 >= 0 /\ A + U - 101 >= 0 /\ -A + U + 99 >= 0 /\ -T + 10 >= 0 /\ B - T + 10 >= 0 /\ -B - T + 20 >= 0 /\ S - T - 10 >= 0 /\ -S - T + 30 >= 0 /\ O - T + 10 >= 0 /\ -O - T + 20 >= 0 /\ N - T + 10 >= 0 /\ -N - T + 20 >= 0 /\ M - T - 40 >= 0 /\ -M - T + 60 >= 0 /\ A - T - 90 >= 0 /\ -A - T + 110 >= 0 /\ T - 1 >= 0 /\ B + T - 1 >= 0 /\ -B + T + 9 >= 0 /\ S + T - 21 >= 0 /\ -S + T + 19 >= 0 /\ O + T - 1 >= 0 /\ -O + T + 9 >= 0 /\ N + T - 1 >= 0 /\ -N + T + 9 >= 0 /\ M + T - 51 >= 0 /\ -M + T + 49 >= 0 /\ A + T - 101 >= 0 /\ -A + T + 99 >= 0 /\ -B + 10 >= 0 /\ S - B - 10 >= 0 /\ -S - B + 30 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ S + B - 20 >= 0 /\ -S + B + 20 >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -S + 20 >= 0 /\ O - S + 20 >= 0 /\ -O - S + 30 >= 0 /\ N - S + 20 >= 0 /\ -N - S + 30 >= 0 /\ M - S - 30 >= 0 /\ -M - S + 70 >= 0 /\ A - S - 80 >= 0 /\ -A - S + 120 >= 0 /\ S - 20 >= 0 /\ O + S - 20 >= 0 /\ -O + S - 10 >= 0 /\ N + S - 20 >= 0 /\ -N + S - 10 >= 0 /\ M + S - 70 >= 0 /\ -M + S + 30 >= 0 /\ A + S - 120 >= 0 /\ -A + S + 80 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ V >= 1 ] f146(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f166(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, 0, 0, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ V - I + 10 >= 0 /\ -V - I + 20 >= 0 /\ U - I + 9 >= 0 /\ -U - I + 20 >= 0 /\ T - I + 9 >= 0 /\ -T - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ S - I - 10 >= 0 /\ -S - I + 30 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ V + I >= 0 /\ -V + I + 10 >= 0 /\ U + I - 1 >= 0 /\ -U + I + 10 >= 0 /\ T + I - 1 >= 0 /\ -T + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ S + I - 20 >= 0 /\ -S + I + 20 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ V - H + 10 >= 0 /\ -V - H + 20 >= 0 /\ U - H + 9 >= 0 /\ -U - H + 20 >= 0 /\ T - H + 9 >= 0 /\ -T - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ S - H - 10 >= 0 /\ -S - H + 30 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ V + H >= 0 /\ -V + H + 10 >= 0 /\ U + H - 1 >= 0 /\ -U + H + 10 >= 0 /\ T + H - 1 >= 0 /\ -T + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ S + H - 20 >= 0 /\ -S + H + 20 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ V - G + 200 >= 0 /\ -V - G + 210 >= 0 /\ U - G + 199 >= 0 /\ -U - G + 210 >= 0 /\ T - G + 199 >= 0 /\ -T - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ S - G + 180 >= 0 /\ -S - G + 220 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ V + G - 200 >= 0 /\ -V + G - 190 >= 0 /\ U + G - 201 >= 0 /\ -U + G - 190 >= 0 /\ T + G - 201 >= 0 /\ -T + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ S + G - 220 >= 0 /\ -S + G - 180 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ V - C + 10 >= 0 /\ -V - C + 20 >= 0 /\ U - C + 9 >= 0 /\ -U - C + 20 >= 0 /\ T - C + 9 >= 0 /\ -T - C + 20 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ S - C - 10 >= 0 /\ -S - C + 30 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ V + C >= 0 /\ -V + C + 10 >= 0 /\ U + C - 1 >= 0 /\ -U + C + 10 >= 0 /\ T + C - 1 >= 0 /\ -T + C + 10 >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C - 20 >= 0 /\ -S + C + 20 >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ -V + 10 >= 0 /\ U - V + 9 >= 0 /\ -U - V + 20 >= 0 /\ T - V + 9 >= 0 /\ -T - V + 20 >= 0 /\ B - V + 10 >= 0 /\ -B - V + 20 >= 0 /\ S - V - 10 >= 0 /\ -S - V + 30 >= 0 /\ O - V + 10 >= 0 /\ -O - V + 20 >= 0 /\ N - V + 10 >= 0 /\ -N - V + 20 >= 0 /\ M - V - 40 >= 0 /\ -M - V + 60 >= 0 /\ A - V - 90 >= 0 /\ -A - V + 110 >= 0 /\ V >= 0 /\ U + V - 1 >= 0 /\ -U + V + 10 >= 0 /\ T + V - 1 >= 0 /\ -T + V + 10 >= 0 /\ B + V >= 0 /\ -B + V + 10 >= 0 /\ S + V - 20 >= 0 /\ -S + V + 20 >= 0 /\ O + V >= 0 /\ -O + V + 10 >= 0 /\ N + V >= 0 /\ -N + V + 10 >= 0 /\ M + V - 50 >= 0 /\ -M + V + 50 >= 0 /\ A + V - 100 >= 0 /\ -A + V + 100 >= 0 /\ -U + 10 >= 0 /\ T - U >= 0 /\ -T - U + 20 >= 0 /\ B - U + 10 >= 0 /\ -B - U + 20 >= 0 /\ S - U - 10 >= 0 /\ -S - U + 30 >= 0 /\ O - U + 10 >= 0 /\ -O - U + 20 >= 0 /\ N - U + 10 >= 0 /\ -N - U + 20 >= 0 /\ M - U - 40 >= 0 /\ -M - U + 60 >= 0 /\ A - U - 90 >= 0 /\ -A - U + 110 >= 0 /\ U - 1 >= 0 /\ T + U - 2 >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ -B + U + 9 >= 0 /\ S + U - 21 >= 0 /\ -S + U + 19 >= 0 /\ O + U - 1 >= 0 /\ -O + U + 9 >= 0 /\ N + U - 1 >= 0 /\ -N + U + 9 >= 0 /\ M + U - 51 >= 0 /\ -M + U + 49 >= 0 /\ A + U - 101 >= 0 /\ -A + U + 99 >= 0 /\ -T + 10 >= 0 /\ B - T + 10 >= 0 /\ -B - T + 20 >= 0 /\ S - T - 10 >= 0 /\ -S - T + 30 >= 0 /\ O - T + 10 >= 0 /\ -O - T + 20 >= 0 /\ N - T + 10 >= 0 /\ -N - T + 20 >= 0 /\ M - T - 40 >= 0 /\ -M - T + 60 >= 0 /\ A - T - 90 >= 0 /\ -A - T + 110 >= 0 /\ T - 1 >= 0 /\ B + T - 1 >= 0 /\ -B + T + 9 >= 0 /\ S + T - 21 >= 0 /\ -S + T + 19 >= 0 /\ O + T - 1 >= 0 /\ -O + T + 9 >= 0 /\ N + T - 1 >= 0 /\ -N + T + 9 >= 0 /\ M + T - 51 >= 0 /\ -M + T + 49 >= 0 /\ A + T - 101 >= 0 /\ -A + T + 99 >= 0 /\ -B + 10 >= 0 /\ S - B - 10 >= 0 /\ -S - B + 30 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ S + B - 20 >= 0 /\ -S + B + 20 >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -S + 20 >= 0 /\ O - S + 20 >= 0 /\ -O - S + 30 >= 0 /\ N - S + 20 >= 0 /\ -N - S + 30 >= 0 /\ M - S - 30 >= 0 /\ -M - S + 70 >= 0 /\ A - S - 80 >= 0 /\ -A - S + 120 >= 0 /\ S - 20 >= 0 /\ O + S - 20 >= 0 /\ -O + S - 10 >= 0 /\ N + S - 20 >= 0 /\ -N + S - 10 >= 0 /\ M + S - 70 >= 0 /\ -M + S + 30 >= 0 /\ A + S - 120 >= 0 /\ -A + S + 80 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ V = 0 ] f149(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f166(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ X - I + 10 >= 0 /\ W - I + 9 >= 0 /\ -W - I + 20 >= 0 /\ V - I + 9 >= 0 /\ -V - I + 20 >= 0 /\ U - I + 9 >= 0 /\ -U - I + 20 >= 0 /\ T - I + 9 >= 0 /\ -T - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ S - I - 10 >= 0 /\ -S - I + 30 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ X + I >= 0 /\ W + I - 1 >= 0 /\ -W + I + 10 >= 0 /\ V + I - 1 >= 0 /\ -V + I + 10 >= 0 /\ U + I - 1 >= 0 /\ -U + I + 10 >= 0 /\ T + I - 1 >= 0 /\ -T + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ S + I - 20 >= 0 /\ -S + I + 20 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ X - H + 10 >= 0 /\ W - H + 9 >= 0 /\ -W - H + 20 >= 0 /\ V - H + 9 >= 0 /\ -V - H + 20 >= 0 /\ U - H + 9 >= 0 /\ -U - H + 20 >= 0 /\ T - H + 9 >= 0 /\ -T - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ S - H - 10 >= 0 /\ -S - H + 30 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ X + H >= 0 /\ W + H - 1 >= 0 /\ -W + H + 10 >= 0 /\ V + H - 1 >= 0 /\ -V + H + 10 >= 0 /\ U + H - 1 >= 0 /\ -U + H + 10 >= 0 /\ T + H - 1 >= 0 /\ -T + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ S + H - 20 >= 0 /\ -S + H + 20 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ X - G + 200 >= 0 /\ W - G + 199 >= 0 /\ -W - G + 210 >= 0 /\ V - G + 199 >= 0 /\ -V - G + 210 >= 0 /\ U - G + 199 >= 0 /\ -U - G + 210 >= 0 /\ T - G + 199 >= 0 /\ -T - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ S - G + 180 >= 0 /\ -S - G + 220 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ X + G - 200 >= 0 /\ W + G - 201 >= 0 /\ -W + G - 190 >= 0 /\ V + G - 201 >= 0 /\ -V + G - 190 >= 0 /\ U + G - 201 >= 0 /\ -U + G - 190 >= 0 /\ T + G - 201 >= 0 /\ -T + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ S + G - 220 >= 0 /\ -S + G - 180 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ X - C + 10 >= 0 /\ W - C + 9 >= 0 /\ -W - C + 20 >= 0 /\ V - C + 9 >= 0 /\ -V - C + 20 >= 0 /\ U - C + 9 >= 0 /\ -U - C + 20 >= 0 /\ T - C + 9 >= 0 /\ -T - C + 20 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ S - C - 10 >= 0 /\ -S - C + 30 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ X + C >= 0 /\ W + C - 1 >= 0 /\ -W + C + 10 >= 0 /\ V + C - 1 >= 0 /\ -V + C + 10 >= 0 /\ U + C - 1 >= 0 /\ -U + C + 10 >= 0 /\ T + C - 1 >= 0 /\ -T + C + 10 >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C - 20 >= 0 /\ -S + C + 20 >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ X >= 0 /\ W + X - 1 >= 0 /\ -W + X + 10 >= 0 /\ V + X - 1 >= 0 /\ -V + X + 10 >= 0 /\ U + X - 1 >= 0 /\ -U + X + 10 >= 0 /\ T + X - 1 >= 0 /\ -T + X + 10 >= 0 /\ B + X >= 0 /\ -B + X + 10 >= 0 /\ S + X - 20 >= 0 /\ -S + X + 20 >= 0 /\ O + X >= 0 /\ -O + X + 10 >= 0 /\ N + X >= 0 /\ -N + X + 10 >= 0 /\ M + X - 50 >= 0 /\ -M + X + 50 >= 0 /\ A + X - 100 >= 0 /\ -A + X + 100 >= 0 /\ -W + 10 >= 0 /\ V - W >= 0 /\ -V - W + 20 >= 0 /\ U - W + 9 >= 0 /\ -U - W + 20 >= 0 /\ T - W + 9 >= 0 /\ -T - W + 20 >= 0 /\ B - W + 10 >= 0 /\ -B - W + 20 >= 0 /\ S - W - 10 >= 0 /\ -S - W + 30 >= 0 /\ O - W + 10 >= 0 /\ -O - W + 20 >= 0 /\ N - W + 10 >= 0 /\ -N - W + 20 >= 0 /\ M - W - 40 >= 0 /\ -M - W + 60 >= 0 /\ A - W - 90 >= 0 /\ -A - W + 110 >= 0 /\ W - 1 >= 0 /\ V + W - 2 >= 0 /\ -V + W >= 0 /\ U + W - 2 >= 0 /\ -U + W + 9 >= 0 /\ T + W - 2 >= 0 /\ -T + W + 9 >= 0 /\ B + W - 1 >= 0 /\ -B + W + 9 >= 0 /\ S + W - 21 >= 0 /\ -S + W + 19 >= 0 /\ O + W - 1 >= 0 /\ -O + W + 9 >= 0 /\ N + W - 1 >= 0 /\ -N + W + 9 >= 0 /\ M + W - 51 >= 0 /\ -M + W + 49 >= 0 /\ A + W - 101 >= 0 /\ -A + W + 99 >= 0 /\ -V + 10 >= 0 /\ U - V + 9 >= 0 /\ -U - V + 20 >= 0 /\ T - V + 9 >= 0 /\ -T - V + 20 >= 0 /\ B - V + 10 >= 0 /\ -B - V + 20 >= 0 /\ S - V - 10 >= 0 /\ -S - V + 30 >= 0 /\ O - V + 10 >= 0 /\ -O - V + 20 >= 0 /\ N - V + 10 >= 0 /\ -N - V + 20 >= 0 /\ M - V - 40 >= 0 /\ -M - V + 60 >= 0 /\ A - V - 90 >= 0 /\ -A - V + 110 >= 0 /\ V - 1 >= 0 /\ U + V - 2 >= 0 /\ -U + V + 9 >= 0 /\ T + V - 2 >= 0 /\ -T + V + 9 >= 0 /\ B + V - 1 >= 0 /\ -B + V + 9 >= 0 /\ S + V - 21 >= 0 /\ -S + V + 19 >= 0 /\ O + V - 1 >= 0 /\ -O + V + 9 >= 0 /\ N + V - 1 >= 0 /\ -N + V + 9 >= 0 /\ M + V - 51 >= 0 /\ -M + V + 49 >= 0 /\ A + V - 101 >= 0 /\ -A + V + 99 >= 0 /\ -U + 10 >= 0 /\ T - U >= 0 /\ -T - U + 20 >= 0 /\ B - U + 10 >= 0 /\ -B - U + 20 >= 0 /\ S - U - 10 >= 0 /\ -S - U + 30 >= 0 /\ O - U + 10 >= 0 /\ -O - U + 20 >= 0 /\ N - U + 10 >= 0 /\ -N - U + 20 >= 0 /\ M - U - 40 >= 0 /\ -M - U + 60 >= 0 /\ A - U - 90 >= 0 /\ -A - U + 110 >= 0 /\ U - 1 >= 0 /\ T + U - 2 >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ -B + U + 9 >= 0 /\ S + U - 21 >= 0 /\ -S + U + 19 >= 0 /\ O + U - 1 >= 0 /\ -O + U + 9 >= 0 /\ N + U - 1 >= 0 /\ -N + U + 9 >= 0 /\ M + U - 51 >= 0 /\ -M + U + 49 >= 0 /\ A + U - 101 >= 0 /\ -A + U + 99 >= 0 /\ -T + 10 >= 0 /\ B - T + 10 >= 0 /\ -B - T + 20 >= 0 /\ S - T - 10 >= 0 /\ -S - T + 30 >= 0 /\ O - T + 10 >= 0 /\ -O - T + 20 >= 0 /\ N - T + 10 >= 0 /\ -N - T + 20 >= 0 /\ M - T - 40 >= 0 /\ -M - T + 60 >= 0 /\ A - T - 90 >= 0 /\ -A - T + 110 >= 0 /\ T - 1 >= 0 /\ B + T - 1 >= 0 /\ -B + T + 9 >= 0 /\ S + T - 21 >= 0 /\ -S + T + 19 >= 0 /\ O + T - 1 >= 0 /\ -O + T + 9 >= 0 /\ N + T - 1 >= 0 /\ -N + T + 9 >= 0 /\ M + T - 51 >= 0 /\ -M + T + 49 >= 0 /\ A + T - 101 >= 0 /\ -A + T + 99 >= 0 /\ -B + 10 >= 0 /\ S - B - 10 >= 0 /\ -S - B + 30 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ S + B - 20 >= 0 /\ -S + B + 20 >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -S + 20 >= 0 /\ O - S + 20 >= 0 /\ -O - S + 30 >= 0 /\ N - S + 20 >= 0 /\ -N - S + 30 >= 0 /\ M - S - 30 >= 0 /\ -M - S + 70 >= 0 /\ A - S - 80 >= 0 /\ -A - S + 120 >= 0 /\ S - 20 >= 0 /\ O + S - 20 >= 0 /\ -O + S - 10 >= 0 /\ N + S - 20 >= 0 /\ -N + S - 10 >= 0 /\ M + S - 70 >= 0 /\ -M + S + 30 >= 0 /\ A + S - 120 >= 0 /\ -A + S + 80 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ X >= S ] f149(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f149(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X + 1)) [ -I + 10 >= 0 /\ H - I >= 0 /\ -H - I + 20 >= 0 /\ G - I - 190 >= 0 /\ -G - I + 210 >= 0 /\ C - I + 10 >= 0 /\ -C - I + 20 >= 0 /\ X - I + 10 >= 0 /\ W - I + 9 >= 0 /\ -W - I + 20 >= 0 /\ V - I + 9 >= 0 /\ -V - I + 20 >= 0 /\ U - I + 9 >= 0 /\ -U - I + 20 >= 0 /\ T - I + 9 >= 0 /\ -T - I + 20 >= 0 /\ B - I + 10 >= 0 /\ -B - I + 20 >= 0 /\ S - I - 10 >= 0 /\ -S - I + 30 >= 0 /\ O - I + 10 >= 0 /\ -O - I + 20 >= 0 /\ N - I + 10 >= 0 /\ -N - I + 20 >= 0 /\ M - I - 40 >= 0 /\ -M - I + 60 >= 0 /\ A - I - 90 >= 0 /\ -A - I + 110 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 200 >= 0 /\ -G + I + 200 >= 0 /\ C + I >= 0 /\ -C + I + 10 >= 0 /\ X + I >= 0 /\ W + I - 1 >= 0 /\ -W + I + 10 >= 0 /\ V + I - 1 >= 0 /\ -V + I + 10 >= 0 /\ U + I - 1 >= 0 /\ -U + I + 10 >= 0 /\ T + I - 1 >= 0 /\ -T + I + 10 >= 0 /\ B + I >= 0 /\ -B + I + 10 >= 0 /\ S + I - 20 >= 0 /\ -S + I + 20 >= 0 /\ O + I >= 0 /\ -O + I + 10 >= 0 /\ N + I >= 0 /\ -N + I + 10 >= 0 /\ M + I - 50 >= 0 /\ -M + I + 50 >= 0 /\ A + I - 100 >= 0 /\ -A + I + 100 >= 0 /\ -H + 10 >= 0 /\ G - H - 190 >= 0 /\ -G - H + 210 >= 0 /\ C - H + 10 >= 0 /\ -C - H + 20 >= 0 /\ X - H + 10 >= 0 /\ W - H + 9 >= 0 /\ -W - H + 20 >= 0 /\ V - H + 9 >= 0 /\ -V - H + 20 >= 0 /\ U - H + 9 >= 0 /\ -U - H + 20 >= 0 /\ T - H + 9 >= 0 /\ -T - H + 20 >= 0 /\ B - H + 10 >= 0 /\ -B - H + 20 >= 0 /\ S - H - 10 >= 0 /\ -S - H + 30 >= 0 /\ O - H + 10 >= 0 /\ -O - H + 20 >= 0 /\ N - H + 10 >= 0 /\ -N - H + 20 >= 0 /\ M - H - 40 >= 0 /\ -M - H + 60 >= 0 /\ A - H - 90 >= 0 /\ -A - H + 110 >= 0 /\ H >= 0 /\ G + H - 200 >= 0 /\ -G + H + 200 >= 0 /\ C + H >= 0 /\ -C + H + 10 >= 0 /\ X + H >= 0 /\ W + H - 1 >= 0 /\ -W + H + 10 >= 0 /\ V + H - 1 >= 0 /\ -V + H + 10 >= 0 /\ U + H - 1 >= 0 /\ -U + H + 10 >= 0 /\ T + H - 1 >= 0 /\ -T + H + 10 >= 0 /\ B + H >= 0 /\ -B + H + 10 >= 0 /\ S + H - 20 >= 0 /\ -S + H + 20 >= 0 /\ O + H >= 0 /\ -O + H + 10 >= 0 /\ N + H >= 0 /\ -N + H + 10 >= 0 /\ M + H - 50 >= 0 /\ -M + H + 50 >= 0 /\ A + H - 100 >= 0 /\ -A + H + 100 >= 0 /\ -G + 200 >= 0 /\ C - G + 200 >= 0 /\ -C - G + 210 >= 0 /\ X - G + 200 >= 0 /\ W - G + 199 >= 0 /\ -W - G + 210 >= 0 /\ V - G + 199 >= 0 /\ -V - G + 210 >= 0 /\ U - G + 199 >= 0 /\ -U - G + 210 >= 0 /\ T - G + 199 >= 0 /\ -T - G + 210 >= 0 /\ B - G + 200 >= 0 /\ -B - G + 210 >= 0 /\ S - G + 180 >= 0 /\ -S - G + 220 >= 0 /\ O - G + 200 >= 0 /\ -O - G + 210 >= 0 /\ N - G + 200 >= 0 /\ -N - G + 210 >= 0 /\ M - G + 150 >= 0 /\ -M - G + 250 >= 0 /\ A - G + 100 >= 0 /\ -A - G + 300 >= 0 /\ G - 200 >= 0 /\ C + G - 200 >= 0 /\ -C + G - 190 >= 0 /\ X + G - 200 >= 0 /\ W + G - 201 >= 0 /\ -W + G - 190 >= 0 /\ V + G - 201 >= 0 /\ -V + G - 190 >= 0 /\ U + G - 201 >= 0 /\ -U + G - 190 >= 0 /\ T + G - 201 >= 0 /\ -T + G - 190 >= 0 /\ B + G - 200 >= 0 /\ -B + G - 190 >= 0 /\ S + G - 220 >= 0 /\ -S + G - 180 >= 0 /\ O + G - 200 >= 0 /\ -O + G - 190 >= 0 /\ N + G - 200 >= 0 /\ -N + G - 190 >= 0 /\ M + G - 250 >= 0 /\ -M + G - 150 >= 0 /\ A + G - 300 >= 0 /\ -A + G - 100 >= 0 /\ -C + 10 >= 0 /\ X - C + 10 >= 0 /\ W - C + 9 >= 0 /\ -W - C + 20 >= 0 /\ V - C + 9 >= 0 /\ -V - C + 20 >= 0 /\ U - C + 9 >= 0 /\ -U - C + 20 >= 0 /\ T - C + 9 >= 0 /\ -T - C + 20 >= 0 /\ B - C >= 0 /\ -B - C + 20 >= 0 /\ S - C - 10 >= 0 /\ -S - C + 30 >= 0 /\ O - C + 10 >= 0 /\ -O - C + 20 >= 0 /\ N - C + 10 >= 0 /\ -N - C + 20 >= 0 /\ M - C - 40 >= 0 /\ -M - C + 60 >= 0 /\ A - C - 90 >= 0 /\ -A - C + 110 >= 0 /\ C >= 0 /\ X + C >= 0 /\ W + C - 1 >= 0 /\ -W + C + 10 >= 0 /\ V + C - 1 >= 0 /\ -V + C + 10 >= 0 /\ U + C - 1 >= 0 /\ -U + C + 10 >= 0 /\ T + C - 1 >= 0 /\ -T + C + 10 >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C - 20 >= 0 /\ -S + C + 20 >= 0 /\ O + C >= 0 /\ -O + C + 10 >= 0 /\ N + C >= 0 /\ -N + C + 10 >= 0 /\ M + C - 50 >= 0 /\ -M + C + 50 >= 0 /\ A + C - 100 >= 0 /\ -A + C + 100 >= 0 /\ X >= 0 /\ W + X - 1 >= 0 /\ -W + X + 10 >= 0 /\ V + X - 1 >= 0 /\ -V + X + 10 >= 0 /\ U + X - 1 >= 0 /\ -U + X + 10 >= 0 /\ T + X - 1 >= 0 /\ -T + X + 10 >= 0 /\ B + X >= 0 /\ -B + X + 10 >= 0 /\ S + X - 20 >= 0 /\ -S + X + 20 >= 0 /\ O + X >= 0 /\ -O + X + 10 >= 0 /\ N + X >= 0 /\ -N + X + 10 >= 0 /\ M + X - 50 >= 0 /\ -M + X + 50 >= 0 /\ A + X - 100 >= 0 /\ -A + X + 100 >= 0 /\ -W + 10 >= 0 /\ V - W >= 0 /\ -V - W + 20 >= 0 /\ U - W + 9 >= 0 /\ -U - W + 20 >= 0 /\ T - W + 9 >= 0 /\ -T - W + 20 >= 0 /\ B - W + 10 >= 0 /\ -B - W + 20 >= 0 /\ S - W - 10 >= 0 /\ -S - W + 30 >= 0 /\ O - W + 10 >= 0 /\ -O - W + 20 >= 0 /\ N - W + 10 >= 0 /\ -N - W + 20 >= 0 /\ M - W - 40 >= 0 /\ -M - W + 60 >= 0 /\ A - W - 90 >= 0 /\ -A - W + 110 >= 0 /\ W - 1 >= 0 /\ V + W - 2 >= 0 /\ -V + W >= 0 /\ U + W - 2 >= 0 /\ -U + W + 9 >= 0 /\ T + W - 2 >= 0 /\ -T + W + 9 >= 0 /\ B + W - 1 >= 0 /\ -B + W + 9 >= 0 /\ S + W - 21 >= 0 /\ -S + W + 19 >= 0 /\ O + W - 1 >= 0 /\ -O + W + 9 >= 0 /\ N + W - 1 >= 0 /\ -N + W + 9 >= 0 /\ M + W - 51 >= 0 /\ -M + W + 49 >= 0 /\ A + W - 101 >= 0 /\ -A + W + 99 >= 0 /\ -V + 10 >= 0 /\ U - V + 9 >= 0 /\ -U - V + 20 >= 0 /\ T - V + 9 >= 0 /\ -T - V + 20 >= 0 /\ B - V + 10 >= 0 /\ -B - V + 20 >= 0 /\ S - V - 10 >= 0 /\ -S - V + 30 >= 0 /\ O - V + 10 >= 0 /\ -O - V + 20 >= 0 /\ N - V + 10 >= 0 /\ -N - V + 20 >= 0 /\ M - V - 40 >= 0 /\ -M - V + 60 >= 0 /\ A - V - 90 >= 0 /\ -A - V + 110 >= 0 /\ V - 1 >= 0 /\ U + V - 2 >= 0 /\ -U + V + 9 >= 0 /\ T + V - 2 >= 0 /\ -T + V + 9 >= 0 /\ B + V - 1 >= 0 /\ -B + V + 9 >= 0 /\ S + V - 21 >= 0 /\ -S + V + 19 >= 0 /\ O + V - 1 >= 0 /\ -O + V + 9 >= 0 /\ N + V - 1 >= 0 /\ -N + V + 9 >= 0 /\ M + V - 51 >= 0 /\ -M + V + 49 >= 0 /\ A + V - 101 >= 0 /\ -A + V + 99 >= 0 /\ -U + 10 >= 0 /\ T - U >= 0 /\ -T - U + 20 >= 0 /\ B - U + 10 >= 0 /\ -B - U + 20 >= 0 /\ S - U - 10 >= 0 /\ -S - U + 30 >= 0 /\ O - U + 10 >= 0 /\ -O - U + 20 >= 0 /\ N - U + 10 >= 0 /\ -N - U + 20 >= 0 /\ M - U - 40 >= 0 /\ -M - U + 60 >= 0 /\ A - U - 90 >= 0 /\ -A - U + 110 >= 0 /\ U - 1 >= 0 /\ T + U - 2 >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ -B + U + 9 >= 0 /\ S + U - 21 >= 0 /\ -S + U + 19 >= 0 /\ O + U - 1 >= 0 /\ -O + U + 9 >= 0 /\ N + U - 1 >= 0 /\ -N + U + 9 >= 0 /\ M + U - 51 >= 0 /\ -M + U + 49 >= 0 /\ A + U - 101 >= 0 /\ -A + U + 99 >= 0 /\ -T + 10 >= 0 /\ B - T + 10 >= 0 /\ -B - T + 20 >= 0 /\ S - T - 10 >= 0 /\ -S - T + 30 >= 0 /\ O - T + 10 >= 0 /\ -O - T + 20 >= 0 /\ N - T + 10 >= 0 /\ -N - T + 20 >= 0 /\ M - T - 40 >= 0 /\ -M - T + 60 >= 0 /\ A - T - 90 >= 0 /\ -A - T + 110 >= 0 /\ T - 1 >= 0 /\ B + T - 1 >= 0 /\ -B + T + 9 >= 0 /\ S + T - 21 >= 0 /\ -S + T + 19 >= 0 /\ O + T - 1 >= 0 /\ -O + T + 9 >= 0 /\ N + T - 1 >= 0 /\ -N + T + 9 >= 0 /\ M + T - 51 >= 0 /\ -M + T + 49 >= 0 /\ A + T - 101 >= 0 /\ -A + T + 99 >= 0 /\ -B + 10 >= 0 /\ S - B - 10 >= 0 /\ -S - B + 30 >= 0 /\ O - B + 10 >= 0 /\ -O - B + 20 >= 0 /\ N - B + 10 >= 0 /\ -N - B + 20 >= 0 /\ M - B - 40 >= 0 /\ -M - B + 60 >= 0 /\ A - B - 90 >= 0 /\ -A - B + 110 >= 0 /\ B >= 0 /\ S + B - 20 >= 0 /\ -S + B + 20 >= 0 /\ O + B >= 0 /\ -O + B + 10 >= 0 /\ N + B >= 0 /\ -N + B + 10 >= 0 /\ M + B - 50 >= 0 /\ -M + B + 50 >= 0 /\ A + B - 100 >= 0 /\ -A + B + 100 >= 0 /\ -S + 20 >= 0 /\ O - S + 20 >= 0 /\ -O - S + 30 >= 0 /\ N - S + 20 >= 0 /\ -N - S + 30 >= 0 /\ M - S - 30 >= 0 /\ -M - S + 70 >= 0 /\ A - S - 80 >= 0 /\ -A - S + 120 >= 0 /\ S - 20 >= 0 /\ O + S - 20 >= 0 /\ -O + S - 10 >= 0 /\ N + S - 20 >= 0 /\ -N + S - 10 >= 0 /\ M + S - 70 >= 0 /\ -M + S + 30 >= 0 /\ A + S - 120 >= 0 /\ -A + S + 80 >= 0 /\ -O + 10 >= 0 /\ N - O >= 0 /\ -N - O + 20 >= 0 /\ M - O - 40 >= 0 /\ -M - O + 60 >= 0 /\ A - O - 90 >= 0 /\ -A - O + 110 >= 0 /\ O >= 0 /\ N + O >= 0 /\ -N + O >= 0 /\ M + O - 50 >= 0 /\ -M + O + 50 >= 0 /\ A + O - 100 >= 0 /\ -A + O + 100 >= 0 /\ -N + 10 >= 0 /\ M - N - 40 >= 0 /\ -M - N + 60 >= 0 /\ A - N - 90 >= 0 /\ -A - N + 110 >= 0 /\ N >= 0 /\ M + N - 50 >= 0 /\ -M + N + 50 >= 0 /\ A + N - 100 >= 0 /\ -A + N + 100 >= 0 /\ -M + 50 >= 0 /\ A - M - 50 >= 0 /\ -A - M + 150 >= 0 /\ M - 50 >= 0 /\ A + M - 150 >= 0 /\ -A + M + 50 >= 0 /\ -A + 100 >= 0 /\ A - 100 >= 0 /\ S >= X + 1 ] )