(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G H I J K L M N O P Q R) (RULES f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R) -> Com_1(f18(3, 3, 0, 3, E, F, G, H, I, J, K, L, M, N, O, P, Q, R)) f18(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R) -> Com_1(f25(A, B, C, D, D, D, -3, 4, 0, J, K, L, M, N, O, P, Q, R)) [ -D + 3 >= 0 /\ C - D + 3 >= 0 /\ -C - D + 3 >= 0 /\ B - D >= 0 /\ -B - D + 6 >= 0 /\ A - D >= 0 /\ -A - D + 6 >= 0 /\ D - 3 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 3 >= 0 /\ B + D - 6 >= 0 /\ -B + D >= 0 /\ A + D - 6 >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B - C - 3 >= 0 /\ -B - C + 3 >= 0 /\ A - C - 3 >= 0 /\ -A - C + 3 >= 0 /\ C >= 0 /\ B + C - 3 >= 0 /\ -B + C + 3 >= 0 /\ A + C - 3 >= 0 /\ -A + C + 3 >= 0 /\ -B + 3 >= 0 /\ A - B >= 0 /\ -A - B + 6 >= 0 /\ B - 3 >= 0 /\ A + B - 6 >= 0 /\ -A + B >= 0 /\ -A + 3 >= 0 /\ A - 3 >= 0 ] f25(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R) -> Com_1(f33(A, B, C, D, E, F, G, H, I, J, H, L, M, N, O, P, Q, R)) [ -I >= 0 /\ H - I - 4 >= 0 /\ -H - I + 4 >= 0 /\ G - I + 3 >= 0 /\ -G - I - 3 >= 0 /\ F - I - 3 >= 0 /\ -F - I + 3 >= 0 /\ E - I - 3 >= 0 /\ -E - I + 3 >= 0 /\ D - I - 3 >= 0 /\ -D - I + 3 >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ B - I - 3 >= 0 /\ -B - I + 3 >= 0 /\ A - I - 3 >= 0 /\ -A - I + 3 >= 0 /\ I >= 0 /\ H + I - 4 >= 0 /\ -H + I + 4 >= 0 /\ G + I + 3 >= 0 /\ -G + I - 3 >= 0 /\ F + I - 3 >= 0 /\ -F + I + 3 >= 0 /\ E + I - 3 >= 0 /\ -E + I + 3 >= 0 /\ D + I - 3 >= 0 /\ -D + I + 3 >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ B + I - 3 >= 0 /\ -B + I + 3 >= 0 /\ A + I - 3 >= 0 /\ -A + I + 3 >= 0 /\ -H + 4 >= 0 /\ G - H + 7 >= 0 /\ -G - H + 1 >= 0 /\ F - H + 1 >= 0 /\ -F - H + 7 >= 0 /\ E - H + 1 >= 0 /\ -E - H + 7 >= 0 /\ D - H + 1 >= 0 /\ -D - H + 7 >= 0 /\ C - H + 4 >= 0 /\ -C - H + 4 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 7 >= 0 /\ A - H + 1 >= 0 /\ -A - H + 7 >= 0 /\ H - 4 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 7 >= 0 /\ F + H - 7 >= 0 /\ -F + H - 1 >= 0 /\ E + H - 7 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 7 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 4 >= 0 /\ -C + H - 4 >= 0 /\ B + H - 7 >= 0 /\ -B + H - 1 >= 0 /\ A + H - 7 >= 0 /\ -A + H - 1 >= 0 /\ -G - 3 >= 0 /\ F - G - 6 >= 0 /\ -F - G >= 0 /\ E - G - 6 >= 0 /\ -E - G >= 0 /\ D - G - 6 >= 0 /\ -D - G >= 0 /\ C - G - 3 >= 0 /\ -C - G - 3 >= 0 /\ B - G - 6 >= 0 /\ -B - G >= 0 /\ A - G - 6 >= 0 /\ -A - G >= 0 /\ G + 3 >= 0 /\ F + G >= 0 /\ -F + G + 6 >= 0 /\ E + G >= 0 /\ -E + G + 6 >= 0 /\ D + G >= 0 /\ -D + G + 6 >= 0 /\ C + G + 3 >= 0 /\ -C + G + 3 >= 0 /\ B + G >= 0 /\ -B + G + 6 >= 0 /\ A + G >= 0 /\ -A + G + 6 >= 0 /\ -F + 3 >= 0 /\ E - F >= 0 /\ -E - F + 6 >= 0 /\ D - F >= 0 /\ -D - F + 6 >= 0 /\ C - F + 3 >= 0 /\ -C - F + 3 >= 0 /\ B - F >= 0 /\ -B - F + 6 >= 0 /\ A - F >= 0 /\ -A - F + 6 >= 0 /\ F - 3 >= 0 /\ E + F - 6 >= 0 /\ -E + F >= 0 /\ D + F - 6 >= 0 /\ -D + F >= 0 /\ C + F - 3 >= 0 /\ -C + F - 3 >= 0 /\ B + F - 6 >= 0 /\ -B + F >= 0 /\ A + F - 6 >= 0 /\ -A + F >= 0 /\ -E + 3 >= 0 /\ D - E >= 0 /\ -D - E + 6 >= 0 /\ C - E + 3 >= 0 /\ -C - E + 3 >= 0 /\ B - E >= 0 /\ -B - E + 6 >= 0 /\ A - E >= 0 /\ -A - E + 6 >= 0 /\ E - 3 >= 0 /\ D + E - 6 >= 0 /\ -D + E >= 0 /\ C + E - 3 >= 0 /\ -C + E - 3 >= 0 /\ B + E - 6 >= 0 /\ -B + E >= 0 /\ A + E - 6 >= 0 /\ -A + E >= 0 /\ -D + 3 >= 0 /\ C - D + 3 >= 0 /\ -C - D + 3 >= 0 /\ B - D >= 0 /\ -B - D + 6 >= 0 /\ A - D >= 0 /\ -A - D + 6 >= 0 /\ D - 3 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 3 >= 0 /\ B + D - 6 >= 0 /\ -B + D >= 0 /\ A + D - 6 >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B - C - 3 >= 0 /\ -B - C + 3 >= 0 /\ A - C - 3 >= 0 /\ -A - C + 3 >= 0 /\ C >= 0 /\ B + C - 3 >= 0 /\ -B + C + 3 >= 0 /\ A + C - 3 >= 0 /\ -A + C + 3 >= 0 /\ -B + 3 >= 0 /\ A - B >= 0 /\ -A - B + 6 >= 0 /\ B - 3 >= 0 /\ A + B - 6 >= 0 /\ -A + B >= 0 /\ -A + 3 >= 0 /\ A - 3 >= 0 /\ I >= G + 1 ] f33(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R) -> Com_1(f40(A, B, C, D, E, F, G, H, I, K, K, K, 3, -6, 0, P, Q, R)) [ -I >= 0 /\ H - I - 4 >= 0 /\ -H - I + 4 >= 0 /\ G - I + 3 >= 0 /\ -G - I - 3 >= 0 /\ F - I - 3 >= 0 /\ -F - I + 3 >= 0 /\ E - I - 3 >= 0 /\ -E - I + 3 >= 0 /\ D - I - 3 >= 0 /\ -D - I + 3 >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ B - I - 3 >= 0 /\ -B - I + 3 >= 0 /\ K - I - 4 >= 0 /\ -K - I + 4 >= 0 /\ A - I - 3 >= 0 /\ -A - I + 3 >= 0 /\ I >= 0 /\ H + I - 4 >= 0 /\ -H + I + 4 >= 0 /\ G + I + 3 >= 0 /\ -G + I - 3 >= 0 /\ F + I - 3 >= 0 /\ -F + I + 3 >= 0 /\ E + I - 3 >= 0 /\ -E + I + 3 >= 0 /\ D + I - 3 >= 0 /\ -D + I + 3 >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ B + I - 3 >= 0 /\ -B + I + 3 >= 0 /\ K + I - 4 >= 0 /\ -K + I + 4 >= 0 /\ A + I - 3 >= 0 /\ -A + I + 3 >= 0 /\ -H + 4 >= 0 /\ G - H + 7 >= 0 /\ -G - H + 1 >= 0 /\ F - H + 1 >= 0 /\ -F - H + 7 >= 0 /\ E - H + 1 >= 0 /\ -E - H + 7 >= 0 /\ D - H + 1 >= 0 /\ -D - H + 7 >= 0 /\ C - H + 4 >= 0 /\ -C - H + 4 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 7 >= 0 /\ K - H >= 0 /\ -K - H + 8 >= 0 /\ A - H + 1 >= 0 /\ -A - H + 7 >= 0 /\ H - 4 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 7 >= 0 /\ F + H - 7 >= 0 /\ -F + H - 1 >= 0 /\ E + H - 7 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 7 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 4 >= 0 /\ -C + H - 4 >= 0 /\ B + H - 7 >= 0 /\ -B + H - 1 >= 0 /\ K + H - 8 >= 0 /\ -K + H >= 0 /\ A + H - 7 >= 0 /\ -A + H - 1 >= 0 /\ -G - 3 >= 0 /\ F - G - 6 >= 0 /\ -F - G >= 0 /\ E - G - 6 >= 0 /\ -E - G >= 0 /\ D - G - 6 >= 0 /\ -D - G >= 0 /\ C - G - 3 >= 0 /\ -C - G - 3 >= 0 /\ B - G - 6 >= 0 /\ -B - G >= 0 /\ K - G - 7 >= 0 /\ -K - G + 1 >= 0 /\ A - G - 6 >= 0 /\ -A - G >= 0 /\ G + 3 >= 0 /\ F + G >= 0 /\ -F + G + 6 >= 0 /\ E + G >= 0 /\ -E + G + 6 >= 0 /\ D + G >= 0 /\ -D + G + 6 >= 0 /\ C + G + 3 >= 0 /\ -C + G + 3 >= 0 /\ B + G >= 0 /\ -B + G + 6 >= 0 /\ K + G - 1 >= 0 /\ -K + G + 7 >= 0 /\ A + G >= 0 /\ -A + G + 6 >= 0 /\ -F + 3 >= 0 /\ E - F >= 0 /\ -E - F + 6 >= 0 /\ D - F >= 0 /\ -D - F + 6 >= 0 /\ C - F + 3 >= 0 /\ -C - F + 3 >= 0 /\ B - F >= 0 /\ -B - F + 6 >= 0 /\ K - F - 1 >= 0 /\ -K - F + 7 >= 0 /\ A - F >= 0 /\ -A - F + 6 >= 0 /\ F - 3 >= 0 /\ E + F - 6 >= 0 /\ -E + F >= 0 /\ D + F - 6 >= 0 /\ -D + F >= 0 /\ C + F - 3 >= 0 /\ -C + F - 3 >= 0 /\ B + F - 6 >= 0 /\ -B + F >= 0 /\ K + F - 7 >= 0 /\ -K + F + 1 >= 0 /\ A + F - 6 >= 0 /\ -A + F >= 0 /\ -E + 3 >= 0 /\ D - E >= 0 /\ -D - E + 6 >= 0 /\ C - E + 3 >= 0 /\ -C - E + 3 >= 0 /\ B - E >= 0 /\ -B - E + 6 >= 0 /\ K - E - 1 >= 0 /\ -K - E + 7 >= 0 /\ A - E >= 0 /\ -A - E + 6 >= 0 /\ E - 3 >= 0 /\ D + E - 6 >= 0 /\ -D + E >= 0 /\ C + E - 3 >= 0 /\ -C + E - 3 >= 0 /\ B + E - 6 >= 0 /\ -B + E >= 0 /\ K + E - 7 >= 0 /\ -K + E + 1 >= 0 /\ A + E - 6 >= 0 /\ -A + E >= 0 /\ -D + 3 >= 0 /\ C - D + 3 >= 0 /\ -C - D + 3 >= 0 /\ B - D >= 0 /\ -B - D + 6 >= 0 /\ K - D - 1 >= 0 /\ -K - D + 7 >= 0 /\ A - D >= 0 /\ -A - D + 6 >= 0 /\ D - 3 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 3 >= 0 /\ B + D - 6 >= 0 /\ -B + D >= 0 /\ K + D - 7 >= 0 /\ -K + D + 1 >= 0 /\ A + D - 6 >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B - C - 3 >= 0 /\ -B - C + 3 >= 0 /\ K - C - 4 >= 0 /\ -K - C + 4 >= 0 /\ A - C - 3 >= 0 /\ -A - C + 3 >= 0 /\ C >= 0 /\ B + C - 3 >= 0 /\ -B + C + 3 >= 0 /\ K + C - 4 >= 0 /\ -K + C + 4 >= 0 /\ A + C - 3 >= 0 /\ -A + C + 3 >= 0 /\ -B + 3 >= 0 /\ K - B - 1 >= 0 /\ -K - B + 7 >= 0 /\ A - B >= 0 /\ -A - B + 6 >= 0 /\ B - 3 >= 0 /\ K + B - 7 >= 0 /\ -K + B + 1 >= 0 /\ A + B - 6 >= 0 /\ -A + B >= 0 /\ -K + 4 >= 0 /\ A - K + 1 >= 0 /\ -A - K + 7 >= 0 /\ K - 4 >= 0 /\ A + K - 7 >= 0 /\ -A + K - 1 >= 0 /\ -A + 3 >= 0 /\ A - 3 >= 0 ] f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R) -> Com_1(f40(A, B, C, D, E, F, G, H, I, J, K, L, M, N + M, O, P, Q, R)) [ -I >= 0 /\ H - I - 4 >= 0 /\ -H - I + 4 >= 0 /\ G - I + 3 >= 0 /\ -G - I - 3 >= 0 /\ F - I - 3 >= 0 /\ -F - I + 3 >= 0 /\ E - I - 3 >= 0 /\ -E - I + 3 >= 0 /\ D - I - 3 >= 0 /\ -D - I + 3 >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ B - I - 3 >= 0 /\ -B - I + 3 >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I + 6 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 3 >= 0 /\ L - I - 4 >= 0 /\ -L - I + 4 >= 0 /\ K - I - 4 >= 0 /\ -K - I + 4 >= 0 /\ J - I - 4 >= 0 /\ -J - I + 4 >= 0 /\ A - I - 3 >= 0 /\ -A - I + 3 >= 0 /\ I >= 0 /\ H + I - 4 >= 0 /\ -H + I + 4 >= 0 /\ G + I + 3 >= 0 /\ -G + I - 3 >= 0 /\ F + I - 3 >= 0 /\ -F + I + 3 >= 0 /\ E + I - 3 >= 0 /\ -E + I + 3 >= 0 /\ D + I - 3 >= 0 /\ -D + I + 3 >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ B + I - 3 >= 0 /\ -B + I + 3 >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I + 6 >= 0 /\ M + I - 3 >= 0 /\ -M + I + 3 >= 0 /\ L + I - 4 >= 0 /\ -L + I + 4 >= 0 /\ K + I - 4 >= 0 /\ -K + I + 4 >= 0 /\ J + I - 4 >= 0 /\ -J + I + 4 >= 0 /\ A + I - 3 >= 0 /\ -A + I + 3 >= 0 /\ -H + 4 >= 0 /\ G - H + 7 >= 0 /\ -G - H + 1 >= 0 /\ F - H + 1 >= 0 /\ -F - H + 7 >= 0 /\ E - H + 1 >= 0 /\ -E - H + 7 >= 0 /\ D - H + 1 >= 0 /\ -D - H + 7 >= 0 /\ C - H + 4 >= 0 /\ -C - H + 4 >= 0 /\ B - H + 1 >= 0 /\ -B - H + 7 >= 0 /\ O - H + 4 >= 0 /\ -O - H + 4 >= 0 /\ N - H + 10 >= 0 /\ M - H + 1 >= 0 /\ -M - H + 7 >= 0 /\ L - H >= 0 /\ -L - H + 8 >= 0 /\ K - H >= 0 /\ -K - H + 8 >= 0 /\ J - H >= 0 /\ -J - H + 8 >= 0 /\ A - H + 1 >= 0 /\ -A - H + 7 >= 0 /\ H - 4 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 7 >= 0 /\ F + H - 7 >= 0 /\ -F + H - 1 >= 0 /\ E + H - 7 >= 0 /\ -E + H - 1 >= 0 /\ D + H - 7 >= 0 /\ -D + H - 1 >= 0 /\ C + H - 4 >= 0 /\ -C + H - 4 >= 0 /\ B + H - 7 >= 0 /\ -B + H - 1 >= 0 /\ O + H - 4 >= 0 /\ -O + H - 4 >= 0 /\ N + H + 2 >= 0 /\ M + H - 7 >= 0 /\ -M + H - 1 >= 0 /\ L + H - 8 >= 0 /\ -L + H >= 0 /\ K + H - 8 >= 0 /\ -K + H >= 0 /\ J + H - 8 >= 0 /\ -J + H >= 0 /\ A + H - 7 >= 0 /\ -A + H - 1 >= 0 /\ -G - 3 >= 0 /\ F - G - 6 >= 0 /\ -F - G >= 0 /\ E - G - 6 >= 0 /\ -E - G >= 0 /\ D - G - 6 >= 0 /\ -D - G >= 0 /\ C - G - 3 >= 0 /\ -C - G - 3 >= 0 /\ B - G - 6 >= 0 /\ -B - G >= 0 /\ O - G - 3 >= 0 /\ -O - G - 3 >= 0 /\ N - G + 3 >= 0 /\ M - G - 6 >= 0 /\ -M - G >= 0 /\ L - G - 7 >= 0 /\ -L - G + 1 >= 0 /\ K - G - 7 >= 0 /\ -K - G + 1 >= 0 /\ J - G - 7 >= 0 /\ -J - G + 1 >= 0 /\ A - G - 6 >= 0 /\ -A - G >= 0 /\ G + 3 >= 0 /\ F + G >= 0 /\ -F + G + 6 >= 0 /\ E + G >= 0 /\ -E + G + 6 >= 0 /\ D + G >= 0 /\ -D + G + 6 >= 0 /\ C + G + 3 >= 0 /\ -C + G + 3 >= 0 /\ B + G >= 0 /\ -B + G + 6 >= 0 /\ O + G + 3 >= 0 /\ -O + G + 3 >= 0 /\ N + G + 9 >= 0 /\ M + G >= 0 /\ -M + G + 6 >= 0 /\ L + G - 1 >= 0 /\ -L + G + 7 >= 0 /\ K + G - 1 >= 0 /\ -K + G + 7 >= 0 /\ J + G - 1 >= 0 /\ -J + G + 7 >= 0 /\ A + G >= 0 /\ -A + G + 6 >= 0 /\ -F + 3 >= 0 /\ E - F >= 0 /\ -E - F + 6 >= 0 /\ D - F >= 0 /\ -D - F + 6 >= 0 /\ C - F + 3 >= 0 /\ -C - F + 3 >= 0 /\ B - F >= 0 /\ -B - F + 6 >= 0 /\ O - F + 3 >= 0 /\ -O - F + 3 >= 0 /\ N - F + 9 >= 0 /\ M - F >= 0 /\ -M - F + 6 >= 0 /\ L - F - 1 >= 0 /\ -L - F + 7 >= 0 /\ K - F - 1 >= 0 /\ -K - F + 7 >= 0 /\ J - F - 1 >= 0 /\ -J - F + 7 >= 0 /\ A - F >= 0 /\ -A - F + 6 >= 0 /\ F - 3 >= 0 /\ E + F - 6 >= 0 /\ -E + F >= 0 /\ D + F - 6 >= 0 /\ -D + F >= 0 /\ C + F - 3 >= 0 /\ -C + F - 3 >= 0 /\ B + F - 6 >= 0 /\ -B + F >= 0 /\ O + F - 3 >= 0 /\ -O + F - 3 >= 0 /\ N + F + 3 >= 0 /\ M + F - 6 >= 0 /\ -M + F >= 0 /\ L + F - 7 >= 0 /\ -L + F + 1 >= 0 /\ K + F - 7 >= 0 /\ -K + F + 1 >= 0 /\ J + F - 7 >= 0 /\ -J + F + 1 >= 0 /\ A + F - 6 >= 0 /\ -A + F >= 0 /\ -E + 3 >= 0 /\ D - E >= 0 /\ -D - E + 6 >= 0 /\ C - E + 3 >= 0 /\ -C - E + 3 >= 0 /\ B - E >= 0 /\ -B - E + 6 >= 0 /\ O - E + 3 >= 0 /\ -O - E + 3 >= 0 /\ N - E + 9 >= 0 /\ M - E >= 0 /\ -M - E + 6 >= 0 /\ L - E - 1 >= 0 /\ -L - E + 7 >= 0 /\ K - E - 1 >= 0 /\ -K - E + 7 >= 0 /\ J - E - 1 >= 0 /\ -J - E + 7 >= 0 /\ A - E >= 0 /\ -A - E + 6 >= 0 /\ E - 3 >= 0 /\ D + E - 6 >= 0 /\ -D + E >= 0 /\ C + E - 3 >= 0 /\ -C + E - 3 >= 0 /\ B + E - 6 >= 0 /\ -B + E >= 0 /\ O + E - 3 >= 0 /\ -O + E - 3 >= 0 /\ N + E + 3 >= 0 /\ M + E - 6 >= 0 /\ -M + E >= 0 /\ L + E - 7 >= 0 /\ -L + E + 1 >= 0 /\ K + E - 7 >= 0 /\ -K + E + 1 >= 0 /\ J + E - 7 >= 0 /\ -J + E + 1 >= 0 /\ A + E - 6 >= 0 /\ -A + E >= 0 /\ -D + 3 >= 0 /\ C - D + 3 >= 0 /\ -C - D + 3 >= 0 /\ B - D >= 0 /\ -B - D + 6 >= 0 /\ O - D + 3 >= 0 /\ -O - D + 3 >= 0 /\ N - D + 9 >= 0 /\ M - D >= 0 /\ -M - D + 6 >= 0 /\ L - D - 1 >= 0 /\ -L - D + 7 >= 0 /\ K - D - 1 >= 0 /\ -K - D + 7 >= 0 /\ J - D - 1 >= 0 /\ -J - D + 7 >= 0 /\ A - D >= 0 /\ -A - D + 6 >= 0 /\ D - 3 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 3 >= 0 /\ B + D - 6 >= 0 /\ -B + D >= 0 /\ O + D - 3 >= 0 /\ -O + D - 3 >= 0 /\ N + D + 3 >= 0 /\ M + D - 6 >= 0 /\ -M + D >= 0 /\ L + D - 7 >= 0 /\ -L + D + 1 >= 0 /\ K + D - 7 >= 0 /\ -K + D + 1 >= 0 /\ J + D - 7 >= 0 /\ -J + D + 1 >= 0 /\ A + D - 6 >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B - C - 3 >= 0 /\ -B - C + 3 >= 0 /\ O - C >= 0 /\ -O - C >= 0 /\ N - C + 6 >= 0 /\ M - C - 3 >= 0 /\ -M - C + 3 >= 0 /\ L - C - 4 >= 0 /\ -L - C + 4 >= 0 /\ K - C - 4 >= 0 /\ -K - C + 4 >= 0 /\ J - C - 4 >= 0 /\ -J - C + 4 >= 0 /\ A - C - 3 >= 0 /\ -A - C + 3 >= 0 /\ C >= 0 /\ B + C - 3 >= 0 /\ -B + C + 3 >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C + 6 >= 0 /\ M + C - 3 >= 0 /\ -M + C + 3 >= 0 /\ L + C - 4 >= 0 /\ -L + C + 4 >= 0 /\ K + C - 4 >= 0 /\ -K + C + 4 >= 0 /\ J + C - 4 >= 0 /\ -J + C + 4 >= 0 /\ A + C - 3 >= 0 /\ -A + C + 3 >= 0 /\ -B + 3 >= 0 /\ O - B + 3 >= 0 /\ -O - B + 3 >= 0 /\ N - B + 9 >= 0 /\ M - B >= 0 /\ -M - B + 6 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ K - B - 1 >= 0 /\ -K - B + 7 >= 0 /\ J - B - 1 >= 0 /\ -J - B + 7 >= 0 /\ A - B >= 0 /\ -A - B + 6 >= 0 /\ B - 3 >= 0 /\ O + B - 3 >= 0 /\ -O + B - 3 >= 0 /\ N + B + 3 >= 0 /\ M + B - 6 >= 0 /\ -M + B >= 0 /\ L + B - 7 >= 0 /\ -L + B + 1 >= 0 /\ K + B - 7 >= 0 /\ -K + B + 1 >= 0 /\ J + B - 7 >= 0 /\ -J + B + 1 >= 0 /\ A + B - 6 >= 0 /\ -A + B >= 0 /\ -O >= 0 /\ N - O + 6 >= 0 /\ M - O - 3 >= 0 /\ -M - O + 3 >= 0 /\ L - O - 4 >= 0 /\ -L - O + 4 >= 0 /\ K - O - 4 >= 0 /\ -K - O + 4 >= 0 /\ J - O - 4 >= 0 /\ -J - O + 4 >= 0 /\ A - O - 3 >= 0 /\ -A - O + 3 >= 0 /\ O >= 0 /\ N + O + 6 >= 0 /\ M + O - 3 >= 0 /\ -M + O + 3 >= 0 /\ L + O - 4 >= 0 /\ -L + O + 4 >= 0 /\ K + O - 4 >= 0 /\ -K + O + 4 >= 0 /\ J + O - 4 >= 0 /\ -J + O + 4 >= 0 /\ A + O - 3 >= 0 /\ -A + O + 3 >= 0 /\ N + 6 >= 0 /\ M + N + 3 >= 0 /\ -M + N + 9 >= 0 /\ L + N + 2 >= 0 /\ -L + N + 10 >= 0 /\ K + N + 2 >= 0 /\ -K + N + 10 >= 0 /\ J + N + 2 >= 0 /\ -J + N + 10 >= 0 /\ A + N + 3 >= 0 /\ -A + N + 9 >= 0 /\ -M + 3 >= 0 /\ L - M - 1 >= 0 /\ -L - M + 7 >= 0 /\ K - M - 1 >= 0 /\ -K - M + 7 >= 0 /\ J - M - 1 >= 0 /\ -J - M + 7 >= 0 /\ A - M >= 0 /\ -A - M + 6 >= 0 /\ M - 3 >= 0 /\ L + M - 7 >= 0 /\ -L + M + 1 >= 0 /\ K + M - 7 >= 0 /\ -K + M + 1 >= 0 /\ J + M - 7 >= 0 /\ -J + M + 1 >= 0 /\ A + M - 6 >= 0 /\ -A + M >= 0 /\ -L + 4 >= 0 /\ K - L >= 0 /\ -K - L + 8 >= 0 /\ J - L >= 0 /\ -J - L + 8 >= 0 /\ A - L + 1 >= 0 /\ -A - L + 7 >= 0 /\ L - 4 >= 0 /\ K + L - 8 >= 0 /\ -K + L >= 0 /\ J + L - 8 >= 0 /\ -J + L >= 0 /\ A + L - 7 >= 0 /\ -A + L - 1 >= 0 /\ -K + 4 >= 0 /\ J - K >= 0 /\ -J - K + 8 >= 0 /\ A - K + 1 >= 0 /\ -A - K + 7 >= 0 /\ K - 4 >= 0 /\ J + K - 8 >= 0 /\ -J + K >= 0 /\ A + K - 7 >= 0 /\ -A + K - 1 >= 0 /\ -J + 4 >= 0 /\ A - J + 1 >= 0 /\ -A - J + 7 >= 0 /\ J - 4 >= 0 /\ A + J - 7 >= 0 /\ -A + J - 1 >= 0 /\ -A + 3 >= 0 /\ A - 3 >= 0 /\ M >= 1 /\ M >= O ] )