(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f999))
(VAR A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1 C1)
(RULES
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f2(0, 0, 0, D + C, E + B - 1, F + A - 1, G + 1, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I >= 0 /\ H - I >= 0 /\ -H - I >= 0 /\ G - I >= 0 /\ F - I >= 0 /\ E - I >= 0 /\ D - I >= 0 /\ -D - I >= 0 /\ C - I >= 0 /\ B1 - I >= 0 /\ -B1 - I >= 0 /\ A1 - I >= 0 /\ -A1 - I >= 0 /\ Z - I >= 0 /\ -Z - I >= 0 /\ Y - I >= 0 /\ -Y - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ W - I >= 0 /\ -W - I >= 0 /\ V - I >= 0 /\ -V - I >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ B - I - 1 >= 0 /\ S - I >= 0 /\ -S - I >= 0 /\ R - I >= 0 /\ -R - I >= 0 /\ Q - I >= 0 /\ -Q - I >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I >= 0 /\ M - I >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ J - I >= 0 /\ A - I - 1 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I >= 0 /\ F + I >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ -D + I >= 0 /\ C + I >= 0 /\ B1 + I >= 0 /\ -B1 + I >= 0 /\ A1 + I >= 0 /\ -A1 + I >= 0 /\ Z + I >= 0 /\ -Z + I >= 0 /\ Y + I >= 0 /\ -Y + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ W + I >= 0 /\ -W + I >= 0 /\ V + I >= 0 /\ -V + I >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ B + I - 1 >= 0 /\ S + I >= 0 /\ -S + I >= 0 /\ R + I >= 0 /\ -R + I >= 0 /\ Q + I >= 0 /\ -Q + I >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I >= 0 /\ M + I >= 0 /\ L + I >= 0 /\ K + I >= 0 /\ J + I >= 0 /\ A + I - 1 >= 0 /\ -H >= 0 /\ G - H >= 0 /\ F - H >= 0 /\ E - H >= 0 /\ D - H >= 0 /\ -D - H >= 0 /\ C - H >= 0 /\ B1 - H >= 0 /\ -B1 - H >= 0 /\ A1 - H >= 0 /\ -A1 - H >= 0 /\ Z - H >= 0 /\ -Z - H >= 0 /\ Y - H >= 0 /\ -Y - H >= 0 /\ X - H >= 0 /\ -X - H >= 0 /\ W - H >= 0 /\ -W - H >= 0 /\ V - H >= 0 /\ -V - H >= 0 /\ U - H >= 0 /\ -U - H >= 0 /\ T - H >= 0 /\ -T - H >= 0 /\ B - H - 1 >= 0 /\ S - H >= 0 /\ -S - H >= 0 /\ R - H >= 0 /\ -R - H >= 0 /\ Q - H >= 0 /\ -Q - H >= 0 /\ P - H >= 0 /\ -P - H >= 0 /\ O - H >= 0 /\ -O - H >= 0 /\ N - H >= 0 /\ M - H >= 0 /\ L - H >= 0 /\ K - H >= 0 /\ J - H >= 0 /\ A - H - 1 >= 0 /\ H >= 0 /\ G + H >= 0 /\ F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H >= 0 /\ B1 + H >= 0 /\ -B1 + H >= 0 /\ A1 + H >= 0 /\ -A1 + H >= 0 /\ Z + H >= 0 /\ -Z + H >= 0 /\ Y + H >= 0 /\ -Y + H >= 0 /\ X + H >= 0 /\ -X + H >= 0 /\ W + H >= 0 /\ -W + H >= 0 /\ V + H >= 0 /\ -V + H >= 0 /\ U + H >= 0 /\ -U + H >= 0 /\ T + H >= 0 /\ -T + H >= 0 /\ B + H - 1 >= 0 /\ S + H >= 0 /\ -S + H >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ Q + H >= 0 /\ -Q + H >= 0 /\ P + H >= 0 /\ -P + H >= 0 /\ O + H >= 0 /\ -O + H >= 0 /\ N + H >= 0 /\ M + H >= 0 /\ L + H >= 0 /\ K + H >= 0 /\ J + H >= 0 /\ A + H - 1 >= 0 /\ G >= 0 /\ F + G >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ -D + G >= 0 /\ C + G >= 0 /\ B1 + G >= 0 /\ -B1 + G >= 0 /\ A1 + G >= 0 /\ -A1 + G >= 0 /\ Z + G >= 0 /\ -Z + G >= 0 /\ Y + G >= 0 /\ -Y + G >= 0 /\ X + G >= 0 /\ -X + G >= 0 /\ W + G >= 0 /\ -W + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ T + G >= 0 /\ -T + G >= 0 /\ B + G - 1 >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ P + G >= 0 /\ -P + G >= 0 /\ O + G >= 0 /\ -O + G >= 0 /\ N + G >= 0 /\ M + G >= 0 /\ L + G >= 0 /\ K + G >= 0 /\ J + G >= 0 /\ A + G - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B1 + F >= 0 /\ -B1 + F >= 0 /\ A1 + F >= 0 /\ -A1 + F >= 0 /\ Z + F >= 0 /\ -Z + F >= 0 /\ Y + F >= 0 /\ -Y + F >= 0 /\ X + F >= 0 /\ -X + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ U + F >= 0 /\ -U + F >= 0 /\ T + F >= 0 /\ -T + F >= 0 /\ B + F - 1 >= 0 /\ S + F >= 0 /\ -S + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ Q + F >= 0 /\ -Q + F >= 0 /\ P + F >= 0 /\ -P + F >= 0 /\ O + F >= 0 /\ -O + F >= 0 /\ N + F >= 0 /\ M + F >= 0 /\ L + F >= 0 /\ K + F >= 0 /\ J + F >= 0 /\ A + F - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ C + E >= 0 /\ B1 + E >= 0 /\ -B1 + E >= 0 /\ A1 + E >= 0 /\ -A1 + E >= 0 /\ Z + E >= 0 /\ -Z + E >= 0 /\ Y + E >= 0 /\ -Y + E >= 0 /\ X + E >= 0 /\ -X + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ V + E >= 0 /\ -V + E >= 0 /\ U + E >= 0 /\ -U + E >= 0 /\ T + E >= 0 /\ -T + E >= 0 /\ B + E - 1 >= 0 /\ S + E >= 0 /\ -S + E >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E >= 0 /\ -Q + E >= 0 /\ P + E >= 0 /\ -P + E >= 0 /\ O + E >= 0 /\ -O + E >= 0 /\ N + E >= 0 /\ M + E >= 0 /\ L + E >= 0 /\ K + E >= 0 /\ J + E >= 0 /\ A + E - 1 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ B1 - D >= 0 /\ -B1 - D >= 0 /\ A1 - D >= 0 /\ -A1 - D >= 0 /\ Z - D >= 0 /\ -Z - D >= 0 /\ Y - D >= 0 /\ -Y - D >= 0 /\ X - D >= 0 /\ -X - D >= 0 /\ W - D >= 0 /\ -W - D >= 0 /\ V - D >= 0 /\ -V - D >= 0 /\ U - D >= 0 /\ -U - D >= 0 /\ T - D >= 0 /\ -T - D >= 0 /\ B - D - 1 >= 0 /\ S - D >= 0 /\ -S - D >= 0 /\ R - D >= 0 /\ -R - D >= 0 /\ Q - D >= 0 /\ -Q - D >= 0 /\ P - D >= 0 /\ -P - D >= 0 /\ O - D >= 0 /\ -O - D >= 0 /\ N - D >= 0 /\ M - D >= 0 /\ L - D >= 0 /\ K - D >= 0 /\ J - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B1 + D >= 0 /\ -B1 + D >= 0 /\ A1 + D >= 0 /\ -A1 + D >= 0 /\ Z + D >= 0 /\ -Z + D >= 0 /\ Y + D >= 0 /\ -Y + D >= 0 /\ X + D >= 0 /\ -X + D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ V + D >= 0 /\ -V + D >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ T + D >= 0 /\ -T + D >= 0 /\ B + D - 1 >= 0 /\ S + D >= 0 /\ -S + D >= 0 /\ R + D >= 0 /\ -R + D >= 0 /\ Q + D >= 0 /\ -Q + D >= 0 /\ P + D >= 0 /\ -P + D >= 0 /\ O + D >= 0 /\ -O + D >= 0 /\ N + D >= 0 /\ M + D >= 0 /\ L + D >= 0 /\ K + D >= 0 /\ J + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B1 + C >= 0 /\ -B1 + C >= 0 /\ A1 + C >= 0 /\ -A1 + C >= 0 /\ Z + C >= 0 /\ -Z + C >= 0 /\ Y + C >= 0 /\ -Y + C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ V + C >= 0 /\ -V + C >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ B + C - 1 >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ P + C >= 0 /\ -P + C >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C >= 0 /\ M + C >= 0 /\ L + C >= 0 /\ K + C >= 0 /\ J + C >= 0 /\ A + C - 1 >= 0 /\ -B1 >= 0 /\ A1 - B1 >= 0 /\ -A1 - B1 >= 0 /\ Z - B1 >= 0 /\ -Z - B1 >= 0 /\ Y - B1 >= 0 /\ -Y - B1 >= 0 /\ X - B1 >= 0 /\ -X - B1 >= 0 /\ W - B1 >= 0 /\ -W - B1 >= 0 /\ V - B1 >= 0 /\ -V - B1 >= 0 /\ U - B1 >= 0 /\ -U - B1 >= 0 /\ T - B1 >= 0 /\ -T - B1 >= 0 /\ B - B1 - 1 >= 0 /\ S - B1 >= 0 /\ -S - B1 >= 0 /\ R - B1 >= 0 /\ -R - B1 >= 0 /\ Q - B1 >= 0 /\ -Q - B1 >= 0 /\ P - B1 >= 0 /\ -P - B1 >= 0 /\ O - B1 >= 0 /\ -O - B1 >= 0 /\ N - B1 >= 0 /\ M - B1 >= 0 /\ L - B1 >= 0 /\ K - B1 >= 0 /\ J - B1 >= 0 /\ A - B1 - 1 >= 0 /\ B1 >= 0 /\ A1 + B1 >= 0 /\ -A1 + B1 >= 0 /\ Z + B1 >= 0 /\ -Z + B1 >= 0 /\ Y + B1 >= 0 /\ -Y + B1 >= 0 /\ X + B1 >= 0 /\ -X + B1 >= 0 /\ W + B1 >= 0 /\ -W + B1 >= 0 /\ V + B1 >= 0 /\ -V + B1 >= 0 /\ U + B1 >= 0 /\ -U + B1 >= 0 /\ T + B1 >= 0 /\ -T + B1 >= 0 /\ B + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 >= 0 /\ R + B1 >= 0 /\ -R + B1 >= 0 /\ Q + B1 >= 0 /\ -Q + B1 >= 0 /\ P + B1 >= 0 /\ -P + B1 >= 0 /\ O + B1 >= 0 /\ -O + B1 >= 0 /\ N + B1 >= 0 /\ M + B1 >= 0 /\ L + B1 >= 0 /\ K + B1 >= 0 /\ J + B1 >= 0 /\ A + B1 - 1 >= 0 /\ -A1 >= 0 /\ Z - A1 >= 0 /\ -Z - A1 >= 0 /\ Y - A1 >= 0 /\ -Y - A1 >= 0 /\ X - A1 >= 0 /\ -X - A1 >= 0 /\ W - A1 >= 0 /\ -W - A1 >= 0 /\ V - A1 >= 0 /\ -V - A1 >= 0 /\ U - A1 >= 0 /\ -U - A1 >= 0 /\ T - A1 >= 0 /\ -T - A1 >= 0 /\ B - A1 - 1 >= 0 /\ S - A1 >= 0 /\ -S - A1 >= 0 /\ R - A1 >= 0 /\ -R - A1 >= 0 /\ Q - A1 >= 0 /\ -Q - A1 >= 0 /\ P - A1 >= 0 /\ -P - A1 >= 0 /\ O - A1 >= 0 /\ -O - A1 >= 0 /\ N - A1 >= 0 /\ M - A1 >= 0 /\ L - A1 >= 0 /\ K - A1 >= 0 /\ J - A1 >= 0 /\ A - A1 - 1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ -Z + A1 >= 0 /\ Y + A1 >= 0 /\ -Y + A1 >= 0 /\ X + A1 >= 0 /\ -X + A1 >= 0 /\ W + A1 >= 0 /\ -W + A1 >= 0 /\ V + A1 >= 0 /\ -V + A1 >= 0 /\ U + A1 >= 0 /\ -U + A1 >= 0 /\ T + A1 >= 0 /\ -T + A1 >= 0 /\ B + A1 - 1 >= 0 /\ S + A1 >= 0 /\ -S + A1 >= 0 /\ R + A1 >= 0 /\ -R + A1 >= 0 /\ Q + A1 >= 0 /\ -Q + A1 >= 0 /\ P + A1 >= 0 /\ -P + A1 >= 0 /\ O + A1 >= 0 /\ -O + A1 >= 0 /\ N + A1 >= 0 /\ M + A1 >= 0 /\ L + A1 >= 0 /\ K + A1 >= 0 /\ J + A1 >= 0 /\ A + A1 - 1 >= 0 /\ -Z >= 0 /\ Y - Z >= 0 /\ -Y - Z >= 0 /\ X - Z >= 0 /\ -X - Z >= 0 /\ W - Z >= 0 /\ -W - Z >= 0 /\ V - Z >= 0 /\ -V - Z >= 0 /\ U - Z >= 0 /\ -U - Z >= 0 /\ T - Z >= 0 /\ -T - Z >= 0 /\ B - Z - 1 >= 0 /\ S - Z >= 0 /\ -S - Z >= 0 /\ R - Z >= 0 /\ -R - Z >= 0 /\ Q - Z >= 0 /\ -Q - Z >= 0 /\ P - Z >= 0 /\ -P - Z >= 0 /\ O - Z >= 0 /\ -O - Z >= 0 /\ N - Z >= 0 /\ M - Z >= 0 /\ L - Z >= 0 /\ K - Z >= 0 /\ J - Z >= 0 /\ A - Z - 1 >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ -Y + Z >= 0 /\ X + Z >= 0 /\ -X + Z >= 0 /\ W + Z >= 0 /\ -W + Z >= 0 /\ V + Z >= 0 /\ -V + Z >= 0 /\ U + Z >= 0 /\ -U + Z >= 0 /\ T + Z >= 0 /\ -T + Z >= 0 /\ B + Z - 1 >= 0 /\ S + Z >= 0 /\ -S + Z >= 0 /\ R + Z >= 0 /\ -R + Z >= 0 /\ Q + Z >= 0 /\ -Q + Z >= 0 /\ P + Z >= 0 /\ -P + Z >= 0 /\ O + Z >= 0 /\ -O + Z >= 0 /\ N + Z >= 0 /\ M + Z >= 0 /\ L + Z >= 0 /\ K + Z >= 0 /\ J + Z >= 0 /\ A + Z - 1 >= 0 /\ -Y >= 0 /\ X - Y >= 0 /\ -X - Y >= 0 /\ W - Y >= 0 /\ -W - Y >= 0 /\ V - Y >= 0 /\ -V - Y >= 0 /\ U - Y >= 0 /\ -U - Y >= 0 /\ T - Y >= 0 /\ -T - Y >= 0 /\ B - Y - 1 >= 0 /\ S - Y >= 0 /\ -S - Y >= 0 /\ R - Y >= 0 /\ -R - Y >= 0 /\ Q - Y >= 0 /\ -Q - Y >= 0 /\ P - Y >= 0 /\ -P - Y >= 0 /\ O - Y >= 0 /\ -O - Y >= 0 /\ N - Y >= 0 /\ M - Y >= 0 /\ L - Y >= 0 /\ K - Y >= 0 /\ J - Y >= 0 /\ A - Y - 1 >= 0 /\ Y >= 0 /\ X + Y >= 0 /\ -X + Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ V + Y >= 0 /\ -V + Y >= 0 /\ U + Y >= 0 /\ -U + Y >= 0 /\ T + Y >= 0 /\ -T + Y >= 0 /\ B + Y - 1 >= 0 /\ S + Y >= 0 /\ -S + Y >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y >= 0 /\ -Q + Y >= 0 /\ P + Y >= 0 /\ -P + Y >= 0 /\ O + Y >= 0 /\ -O + Y >= 0 /\ N + Y >= 0 /\ M + Y >= 0 /\ L + Y >= 0 /\ K + Y >= 0 /\ J + Y >= 0 /\ A + Y - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ T - X >= 0 /\ -T - X >= 0 /\ B - X - 1 >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ O - X >= 0 /\ -O - X >= 0 /\ N - X >= 0 /\ M - X >= 0 /\ L - X >= 0 /\ K - X >= 0 /\ J - X >= 0 /\ A - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ V + X >= 0 /\ -V + X >= 0 /\ U + X >= 0 /\ -U + X >= 0 /\ T + X >= 0 /\ -T + X >= 0 /\ B + X - 1 >= 0 /\ S + X >= 0 /\ -S + X >= 0 /\ R + X >= 0 /\ -R + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ O + X >= 0 /\ -O + X >= 0 /\ N + X >= 0 /\ M + X >= 0 /\ L + X >= 0 /\ K + X >= 0 /\ J + X >= 0 /\ A + X - 1 >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ U - W >= 0 /\ -U - W >= 0 /\ T - W >= 0 /\ -T - W >= 0 /\ B - W - 1 >= 0 /\ S - W >= 0 /\ -S - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ O - W >= 0 /\ -O - W >= 0 /\ N - W >= 0 /\ M - W >= 0 /\ L - W >= 0 /\ K - W >= 0 /\ J - W >= 0 /\ A - W - 1 >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ U + W >= 0 /\ -U + W >= 0 /\ T + W >= 0 /\ -T + W >= 0 /\ B + W - 1 >= 0 /\ S + W >= 0 /\ -S + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ O + W >= 0 /\ -O + W >= 0 /\ N + W >= 0 /\ M + W >= 0 /\ L + W >= 0 /\ K + W >= 0 /\ J + W >= 0 /\ A + W - 1 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ T - V >= 0 /\ -T - V >= 0 /\ B - V - 1 >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ Q - V >= 0 /\ -Q - V >= 0 /\ P - V >= 0 /\ -P - V >= 0 /\ O - V >= 0 /\ -O - V >= 0 /\ N - V >= 0 /\ M - V >= 0 /\ L - V >= 0 /\ K - V >= 0 /\ J - V >= 0 /\ A - V - 1 >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ T + V >= 0 /\ -T + V >= 0 /\ B + V - 1 >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ Q + V >= 0 /\ -Q + V >= 0 /\ P + V >= 0 /\ -P + V >= 0 /\ O + V >= 0 /\ -O + V >= 0 /\ N + V >= 0 /\ M + V >= 0 /\ L + V >= 0 /\ K + V >= 0 /\ J + V >= 0 /\ A + V - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ B - U - 1 >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ Q - U >= 0 /\ -Q - U >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ N - U >= 0 /\ M - U >= 0 /\ L - U >= 0 /\ K - U >= 0 /\ J - U >= 0 /\ A - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U >= 0 /\ -Q + U >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ N + U >= 0 /\ M + U >= 0 /\ L + U >= 0 /\ K + U >= 0 /\ J + U >= 0 /\ A + U - 1 >= 0 /\ -T >= 0 /\ B - T - 1 >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ Q - T >= 0 /\ -Q - T >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ N - T >= 0 /\ M - T >= 0 /\ L - T >= 0 /\ K - T >= 0 /\ J - T >= 0 /\ A - T - 1 >= 0 /\ T >= 0 /\ B + T - 1 >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ Q + T >= 0 /\ -Q + T >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ N + T >= 0 /\ M + T >= 0 /\ L + T >= 0 /\ K + T >= 0 /\ J + T >= 0 /\ A + T - 1 >= 0 /\ A - B >= 0 /\ B - 1 >= 0 /\ S + B - 1 >= 0 /\ -S + B - 1 >= 0 /\ R + B - 1 >= 0 /\ -R + B - 1 >= 0 /\ Q + B - 1 >= 0 /\ -Q + B - 1 >= 0 /\ P + B - 1 >= 0 /\ -P + B - 1 >= 0 /\ O + B - 1 >= 0 /\ -O + B - 1 >= 0 /\ N + B - 1 >= 0 /\ M + B - 1 >= 0 /\ L + B - 1 >= 0 /\ K + B - 1 >= 0 /\ J + B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ Q - S >= 0 /\ -Q - S >= 0 /\ P - S >= 0 /\ -P - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ N - S >= 0 /\ M - S >= 0 /\ L - S >= 0 /\ K - S >= 0 /\ J - S >= 0 /\ A - S - 1 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ Q + S >= 0 /\ -Q + S >= 0 /\ P + S >= 0 /\ -P + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ N + S >= 0 /\ M + S >= 0 /\ L + S >= 0 /\ K + S >= 0 /\ J + S >= 0 /\ A + S - 1 >= 0 /\ -R >= 0 /\ Q - R >= 0 /\ -Q - R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ N - R >= 0 /\ M - R >= 0 /\ L - R >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ A - R - 1 >= 0 /\ R >= 0 /\ Q + R >= 0 /\ -Q + R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ N + R >= 0 /\ M + R >= 0 /\ L + R >= 0 /\ K + R >= 0 /\ J + R >= 0 /\ A + R - 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ O - Q >= 0 /\ -O - Q >= 0 /\ N - Q >= 0 /\ M - Q >= 0 /\ L - Q >= 0 /\ K - Q >= 0 /\ J - Q >= 0 /\ A - Q - 1 >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ O + Q >= 0 /\ -O + Q >= 0 /\ N + Q >= 0 /\ M + Q >= 0 /\ L + Q >= 0 /\ K + Q >= 0 /\ J + Q >= 0 /\ A + Q - 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ N - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ K - P >= 0 /\ J - P >= 0 /\ A - P - 1 >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ N + P >= 0 /\ M + P >= 0 /\ L + P >= 0 /\ K + P >= 0 /\ J + P >= 0 /\ A + P - 1 >= 0 /\ -O >= 0 /\ N - O >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ A - O - 1 >= 0 /\ O >= 0 /\ N + O >= 0 /\ M + O >= 0 /\ L + O >= 0 /\ K + O >= 0 /\ J + O >= 0 /\ A + O - 1 >= 0 /\ N >= 0 /\ M + N >= 0 /\ L + N >= 0 /\ K + N >= 0 /\ J + N >= 0 /\ A + N - 1 >= 0 /\ M >= 0 /\ L + M >= 0 /\ K + M >= 0 /\ J + M >= 0 /\ A + M - 1 >= 0 /\ J - L >= 0 /\ L >= 0 /\ K + L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L - 1 >= 0 /\ K >= 0 /\ J + K >= 0 /\ A + K - 1 >= 0 /\ J >= 0 /\ A + J - 1 >= 0 /\ A - 1 >= 0 /\ A >= 1 /\ B >= 1 ]
  f999(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f1(1, 1, H - 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, C1)) [ H >= 1 /\ C = 0 /\ B = 0 /\ A = 0 /\ D = 0 /\ E = 0 /\ F = 0 /\ G = 0 /\ I = 0 /\ J = 0 /\ K = 0 /\ L = 0 /\ M = 0 /\ N = 0 /\ O = 0 /\ P = 0 /\ Q = 0 /\ R = 0 /\ S = 0 /\ T = 0 /\ U = 0 /\ V = 0 /\ W = 0 /\ X = 0 /\ Y = 0 /\ Z = 0 /\ A1 = 0 /\ B1 = 0 ]
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f1(A + 1, B + 1, H + C - 1, D, E, F, G, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I >= 0 /\ H - I >= 0 /\ -H - I >= 0 /\ G - I >= 0 /\ F - I >= 0 /\ E - I >= 0 /\ D - I >= 0 /\ -D - I >= 0 /\ C - I >= 0 /\ B1 - I >= 0 /\ -B1 - I >= 0 /\ A1 - I >= 0 /\ -A1 - I >= 0 /\ Z - I >= 0 /\ -Z - I >= 0 /\ Y - I >= 0 /\ -Y - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ W - I >= 0 /\ -W - I >= 0 /\ V - I >= 0 /\ -V - I >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ B - I - 1 >= 0 /\ S - I >= 0 /\ -S - I >= 0 /\ R - I >= 0 /\ -R - I >= 0 /\ Q - I >= 0 /\ -Q - I >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I >= 0 /\ M - I >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ J - I >= 0 /\ A - I - 1 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I >= 0 /\ F + I >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ -D + I >= 0 /\ C + I >= 0 /\ B1 + I >= 0 /\ -B1 + I >= 0 /\ A1 + I >= 0 /\ -A1 + I >= 0 /\ Z + I >= 0 /\ -Z + I >= 0 /\ Y + I >= 0 /\ -Y + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ W + I >= 0 /\ -W + I >= 0 /\ V + I >= 0 /\ -V + I >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ B + I - 1 >= 0 /\ S + I >= 0 /\ -S + I >= 0 /\ R + I >= 0 /\ -R + I >= 0 /\ Q + I >= 0 /\ -Q + I >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I >= 0 /\ M + I >= 0 /\ L + I >= 0 /\ K + I >= 0 /\ J + I >= 0 /\ A + I - 1 >= 0 /\ -H >= 0 /\ G - H >= 0 /\ F - H >= 0 /\ E - H >= 0 /\ D - H >= 0 /\ -D - H >= 0 /\ C - H >= 0 /\ B1 - H >= 0 /\ -B1 - H >= 0 /\ A1 - H >= 0 /\ -A1 - H >= 0 /\ Z - H >= 0 /\ -Z - H >= 0 /\ Y - H >= 0 /\ -Y - H >= 0 /\ X - H >= 0 /\ -X - H >= 0 /\ W - H >= 0 /\ -W - H >= 0 /\ V - H >= 0 /\ -V - H >= 0 /\ U - H >= 0 /\ -U - H >= 0 /\ T - H >= 0 /\ -T - H >= 0 /\ B - H - 1 >= 0 /\ S - H >= 0 /\ -S - H >= 0 /\ R - H >= 0 /\ -R - H >= 0 /\ Q - H >= 0 /\ -Q - H >= 0 /\ P - H >= 0 /\ -P - H >= 0 /\ O - H >= 0 /\ -O - H >= 0 /\ N - H >= 0 /\ M - H >= 0 /\ L - H >= 0 /\ K - H >= 0 /\ J - H >= 0 /\ A - H - 1 >= 0 /\ H >= 0 /\ G + H >= 0 /\ F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H >= 0 /\ B1 + H >= 0 /\ -B1 + H >= 0 /\ A1 + H >= 0 /\ -A1 + H >= 0 /\ Z + H >= 0 /\ -Z + H >= 0 /\ Y + H >= 0 /\ -Y + H >= 0 /\ X + H >= 0 /\ -X + H >= 0 /\ W + H >= 0 /\ -W + H >= 0 /\ V + H >= 0 /\ -V + H >= 0 /\ U + H >= 0 /\ -U + H >= 0 /\ T + H >= 0 /\ -T + H >= 0 /\ B + H - 1 >= 0 /\ S + H >= 0 /\ -S + H >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ Q + H >= 0 /\ -Q + H >= 0 /\ P + H >= 0 /\ -P + H >= 0 /\ O + H >= 0 /\ -O + H >= 0 /\ N + H >= 0 /\ M + H >= 0 /\ L + H >= 0 /\ K + H >= 0 /\ J + H >= 0 /\ A + H - 1 >= 0 /\ G >= 0 /\ F + G >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ -D + G >= 0 /\ C + G >= 0 /\ B1 + G >= 0 /\ -B1 + G >= 0 /\ A1 + G >= 0 /\ -A1 + G >= 0 /\ Z + G >= 0 /\ -Z + G >= 0 /\ Y + G >= 0 /\ -Y + G >= 0 /\ X + G >= 0 /\ -X + G >= 0 /\ W + G >= 0 /\ -W + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ T + G >= 0 /\ -T + G >= 0 /\ B + G - 1 >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ P + G >= 0 /\ -P + G >= 0 /\ O + G >= 0 /\ -O + G >= 0 /\ N + G >= 0 /\ M + G >= 0 /\ L + G >= 0 /\ K + G >= 0 /\ J + G >= 0 /\ A + G - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B1 + F >= 0 /\ -B1 + F >= 0 /\ A1 + F >= 0 /\ -A1 + F >= 0 /\ Z + F >= 0 /\ -Z + F >= 0 /\ Y + F >= 0 /\ -Y + F >= 0 /\ X + F >= 0 /\ -X + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ U + F >= 0 /\ -U + F >= 0 /\ T + F >= 0 /\ -T + F >= 0 /\ B + F - 1 >= 0 /\ S + F >= 0 /\ -S + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ Q + F >= 0 /\ -Q + F >= 0 /\ P + F >= 0 /\ -P + F >= 0 /\ O + F >= 0 /\ -O + F >= 0 /\ N + F >= 0 /\ M + F >= 0 /\ L + F >= 0 /\ K + F >= 0 /\ J + F >= 0 /\ A + F - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ C + E >= 0 /\ B1 + E >= 0 /\ -B1 + E >= 0 /\ A1 + E >= 0 /\ -A1 + E >= 0 /\ Z + E >= 0 /\ -Z + E >= 0 /\ Y + E >= 0 /\ -Y + E >= 0 /\ X + E >= 0 /\ -X + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ V + E >= 0 /\ -V + E >= 0 /\ U + E >= 0 /\ -U + E >= 0 /\ T + E >= 0 /\ -T + E >= 0 /\ B + E - 1 >= 0 /\ S + E >= 0 /\ -S + E >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E >= 0 /\ -Q + E >= 0 /\ P + E >= 0 /\ -P + E >= 0 /\ O + E >= 0 /\ -O + E >= 0 /\ N + E >= 0 /\ M + E >= 0 /\ L + E >= 0 /\ K + E >= 0 /\ J + E >= 0 /\ A + E - 1 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ B1 - D >= 0 /\ -B1 - D >= 0 /\ A1 - D >= 0 /\ -A1 - D >= 0 /\ Z - D >= 0 /\ -Z - D >= 0 /\ Y - D >= 0 /\ -Y - D >= 0 /\ X - D >= 0 /\ -X - D >= 0 /\ W - D >= 0 /\ -W - D >= 0 /\ V - D >= 0 /\ -V - D >= 0 /\ U - D >= 0 /\ -U - D >= 0 /\ T - D >= 0 /\ -T - D >= 0 /\ B - D - 1 >= 0 /\ S - D >= 0 /\ -S - D >= 0 /\ R - D >= 0 /\ -R - D >= 0 /\ Q - D >= 0 /\ -Q - D >= 0 /\ P - D >= 0 /\ -P - D >= 0 /\ O - D >= 0 /\ -O - D >= 0 /\ N - D >= 0 /\ M - D >= 0 /\ L - D >= 0 /\ K - D >= 0 /\ J - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B1 + D >= 0 /\ -B1 + D >= 0 /\ A1 + D >= 0 /\ -A1 + D >= 0 /\ Z + D >= 0 /\ -Z + D >= 0 /\ Y + D >= 0 /\ -Y + D >= 0 /\ X + D >= 0 /\ -X + D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ V + D >= 0 /\ -V + D >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ T + D >= 0 /\ -T + D >= 0 /\ B + D - 1 >= 0 /\ S + D >= 0 /\ -S + D >= 0 /\ R + D >= 0 /\ -R + D >= 0 /\ Q + D >= 0 /\ -Q + D >= 0 /\ P + D >= 0 /\ -P + D >= 0 /\ O + D >= 0 /\ -O + D >= 0 /\ N + D >= 0 /\ M + D >= 0 /\ L + D >= 0 /\ K + D >= 0 /\ J + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B1 + C >= 0 /\ -B1 + C >= 0 /\ A1 + C >= 0 /\ -A1 + C >= 0 /\ Z + C >= 0 /\ -Z + C >= 0 /\ Y + C >= 0 /\ -Y + C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ V + C >= 0 /\ -V + C >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ B + C - 1 >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ P + C >= 0 /\ -P + C >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C >= 0 /\ M + C >= 0 /\ L + C >= 0 /\ K + C >= 0 /\ J + C >= 0 /\ A + C - 1 >= 0 /\ -B1 >= 0 /\ A1 - B1 >= 0 /\ -A1 - B1 >= 0 /\ Z - B1 >= 0 /\ -Z - B1 >= 0 /\ Y - B1 >= 0 /\ -Y - B1 >= 0 /\ X - B1 >= 0 /\ -X - B1 >= 0 /\ W - B1 >= 0 /\ -W - B1 >= 0 /\ V - B1 >= 0 /\ -V - B1 >= 0 /\ U - B1 >= 0 /\ -U - B1 >= 0 /\ T - B1 >= 0 /\ -T - B1 >= 0 /\ B - B1 - 1 >= 0 /\ S - B1 >= 0 /\ -S - B1 >= 0 /\ R - B1 >= 0 /\ -R - B1 >= 0 /\ Q - B1 >= 0 /\ -Q - B1 >= 0 /\ P - B1 >= 0 /\ -P - B1 >= 0 /\ O - B1 >= 0 /\ -O - B1 >= 0 /\ N - B1 >= 0 /\ M - B1 >= 0 /\ L - B1 >= 0 /\ K - B1 >= 0 /\ J - B1 >= 0 /\ A - B1 - 1 >= 0 /\ B1 >= 0 /\ A1 + B1 >= 0 /\ -A1 + B1 >= 0 /\ Z + B1 >= 0 /\ -Z + B1 >= 0 /\ Y + B1 >= 0 /\ -Y + B1 >= 0 /\ X + B1 >= 0 /\ -X + B1 >= 0 /\ W + B1 >= 0 /\ -W + B1 >= 0 /\ V + B1 >= 0 /\ -V + B1 >= 0 /\ U + B1 >= 0 /\ -U + B1 >= 0 /\ T + B1 >= 0 /\ -T + B1 >= 0 /\ B + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 >= 0 /\ R + B1 >= 0 /\ -R + B1 >= 0 /\ Q + B1 >= 0 /\ -Q + B1 >= 0 /\ P + B1 >= 0 /\ -P + B1 >= 0 /\ O + B1 >= 0 /\ -O + B1 >= 0 /\ N + B1 >= 0 /\ M + B1 >= 0 /\ L + B1 >= 0 /\ K + B1 >= 0 /\ J + B1 >= 0 /\ A + B1 - 1 >= 0 /\ -A1 >= 0 /\ Z - A1 >= 0 /\ -Z - A1 >= 0 /\ Y - A1 >= 0 /\ -Y - A1 >= 0 /\ X - A1 >= 0 /\ -X - A1 >= 0 /\ W - A1 >= 0 /\ -W - A1 >= 0 /\ V - A1 >= 0 /\ -V - A1 >= 0 /\ U - A1 >= 0 /\ -U - A1 >= 0 /\ T - A1 >= 0 /\ -T - A1 >= 0 /\ B - A1 - 1 >= 0 /\ S - A1 >= 0 /\ -S - A1 >= 0 /\ R - A1 >= 0 /\ -R - A1 >= 0 /\ Q - A1 >= 0 /\ -Q - A1 >= 0 /\ P - A1 >= 0 /\ -P - A1 >= 0 /\ O - A1 >= 0 /\ -O - A1 >= 0 /\ N - A1 >= 0 /\ M - A1 >= 0 /\ L - A1 >= 0 /\ K - A1 >= 0 /\ J - A1 >= 0 /\ A - A1 - 1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ -Z + A1 >= 0 /\ Y + A1 >= 0 /\ -Y + A1 >= 0 /\ X + A1 >= 0 /\ -X + A1 >= 0 /\ W + A1 >= 0 /\ -W + A1 >= 0 /\ V + A1 >= 0 /\ -V + A1 >= 0 /\ U + A1 >= 0 /\ -U + A1 >= 0 /\ T + A1 >= 0 /\ -T + A1 >= 0 /\ B + A1 - 1 >= 0 /\ S + A1 >= 0 /\ -S + A1 >= 0 /\ R + A1 >= 0 /\ -R + A1 >= 0 /\ Q + A1 >= 0 /\ -Q + A1 >= 0 /\ P + A1 >= 0 /\ -P + A1 >= 0 /\ O + A1 >= 0 /\ -O + A1 >= 0 /\ N + A1 >= 0 /\ M + A1 >= 0 /\ L + A1 >= 0 /\ K + A1 >= 0 /\ J + A1 >= 0 /\ A + A1 - 1 >= 0 /\ -Z >= 0 /\ Y - Z >= 0 /\ -Y - Z >= 0 /\ X - Z >= 0 /\ -X - Z >= 0 /\ W - Z >= 0 /\ -W - Z >= 0 /\ V - Z >= 0 /\ -V - Z >= 0 /\ U - Z >= 0 /\ -U - Z >= 0 /\ T - Z >= 0 /\ -T - Z >= 0 /\ B - Z - 1 >= 0 /\ S - Z >= 0 /\ -S - Z >= 0 /\ R - Z >= 0 /\ -R - Z >= 0 /\ Q - Z >= 0 /\ -Q - Z >= 0 /\ P - Z >= 0 /\ -P - Z >= 0 /\ O - Z >= 0 /\ -O - Z >= 0 /\ N - Z >= 0 /\ M - Z >= 0 /\ L - Z >= 0 /\ K - Z >= 0 /\ J - Z >= 0 /\ A - Z - 1 >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ -Y + Z >= 0 /\ X + Z >= 0 /\ -X + Z >= 0 /\ W + Z >= 0 /\ -W + Z >= 0 /\ V + Z >= 0 /\ -V + Z >= 0 /\ U + Z >= 0 /\ -U + Z >= 0 /\ T + Z >= 0 /\ -T + Z >= 0 /\ B + Z - 1 >= 0 /\ S + Z >= 0 /\ -S + Z >= 0 /\ R + Z >= 0 /\ -R + Z >= 0 /\ Q + Z >= 0 /\ -Q + Z >= 0 /\ P + Z >= 0 /\ -P + Z >= 0 /\ O + Z >= 0 /\ -O + Z >= 0 /\ N + Z >= 0 /\ M + Z >= 0 /\ L + Z >= 0 /\ K + Z >= 0 /\ J + Z >= 0 /\ A + Z - 1 >= 0 /\ -Y >= 0 /\ X - Y >= 0 /\ -X - Y >= 0 /\ W - Y >= 0 /\ -W - Y >= 0 /\ V - Y >= 0 /\ -V - Y >= 0 /\ U - Y >= 0 /\ -U - Y >= 0 /\ T - Y >= 0 /\ -T - Y >= 0 /\ B - Y - 1 >= 0 /\ S - Y >= 0 /\ -S - Y >= 0 /\ R - Y >= 0 /\ -R - Y >= 0 /\ Q - Y >= 0 /\ -Q - Y >= 0 /\ P - Y >= 0 /\ -P - Y >= 0 /\ O - Y >= 0 /\ -O - Y >= 0 /\ N - Y >= 0 /\ M - Y >= 0 /\ L - Y >= 0 /\ K - Y >= 0 /\ J - Y >= 0 /\ A - Y - 1 >= 0 /\ Y >= 0 /\ X + Y >= 0 /\ -X + Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ V + Y >= 0 /\ -V + Y >= 0 /\ U + Y >= 0 /\ -U + Y >= 0 /\ T + Y >= 0 /\ -T + Y >= 0 /\ B + Y - 1 >= 0 /\ S + Y >= 0 /\ -S + Y >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y >= 0 /\ -Q + Y >= 0 /\ P + Y >= 0 /\ -P + Y >= 0 /\ O + Y >= 0 /\ -O + Y >= 0 /\ N + Y >= 0 /\ M + Y >= 0 /\ L + Y >= 0 /\ K + Y >= 0 /\ J + Y >= 0 /\ A + Y - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ T - X >= 0 /\ -T - X >= 0 /\ B - X - 1 >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ O - X >= 0 /\ -O - X >= 0 /\ N - X >= 0 /\ M - X >= 0 /\ L - X >= 0 /\ K - X >= 0 /\ J - X >= 0 /\ A - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ V + X >= 0 /\ -V + X >= 0 /\ U + X >= 0 /\ -U + X >= 0 /\ T + X >= 0 /\ -T + X >= 0 /\ B + X - 1 >= 0 /\ S + X >= 0 /\ -S + X >= 0 /\ R + X >= 0 /\ -R + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ O + X >= 0 /\ -O + X >= 0 /\ N + X >= 0 /\ M + X >= 0 /\ L + X >= 0 /\ K + X >= 0 /\ J + X >= 0 /\ A + X - 1 >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ U - W >= 0 /\ -U - W >= 0 /\ T - W >= 0 /\ -T - W >= 0 /\ B - W - 1 >= 0 /\ S - W >= 0 /\ -S - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ O - W >= 0 /\ -O - W >= 0 /\ N - W >= 0 /\ M - W >= 0 /\ L - W >= 0 /\ K - W >= 0 /\ J - W >= 0 /\ A - W - 1 >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ U + W >= 0 /\ -U + W >= 0 /\ T + W >= 0 /\ -T + W >= 0 /\ B + W - 1 >= 0 /\ S + W >= 0 /\ -S + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ O + W >= 0 /\ -O + W >= 0 /\ N + W >= 0 /\ M + W >= 0 /\ L + W >= 0 /\ K + W >= 0 /\ J + W >= 0 /\ A + W - 1 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ T - V >= 0 /\ -T - V >= 0 /\ B - V - 1 >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ Q - V >= 0 /\ -Q - V >= 0 /\ P - V >= 0 /\ -P - V >= 0 /\ O - V >= 0 /\ -O - V >= 0 /\ N - V >= 0 /\ M - V >= 0 /\ L - V >= 0 /\ K - V >= 0 /\ J - V >= 0 /\ A - V - 1 >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ T + V >= 0 /\ -T + V >= 0 /\ B + V - 1 >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ Q + V >= 0 /\ -Q + V >= 0 /\ P + V >= 0 /\ -P + V >= 0 /\ O + V >= 0 /\ -O + V >= 0 /\ N + V >= 0 /\ M + V >= 0 /\ L + V >= 0 /\ K + V >= 0 /\ J + V >= 0 /\ A + V - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ B - U - 1 >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ Q - U >= 0 /\ -Q - U >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ N - U >= 0 /\ M - U >= 0 /\ L - U >= 0 /\ K - U >= 0 /\ J - U >= 0 /\ A - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U >= 0 /\ -Q + U >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ N + U >= 0 /\ M + U >= 0 /\ L + U >= 0 /\ K + U >= 0 /\ J + U >= 0 /\ A + U - 1 >= 0 /\ -T >= 0 /\ B - T - 1 >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ Q - T >= 0 /\ -Q - T >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ N - T >= 0 /\ M - T >= 0 /\ L - T >= 0 /\ K - T >= 0 /\ J - T >= 0 /\ A - T - 1 >= 0 /\ T >= 0 /\ B + T - 1 >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ Q + T >= 0 /\ -Q + T >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ N + T >= 0 /\ M + T >= 0 /\ L + T >= 0 /\ K + T >= 0 /\ J + T >= 0 /\ A + T - 1 >= 0 /\ A - B >= 0 /\ B - 1 >= 0 /\ S + B - 1 >= 0 /\ -S + B - 1 >= 0 /\ R + B - 1 >= 0 /\ -R + B - 1 >= 0 /\ Q + B - 1 >= 0 /\ -Q + B - 1 >= 0 /\ P + B - 1 >= 0 /\ -P + B - 1 >= 0 /\ O + B - 1 >= 0 /\ -O + B - 1 >= 0 /\ N + B - 1 >= 0 /\ M + B - 1 >= 0 /\ L + B - 1 >= 0 /\ K + B - 1 >= 0 /\ J + B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ Q - S >= 0 /\ -Q - S >= 0 /\ P - S >= 0 /\ -P - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ N - S >= 0 /\ M - S >= 0 /\ L - S >= 0 /\ K - S >= 0 /\ J - S >= 0 /\ A - S - 1 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ Q + S >= 0 /\ -Q + S >= 0 /\ P + S >= 0 /\ -P + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ N + S >= 0 /\ M + S >= 0 /\ L + S >= 0 /\ K + S >= 0 /\ J + S >= 0 /\ A + S - 1 >= 0 /\ -R >= 0 /\ Q - R >= 0 /\ -Q - R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ N - R >= 0 /\ M - R >= 0 /\ L - R >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ A - R - 1 >= 0 /\ R >= 0 /\ Q + R >= 0 /\ -Q + R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ N + R >= 0 /\ M + R >= 0 /\ L + R >= 0 /\ K + R >= 0 /\ J + R >= 0 /\ A + R - 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ O - Q >= 0 /\ -O - Q >= 0 /\ N - Q >= 0 /\ M - Q >= 0 /\ L - Q >= 0 /\ K - Q >= 0 /\ J - Q >= 0 /\ A - Q - 1 >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ O + Q >= 0 /\ -O + Q >= 0 /\ N + Q >= 0 /\ M + Q >= 0 /\ L + Q >= 0 /\ K + Q >= 0 /\ J + Q >= 0 /\ A + Q - 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ N - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ K - P >= 0 /\ J - P >= 0 /\ A - P - 1 >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ N + P >= 0 /\ M + P >= 0 /\ L + P >= 0 /\ K + P >= 0 /\ J + P >= 0 /\ A + P - 1 >= 0 /\ -O >= 0 /\ N - O >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ A - O - 1 >= 0 /\ O >= 0 /\ N + O >= 0 /\ M + O >= 0 /\ L + O >= 0 /\ K + O >= 0 /\ J + O >= 0 /\ A + O - 1 >= 0 /\ N >= 0 /\ M + N >= 0 /\ L + N >= 0 /\ K + N >= 0 /\ J + N >= 0 /\ A + N - 1 >= 0 /\ M >= 0 /\ L + M >= 0 /\ K + M >= 0 /\ J + M >= 0 /\ A + M - 1 >= 0 /\ J - L >= 0 /\ L >= 0 /\ K + L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L - 1 >= 0 /\ K >= 0 /\ J + K >= 0 /\ A + K - 1 >= 0 /\ J >= 0 /\ A + J - 1 >= 0 /\ A - 1 >= 0 /\ H + C >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f1(A + 1, B + 1, C + H + D - 1, 0, E, F, G, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I >= 0 /\ H - I >= 0 /\ -H - I >= 0 /\ G - I - 1 >= 0 /\ F - I >= 0 /\ E - I >= 0 /\ D - I >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ B1 - I >= 0 /\ -B1 - I >= 0 /\ A1 - I >= 0 /\ -A1 - I >= 0 /\ Z - I >= 0 /\ -Z - I >= 0 /\ Y - I >= 0 /\ -Y - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ W - I >= 0 /\ -W - I >= 0 /\ V - I >= 0 /\ -V - I >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ B - I >= 0 /\ -B - I >= 0 /\ S - I >= 0 /\ -S - I >= 0 /\ R - I >= 0 /\ -R - I >= 0 /\ Q - I >= 0 /\ -Q - I >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I >= 0 /\ M - I >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ J - I >= 0 /\ A - I >= 0 /\ -A - I >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ B1 + I >= 0 /\ -B1 + I >= 0 /\ A1 + I >= 0 /\ -A1 + I >= 0 /\ Z + I >= 0 /\ -Z + I >= 0 /\ Y + I >= 0 /\ -Y + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ W + I >= 0 /\ -W + I >= 0 /\ V + I >= 0 /\ -V + I >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ S + I >= 0 /\ -S + I >= 0 /\ R + I >= 0 /\ -R + I >= 0 /\ Q + I >= 0 /\ -Q + I >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I >= 0 /\ M + I >= 0 /\ L + I >= 0 /\ K + I >= 0 /\ J + I >= 0 /\ A + I >= 0 /\ -A + I >= 0 /\ -H >= 0 /\ G - H - 1 >= 0 /\ F - H >= 0 /\ E - H >= 0 /\ D - H >= 0 /\ C - H >= 0 /\ -C - H >= 0 /\ B1 - H >= 0 /\ -B1 - H >= 0 /\ A1 - H >= 0 /\ -A1 - H >= 0 /\ Z - H >= 0 /\ -Z - H >= 0 /\ Y - H >= 0 /\ -Y - H >= 0 /\ X - H >= 0 /\ -X - H >= 0 /\ W - H >= 0 /\ -W - H >= 0 /\ V - H >= 0 /\ -V - H >= 0 /\ U - H >= 0 /\ -U - H >= 0 /\ T - H >= 0 /\ -T - H >= 0 /\ B - H >= 0 /\ -B - H >= 0 /\ S - H >= 0 /\ -S - H >= 0 /\ R - H >= 0 /\ -R - H >= 0 /\ Q - H >= 0 /\ -Q - H >= 0 /\ P - H >= 0 /\ -P - H >= 0 /\ O - H >= 0 /\ -O - H >= 0 /\ N - H >= 0 /\ M - H >= 0 /\ L - H >= 0 /\ K - H >= 0 /\ J - H >= 0 /\ A - H >= 0 /\ -A - H >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B1 + H >= 0 /\ -B1 + H >= 0 /\ A1 + H >= 0 /\ -A1 + H >= 0 /\ Z + H >= 0 /\ -Z + H >= 0 /\ Y + H >= 0 /\ -Y + H >= 0 /\ X + H >= 0 /\ -X + H >= 0 /\ W + H >= 0 /\ -W + H >= 0 /\ V + H >= 0 /\ -V + H >= 0 /\ U + H >= 0 /\ -U + H >= 0 /\ T + H >= 0 /\ -T + H >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ S + H >= 0 /\ -S + H >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ Q + H >= 0 /\ -Q + H >= 0 /\ P + H >= 0 /\ -P + H >= 0 /\ O + H >= 0 /\ -O + H >= 0 /\ N + H >= 0 /\ M + H >= 0 /\ L + H >= 0 /\ K + H >= 0 /\ J + H >= 0 /\ A + H >= 0 /\ -A + H >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 1 >= 0 /\ -C + G - 1 >= 0 /\ B1 + G - 1 >= 0 /\ -B1 + G - 1 >= 0 /\ A1 + G - 1 >= 0 /\ -A1 + G - 1 >= 0 /\ Z + G - 1 >= 0 /\ -Z + G - 1 >= 0 /\ Y + G - 1 >= 0 /\ -Y + G - 1 >= 0 /\ X + G - 1 >= 0 /\ -X + G - 1 >= 0 /\ W + G - 1 >= 0 /\ -W + G - 1 >= 0 /\ V + G - 1 >= 0 /\ -V + G - 1 >= 0 /\ U + G - 1 >= 0 /\ -U + G - 1 >= 0 /\ T + G - 1 >= 0 /\ -T + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G - 1 >= 0 /\ S + G - 1 >= 0 /\ -S + G - 1 >= 0 /\ R + G - 1 >= 0 /\ -R + G - 1 >= 0 /\ Q + G - 1 >= 0 /\ -Q + G - 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G - 1 >= 0 /\ O + G - 1 >= 0 /\ -O + G - 1 >= 0 /\ N + G - 1 >= 0 /\ M + G - 1 >= 0 /\ L + G - 1 >= 0 /\ K + G - 1 >= 0 /\ J + G - 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ C + F >= 0 /\ -C + F >= 0 /\ B1 + F >= 0 /\ -B1 + F >= 0 /\ A1 + F >= 0 /\ -A1 + F >= 0 /\ Z + F >= 0 /\ -Z + F >= 0 /\ Y + F >= 0 /\ -Y + F >= 0 /\ X + F >= 0 /\ -X + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ U + F >= 0 /\ -U + F >= 0 /\ T + F >= 0 /\ -T + F >= 0 /\ B + F >= 0 /\ -B + F >= 0 /\ S + F >= 0 /\ -S + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ Q + F >= 0 /\ -Q + F >= 0 /\ P + F >= 0 /\ -P + F >= 0 /\ O + F >= 0 /\ -O + F >= 0 /\ N + F >= 0 /\ M + F >= 0 /\ L + F >= 0 /\ K + F >= 0 /\ J + F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B1 + E >= 0 /\ -B1 + E >= 0 /\ A1 + E >= 0 /\ -A1 + E >= 0 /\ Z + E >= 0 /\ -Z + E >= 0 /\ Y + E >= 0 /\ -Y + E >= 0 /\ X + E >= 0 /\ -X + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ V + E >= 0 /\ -V + E >= 0 /\ U + E >= 0 /\ -U + E >= 0 /\ T + E >= 0 /\ -T + E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ S + E >= 0 /\ -S + E >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E >= 0 /\ -Q + E >= 0 /\ P + E >= 0 /\ -P + E >= 0 /\ O + E >= 0 /\ -O + E >= 0 /\ N + E >= 0 /\ M + E >= 0 /\ L + E >= 0 /\ K + E >= 0 /\ J + E >= 0 /\ A + E >= 0 /\ -A + E >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B1 + D >= 0 /\ -B1 + D >= 0 /\ A1 + D >= 0 /\ -A1 + D >= 0 /\ Z + D >= 0 /\ -Z + D >= 0 /\ Y + D >= 0 /\ -Y + D >= 0 /\ X + D >= 0 /\ -X + D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ V + D >= 0 /\ -V + D >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ T + D >= 0 /\ -T + D >= 0 /\ B + D >= 0 /\ -B + D >= 0 /\ S + D >= 0 /\ -S + D >= 0 /\ R + D >= 0 /\ -R + D >= 0 /\ Q + D >= 0 /\ -Q + D >= 0 /\ P + D >= 0 /\ -P + D >= 0 /\ O + D >= 0 /\ -O + D >= 0 /\ N + D >= 0 /\ M + D >= 0 /\ L + D >= 0 /\ K + D >= 0 /\ J + D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B1 - C >= 0 /\ -B1 - C >= 0 /\ A1 - C >= 0 /\ -A1 - C >= 0 /\ Z - C >= 0 /\ -Z - C >= 0 /\ Y - C >= 0 /\ -Y - C >= 0 /\ X - C >= 0 /\ -X - C >= 0 /\ W - C >= 0 /\ -W - C >= 0 /\ V - C >= 0 /\ -V - C >= 0 /\ U - C >= 0 /\ -U - C >= 0 /\ T - C >= 0 /\ -T - C >= 0 /\ B - C >= 0 /\ -B - C >= 0 /\ S - C >= 0 /\ -S - C >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C >= 0 /\ -Q - C >= 0 /\ P - C >= 0 /\ -P - C >= 0 /\ O - C >= 0 /\ -O - C >= 0 /\ N - C >= 0 /\ M - C >= 0 /\ L - C >= 0 /\ K - C >= 0 /\ J - C >= 0 /\ A - C >= 0 /\ -A - C >= 0 /\ C >= 0 /\ B1 + C >= 0 /\ -B1 + C >= 0 /\ A1 + C >= 0 /\ -A1 + C >= 0 /\ Z + C >= 0 /\ -Z + C >= 0 /\ Y + C >= 0 /\ -Y + C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ V + C >= 0 /\ -V + C >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ P + C >= 0 /\ -P + C >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C >= 0 /\ M + C >= 0 /\ L + C >= 0 /\ K + C >= 0 /\ J + C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ -B1 >= 0 /\ A1 - B1 >= 0 /\ -A1 - B1 >= 0 /\ Z - B1 >= 0 /\ -Z - B1 >= 0 /\ Y - B1 >= 0 /\ -Y - B1 >= 0 /\ X - B1 >= 0 /\ -X - B1 >= 0 /\ W - B1 >= 0 /\ -W - B1 >= 0 /\ V - B1 >= 0 /\ -V - B1 >= 0 /\ U - B1 >= 0 /\ -U - B1 >= 0 /\ T - B1 >= 0 /\ -T - B1 >= 0 /\ B - B1 >= 0 /\ -B - B1 >= 0 /\ S - B1 >= 0 /\ -S - B1 >= 0 /\ R - B1 >= 0 /\ -R - B1 >= 0 /\ Q - B1 >= 0 /\ -Q - B1 >= 0 /\ P - B1 >= 0 /\ -P - B1 >= 0 /\ O - B1 >= 0 /\ -O - B1 >= 0 /\ N - B1 >= 0 /\ M - B1 >= 0 /\ L - B1 >= 0 /\ K - B1 >= 0 /\ J - B1 >= 0 /\ A - B1 >= 0 /\ -A - B1 >= 0 /\ B1 >= 0 /\ A1 + B1 >= 0 /\ -A1 + B1 >= 0 /\ Z + B1 >= 0 /\ -Z + B1 >= 0 /\ Y + B1 >= 0 /\ -Y + B1 >= 0 /\ X + B1 >= 0 /\ -X + B1 >= 0 /\ W + B1 >= 0 /\ -W + B1 >= 0 /\ V + B1 >= 0 /\ -V + B1 >= 0 /\ U + B1 >= 0 /\ -U + B1 >= 0 /\ T + B1 >= 0 /\ -T + B1 >= 0 /\ B + B1 >= 0 /\ -B + B1 >= 0 /\ S + B1 >= 0 /\ -S + B1 >= 0 /\ R + B1 >= 0 /\ -R + B1 >= 0 /\ Q + B1 >= 0 /\ -Q + B1 >= 0 /\ P + B1 >= 0 /\ -P + B1 >= 0 /\ O + B1 >= 0 /\ -O + B1 >= 0 /\ N + B1 >= 0 /\ M + B1 >= 0 /\ L + B1 >= 0 /\ K + B1 >= 0 /\ J + B1 >= 0 /\ A + B1 >= 0 /\ -A + B1 >= 0 /\ -A1 >= 0 /\ Z - A1 >= 0 /\ -Z - A1 >= 0 /\ Y - A1 >= 0 /\ -Y - A1 >= 0 /\ X - A1 >= 0 /\ -X - A1 >= 0 /\ W - A1 >= 0 /\ -W - A1 >= 0 /\ V - A1 >= 0 /\ -V - A1 >= 0 /\ U - A1 >= 0 /\ -U - A1 >= 0 /\ T - A1 >= 0 /\ -T - A1 >= 0 /\ B - A1 >= 0 /\ -B - A1 >= 0 /\ S - A1 >= 0 /\ -S - A1 >= 0 /\ R - A1 >= 0 /\ -R - A1 >= 0 /\ Q - A1 >= 0 /\ -Q - A1 >= 0 /\ P - A1 >= 0 /\ -P - A1 >= 0 /\ O - A1 >= 0 /\ -O - A1 >= 0 /\ N - A1 >= 0 /\ M - A1 >= 0 /\ L - A1 >= 0 /\ K - A1 >= 0 /\ J - A1 >= 0 /\ A - A1 >= 0 /\ -A - A1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ -Z + A1 >= 0 /\ Y + A1 >= 0 /\ -Y + A1 >= 0 /\ X + A1 >= 0 /\ -X + A1 >= 0 /\ W + A1 >= 0 /\ -W + A1 >= 0 /\ V + A1 >= 0 /\ -V + A1 >= 0 /\ U + A1 >= 0 /\ -U + A1 >= 0 /\ T + A1 >= 0 /\ -T + A1 >= 0 /\ B + A1 >= 0 /\ -B + A1 >= 0 /\ S + A1 >= 0 /\ -S + A1 >= 0 /\ R + A1 >= 0 /\ -R + A1 >= 0 /\ Q + A1 >= 0 /\ -Q + A1 >= 0 /\ P + A1 >= 0 /\ -P + A1 >= 0 /\ O + A1 >= 0 /\ -O + A1 >= 0 /\ N + A1 >= 0 /\ M + A1 >= 0 /\ L + A1 >= 0 /\ K + A1 >= 0 /\ J + A1 >= 0 /\ A + A1 >= 0 /\ -A + A1 >= 0 /\ -Z >= 0 /\ Y - Z >= 0 /\ -Y - Z >= 0 /\ X - Z >= 0 /\ -X - Z >= 0 /\ W - Z >= 0 /\ -W - Z >= 0 /\ V - Z >= 0 /\ -V - Z >= 0 /\ U - Z >= 0 /\ -U - Z >= 0 /\ T - Z >= 0 /\ -T - Z >= 0 /\ B - Z >= 0 /\ -B - Z >= 0 /\ S - Z >= 0 /\ -S - Z >= 0 /\ R - Z >= 0 /\ -R - Z >= 0 /\ Q - Z >= 0 /\ -Q - Z >= 0 /\ P - Z >= 0 /\ -P - Z >= 0 /\ O - Z >= 0 /\ -O - Z >= 0 /\ N - Z >= 0 /\ M - Z >= 0 /\ L - Z >= 0 /\ K - Z >= 0 /\ J - Z >= 0 /\ A - Z >= 0 /\ -A - Z >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ -Y + Z >= 0 /\ X + Z >= 0 /\ -X + Z >= 0 /\ W + Z >= 0 /\ -W + Z >= 0 /\ V + Z >= 0 /\ -V + Z >= 0 /\ U + Z >= 0 /\ -U + Z >= 0 /\ T + Z >= 0 /\ -T + Z >= 0 /\ B + Z >= 0 /\ -B + Z >= 0 /\ S + Z >= 0 /\ -S + Z >= 0 /\ R + Z >= 0 /\ -R + Z >= 0 /\ Q + Z >= 0 /\ -Q + Z >= 0 /\ P + Z >= 0 /\ -P + Z >= 0 /\ O + Z >= 0 /\ -O + Z >= 0 /\ N + Z >= 0 /\ M + Z >= 0 /\ L + Z >= 0 /\ K + Z >= 0 /\ J + Z >= 0 /\ A + Z >= 0 /\ -A + Z >= 0 /\ -Y >= 0 /\ X - Y >= 0 /\ -X - Y >= 0 /\ W - Y >= 0 /\ -W - Y >= 0 /\ V - Y >= 0 /\ -V - Y >= 0 /\ U - Y >= 0 /\ -U - Y >= 0 /\ T - Y >= 0 /\ -T - Y >= 0 /\ B - Y >= 0 /\ -B - Y >= 0 /\ S - Y >= 0 /\ -S - Y >= 0 /\ R - Y >= 0 /\ -R - Y >= 0 /\ Q - Y >= 0 /\ -Q - Y >= 0 /\ P - Y >= 0 /\ -P - Y >= 0 /\ O - Y >= 0 /\ -O - Y >= 0 /\ N - Y >= 0 /\ M - Y >= 0 /\ L - Y >= 0 /\ K - Y >= 0 /\ J - Y >= 0 /\ A - Y >= 0 /\ -A - Y >= 0 /\ Y >= 0 /\ X + Y >= 0 /\ -X + Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ V + Y >= 0 /\ -V + Y >= 0 /\ U + Y >= 0 /\ -U + Y >= 0 /\ T + Y >= 0 /\ -T + Y >= 0 /\ B + Y >= 0 /\ -B + Y >= 0 /\ S + Y >= 0 /\ -S + Y >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y >= 0 /\ -Q + Y >= 0 /\ P + Y >= 0 /\ -P + Y >= 0 /\ O + Y >= 0 /\ -O + Y >= 0 /\ N + Y >= 0 /\ M + Y >= 0 /\ L + Y >= 0 /\ K + Y >= 0 /\ J + Y >= 0 /\ A + Y >= 0 /\ -A + Y >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ T - X >= 0 /\ -T - X >= 0 /\ B - X >= 0 /\ -B - X >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ O - X >= 0 /\ -O - X >= 0 /\ N - X >= 0 /\ M - X >= 0 /\ L - X >= 0 /\ K - X >= 0 /\ J - X >= 0 /\ A - X >= 0 /\ -A - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ V + X >= 0 /\ -V + X >= 0 /\ U + X >= 0 /\ -U + X >= 0 /\ T + X >= 0 /\ -T + X >= 0 /\ B + X >= 0 /\ -B + X >= 0 /\ S + X >= 0 /\ -S + X >= 0 /\ R + X >= 0 /\ -R + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ O + X >= 0 /\ -O + X >= 0 /\ N + X >= 0 /\ M + X >= 0 /\ L + X >= 0 /\ K + X >= 0 /\ J + X >= 0 /\ A + X >= 0 /\ -A + X >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ U - W >= 0 /\ -U - W >= 0 /\ T - W >= 0 /\ -T - W >= 0 /\ B - W >= 0 /\ -B - W >= 0 /\ S - W >= 0 /\ -S - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ O - W >= 0 /\ -O - W >= 0 /\ N - W >= 0 /\ M - W >= 0 /\ L - W >= 0 /\ K - W >= 0 /\ J - W >= 0 /\ A - W >= 0 /\ -A - W >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ U + W >= 0 /\ -U + W >= 0 /\ T + W >= 0 /\ -T + W >= 0 /\ B + W >= 0 /\ -B + W >= 0 /\ S + W >= 0 /\ -S + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ O + W >= 0 /\ -O + W >= 0 /\ N + W >= 0 /\ M + W >= 0 /\ L + W >= 0 /\ K + W >= 0 /\ J + W >= 0 /\ A + W >= 0 /\ -A + W >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ T - V >= 0 /\ -T - V >= 0 /\ B - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ Q - V >= 0 /\ -Q - V >= 0 /\ P - V >= 0 /\ -P - V >= 0 /\ O - V >= 0 /\ -O - V >= 0 /\ N - V >= 0 /\ M - V >= 0 /\ L - V >= 0 /\ K - V >= 0 /\ J - V >= 0 /\ A - V >= 0 /\ -A - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ T + V >= 0 /\ -T + V >= 0 /\ B + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ Q + V >= 0 /\ -Q + V >= 0 /\ P + V >= 0 /\ -P + V >= 0 /\ O + V >= 0 /\ -O + V >= 0 /\ N + V >= 0 /\ M + V >= 0 /\ L + V >= 0 /\ K + V >= 0 /\ J + V >= 0 /\ A + V >= 0 /\ -A + V >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ B - U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ Q - U >= 0 /\ -Q - U >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ N - U >= 0 /\ M - U >= 0 /\ L - U >= 0 /\ K - U >= 0 /\ J - U >= 0 /\ A - U >= 0 /\ -A - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ B + U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U >= 0 /\ -Q + U >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ N + U >= 0 /\ M + U >= 0 /\ L + U >= 0 /\ K + U >= 0 /\ J + U >= 0 /\ A + U >= 0 /\ -A + U >= 0 /\ -T >= 0 /\ B - T >= 0 /\ -B - T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ Q - T >= 0 /\ -Q - T >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ N - T >= 0 /\ M - T >= 0 /\ L - T >= 0 /\ K - T >= 0 /\ J - T >= 0 /\ A - T >= 0 /\ -A - T >= 0 /\ T >= 0 /\ B + T >= 0 /\ -B + T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ Q + T >= 0 /\ -Q + T >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ N + T >= 0 /\ M + T >= 0 /\ L + T >= 0 /\ K + T >= 0 /\ J + T >= 0 /\ A + T >= 0 /\ -A + T >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ Q - B >= 0 /\ -Q - B >= 0 /\ P - B >= 0 /\ -P - B >= 0 /\ O - B >= 0 /\ -O - B >= 0 /\ N - B >= 0 /\ M - B >= 0 /\ L - B >= 0 /\ K - B >= 0 /\ J - B >= 0 /\ A - B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ S + B >= 0 /\ -S + B >= 0 /\ R + B >= 0 /\ -R + B >= 0 /\ Q + B >= 0 /\ -Q + B >= 0 /\ P + B >= 0 /\ -P + B >= 0 /\ O + B >= 0 /\ -O + B >= 0 /\ N + B >= 0 /\ M + B >= 0 /\ L + B >= 0 /\ K + B >= 0 /\ J + B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ Q - S >= 0 /\ -Q - S >= 0 /\ P - S >= 0 /\ -P - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ N - S >= 0 /\ M - S >= 0 /\ L - S >= 0 /\ K - S >= 0 /\ J - S >= 0 /\ A - S >= 0 /\ -A - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ Q + S >= 0 /\ -Q + S >= 0 /\ P + S >= 0 /\ -P + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ N + S >= 0 /\ M + S >= 0 /\ L + S >= 0 /\ K + S >= 0 /\ J + S >= 0 /\ A + S >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R >= 0 /\ -Q - R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ N - R >= 0 /\ M - R >= 0 /\ L - R >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ A - R >= 0 /\ -A - R >= 0 /\ R >= 0 /\ Q + R >= 0 /\ -Q + R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ N + R >= 0 /\ M + R >= 0 /\ L + R >= 0 /\ K + R >= 0 /\ J + R >= 0 /\ A + R >= 0 /\ -A + R >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ O - Q >= 0 /\ -O - Q >= 0 /\ N - Q >= 0 /\ M - Q >= 0 /\ L - Q >= 0 /\ K - Q >= 0 /\ J - Q >= 0 /\ A - Q >= 0 /\ -A - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ O + Q >= 0 /\ -O + Q >= 0 /\ N + Q >= 0 /\ M + Q >= 0 /\ L + Q >= 0 /\ K + Q >= 0 /\ J + Q >= 0 /\ A + Q >= 0 /\ -A + Q >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ N - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ K - P >= 0 /\ J - P >= 0 /\ A - P >= 0 /\ -A - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ N + P >= 0 /\ M + P >= 0 /\ L + P >= 0 /\ K + P >= 0 /\ J + P >= 0 /\ A + P >= 0 /\ -A + P >= 0 /\ -O >= 0 /\ N - O >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ A - O >= 0 /\ -A - O >= 0 /\ O >= 0 /\ N + O >= 0 /\ M + O >= 0 /\ L + O >= 0 /\ K + O >= 0 /\ J + O >= 0 /\ A + O >= 0 /\ -A + O >= 0 /\ N >= 0 /\ M + N >= 0 /\ L + N >= 0 /\ K + N >= 0 /\ J + N >= 0 /\ A + N >= 0 /\ -A + N >= 0 /\ M >= 0 /\ L + M >= 0 /\ K + M >= 0 /\ J + M >= 0 /\ A + M >= 0 /\ -A + M >= 0 /\ J - L >= 0 /\ L >= 0 /\ K + L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L >= 0 /\ -A + L >= 0 /\ K >= 0 /\ J + K >= 0 /\ A + K >= 0 /\ -A + K >= 0 /\ J >= 0 /\ A + J >= 0 /\ -A + J >= 0 /\ -A >= 0 /\ A >= 0 /\ H + D >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f2(A, B, C, I + D - 1, K + E, M + F, N + G, H, 0, J + 1, 0, L + 1, 0, 0, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I >= 0 /\ H - I >= 0 /\ -H - I >= 0 /\ G - I - 1 >= 0 /\ F - I >= 0 /\ E - I >= 0 /\ D - I >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ B1 - I >= 0 /\ -B1 - I >= 0 /\ A1 - I >= 0 /\ -A1 - I >= 0 /\ Z - I >= 0 /\ -Z - I >= 0 /\ Y - I >= 0 /\ -Y - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ W - I >= 0 /\ -W - I >= 0 /\ V - I >= 0 /\ -V - I >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ B - I >= 0 /\ -B - I >= 0 /\ S - I >= 0 /\ -S - I >= 0 /\ R - I >= 0 /\ -R - I >= 0 /\ Q - I >= 0 /\ -Q - I >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I >= 0 /\ M - I >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ J - I >= 0 /\ A - I >= 0 /\ -A - I >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ B1 + I >= 0 /\ -B1 + I >= 0 /\ A1 + I >= 0 /\ -A1 + I >= 0 /\ Z + I >= 0 /\ -Z + I >= 0 /\ Y + I >= 0 /\ -Y + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ W + I >= 0 /\ -W + I >= 0 /\ V + I >= 0 /\ -V + I >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ S + I >= 0 /\ -S + I >= 0 /\ R + I >= 0 /\ -R + I >= 0 /\ Q + I >= 0 /\ -Q + I >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I >= 0 /\ M + I >= 0 /\ L + I >= 0 /\ K + I >= 0 /\ J + I >= 0 /\ A + I >= 0 /\ -A + I >= 0 /\ -H >= 0 /\ G - H - 1 >= 0 /\ F - H >= 0 /\ E - H >= 0 /\ D - H >= 0 /\ C - H >= 0 /\ -C - H >= 0 /\ B1 - H >= 0 /\ -B1 - H >= 0 /\ A1 - H >= 0 /\ -A1 - H >= 0 /\ Z - H >= 0 /\ -Z - H >= 0 /\ Y - H >= 0 /\ -Y - H >= 0 /\ X - H >= 0 /\ -X - H >= 0 /\ W - H >= 0 /\ -W - H >= 0 /\ V - H >= 0 /\ -V - H >= 0 /\ U - H >= 0 /\ -U - H >= 0 /\ T - H >= 0 /\ -T - H >= 0 /\ B - H >= 0 /\ -B - H >= 0 /\ S - H >= 0 /\ -S - H >= 0 /\ R - H >= 0 /\ -R - H >= 0 /\ Q - H >= 0 /\ -Q - H >= 0 /\ P - H >= 0 /\ -P - H >= 0 /\ O - H >= 0 /\ -O - H >= 0 /\ N - H >= 0 /\ M - H >= 0 /\ L - H >= 0 /\ K - H >= 0 /\ J - H >= 0 /\ A - H >= 0 /\ -A - H >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B1 + H >= 0 /\ -B1 + H >= 0 /\ A1 + H >= 0 /\ -A1 + H >= 0 /\ Z + H >= 0 /\ -Z + H >= 0 /\ Y + H >= 0 /\ -Y + H >= 0 /\ X + H >= 0 /\ -X + H >= 0 /\ W + H >= 0 /\ -W + H >= 0 /\ V + H >= 0 /\ -V + H >= 0 /\ U + H >= 0 /\ -U + H >= 0 /\ T + H >= 0 /\ -T + H >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ S + H >= 0 /\ -S + H >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ Q + H >= 0 /\ -Q + H >= 0 /\ P + H >= 0 /\ -P + H >= 0 /\ O + H >= 0 /\ -O + H >= 0 /\ N + H >= 0 /\ M + H >= 0 /\ L + H >= 0 /\ K + H >= 0 /\ J + H >= 0 /\ A + H >= 0 /\ -A + H >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 1 >= 0 /\ -C + G - 1 >= 0 /\ B1 + G - 1 >= 0 /\ -B1 + G - 1 >= 0 /\ A1 + G - 1 >= 0 /\ -A1 + G - 1 >= 0 /\ Z + G - 1 >= 0 /\ -Z + G - 1 >= 0 /\ Y + G - 1 >= 0 /\ -Y + G - 1 >= 0 /\ X + G - 1 >= 0 /\ -X + G - 1 >= 0 /\ W + G - 1 >= 0 /\ -W + G - 1 >= 0 /\ V + G - 1 >= 0 /\ -V + G - 1 >= 0 /\ U + G - 1 >= 0 /\ -U + G - 1 >= 0 /\ T + G - 1 >= 0 /\ -T + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G - 1 >= 0 /\ S + G - 1 >= 0 /\ -S + G - 1 >= 0 /\ R + G - 1 >= 0 /\ -R + G - 1 >= 0 /\ Q + G - 1 >= 0 /\ -Q + G - 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G - 1 >= 0 /\ O + G - 1 >= 0 /\ -O + G - 1 >= 0 /\ N + G - 1 >= 0 /\ M + G - 1 >= 0 /\ L + G - 1 >= 0 /\ K + G - 1 >= 0 /\ J + G - 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ C + F >= 0 /\ -C + F >= 0 /\ B1 + F >= 0 /\ -B1 + F >= 0 /\ A1 + F >= 0 /\ -A1 + F >= 0 /\ Z + F >= 0 /\ -Z + F >= 0 /\ Y + F >= 0 /\ -Y + F >= 0 /\ X + F >= 0 /\ -X + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ U + F >= 0 /\ -U + F >= 0 /\ T + F >= 0 /\ -T + F >= 0 /\ B + F >= 0 /\ -B + F >= 0 /\ S + F >= 0 /\ -S + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ Q + F >= 0 /\ -Q + F >= 0 /\ P + F >= 0 /\ -P + F >= 0 /\ O + F >= 0 /\ -O + F >= 0 /\ N + F >= 0 /\ M + F >= 0 /\ L + F >= 0 /\ K + F >= 0 /\ J + F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B1 + E >= 0 /\ -B1 + E >= 0 /\ A1 + E >= 0 /\ -A1 + E >= 0 /\ Z + E >= 0 /\ -Z + E >= 0 /\ Y + E >= 0 /\ -Y + E >= 0 /\ X + E >= 0 /\ -X + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ V + E >= 0 /\ -V + E >= 0 /\ U + E >= 0 /\ -U + E >= 0 /\ T + E >= 0 /\ -T + E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ S + E >= 0 /\ -S + E >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E >= 0 /\ -Q + E >= 0 /\ P + E >= 0 /\ -P + E >= 0 /\ O + E >= 0 /\ -O + E >= 0 /\ N + E >= 0 /\ M + E >= 0 /\ L + E >= 0 /\ K + E >= 0 /\ J + E >= 0 /\ A + E >= 0 /\ -A + E >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B1 + D >= 0 /\ -B1 + D >= 0 /\ A1 + D >= 0 /\ -A1 + D >= 0 /\ Z + D >= 0 /\ -Z + D >= 0 /\ Y + D >= 0 /\ -Y + D >= 0 /\ X + D >= 0 /\ -X + D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ V + D >= 0 /\ -V + D >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ T + D >= 0 /\ -T + D >= 0 /\ B + D >= 0 /\ -B + D >= 0 /\ S + D >= 0 /\ -S + D >= 0 /\ R + D >= 0 /\ -R + D >= 0 /\ Q + D >= 0 /\ -Q + D >= 0 /\ P + D >= 0 /\ -P + D >= 0 /\ O + D >= 0 /\ -O + D >= 0 /\ N + D >= 0 /\ M + D >= 0 /\ L + D >= 0 /\ K + D >= 0 /\ J + D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B1 - C >= 0 /\ -B1 - C >= 0 /\ A1 - C >= 0 /\ -A1 - C >= 0 /\ Z - C >= 0 /\ -Z - C >= 0 /\ Y - C >= 0 /\ -Y - C >= 0 /\ X - C >= 0 /\ -X - C >= 0 /\ W - C >= 0 /\ -W - C >= 0 /\ V - C >= 0 /\ -V - C >= 0 /\ U - C >= 0 /\ -U - C >= 0 /\ T - C >= 0 /\ -T - C >= 0 /\ B - C >= 0 /\ -B - C >= 0 /\ S - C >= 0 /\ -S - C >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C >= 0 /\ -Q - C >= 0 /\ P - C >= 0 /\ -P - C >= 0 /\ O - C >= 0 /\ -O - C >= 0 /\ N - C >= 0 /\ M - C >= 0 /\ L - C >= 0 /\ K - C >= 0 /\ J - C >= 0 /\ A - C >= 0 /\ -A - C >= 0 /\ C >= 0 /\ B1 + C >= 0 /\ -B1 + C >= 0 /\ A1 + C >= 0 /\ -A1 + C >= 0 /\ Z + C >= 0 /\ -Z + C >= 0 /\ Y + C >= 0 /\ -Y + C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ V + C >= 0 /\ -V + C >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ P + C >= 0 /\ -P + C >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C >= 0 /\ M + C >= 0 /\ L + C >= 0 /\ K + C >= 0 /\ J + C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ -B1 >= 0 /\ A1 - B1 >= 0 /\ -A1 - B1 >= 0 /\ Z - B1 >= 0 /\ -Z - B1 >= 0 /\ Y - B1 >= 0 /\ -Y - B1 >= 0 /\ X - B1 >= 0 /\ -X - B1 >= 0 /\ W - B1 >= 0 /\ -W - B1 >= 0 /\ V - B1 >= 0 /\ -V - B1 >= 0 /\ U - B1 >= 0 /\ -U - B1 >= 0 /\ T - B1 >= 0 /\ -T - B1 >= 0 /\ B - B1 >= 0 /\ -B - B1 >= 0 /\ S - B1 >= 0 /\ -S - B1 >= 0 /\ R - B1 >= 0 /\ -R - B1 >= 0 /\ Q - B1 >= 0 /\ -Q - B1 >= 0 /\ P - B1 >= 0 /\ -P - B1 >= 0 /\ O - B1 >= 0 /\ -O - B1 >= 0 /\ N - B1 >= 0 /\ M - B1 >= 0 /\ L - B1 >= 0 /\ K - B1 >= 0 /\ J - B1 >= 0 /\ A - B1 >= 0 /\ -A - B1 >= 0 /\ B1 >= 0 /\ A1 + B1 >= 0 /\ -A1 + B1 >= 0 /\ Z + B1 >= 0 /\ -Z + B1 >= 0 /\ Y + B1 >= 0 /\ -Y + B1 >= 0 /\ X + B1 >= 0 /\ -X + B1 >= 0 /\ W + B1 >= 0 /\ -W + B1 >= 0 /\ V + B1 >= 0 /\ -V + B1 >= 0 /\ U + B1 >= 0 /\ -U + B1 >= 0 /\ T + B1 >= 0 /\ -T + B1 >= 0 /\ B + B1 >= 0 /\ -B + B1 >= 0 /\ S + B1 >= 0 /\ -S + B1 >= 0 /\ R + B1 >= 0 /\ -R + B1 >= 0 /\ Q + B1 >= 0 /\ -Q + B1 >= 0 /\ P + B1 >= 0 /\ -P + B1 >= 0 /\ O + B1 >= 0 /\ -O + B1 >= 0 /\ N + B1 >= 0 /\ M + B1 >= 0 /\ L + B1 >= 0 /\ K + B1 >= 0 /\ J + B1 >= 0 /\ A + B1 >= 0 /\ -A + B1 >= 0 /\ -A1 >= 0 /\ Z - A1 >= 0 /\ -Z - A1 >= 0 /\ Y - A1 >= 0 /\ -Y - A1 >= 0 /\ X - A1 >= 0 /\ -X - A1 >= 0 /\ W - A1 >= 0 /\ -W - A1 >= 0 /\ V - A1 >= 0 /\ -V - A1 >= 0 /\ U - A1 >= 0 /\ -U - A1 >= 0 /\ T - A1 >= 0 /\ -T - A1 >= 0 /\ B - A1 >= 0 /\ -B - A1 >= 0 /\ S - A1 >= 0 /\ -S - A1 >= 0 /\ R - A1 >= 0 /\ -R - A1 >= 0 /\ Q - A1 >= 0 /\ -Q - A1 >= 0 /\ P - A1 >= 0 /\ -P - A1 >= 0 /\ O - A1 >= 0 /\ -O - A1 >= 0 /\ N - A1 >= 0 /\ M - A1 >= 0 /\ L - A1 >= 0 /\ K - A1 >= 0 /\ J - A1 >= 0 /\ A - A1 >= 0 /\ -A - A1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ -Z + A1 >= 0 /\ Y + A1 >= 0 /\ -Y + A1 >= 0 /\ X + A1 >= 0 /\ -X + A1 >= 0 /\ W + A1 >= 0 /\ -W + A1 >= 0 /\ V + A1 >= 0 /\ -V + A1 >= 0 /\ U + A1 >= 0 /\ -U + A1 >= 0 /\ T + A1 >= 0 /\ -T + A1 >= 0 /\ B + A1 >= 0 /\ -B + A1 >= 0 /\ S + A1 >= 0 /\ -S + A1 >= 0 /\ R + A1 >= 0 /\ -R + A1 >= 0 /\ Q + A1 >= 0 /\ -Q + A1 >= 0 /\ P + A1 >= 0 /\ -P + A1 >= 0 /\ O + A1 >= 0 /\ -O + A1 >= 0 /\ N + A1 >= 0 /\ M + A1 >= 0 /\ L + A1 >= 0 /\ K + A1 >= 0 /\ J + A1 >= 0 /\ A + A1 >= 0 /\ -A + A1 >= 0 /\ -Z >= 0 /\ Y - Z >= 0 /\ -Y - Z >= 0 /\ X - Z >= 0 /\ -X - Z >= 0 /\ W - Z >= 0 /\ -W - Z >= 0 /\ V - Z >= 0 /\ -V - Z >= 0 /\ U - Z >= 0 /\ -U - Z >= 0 /\ T - Z >= 0 /\ -T - Z >= 0 /\ B - Z >= 0 /\ -B - Z >= 0 /\ S - Z >= 0 /\ -S - Z >= 0 /\ R - Z >= 0 /\ -R - Z >= 0 /\ Q - Z >= 0 /\ -Q - Z >= 0 /\ P - Z >= 0 /\ -P - Z >= 0 /\ O - Z >= 0 /\ -O - Z >= 0 /\ N - Z >= 0 /\ M - Z >= 0 /\ L - Z >= 0 /\ K - Z >= 0 /\ J - Z >= 0 /\ A - Z >= 0 /\ -A - Z >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ -Y + Z >= 0 /\ X + Z >= 0 /\ -X + Z >= 0 /\ W + Z >= 0 /\ -W + Z >= 0 /\ V + Z >= 0 /\ -V + Z >= 0 /\ U + Z >= 0 /\ -U + Z >= 0 /\ T + Z >= 0 /\ -T + Z >= 0 /\ B + Z >= 0 /\ -B + Z >= 0 /\ S + Z >= 0 /\ -S + Z >= 0 /\ R + Z >= 0 /\ -R + Z >= 0 /\ Q + Z >= 0 /\ -Q + Z >= 0 /\ P + Z >= 0 /\ -P + Z >= 0 /\ O + Z >= 0 /\ -O + Z >= 0 /\ N + Z >= 0 /\ M + Z >= 0 /\ L + Z >= 0 /\ K + Z >= 0 /\ J + Z >= 0 /\ A + Z >= 0 /\ -A + Z >= 0 /\ -Y >= 0 /\ X - Y >= 0 /\ -X - Y >= 0 /\ W - Y >= 0 /\ -W - Y >= 0 /\ V - Y >= 0 /\ -V - Y >= 0 /\ U - Y >= 0 /\ -U - Y >= 0 /\ T - Y >= 0 /\ -T - Y >= 0 /\ B - Y >= 0 /\ -B - Y >= 0 /\ S - Y >= 0 /\ -S - Y >= 0 /\ R - Y >= 0 /\ -R - Y >= 0 /\ Q - Y >= 0 /\ -Q - Y >= 0 /\ P - Y >= 0 /\ -P - Y >= 0 /\ O - Y >= 0 /\ -O - Y >= 0 /\ N - Y >= 0 /\ M - Y >= 0 /\ L - Y >= 0 /\ K - Y >= 0 /\ J - Y >= 0 /\ A - Y >= 0 /\ -A - Y >= 0 /\ Y >= 0 /\ X + Y >= 0 /\ -X + Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ V + Y >= 0 /\ -V + Y >= 0 /\ U + Y >= 0 /\ -U + Y >= 0 /\ T + Y >= 0 /\ -T + Y >= 0 /\ B + Y >= 0 /\ -B + Y >= 0 /\ S + Y >= 0 /\ -S + Y >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y >= 0 /\ -Q + Y >= 0 /\ P + Y >= 0 /\ -P + Y >= 0 /\ O + Y >= 0 /\ -O + Y >= 0 /\ N + Y >= 0 /\ M + Y >= 0 /\ L + Y >= 0 /\ K + Y >= 0 /\ J + Y >= 0 /\ A + Y >= 0 /\ -A + Y >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ T - X >= 0 /\ -T - X >= 0 /\ B - X >= 0 /\ -B - X >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ O - X >= 0 /\ -O - X >= 0 /\ N - X >= 0 /\ M - X >= 0 /\ L - X >= 0 /\ K - X >= 0 /\ J - X >= 0 /\ A - X >= 0 /\ -A - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ V + X >= 0 /\ -V + X >= 0 /\ U + X >= 0 /\ -U + X >= 0 /\ T + X >= 0 /\ -T + X >= 0 /\ B + X >= 0 /\ -B + X >= 0 /\ S + X >= 0 /\ -S + X >= 0 /\ R + X >= 0 /\ -R + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ O + X >= 0 /\ -O + X >= 0 /\ N + X >= 0 /\ M + X >= 0 /\ L + X >= 0 /\ K + X >= 0 /\ J + X >= 0 /\ A + X >= 0 /\ -A + X >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ U - W >= 0 /\ -U - W >= 0 /\ T - W >= 0 /\ -T - W >= 0 /\ B - W >= 0 /\ -B - W >= 0 /\ S - W >= 0 /\ -S - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ O - W >= 0 /\ -O - W >= 0 /\ N - W >= 0 /\ M - W >= 0 /\ L - W >= 0 /\ K - W >= 0 /\ J - W >= 0 /\ A - W >= 0 /\ -A - W >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ U + W >= 0 /\ -U + W >= 0 /\ T + W >= 0 /\ -T + W >= 0 /\ B + W >= 0 /\ -B + W >= 0 /\ S + W >= 0 /\ -S + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ O + W >= 0 /\ -O + W >= 0 /\ N + W >= 0 /\ M + W >= 0 /\ L + W >= 0 /\ K + W >= 0 /\ J + W >= 0 /\ A + W >= 0 /\ -A + W >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ T - V >= 0 /\ -T - V >= 0 /\ B - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ Q - V >= 0 /\ -Q - V >= 0 /\ P - V >= 0 /\ -P - V >= 0 /\ O - V >= 0 /\ -O - V >= 0 /\ N - V >= 0 /\ M - V >= 0 /\ L - V >= 0 /\ K - V >= 0 /\ J - V >= 0 /\ A - V >= 0 /\ -A - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ T + V >= 0 /\ -T + V >= 0 /\ B + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ Q + V >= 0 /\ -Q + V >= 0 /\ P + V >= 0 /\ -P + V >= 0 /\ O + V >= 0 /\ -O + V >= 0 /\ N + V >= 0 /\ M + V >= 0 /\ L + V >= 0 /\ K + V >= 0 /\ J + V >= 0 /\ A + V >= 0 /\ -A + V >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ B - U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ Q - U >= 0 /\ -Q - U >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ N - U >= 0 /\ M - U >= 0 /\ L - U >= 0 /\ K - U >= 0 /\ J - U >= 0 /\ A - U >= 0 /\ -A - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ B + U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U >= 0 /\ -Q + U >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ N + U >= 0 /\ M + U >= 0 /\ L + U >= 0 /\ K + U >= 0 /\ J + U >= 0 /\ A + U >= 0 /\ -A + U >= 0 /\ -T >= 0 /\ B - T >= 0 /\ -B - T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ Q - T >= 0 /\ -Q - T >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ N - T >= 0 /\ M - T >= 0 /\ L - T >= 0 /\ K - T >= 0 /\ J - T >= 0 /\ A - T >= 0 /\ -A - T >= 0 /\ T >= 0 /\ B + T >= 0 /\ -B + T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ Q + T >= 0 /\ -Q + T >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ N + T >= 0 /\ M + T >= 0 /\ L + T >= 0 /\ K + T >= 0 /\ J + T >= 0 /\ A + T >= 0 /\ -A + T >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ Q - B >= 0 /\ -Q - B >= 0 /\ P - B >= 0 /\ -P - B >= 0 /\ O - B >= 0 /\ -O - B >= 0 /\ N - B >= 0 /\ M - B >= 0 /\ L - B >= 0 /\ K - B >= 0 /\ J - B >= 0 /\ A - B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ S + B >= 0 /\ -S + B >= 0 /\ R + B >= 0 /\ -R + B >= 0 /\ Q + B >= 0 /\ -Q + B >= 0 /\ P + B >= 0 /\ -P + B >= 0 /\ O + B >= 0 /\ -O + B >= 0 /\ N + B >= 0 /\ M + B >= 0 /\ L + B >= 0 /\ K + B >= 0 /\ J + B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ Q - S >= 0 /\ -Q - S >= 0 /\ P - S >= 0 /\ -P - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ N - S >= 0 /\ M - S >= 0 /\ L - S >= 0 /\ K - S >= 0 /\ J - S >= 0 /\ A - S >= 0 /\ -A - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ Q + S >= 0 /\ -Q + S >= 0 /\ P + S >= 0 /\ -P + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ N + S >= 0 /\ M + S >= 0 /\ L + S >= 0 /\ K + S >= 0 /\ J + S >= 0 /\ A + S >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R >= 0 /\ -Q - R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ N - R >= 0 /\ M - R >= 0 /\ L - R >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ A - R >= 0 /\ -A - R >= 0 /\ R >= 0 /\ Q + R >= 0 /\ -Q + R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ N + R >= 0 /\ M + R >= 0 /\ L + R >= 0 /\ K + R >= 0 /\ J + R >= 0 /\ A + R >= 0 /\ -A + R >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ O - Q >= 0 /\ -O - Q >= 0 /\ N - Q >= 0 /\ M - Q >= 0 /\ L - Q >= 0 /\ K - Q >= 0 /\ J - Q >= 0 /\ A - Q >= 0 /\ -A - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ O + Q >= 0 /\ -O + Q >= 0 /\ N + Q >= 0 /\ M + Q >= 0 /\ L + Q >= 0 /\ K + Q >= 0 /\ J + Q >= 0 /\ A + Q >= 0 /\ -A + Q >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ N - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ K - P >= 0 /\ J - P >= 0 /\ A - P >= 0 /\ -A - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ N + P >= 0 /\ M + P >= 0 /\ L + P >= 0 /\ K + P >= 0 /\ J + P >= 0 /\ A + P >= 0 /\ -A + P >= 0 /\ -O >= 0 /\ N - O >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ A - O >= 0 /\ -A - O >= 0 /\ O >= 0 /\ N + O >= 0 /\ M + O >= 0 /\ L + O >= 0 /\ K + O >= 0 /\ J + O >= 0 /\ A + O >= 0 /\ -A + O >= 0 /\ N >= 0 /\ M + N >= 0 /\ L + N >= 0 /\ K + N >= 0 /\ J + N >= 0 /\ A + N >= 0 /\ -A + N >= 0 /\ M >= 0 /\ L + M >= 0 /\ K + M >= 0 /\ J + M >= 0 /\ A + M >= 0 /\ -A + M >= 0 /\ J - L >= 0 /\ L >= 0 /\ K + L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L >= 0 /\ -A + L >= 0 /\ K >= 0 /\ J + K >= 0 /\ A + K >= 0 /\ -A + K >= 0 /\ J >= 0 /\ A + J >= 0 /\ -A + J >= 0 /\ -A >= 0 /\ A >= 0 /\ D >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f1(A + L + 1, B + J + 1, C + I + D - 1, 0, 0, 0, 0, H, 0, 0, K + E, 0, M + F, N + G, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I >= 0 /\ H - I >= 0 /\ -H - I >= 0 /\ G - I - 1 >= 0 /\ F - I >= 0 /\ E - I >= 0 /\ D - I >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ B1 - I >= 0 /\ -B1 - I >= 0 /\ A1 - I >= 0 /\ -A1 - I >= 0 /\ Z - I >= 0 /\ -Z - I >= 0 /\ Y - I >= 0 /\ -Y - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ W - I >= 0 /\ -W - I >= 0 /\ V - I >= 0 /\ -V - I >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ B - I >= 0 /\ -B - I >= 0 /\ S - I >= 0 /\ -S - I >= 0 /\ R - I >= 0 /\ -R - I >= 0 /\ Q - I >= 0 /\ -Q - I >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I >= 0 /\ M - I >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ J - I >= 0 /\ A - I >= 0 /\ -A - I >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ B1 + I >= 0 /\ -B1 + I >= 0 /\ A1 + I >= 0 /\ -A1 + I >= 0 /\ Z + I >= 0 /\ -Z + I >= 0 /\ Y + I >= 0 /\ -Y + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ W + I >= 0 /\ -W + I >= 0 /\ V + I >= 0 /\ -V + I >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ S + I >= 0 /\ -S + I >= 0 /\ R + I >= 0 /\ -R + I >= 0 /\ Q + I >= 0 /\ -Q + I >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I >= 0 /\ M + I >= 0 /\ L + I >= 0 /\ K + I >= 0 /\ J + I >= 0 /\ A + I >= 0 /\ -A + I >= 0 /\ -H >= 0 /\ G - H - 1 >= 0 /\ F - H >= 0 /\ E - H >= 0 /\ D - H >= 0 /\ C - H >= 0 /\ -C - H >= 0 /\ B1 - H >= 0 /\ -B1 - H >= 0 /\ A1 - H >= 0 /\ -A1 - H >= 0 /\ Z - H >= 0 /\ -Z - H >= 0 /\ Y - H >= 0 /\ -Y - H >= 0 /\ X - H >= 0 /\ -X - H >= 0 /\ W - H >= 0 /\ -W - H >= 0 /\ V - H >= 0 /\ -V - H >= 0 /\ U - H >= 0 /\ -U - H >= 0 /\ T - H >= 0 /\ -T - H >= 0 /\ B - H >= 0 /\ -B - H >= 0 /\ S - H >= 0 /\ -S - H >= 0 /\ R - H >= 0 /\ -R - H >= 0 /\ Q - H >= 0 /\ -Q - H >= 0 /\ P - H >= 0 /\ -P - H >= 0 /\ O - H >= 0 /\ -O - H >= 0 /\ N - H >= 0 /\ M - H >= 0 /\ L - H >= 0 /\ K - H >= 0 /\ J - H >= 0 /\ A - H >= 0 /\ -A - H >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B1 + H >= 0 /\ -B1 + H >= 0 /\ A1 + H >= 0 /\ -A1 + H >= 0 /\ Z + H >= 0 /\ -Z + H >= 0 /\ Y + H >= 0 /\ -Y + H >= 0 /\ X + H >= 0 /\ -X + H >= 0 /\ W + H >= 0 /\ -W + H >= 0 /\ V + H >= 0 /\ -V + H >= 0 /\ U + H >= 0 /\ -U + H >= 0 /\ T + H >= 0 /\ -T + H >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ S + H >= 0 /\ -S + H >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ Q + H >= 0 /\ -Q + H >= 0 /\ P + H >= 0 /\ -P + H >= 0 /\ O + H >= 0 /\ -O + H >= 0 /\ N + H >= 0 /\ M + H >= 0 /\ L + H >= 0 /\ K + H >= 0 /\ J + H >= 0 /\ A + H >= 0 /\ -A + H >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 1 >= 0 /\ -C + G - 1 >= 0 /\ B1 + G - 1 >= 0 /\ -B1 + G - 1 >= 0 /\ A1 + G - 1 >= 0 /\ -A1 + G - 1 >= 0 /\ Z + G - 1 >= 0 /\ -Z + G - 1 >= 0 /\ Y + G - 1 >= 0 /\ -Y + G - 1 >= 0 /\ X + G - 1 >= 0 /\ -X + G - 1 >= 0 /\ W + G - 1 >= 0 /\ -W + G - 1 >= 0 /\ V + G - 1 >= 0 /\ -V + G - 1 >= 0 /\ U + G - 1 >= 0 /\ -U + G - 1 >= 0 /\ T + G - 1 >= 0 /\ -T + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G - 1 >= 0 /\ S + G - 1 >= 0 /\ -S + G - 1 >= 0 /\ R + G - 1 >= 0 /\ -R + G - 1 >= 0 /\ Q + G - 1 >= 0 /\ -Q + G - 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G - 1 >= 0 /\ O + G - 1 >= 0 /\ -O + G - 1 >= 0 /\ N + G - 1 >= 0 /\ M + G - 1 >= 0 /\ L + G - 1 >= 0 /\ K + G - 1 >= 0 /\ J + G - 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ C + F >= 0 /\ -C + F >= 0 /\ B1 + F >= 0 /\ -B1 + F >= 0 /\ A1 + F >= 0 /\ -A1 + F >= 0 /\ Z + F >= 0 /\ -Z + F >= 0 /\ Y + F >= 0 /\ -Y + F >= 0 /\ X + F >= 0 /\ -X + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ U + F >= 0 /\ -U + F >= 0 /\ T + F >= 0 /\ -T + F >= 0 /\ B + F >= 0 /\ -B + F >= 0 /\ S + F >= 0 /\ -S + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ Q + F >= 0 /\ -Q + F >= 0 /\ P + F >= 0 /\ -P + F >= 0 /\ O + F >= 0 /\ -O + F >= 0 /\ N + F >= 0 /\ M + F >= 0 /\ L + F >= 0 /\ K + F >= 0 /\ J + F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B1 + E >= 0 /\ -B1 + E >= 0 /\ A1 + E >= 0 /\ -A1 + E >= 0 /\ Z + E >= 0 /\ -Z + E >= 0 /\ Y + E >= 0 /\ -Y + E >= 0 /\ X + E >= 0 /\ -X + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ V + E >= 0 /\ -V + E >= 0 /\ U + E >= 0 /\ -U + E >= 0 /\ T + E >= 0 /\ -T + E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ S + E >= 0 /\ -S + E >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E >= 0 /\ -Q + E >= 0 /\ P + E >= 0 /\ -P + E >= 0 /\ O + E >= 0 /\ -O + E >= 0 /\ N + E >= 0 /\ M + E >= 0 /\ L + E >= 0 /\ K + E >= 0 /\ J + E >= 0 /\ A + E >= 0 /\ -A + E >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B1 + D >= 0 /\ -B1 + D >= 0 /\ A1 + D >= 0 /\ -A1 + D >= 0 /\ Z + D >= 0 /\ -Z + D >= 0 /\ Y + D >= 0 /\ -Y + D >= 0 /\ X + D >= 0 /\ -X + D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ V + D >= 0 /\ -V + D >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ T + D >= 0 /\ -T + D >= 0 /\ B + D >= 0 /\ -B + D >= 0 /\ S + D >= 0 /\ -S + D >= 0 /\ R + D >= 0 /\ -R + D >= 0 /\ Q + D >= 0 /\ -Q + D >= 0 /\ P + D >= 0 /\ -P + D >= 0 /\ O + D >= 0 /\ -O + D >= 0 /\ N + D >= 0 /\ M + D >= 0 /\ L + D >= 0 /\ K + D >= 0 /\ J + D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B1 - C >= 0 /\ -B1 - C >= 0 /\ A1 - C >= 0 /\ -A1 - C >= 0 /\ Z - C >= 0 /\ -Z - C >= 0 /\ Y - C >= 0 /\ -Y - C >= 0 /\ X - C >= 0 /\ -X - C >= 0 /\ W - C >= 0 /\ -W - C >= 0 /\ V - C >= 0 /\ -V - C >= 0 /\ U - C >= 0 /\ -U - C >= 0 /\ T - C >= 0 /\ -T - C >= 0 /\ B - C >= 0 /\ -B - C >= 0 /\ S - C >= 0 /\ -S - C >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C >= 0 /\ -Q - C >= 0 /\ P - C >= 0 /\ -P - C >= 0 /\ O - C >= 0 /\ -O - C >= 0 /\ N - C >= 0 /\ M - C >= 0 /\ L - C >= 0 /\ K - C >= 0 /\ J - C >= 0 /\ A - C >= 0 /\ -A - C >= 0 /\ C >= 0 /\ B1 + C >= 0 /\ -B1 + C >= 0 /\ A1 + C >= 0 /\ -A1 + C >= 0 /\ Z + C >= 0 /\ -Z + C >= 0 /\ Y + C >= 0 /\ -Y + C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ V + C >= 0 /\ -V + C >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ P + C >= 0 /\ -P + C >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C >= 0 /\ M + C >= 0 /\ L + C >= 0 /\ K + C >= 0 /\ J + C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ -B1 >= 0 /\ A1 - B1 >= 0 /\ -A1 - B1 >= 0 /\ Z - B1 >= 0 /\ -Z - B1 >= 0 /\ Y - B1 >= 0 /\ -Y - B1 >= 0 /\ X - B1 >= 0 /\ -X - B1 >= 0 /\ W - B1 >= 0 /\ -W - B1 >= 0 /\ V - B1 >= 0 /\ -V - B1 >= 0 /\ U - B1 >= 0 /\ -U - B1 >= 0 /\ T - B1 >= 0 /\ -T - B1 >= 0 /\ B - B1 >= 0 /\ -B - B1 >= 0 /\ S - B1 >= 0 /\ -S - B1 >= 0 /\ R - B1 >= 0 /\ -R - B1 >= 0 /\ Q - B1 >= 0 /\ -Q - B1 >= 0 /\ P - B1 >= 0 /\ -P - B1 >= 0 /\ O - B1 >= 0 /\ -O - B1 >= 0 /\ N - B1 >= 0 /\ M - B1 >= 0 /\ L - B1 >= 0 /\ K - B1 >= 0 /\ J - B1 >= 0 /\ A - B1 >= 0 /\ -A - B1 >= 0 /\ B1 >= 0 /\ A1 + B1 >= 0 /\ -A1 + B1 >= 0 /\ Z + B1 >= 0 /\ -Z + B1 >= 0 /\ Y + B1 >= 0 /\ -Y + B1 >= 0 /\ X + B1 >= 0 /\ -X + B1 >= 0 /\ W + B1 >= 0 /\ -W + B1 >= 0 /\ V + B1 >= 0 /\ -V + B1 >= 0 /\ U + B1 >= 0 /\ -U + B1 >= 0 /\ T + B1 >= 0 /\ -T + B1 >= 0 /\ B + B1 >= 0 /\ -B + B1 >= 0 /\ S + B1 >= 0 /\ -S + B1 >= 0 /\ R + B1 >= 0 /\ -R + B1 >= 0 /\ Q + B1 >= 0 /\ -Q + B1 >= 0 /\ P + B1 >= 0 /\ -P + B1 >= 0 /\ O + B1 >= 0 /\ -O + B1 >= 0 /\ N + B1 >= 0 /\ M + B1 >= 0 /\ L + B1 >= 0 /\ K + B1 >= 0 /\ J + B1 >= 0 /\ A + B1 >= 0 /\ -A + B1 >= 0 /\ -A1 >= 0 /\ Z - A1 >= 0 /\ -Z - A1 >= 0 /\ Y - A1 >= 0 /\ -Y - A1 >= 0 /\ X - A1 >= 0 /\ -X - A1 >= 0 /\ W - A1 >= 0 /\ -W - A1 >= 0 /\ V - A1 >= 0 /\ -V - A1 >= 0 /\ U - A1 >= 0 /\ -U - A1 >= 0 /\ T - A1 >= 0 /\ -T - A1 >= 0 /\ B - A1 >= 0 /\ -B - A1 >= 0 /\ S - A1 >= 0 /\ -S - A1 >= 0 /\ R - A1 >= 0 /\ -R - A1 >= 0 /\ Q - A1 >= 0 /\ -Q - A1 >= 0 /\ P - A1 >= 0 /\ -P - A1 >= 0 /\ O - A1 >= 0 /\ -O - A1 >= 0 /\ N - A1 >= 0 /\ M - A1 >= 0 /\ L - A1 >= 0 /\ K - A1 >= 0 /\ J - A1 >= 0 /\ A - A1 >= 0 /\ -A - A1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ -Z + A1 >= 0 /\ Y + A1 >= 0 /\ -Y + A1 >= 0 /\ X + A1 >= 0 /\ -X + A1 >= 0 /\ W + A1 >= 0 /\ -W + A1 >= 0 /\ V + A1 >= 0 /\ -V + A1 >= 0 /\ U + A1 >= 0 /\ -U + A1 >= 0 /\ T + A1 >= 0 /\ -T + A1 >= 0 /\ B + A1 >= 0 /\ -B + A1 >= 0 /\ S + A1 >= 0 /\ -S + A1 >= 0 /\ R + A1 >= 0 /\ -R + A1 >= 0 /\ Q + A1 >= 0 /\ -Q + A1 >= 0 /\ P + A1 >= 0 /\ -P + A1 >= 0 /\ O + A1 >= 0 /\ -O + A1 >= 0 /\ N + A1 >= 0 /\ M + A1 >= 0 /\ L + A1 >= 0 /\ K + A1 >= 0 /\ J + A1 >= 0 /\ A + A1 >= 0 /\ -A + A1 >= 0 /\ -Z >= 0 /\ Y - Z >= 0 /\ -Y - Z >= 0 /\ X - Z >= 0 /\ -X - Z >= 0 /\ W - Z >= 0 /\ -W - Z >= 0 /\ V - Z >= 0 /\ -V - Z >= 0 /\ U - Z >= 0 /\ -U - Z >= 0 /\ T - Z >= 0 /\ -T - Z >= 0 /\ B - Z >= 0 /\ -B - Z >= 0 /\ S - Z >= 0 /\ -S - Z >= 0 /\ R - Z >= 0 /\ -R - Z >= 0 /\ Q - Z >= 0 /\ -Q - Z >= 0 /\ P - Z >= 0 /\ -P - Z >= 0 /\ O - Z >= 0 /\ -O - Z >= 0 /\ N - Z >= 0 /\ M - Z >= 0 /\ L - Z >= 0 /\ K - Z >= 0 /\ J - Z >= 0 /\ A - Z >= 0 /\ -A - Z >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ -Y + Z >= 0 /\ X + Z >= 0 /\ -X + Z >= 0 /\ W + Z >= 0 /\ -W + Z >= 0 /\ V + Z >= 0 /\ -V + Z >= 0 /\ U + Z >= 0 /\ -U + Z >= 0 /\ T + Z >= 0 /\ -T + Z >= 0 /\ B + Z >= 0 /\ -B + Z >= 0 /\ S + Z >= 0 /\ -S + Z >= 0 /\ R + Z >= 0 /\ -R + Z >= 0 /\ Q + Z >= 0 /\ -Q + Z >= 0 /\ P + Z >= 0 /\ -P + Z >= 0 /\ O + Z >= 0 /\ -O + Z >= 0 /\ N + Z >= 0 /\ M + Z >= 0 /\ L + Z >= 0 /\ K + Z >= 0 /\ J + Z >= 0 /\ A + Z >= 0 /\ -A + Z >= 0 /\ -Y >= 0 /\ X - Y >= 0 /\ -X - Y >= 0 /\ W - Y >= 0 /\ -W - Y >= 0 /\ V - Y >= 0 /\ -V - Y >= 0 /\ U - Y >= 0 /\ -U - Y >= 0 /\ T - Y >= 0 /\ -T - Y >= 0 /\ B - Y >= 0 /\ -B - Y >= 0 /\ S - Y >= 0 /\ -S - Y >= 0 /\ R - Y >= 0 /\ -R - Y >= 0 /\ Q - Y >= 0 /\ -Q - Y >= 0 /\ P - Y >= 0 /\ -P - Y >= 0 /\ O - Y >= 0 /\ -O - Y >= 0 /\ N - Y >= 0 /\ M - Y >= 0 /\ L - Y >= 0 /\ K - Y >= 0 /\ J - Y >= 0 /\ A - Y >= 0 /\ -A - Y >= 0 /\ Y >= 0 /\ X + Y >= 0 /\ -X + Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ V + Y >= 0 /\ -V + Y >= 0 /\ U + Y >= 0 /\ -U + Y >= 0 /\ T + Y >= 0 /\ -T + Y >= 0 /\ B + Y >= 0 /\ -B + Y >= 0 /\ S + Y >= 0 /\ -S + Y >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y >= 0 /\ -Q + Y >= 0 /\ P + Y >= 0 /\ -P + Y >= 0 /\ O + Y >= 0 /\ -O + Y >= 0 /\ N + Y >= 0 /\ M + Y >= 0 /\ L + Y >= 0 /\ K + Y >= 0 /\ J + Y >= 0 /\ A + Y >= 0 /\ -A + Y >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ T - X >= 0 /\ -T - X >= 0 /\ B - X >= 0 /\ -B - X >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ O - X >= 0 /\ -O - X >= 0 /\ N - X >= 0 /\ M - X >= 0 /\ L - X >= 0 /\ K - X >= 0 /\ J - X >= 0 /\ A - X >= 0 /\ -A - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ V + X >= 0 /\ -V + X >= 0 /\ U + X >= 0 /\ -U + X >= 0 /\ T + X >= 0 /\ -T + X >= 0 /\ B + X >= 0 /\ -B + X >= 0 /\ S + X >= 0 /\ -S + X >= 0 /\ R + X >= 0 /\ -R + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ O + X >= 0 /\ -O + X >= 0 /\ N + X >= 0 /\ M + X >= 0 /\ L + X >= 0 /\ K + X >= 0 /\ J + X >= 0 /\ A + X >= 0 /\ -A + X >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ U - W >= 0 /\ -U - W >= 0 /\ T - W >= 0 /\ -T - W >= 0 /\ B - W >= 0 /\ -B - W >= 0 /\ S - W >= 0 /\ -S - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ O - W >= 0 /\ -O - W >= 0 /\ N - W >= 0 /\ M - W >= 0 /\ L - W >= 0 /\ K - W >= 0 /\ J - W >= 0 /\ A - W >= 0 /\ -A - W >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ U + W >= 0 /\ -U + W >= 0 /\ T + W >= 0 /\ -T + W >= 0 /\ B + W >= 0 /\ -B + W >= 0 /\ S + W >= 0 /\ -S + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ O + W >= 0 /\ -O + W >= 0 /\ N + W >= 0 /\ M + W >= 0 /\ L + W >= 0 /\ K + W >= 0 /\ J + W >= 0 /\ A + W >= 0 /\ -A + W >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ T - V >= 0 /\ -T - V >= 0 /\ B - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ Q - V >= 0 /\ -Q - V >= 0 /\ P - V >= 0 /\ -P - V >= 0 /\ O - V >= 0 /\ -O - V >= 0 /\ N - V >= 0 /\ M - V >= 0 /\ L - V >= 0 /\ K - V >= 0 /\ J - V >= 0 /\ A - V >= 0 /\ -A - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ T + V >= 0 /\ -T + V >= 0 /\ B + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ Q + V >= 0 /\ -Q + V >= 0 /\ P + V >= 0 /\ -P + V >= 0 /\ O + V >= 0 /\ -O + V >= 0 /\ N + V >= 0 /\ M + V >= 0 /\ L + V >= 0 /\ K + V >= 0 /\ J + V >= 0 /\ A + V >= 0 /\ -A + V >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ B - U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ Q - U >= 0 /\ -Q - U >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ N - U >= 0 /\ M - U >= 0 /\ L - U >= 0 /\ K - U >= 0 /\ J - U >= 0 /\ A - U >= 0 /\ -A - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ B + U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U >= 0 /\ -Q + U >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ N + U >= 0 /\ M + U >= 0 /\ L + U >= 0 /\ K + U >= 0 /\ J + U >= 0 /\ A + U >= 0 /\ -A + U >= 0 /\ -T >= 0 /\ B - T >= 0 /\ -B - T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ Q - T >= 0 /\ -Q - T >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ N - T >= 0 /\ M - T >= 0 /\ L - T >= 0 /\ K - T >= 0 /\ J - T >= 0 /\ A - T >= 0 /\ -A - T >= 0 /\ T >= 0 /\ B + T >= 0 /\ -B + T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ Q + T >= 0 /\ -Q + T >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ N + T >= 0 /\ M + T >= 0 /\ L + T >= 0 /\ K + T >= 0 /\ J + T >= 0 /\ A + T >= 0 /\ -A + T >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ Q - B >= 0 /\ -Q - B >= 0 /\ P - B >= 0 /\ -P - B >= 0 /\ O - B >= 0 /\ -O - B >= 0 /\ N - B >= 0 /\ M - B >= 0 /\ L - B >= 0 /\ K - B >= 0 /\ J - B >= 0 /\ A - B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ S + B >= 0 /\ -S + B >= 0 /\ R + B >= 0 /\ -R + B >= 0 /\ Q + B >= 0 /\ -Q + B >= 0 /\ P + B >= 0 /\ -P + B >= 0 /\ O + B >= 0 /\ -O + B >= 0 /\ N + B >= 0 /\ M + B >= 0 /\ L + B >= 0 /\ K + B >= 0 /\ J + B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ Q - S >= 0 /\ -Q - S >= 0 /\ P - S >= 0 /\ -P - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ N - S >= 0 /\ M - S >= 0 /\ L - S >= 0 /\ K - S >= 0 /\ J - S >= 0 /\ A - S >= 0 /\ -A - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ Q + S >= 0 /\ -Q + S >= 0 /\ P + S >= 0 /\ -P + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ N + S >= 0 /\ M + S >= 0 /\ L + S >= 0 /\ K + S >= 0 /\ J + S >= 0 /\ A + S >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R >= 0 /\ -Q - R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ N - R >= 0 /\ M - R >= 0 /\ L - R >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ A - R >= 0 /\ -A - R >= 0 /\ R >= 0 /\ Q + R >= 0 /\ -Q + R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ N + R >= 0 /\ M + R >= 0 /\ L + R >= 0 /\ K + R >= 0 /\ J + R >= 0 /\ A + R >= 0 /\ -A + R >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ O - Q >= 0 /\ -O - Q >= 0 /\ N - Q >= 0 /\ M - Q >= 0 /\ L - Q >= 0 /\ K - Q >= 0 /\ J - Q >= 0 /\ A - Q >= 0 /\ -A - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ O + Q >= 0 /\ -O + Q >= 0 /\ N + Q >= 0 /\ M + Q >= 0 /\ L + Q >= 0 /\ K + Q >= 0 /\ J + Q >= 0 /\ A + Q >= 0 /\ -A + Q >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ N - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ K - P >= 0 /\ J - P >= 0 /\ A - P >= 0 /\ -A - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ N + P >= 0 /\ M + P >= 0 /\ L + P >= 0 /\ K + P >= 0 /\ J + P >= 0 /\ A + P >= 0 /\ -A + P >= 0 /\ -O >= 0 /\ N - O >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ A - O >= 0 /\ -A - O >= 0 /\ O >= 0 /\ N + O >= 0 /\ M + O >= 0 /\ L + O >= 0 /\ K + O >= 0 /\ J + O >= 0 /\ A + O >= 0 /\ -A + O >= 0 /\ N >= 0 /\ M + N >= 0 /\ L + N >= 0 /\ K + N >= 0 /\ J + N >= 0 /\ A + N >= 0 /\ -A + N >= 0 /\ M >= 0 /\ L + M >= 0 /\ K + M >= 0 /\ J + M >= 0 /\ A + M >= 0 /\ -A + M >= 0 /\ J - L >= 0 /\ L >= 0 /\ K + L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L >= 0 /\ -A + L >= 0 /\ K >= 0 /\ J + K >= 0 /\ A + K >= 0 /\ -A + K >= 0 /\ J >= 0 /\ A + J >= 0 /\ -A + J >= 0 /\ -A >= 0 /\ A >= 0 /\ D >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f1(A + 1, B + 1, C + H + I + D - 2, 0, 0, 0, 0, 0, 0, J + 1, K + E, L + 1, M + F, N + G, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I >= 0 /\ H - I >= 0 /\ -H - I >= 0 /\ G - I - 1 >= 0 /\ F - I >= 0 /\ E - I >= 0 /\ D - I >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ B1 - I >= 0 /\ -B1 - I >= 0 /\ A1 - I >= 0 /\ -A1 - I >= 0 /\ Z - I >= 0 /\ -Z - I >= 0 /\ Y - I >= 0 /\ -Y - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ W - I >= 0 /\ -W - I >= 0 /\ V - I >= 0 /\ -V - I >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ B - I >= 0 /\ -B - I >= 0 /\ S - I >= 0 /\ -S - I >= 0 /\ R - I >= 0 /\ -R - I >= 0 /\ Q - I >= 0 /\ -Q - I >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I >= 0 /\ M - I >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ J - I >= 0 /\ A - I >= 0 /\ -A - I >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ B1 + I >= 0 /\ -B1 + I >= 0 /\ A1 + I >= 0 /\ -A1 + I >= 0 /\ Z + I >= 0 /\ -Z + I >= 0 /\ Y + I >= 0 /\ -Y + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ W + I >= 0 /\ -W + I >= 0 /\ V + I >= 0 /\ -V + I >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ S + I >= 0 /\ -S + I >= 0 /\ R + I >= 0 /\ -R + I >= 0 /\ Q + I >= 0 /\ -Q + I >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I >= 0 /\ M + I >= 0 /\ L + I >= 0 /\ K + I >= 0 /\ J + I >= 0 /\ A + I >= 0 /\ -A + I >= 0 /\ -H >= 0 /\ G - H - 1 >= 0 /\ F - H >= 0 /\ E - H >= 0 /\ D - H >= 0 /\ C - H >= 0 /\ -C - H >= 0 /\ B1 - H >= 0 /\ -B1 - H >= 0 /\ A1 - H >= 0 /\ -A1 - H >= 0 /\ Z - H >= 0 /\ -Z - H >= 0 /\ Y - H >= 0 /\ -Y - H >= 0 /\ X - H >= 0 /\ -X - H >= 0 /\ W - H >= 0 /\ -W - H >= 0 /\ V - H >= 0 /\ -V - H >= 0 /\ U - H >= 0 /\ -U - H >= 0 /\ T - H >= 0 /\ -T - H >= 0 /\ B - H >= 0 /\ -B - H >= 0 /\ S - H >= 0 /\ -S - H >= 0 /\ R - H >= 0 /\ -R - H >= 0 /\ Q - H >= 0 /\ -Q - H >= 0 /\ P - H >= 0 /\ -P - H >= 0 /\ O - H >= 0 /\ -O - H >= 0 /\ N - H >= 0 /\ M - H >= 0 /\ L - H >= 0 /\ K - H >= 0 /\ J - H >= 0 /\ A - H >= 0 /\ -A - H >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B1 + H >= 0 /\ -B1 + H >= 0 /\ A1 + H >= 0 /\ -A1 + H >= 0 /\ Z + H >= 0 /\ -Z + H >= 0 /\ Y + H >= 0 /\ -Y + H >= 0 /\ X + H >= 0 /\ -X + H >= 0 /\ W + H >= 0 /\ -W + H >= 0 /\ V + H >= 0 /\ -V + H >= 0 /\ U + H >= 0 /\ -U + H >= 0 /\ T + H >= 0 /\ -T + H >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ S + H >= 0 /\ -S + H >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ Q + H >= 0 /\ -Q + H >= 0 /\ P + H >= 0 /\ -P + H >= 0 /\ O + H >= 0 /\ -O + H >= 0 /\ N + H >= 0 /\ M + H >= 0 /\ L + H >= 0 /\ K + H >= 0 /\ J + H >= 0 /\ A + H >= 0 /\ -A + H >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 1 >= 0 /\ -C + G - 1 >= 0 /\ B1 + G - 1 >= 0 /\ -B1 + G - 1 >= 0 /\ A1 + G - 1 >= 0 /\ -A1 + G - 1 >= 0 /\ Z + G - 1 >= 0 /\ -Z + G - 1 >= 0 /\ Y + G - 1 >= 0 /\ -Y + G - 1 >= 0 /\ X + G - 1 >= 0 /\ -X + G - 1 >= 0 /\ W + G - 1 >= 0 /\ -W + G - 1 >= 0 /\ V + G - 1 >= 0 /\ -V + G - 1 >= 0 /\ U + G - 1 >= 0 /\ -U + G - 1 >= 0 /\ T + G - 1 >= 0 /\ -T + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G - 1 >= 0 /\ S + G - 1 >= 0 /\ -S + G - 1 >= 0 /\ R + G - 1 >= 0 /\ -R + G - 1 >= 0 /\ Q + G - 1 >= 0 /\ -Q + G - 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G - 1 >= 0 /\ O + G - 1 >= 0 /\ -O + G - 1 >= 0 /\ N + G - 1 >= 0 /\ M + G - 1 >= 0 /\ L + G - 1 >= 0 /\ K + G - 1 >= 0 /\ J + G - 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ C + F >= 0 /\ -C + F >= 0 /\ B1 + F >= 0 /\ -B1 + F >= 0 /\ A1 + F >= 0 /\ -A1 + F >= 0 /\ Z + F >= 0 /\ -Z + F >= 0 /\ Y + F >= 0 /\ -Y + F >= 0 /\ X + F >= 0 /\ -X + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ U + F >= 0 /\ -U + F >= 0 /\ T + F >= 0 /\ -T + F >= 0 /\ B + F >= 0 /\ -B + F >= 0 /\ S + F >= 0 /\ -S + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ Q + F >= 0 /\ -Q + F >= 0 /\ P + F >= 0 /\ -P + F >= 0 /\ O + F >= 0 /\ -O + F >= 0 /\ N + F >= 0 /\ M + F >= 0 /\ L + F >= 0 /\ K + F >= 0 /\ J + F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B1 + E >= 0 /\ -B1 + E >= 0 /\ A1 + E >= 0 /\ -A1 + E >= 0 /\ Z + E >= 0 /\ -Z + E >= 0 /\ Y + E >= 0 /\ -Y + E >= 0 /\ X + E >= 0 /\ -X + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ V + E >= 0 /\ -V + E >= 0 /\ U + E >= 0 /\ -U + E >= 0 /\ T + E >= 0 /\ -T + E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ S + E >= 0 /\ -S + E >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E >= 0 /\ -Q + E >= 0 /\ P + E >= 0 /\ -P + E >= 0 /\ O + E >= 0 /\ -O + E >= 0 /\ N + E >= 0 /\ M + E >= 0 /\ L + E >= 0 /\ K + E >= 0 /\ J + E >= 0 /\ A + E >= 0 /\ -A + E >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B1 + D >= 0 /\ -B1 + D >= 0 /\ A1 + D >= 0 /\ -A1 + D >= 0 /\ Z + D >= 0 /\ -Z + D >= 0 /\ Y + D >= 0 /\ -Y + D >= 0 /\ X + D >= 0 /\ -X + D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ V + D >= 0 /\ -V + D >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ T + D >= 0 /\ -T + D >= 0 /\ B + D >= 0 /\ -B + D >= 0 /\ S + D >= 0 /\ -S + D >= 0 /\ R + D >= 0 /\ -R + D >= 0 /\ Q + D >= 0 /\ -Q + D >= 0 /\ P + D >= 0 /\ -P + D >= 0 /\ O + D >= 0 /\ -O + D >= 0 /\ N + D >= 0 /\ M + D >= 0 /\ L + D >= 0 /\ K + D >= 0 /\ J + D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B1 - C >= 0 /\ -B1 - C >= 0 /\ A1 - C >= 0 /\ -A1 - C >= 0 /\ Z - C >= 0 /\ -Z - C >= 0 /\ Y - C >= 0 /\ -Y - C >= 0 /\ X - C >= 0 /\ -X - C >= 0 /\ W - C >= 0 /\ -W - C >= 0 /\ V - C >= 0 /\ -V - C >= 0 /\ U - C >= 0 /\ -U - C >= 0 /\ T - C >= 0 /\ -T - C >= 0 /\ B - C >= 0 /\ -B - C >= 0 /\ S - C >= 0 /\ -S - C >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C >= 0 /\ -Q - C >= 0 /\ P - C >= 0 /\ -P - C >= 0 /\ O - C >= 0 /\ -O - C >= 0 /\ N - C >= 0 /\ M - C >= 0 /\ L - C >= 0 /\ K - C >= 0 /\ J - C >= 0 /\ A - C >= 0 /\ -A - C >= 0 /\ C >= 0 /\ B1 + C >= 0 /\ -B1 + C >= 0 /\ A1 + C >= 0 /\ -A1 + C >= 0 /\ Z + C >= 0 /\ -Z + C >= 0 /\ Y + C >= 0 /\ -Y + C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ V + C >= 0 /\ -V + C >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ P + C >= 0 /\ -P + C >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C >= 0 /\ M + C >= 0 /\ L + C >= 0 /\ K + C >= 0 /\ J + C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ -B1 >= 0 /\ A1 - B1 >= 0 /\ -A1 - B1 >= 0 /\ Z - B1 >= 0 /\ -Z - B1 >= 0 /\ Y - B1 >= 0 /\ -Y - B1 >= 0 /\ X - B1 >= 0 /\ -X - B1 >= 0 /\ W - B1 >= 0 /\ -W - B1 >= 0 /\ V - B1 >= 0 /\ -V - B1 >= 0 /\ U - B1 >= 0 /\ -U - B1 >= 0 /\ T - B1 >= 0 /\ -T - B1 >= 0 /\ B - B1 >= 0 /\ -B - B1 >= 0 /\ S - B1 >= 0 /\ -S - B1 >= 0 /\ R - B1 >= 0 /\ -R - B1 >= 0 /\ Q - B1 >= 0 /\ -Q - B1 >= 0 /\ P - B1 >= 0 /\ -P - B1 >= 0 /\ O - B1 >= 0 /\ -O - B1 >= 0 /\ N - B1 >= 0 /\ M - B1 >= 0 /\ L - B1 >= 0 /\ K - B1 >= 0 /\ J - B1 >= 0 /\ A - B1 >= 0 /\ -A - B1 >= 0 /\ B1 >= 0 /\ A1 + B1 >= 0 /\ -A1 + B1 >= 0 /\ Z + B1 >= 0 /\ -Z + B1 >= 0 /\ Y + B1 >= 0 /\ -Y + B1 >= 0 /\ X + B1 >= 0 /\ -X + B1 >= 0 /\ W + B1 >= 0 /\ -W + B1 >= 0 /\ V + B1 >= 0 /\ -V + B1 >= 0 /\ U + B1 >= 0 /\ -U + B1 >= 0 /\ T + B1 >= 0 /\ -T + B1 >= 0 /\ B + B1 >= 0 /\ -B + B1 >= 0 /\ S + B1 >= 0 /\ -S + B1 >= 0 /\ R + B1 >= 0 /\ -R + B1 >= 0 /\ Q + B1 >= 0 /\ -Q + B1 >= 0 /\ P + B1 >= 0 /\ -P + B1 >= 0 /\ O + B1 >= 0 /\ -O + B1 >= 0 /\ N + B1 >= 0 /\ M + B1 >= 0 /\ L + B1 >= 0 /\ K + B1 >= 0 /\ J + B1 >= 0 /\ A + B1 >= 0 /\ -A + B1 >= 0 /\ -A1 >= 0 /\ Z - A1 >= 0 /\ -Z - A1 >= 0 /\ Y - A1 >= 0 /\ -Y - A1 >= 0 /\ X - A1 >= 0 /\ -X - A1 >= 0 /\ W - A1 >= 0 /\ -W - A1 >= 0 /\ V - A1 >= 0 /\ -V - A1 >= 0 /\ U - A1 >= 0 /\ -U - A1 >= 0 /\ T - A1 >= 0 /\ -T - A1 >= 0 /\ B - A1 >= 0 /\ -B - A1 >= 0 /\ S - A1 >= 0 /\ -S - A1 >= 0 /\ R - A1 >= 0 /\ -R - A1 >= 0 /\ Q - A1 >= 0 /\ -Q - A1 >= 0 /\ P - A1 >= 0 /\ -P - A1 >= 0 /\ O - A1 >= 0 /\ -O - A1 >= 0 /\ N - A1 >= 0 /\ M - A1 >= 0 /\ L - A1 >= 0 /\ K - A1 >= 0 /\ J - A1 >= 0 /\ A - A1 >= 0 /\ -A - A1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ -Z + A1 >= 0 /\ Y + A1 >= 0 /\ -Y + A1 >= 0 /\ X + A1 >= 0 /\ -X + A1 >= 0 /\ W + A1 >= 0 /\ -W + A1 >= 0 /\ V + A1 >= 0 /\ -V + A1 >= 0 /\ U + A1 >= 0 /\ -U + A1 >= 0 /\ T + A1 >= 0 /\ -T + A1 >= 0 /\ B + A1 >= 0 /\ -B + A1 >= 0 /\ S + A1 >= 0 /\ -S + A1 >= 0 /\ R + A1 >= 0 /\ -R + A1 >= 0 /\ Q + A1 >= 0 /\ -Q + A1 >= 0 /\ P + A1 >= 0 /\ -P + A1 >= 0 /\ O + A1 >= 0 /\ -O + A1 >= 0 /\ N + A1 >= 0 /\ M + A1 >= 0 /\ L + A1 >= 0 /\ K + A1 >= 0 /\ J + A1 >= 0 /\ A + A1 >= 0 /\ -A + A1 >= 0 /\ -Z >= 0 /\ Y - Z >= 0 /\ -Y - Z >= 0 /\ X - Z >= 0 /\ -X - Z >= 0 /\ W - Z >= 0 /\ -W - Z >= 0 /\ V - Z >= 0 /\ -V - Z >= 0 /\ U - Z >= 0 /\ -U - Z >= 0 /\ T - Z >= 0 /\ -T - Z >= 0 /\ B - Z >= 0 /\ -B - Z >= 0 /\ S - Z >= 0 /\ -S - Z >= 0 /\ R - Z >= 0 /\ -R - Z >= 0 /\ Q - Z >= 0 /\ -Q - Z >= 0 /\ P - Z >= 0 /\ -P - Z >= 0 /\ O - Z >= 0 /\ -O - Z >= 0 /\ N - Z >= 0 /\ M - Z >= 0 /\ L - Z >= 0 /\ K - Z >= 0 /\ J - Z >= 0 /\ A - Z >= 0 /\ -A - Z >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ -Y + Z >= 0 /\ X + Z >= 0 /\ -X + Z >= 0 /\ W + Z >= 0 /\ -W + Z >= 0 /\ V + Z >= 0 /\ -V + Z >= 0 /\ U + Z >= 0 /\ -U + Z >= 0 /\ T + Z >= 0 /\ -T + Z >= 0 /\ B + Z >= 0 /\ -B + Z >= 0 /\ S + Z >= 0 /\ -S + Z >= 0 /\ R + Z >= 0 /\ -R + Z >= 0 /\ Q + Z >= 0 /\ -Q + Z >= 0 /\ P + Z >= 0 /\ -P + Z >= 0 /\ O + Z >= 0 /\ -O + Z >= 0 /\ N + Z >= 0 /\ M + Z >= 0 /\ L + Z >= 0 /\ K + Z >= 0 /\ J + Z >= 0 /\ A + Z >= 0 /\ -A + Z >= 0 /\ -Y >= 0 /\ X - Y >= 0 /\ -X - Y >= 0 /\ W - Y >= 0 /\ -W - Y >= 0 /\ V - Y >= 0 /\ -V - Y >= 0 /\ U - Y >= 0 /\ -U - Y >= 0 /\ T - Y >= 0 /\ -T - Y >= 0 /\ B - Y >= 0 /\ -B - Y >= 0 /\ S - Y >= 0 /\ -S - Y >= 0 /\ R - Y >= 0 /\ -R - Y >= 0 /\ Q - Y >= 0 /\ -Q - Y >= 0 /\ P - Y >= 0 /\ -P - Y >= 0 /\ O - Y >= 0 /\ -O - Y >= 0 /\ N - Y >= 0 /\ M - Y >= 0 /\ L - Y >= 0 /\ K - Y >= 0 /\ J - Y >= 0 /\ A - Y >= 0 /\ -A - Y >= 0 /\ Y >= 0 /\ X + Y >= 0 /\ -X + Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ V + Y >= 0 /\ -V + Y >= 0 /\ U + Y >= 0 /\ -U + Y >= 0 /\ T + Y >= 0 /\ -T + Y >= 0 /\ B + Y >= 0 /\ -B + Y >= 0 /\ S + Y >= 0 /\ -S + Y >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y >= 0 /\ -Q + Y >= 0 /\ P + Y >= 0 /\ -P + Y >= 0 /\ O + Y >= 0 /\ -O + Y >= 0 /\ N + Y >= 0 /\ M + Y >= 0 /\ L + Y >= 0 /\ K + Y >= 0 /\ J + Y >= 0 /\ A + Y >= 0 /\ -A + Y >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ T - X >= 0 /\ -T - X >= 0 /\ B - X >= 0 /\ -B - X >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ O - X >= 0 /\ -O - X >= 0 /\ N - X >= 0 /\ M - X >= 0 /\ L - X >= 0 /\ K - X >= 0 /\ J - X >= 0 /\ A - X >= 0 /\ -A - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ V + X >= 0 /\ -V + X >= 0 /\ U + X >= 0 /\ -U + X >= 0 /\ T + X >= 0 /\ -T + X >= 0 /\ B + X >= 0 /\ -B + X >= 0 /\ S + X >= 0 /\ -S + X >= 0 /\ R + X >= 0 /\ -R + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ O + X >= 0 /\ -O + X >= 0 /\ N + X >= 0 /\ M + X >= 0 /\ L + X >= 0 /\ K + X >= 0 /\ J + X >= 0 /\ A + X >= 0 /\ -A + X >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ U - W >= 0 /\ -U - W >= 0 /\ T - W >= 0 /\ -T - W >= 0 /\ B - W >= 0 /\ -B - W >= 0 /\ S - W >= 0 /\ -S - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ O - W >= 0 /\ -O - W >= 0 /\ N - W >= 0 /\ M - W >= 0 /\ L - W >= 0 /\ K - W >= 0 /\ J - W >= 0 /\ A - W >= 0 /\ -A - W >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ U + W >= 0 /\ -U + W >= 0 /\ T + W >= 0 /\ -T + W >= 0 /\ B + W >= 0 /\ -B + W >= 0 /\ S + W >= 0 /\ -S + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ O + W >= 0 /\ -O + W >= 0 /\ N + W >= 0 /\ M + W >= 0 /\ L + W >= 0 /\ K + W >= 0 /\ J + W >= 0 /\ A + W >= 0 /\ -A + W >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ T - V >= 0 /\ -T - V >= 0 /\ B - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ Q - V >= 0 /\ -Q - V >= 0 /\ P - V >= 0 /\ -P - V >= 0 /\ O - V >= 0 /\ -O - V >= 0 /\ N - V >= 0 /\ M - V >= 0 /\ L - V >= 0 /\ K - V >= 0 /\ J - V >= 0 /\ A - V >= 0 /\ -A - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ T + V >= 0 /\ -T + V >= 0 /\ B + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ Q + V >= 0 /\ -Q + V >= 0 /\ P + V >= 0 /\ -P + V >= 0 /\ O + V >= 0 /\ -O + V >= 0 /\ N + V >= 0 /\ M + V >= 0 /\ L + V >= 0 /\ K + V >= 0 /\ J + V >= 0 /\ A + V >= 0 /\ -A + V >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ B - U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ Q - U >= 0 /\ -Q - U >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ N - U >= 0 /\ M - U >= 0 /\ L - U >= 0 /\ K - U >= 0 /\ J - U >= 0 /\ A - U >= 0 /\ -A - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ B + U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U >= 0 /\ -Q + U >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ N + U >= 0 /\ M + U >= 0 /\ L + U >= 0 /\ K + U >= 0 /\ J + U >= 0 /\ A + U >= 0 /\ -A + U >= 0 /\ -T >= 0 /\ B - T >= 0 /\ -B - T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ Q - T >= 0 /\ -Q - T >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ N - T >= 0 /\ M - T >= 0 /\ L - T >= 0 /\ K - T >= 0 /\ J - T >= 0 /\ A - T >= 0 /\ -A - T >= 0 /\ T >= 0 /\ B + T >= 0 /\ -B + T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ Q + T >= 0 /\ -Q + T >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ N + T >= 0 /\ M + T >= 0 /\ L + T >= 0 /\ K + T >= 0 /\ J + T >= 0 /\ A + T >= 0 /\ -A + T >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ Q - B >= 0 /\ -Q - B >= 0 /\ P - B >= 0 /\ -P - B >= 0 /\ O - B >= 0 /\ -O - B >= 0 /\ N - B >= 0 /\ M - B >= 0 /\ L - B >= 0 /\ K - B >= 0 /\ J - B >= 0 /\ A - B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ S + B >= 0 /\ -S + B >= 0 /\ R + B >= 0 /\ -R + B >= 0 /\ Q + B >= 0 /\ -Q + B >= 0 /\ P + B >= 0 /\ -P + B >= 0 /\ O + B >= 0 /\ -O + B >= 0 /\ N + B >= 0 /\ M + B >= 0 /\ L + B >= 0 /\ K + B >= 0 /\ J + B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ Q - S >= 0 /\ -Q - S >= 0 /\ P - S >= 0 /\ -P - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ N - S >= 0 /\ M - S >= 0 /\ L - S >= 0 /\ K - S >= 0 /\ J - S >= 0 /\ A - S >= 0 /\ -A - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ Q + S >= 0 /\ -Q + S >= 0 /\ P + S >= 0 /\ -P + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ N + S >= 0 /\ M + S >= 0 /\ L + S >= 0 /\ K + S >= 0 /\ J + S >= 0 /\ A + S >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R >= 0 /\ -Q - R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ N - R >= 0 /\ M - R >= 0 /\ L - R >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ A - R >= 0 /\ -A - R >= 0 /\ R >= 0 /\ Q + R >= 0 /\ -Q + R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ N + R >= 0 /\ M + R >= 0 /\ L + R >= 0 /\ K + R >= 0 /\ J + R >= 0 /\ A + R >= 0 /\ -A + R >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ O - Q >= 0 /\ -O - Q >= 0 /\ N - Q >= 0 /\ M - Q >= 0 /\ L - Q >= 0 /\ K - Q >= 0 /\ J - Q >= 0 /\ A - Q >= 0 /\ -A - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ O + Q >= 0 /\ -O + Q >= 0 /\ N + Q >= 0 /\ M + Q >= 0 /\ L + Q >= 0 /\ K + Q >= 0 /\ J + Q >= 0 /\ A + Q >= 0 /\ -A + Q >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ N - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ K - P >= 0 /\ J - P >= 0 /\ A - P >= 0 /\ -A - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ N + P >= 0 /\ M + P >= 0 /\ L + P >= 0 /\ K + P >= 0 /\ J + P >= 0 /\ A + P >= 0 /\ -A + P >= 0 /\ -O >= 0 /\ N - O >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ A - O >= 0 /\ -A - O >= 0 /\ O >= 0 /\ N + O >= 0 /\ M + O >= 0 /\ L + O >= 0 /\ K + O >= 0 /\ J + O >= 0 /\ A + O >= 0 /\ -A + O >= 0 /\ N >= 0 /\ M + N >= 0 /\ L + N >= 0 /\ K + N >= 0 /\ J + N >= 0 /\ A + N >= 0 /\ -A + N >= 0 /\ M >= 0 /\ L + M >= 0 /\ K + M >= 0 /\ J + M >= 0 /\ A + M >= 0 /\ -A + M >= 0 /\ J - L >= 0 /\ L >= 0 /\ K + L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L >= 0 /\ -A + L >= 0 /\ K >= 0 /\ J + K >= 0 /\ A + K >= 0 /\ -A + K >= 0 /\ J >= 0 /\ A + J >= 0 /\ -A + J >= 0 /\ -A >= 0 /\ A >= 0 /\ H + I + D >= 2 /\ D >= 1 ]
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f1(R + A + S + 1, P + B + Q + 1, O + C - 1, D, E, F, G, H, I, J, K, L, M, N, 0, 0, 0, 0, 0, T, U, V, W, X, Y, Z, A1, B1, C1)) [ -I >= 0 /\ H - I >= 0 /\ -H - I >= 0 /\ G - I >= 0 /\ F - I >= 0 /\ E - I >= 0 /\ D - I >= 0 /\ -D - I >= 0 /\ C - I >= 0 /\ B1 - I >= 0 /\ -B1 - I >= 0 /\ A1 - I >= 0 /\ -A1 - I >= 0 /\ Z - I >= 0 /\ -Z - I >= 0 /\ Y - I >= 0 /\ -Y - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ W - I >= 0 /\ -W - I >= 0 /\ V - I >= 0 /\ -V - I >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ B - I - 1 >= 0 /\ S - I >= 0 /\ -S - I >= 0 /\ R - I >= 0 /\ -R - I >= 0 /\ Q - I >= 0 /\ -Q - I >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I >= 0 /\ M - I >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ J - I >= 0 /\ A - I - 1 >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I >= 0 /\ F + I >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ -D + I >= 0 /\ C + I >= 0 /\ B1 + I >= 0 /\ -B1 + I >= 0 /\ A1 + I >= 0 /\ -A1 + I >= 0 /\ Z + I >= 0 /\ -Z + I >= 0 /\ Y + I >= 0 /\ -Y + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ W + I >= 0 /\ -W + I >= 0 /\ V + I >= 0 /\ -V + I >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ B + I - 1 >= 0 /\ S + I >= 0 /\ -S + I >= 0 /\ R + I >= 0 /\ -R + I >= 0 /\ Q + I >= 0 /\ -Q + I >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I >= 0 /\ M + I >= 0 /\ L + I >= 0 /\ K + I >= 0 /\ J + I >= 0 /\ A + I - 1 >= 0 /\ -H >= 0 /\ G - H >= 0 /\ F - H >= 0 /\ E - H >= 0 /\ D - H >= 0 /\ -D - H >= 0 /\ C - H >= 0 /\ B1 - H >= 0 /\ -B1 - H >= 0 /\ A1 - H >= 0 /\ -A1 - H >= 0 /\ Z - H >= 0 /\ -Z - H >= 0 /\ Y - H >= 0 /\ -Y - H >= 0 /\ X - H >= 0 /\ -X - H >= 0 /\ W - H >= 0 /\ -W - H >= 0 /\ V - H >= 0 /\ -V - H >= 0 /\ U - H >= 0 /\ -U - H >= 0 /\ T - H >= 0 /\ -T - H >= 0 /\ B - H - 1 >= 0 /\ S - H >= 0 /\ -S - H >= 0 /\ R - H >= 0 /\ -R - H >= 0 /\ Q - H >= 0 /\ -Q - H >= 0 /\ P - H >= 0 /\ -P - H >= 0 /\ O - H >= 0 /\ -O - H >= 0 /\ N - H >= 0 /\ M - H >= 0 /\ L - H >= 0 /\ K - H >= 0 /\ J - H >= 0 /\ A - H - 1 >= 0 /\ H >= 0 /\ G + H >= 0 /\ F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H >= 0 /\ B1 + H >= 0 /\ -B1 + H >= 0 /\ A1 + H >= 0 /\ -A1 + H >= 0 /\ Z + H >= 0 /\ -Z + H >= 0 /\ Y + H >= 0 /\ -Y + H >= 0 /\ X + H >= 0 /\ -X + H >= 0 /\ W + H >= 0 /\ -W + H >= 0 /\ V + H >= 0 /\ -V + H >= 0 /\ U + H >= 0 /\ -U + H >= 0 /\ T + H >= 0 /\ -T + H >= 0 /\ B + H - 1 >= 0 /\ S + H >= 0 /\ -S + H >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ Q + H >= 0 /\ -Q + H >= 0 /\ P + H >= 0 /\ -P + H >= 0 /\ O + H >= 0 /\ -O + H >= 0 /\ N + H >= 0 /\ M + H >= 0 /\ L + H >= 0 /\ K + H >= 0 /\ J + H >= 0 /\ A + H - 1 >= 0 /\ G >= 0 /\ F + G >= 0 /\ E + G >= 0 /\ D + G >= 0 /\ -D + G >= 0 /\ C + G >= 0 /\ B1 + G >= 0 /\ -B1 + G >= 0 /\ A1 + G >= 0 /\ -A1 + G >= 0 /\ Z + G >= 0 /\ -Z + G >= 0 /\ Y + G >= 0 /\ -Y + G >= 0 /\ X + G >= 0 /\ -X + G >= 0 /\ W + G >= 0 /\ -W + G >= 0 /\ V + G >= 0 /\ -V + G >= 0 /\ U + G >= 0 /\ -U + G >= 0 /\ T + G >= 0 /\ -T + G >= 0 /\ B + G - 1 >= 0 /\ S + G >= 0 /\ -S + G >= 0 /\ R + G >= 0 /\ -R + G >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ P + G >= 0 /\ -P + G >= 0 /\ O + G >= 0 /\ -O + G >= 0 /\ N + G >= 0 /\ M + G >= 0 /\ L + G >= 0 /\ K + G >= 0 /\ J + G >= 0 /\ A + G - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B1 + F >= 0 /\ -B1 + F >= 0 /\ A1 + F >= 0 /\ -A1 + F >= 0 /\ Z + F >= 0 /\ -Z + F >= 0 /\ Y + F >= 0 /\ -Y + F >= 0 /\ X + F >= 0 /\ -X + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ U + F >= 0 /\ -U + F >= 0 /\ T + F >= 0 /\ -T + F >= 0 /\ B + F - 1 >= 0 /\ S + F >= 0 /\ -S + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ Q + F >= 0 /\ -Q + F >= 0 /\ P + F >= 0 /\ -P + F >= 0 /\ O + F >= 0 /\ -O + F >= 0 /\ N + F >= 0 /\ M + F >= 0 /\ L + F >= 0 /\ K + F >= 0 /\ J + F >= 0 /\ A + F - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ C + E >= 0 /\ B1 + E >= 0 /\ -B1 + E >= 0 /\ A1 + E >= 0 /\ -A1 + E >= 0 /\ Z + E >= 0 /\ -Z + E >= 0 /\ Y + E >= 0 /\ -Y + E >= 0 /\ X + E >= 0 /\ -X + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ V + E >= 0 /\ -V + E >= 0 /\ U + E >= 0 /\ -U + E >= 0 /\ T + E >= 0 /\ -T + E >= 0 /\ B + E - 1 >= 0 /\ S + E >= 0 /\ -S + E >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E >= 0 /\ -Q + E >= 0 /\ P + E >= 0 /\ -P + E >= 0 /\ O + E >= 0 /\ -O + E >= 0 /\ N + E >= 0 /\ M + E >= 0 /\ L + E >= 0 /\ K + E >= 0 /\ J + E >= 0 /\ A + E - 1 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ B1 - D >= 0 /\ -B1 - D >= 0 /\ A1 - D >= 0 /\ -A1 - D >= 0 /\ Z - D >= 0 /\ -Z - D >= 0 /\ Y - D >= 0 /\ -Y - D >= 0 /\ X - D >= 0 /\ -X - D >= 0 /\ W - D >= 0 /\ -W - D >= 0 /\ V - D >= 0 /\ -V - D >= 0 /\ U - D >= 0 /\ -U - D >= 0 /\ T - D >= 0 /\ -T - D >= 0 /\ B - D - 1 >= 0 /\ S - D >= 0 /\ -S - D >= 0 /\ R - D >= 0 /\ -R - D >= 0 /\ Q - D >= 0 /\ -Q - D >= 0 /\ P - D >= 0 /\ -P - D >= 0 /\ O - D >= 0 /\ -O - D >= 0 /\ N - D >= 0 /\ M - D >= 0 /\ L - D >= 0 /\ K - D >= 0 /\ J - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B1 + D >= 0 /\ -B1 + D >= 0 /\ A1 + D >= 0 /\ -A1 + D >= 0 /\ Z + D >= 0 /\ -Z + D >= 0 /\ Y + D >= 0 /\ -Y + D >= 0 /\ X + D >= 0 /\ -X + D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ V + D >= 0 /\ -V + D >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ T + D >= 0 /\ -T + D >= 0 /\ B + D - 1 >= 0 /\ S + D >= 0 /\ -S + D >= 0 /\ R + D >= 0 /\ -R + D >= 0 /\ Q + D >= 0 /\ -Q + D >= 0 /\ P + D >= 0 /\ -P + D >= 0 /\ O + D >= 0 /\ -O + D >= 0 /\ N + D >= 0 /\ M + D >= 0 /\ L + D >= 0 /\ K + D >= 0 /\ J + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B1 + C >= 0 /\ -B1 + C >= 0 /\ A1 + C >= 0 /\ -A1 + C >= 0 /\ Z + C >= 0 /\ -Z + C >= 0 /\ Y + C >= 0 /\ -Y + C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ V + C >= 0 /\ -V + C >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ B + C - 1 >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ P + C >= 0 /\ -P + C >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C >= 0 /\ M + C >= 0 /\ L + C >= 0 /\ K + C >= 0 /\ J + C >= 0 /\ A + C - 1 >= 0 /\ -B1 >= 0 /\ A1 - B1 >= 0 /\ -A1 - B1 >= 0 /\ Z - B1 >= 0 /\ -Z - B1 >= 0 /\ Y - B1 >= 0 /\ -Y - B1 >= 0 /\ X - B1 >= 0 /\ -X - B1 >= 0 /\ W - B1 >= 0 /\ -W - B1 >= 0 /\ V - B1 >= 0 /\ -V - B1 >= 0 /\ U - B1 >= 0 /\ -U - B1 >= 0 /\ T - B1 >= 0 /\ -T - B1 >= 0 /\ B - B1 - 1 >= 0 /\ S - B1 >= 0 /\ -S - B1 >= 0 /\ R - B1 >= 0 /\ -R - B1 >= 0 /\ Q - B1 >= 0 /\ -Q - B1 >= 0 /\ P - B1 >= 0 /\ -P - B1 >= 0 /\ O - B1 >= 0 /\ -O - B1 >= 0 /\ N - B1 >= 0 /\ M - B1 >= 0 /\ L - B1 >= 0 /\ K - B1 >= 0 /\ J - B1 >= 0 /\ A - B1 - 1 >= 0 /\ B1 >= 0 /\ A1 + B1 >= 0 /\ -A1 + B1 >= 0 /\ Z + B1 >= 0 /\ -Z + B1 >= 0 /\ Y + B1 >= 0 /\ -Y + B1 >= 0 /\ X + B1 >= 0 /\ -X + B1 >= 0 /\ W + B1 >= 0 /\ -W + B1 >= 0 /\ V + B1 >= 0 /\ -V + B1 >= 0 /\ U + B1 >= 0 /\ -U + B1 >= 0 /\ T + B1 >= 0 /\ -T + B1 >= 0 /\ B + B1 - 1 >= 0 /\ S + B1 >= 0 /\ -S + B1 >= 0 /\ R + B1 >= 0 /\ -R + B1 >= 0 /\ Q + B1 >= 0 /\ -Q + B1 >= 0 /\ P + B1 >= 0 /\ -P + B1 >= 0 /\ O + B1 >= 0 /\ -O + B1 >= 0 /\ N + B1 >= 0 /\ M + B1 >= 0 /\ L + B1 >= 0 /\ K + B1 >= 0 /\ J + B1 >= 0 /\ A + B1 - 1 >= 0 /\ -A1 >= 0 /\ Z - A1 >= 0 /\ -Z - A1 >= 0 /\ Y - A1 >= 0 /\ -Y - A1 >= 0 /\ X - A1 >= 0 /\ -X - A1 >= 0 /\ W - A1 >= 0 /\ -W - A1 >= 0 /\ V - A1 >= 0 /\ -V - A1 >= 0 /\ U - A1 >= 0 /\ -U - A1 >= 0 /\ T - A1 >= 0 /\ -T - A1 >= 0 /\ B - A1 - 1 >= 0 /\ S - A1 >= 0 /\ -S - A1 >= 0 /\ R - A1 >= 0 /\ -R - A1 >= 0 /\ Q - A1 >= 0 /\ -Q - A1 >= 0 /\ P - A1 >= 0 /\ -P - A1 >= 0 /\ O - A1 >= 0 /\ -O - A1 >= 0 /\ N - A1 >= 0 /\ M - A1 >= 0 /\ L - A1 >= 0 /\ K - A1 >= 0 /\ J - A1 >= 0 /\ A - A1 - 1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ -Z + A1 >= 0 /\ Y + A1 >= 0 /\ -Y + A1 >= 0 /\ X + A1 >= 0 /\ -X + A1 >= 0 /\ W + A1 >= 0 /\ -W + A1 >= 0 /\ V + A1 >= 0 /\ -V + A1 >= 0 /\ U + A1 >= 0 /\ -U + A1 >= 0 /\ T + A1 >= 0 /\ -T + A1 >= 0 /\ B + A1 - 1 >= 0 /\ S + A1 >= 0 /\ -S + A1 >= 0 /\ R + A1 >= 0 /\ -R + A1 >= 0 /\ Q + A1 >= 0 /\ -Q + A1 >= 0 /\ P + A1 >= 0 /\ -P + A1 >= 0 /\ O + A1 >= 0 /\ -O + A1 >= 0 /\ N + A1 >= 0 /\ M + A1 >= 0 /\ L + A1 >= 0 /\ K + A1 >= 0 /\ J + A1 >= 0 /\ A + A1 - 1 >= 0 /\ -Z >= 0 /\ Y - Z >= 0 /\ -Y - Z >= 0 /\ X - Z >= 0 /\ -X - Z >= 0 /\ W - Z >= 0 /\ -W - Z >= 0 /\ V - Z >= 0 /\ -V - Z >= 0 /\ U - Z >= 0 /\ -U - Z >= 0 /\ T - Z >= 0 /\ -T - Z >= 0 /\ B - Z - 1 >= 0 /\ S - Z >= 0 /\ -S - Z >= 0 /\ R - Z >= 0 /\ -R - Z >= 0 /\ Q - Z >= 0 /\ -Q - Z >= 0 /\ P - Z >= 0 /\ -P - Z >= 0 /\ O - Z >= 0 /\ -O - Z >= 0 /\ N - Z >= 0 /\ M - Z >= 0 /\ L - Z >= 0 /\ K - Z >= 0 /\ J - Z >= 0 /\ A - Z - 1 >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ -Y + Z >= 0 /\ X + Z >= 0 /\ -X + Z >= 0 /\ W + Z >= 0 /\ -W + Z >= 0 /\ V + Z >= 0 /\ -V + Z >= 0 /\ U + Z >= 0 /\ -U + Z >= 0 /\ T + Z >= 0 /\ -T + Z >= 0 /\ B + Z - 1 >= 0 /\ S + Z >= 0 /\ -S + Z >= 0 /\ R + Z >= 0 /\ -R + Z >= 0 /\ Q + Z >= 0 /\ -Q + Z >= 0 /\ P + Z >= 0 /\ -P + Z >= 0 /\ O + Z >= 0 /\ -O + Z >= 0 /\ N + Z >= 0 /\ M + Z >= 0 /\ L + Z >= 0 /\ K + Z >= 0 /\ J + Z >= 0 /\ A + Z - 1 >= 0 /\ -Y >= 0 /\ X - Y >= 0 /\ -X - Y >= 0 /\ W - Y >= 0 /\ -W - Y >= 0 /\ V - Y >= 0 /\ -V - Y >= 0 /\ U - Y >= 0 /\ -U - Y >= 0 /\ T - Y >= 0 /\ -T - Y >= 0 /\ B - Y - 1 >= 0 /\ S - Y >= 0 /\ -S - Y >= 0 /\ R - Y >= 0 /\ -R - Y >= 0 /\ Q - Y >= 0 /\ -Q - Y >= 0 /\ P - Y >= 0 /\ -P - Y >= 0 /\ O - Y >= 0 /\ -O - Y >= 0 /\ N - Y >= 0 /\ M - Y >= 0 /\ L - Y >= 0 /\ K - Y >= 0 /\ J - Y >= 0 /\ A - Y - 1 >= 0 /\ Y >= 0 /\ X + Y >= 0 /\ -X + Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ V + Y >= 0 /\ -V + Y >= 0 /\ U + Y >= 0 /\ -U + Y >= 0 /\ T + Y >= 0 /\ -T + Y >= 0 /\ B + Y - 1 >= 0 /\ S + Y >= 0 /\ -S + Y >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y >= 0 /\ -Q + Y >= 0 /\ P + Y >= 0 /\ -P + Y >= 0 /\ O + Y >= 0 /\ -O + Y >= 0 /\ N + Y >= 0 /\ M + Y >= 0 /\ L + Y >= 0 /\ K + Y >= 0 /\ J + Y >= 0 /\ A + Y - 1 >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ T - X >= 0 /\ -T - X >= 0 /\ B - X - 1 >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ O - X >= 0 /\ -O - X >= 0 /\ N - X >= 0 /\ M - X >= 0 /\ L - X >= 0 /\ K - X >= 0 /\ J - X >= 0 /\ A - X - 1 >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ V + X >= 0 /\ -V + X >= 0 /\ U + X >= 0 /\ -U + X >= 0 /\ T + X >= 0 /\ -T + X >= 0 /\ B + X - 1 >= 0 /\ S + X >= 0 /\ -S + X >= 0 /\ R + X >= 0 /\ -R + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ O + X >= 0 /\ -O + X >= 0 /\ N + X >= 0 /\ M + X >= 0 /\ L + X >= 0 /\ K + X >= 0 /\ J + X >= 0 /\ A + X - 1 >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ U - W >= 0 /\ -U - W >= 0 /\ T - W >= 0 /\ -T - W >= 0 /\ B - W - 1 >= 0 /\ S - W >= 0 /\ -S - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ O - W >= 0 /\ -O - W >= 0 /\ N - W >= 0 /\ M - W >= 0 /\ L - W >= 0 /\ K - W >= 0 /\ J - W >= 0 /\ A - W - 1 >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ U + W >= 0 /\ -U + W >= 0 /\ T + W >= 0 /\ -T + W >= 0 /\ B + W - 1 >= 0 /\ S + W >= 0 /\ -S + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ O + W >= 0 /\ -O + W >= 0 /\ N + W >= 0 /\ M + W >= 0 /\ L + W >= 0 /\ K + W >= 0 /\ J + W >= 0 /\ A + W - 1 >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ T - V >= 0 /\ -T - V >= 0 /\ B - V - 1 >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ Q - V >= 0 /\ -Q - V >= 0 /\ P - V >= 0 /\ -P - V >= 0 /\ O - V >= 0 /\ -O - V >= 0 /\ N - V >= 0 /\ M - V >= 0 /\ L - V >= 0 /\ K - V >= 0 /\ J - V >= 0 /\ A - V - 1 >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ T + V >= 0 /\ -T + V >= 0 /\ B + V - 1 >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ Q + V >= 0 /\ -Q + V >= 0 /\ P + V >= 0 /\ -P + V >= 0 /\ O + V >= 0 /\ -O + V >= 0 /\ N + V >= 0 /\ M + V >= 0 /\ L + V >= 0 /\ K + V >= 0 /\ J + V >= 0 /\ A + V - 1 >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ B - U - 1 >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ Q - U >= 0 /\ -Q - U >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ N - U >= 0 /\ M - U >= 0 /\ L - U >= 0 /\ K - U >= 0 /\ J - U >= 0 /\ A - U - 1 >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ B + U - 1 >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U >= 0 /\ -Q + U >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ N + U >= 0 /\ M + U >= 0 /\ L + U >= 0 /\ K + U >= 0 /\ J + U >= 0 /\ A + U - 1 >= 0 /\ -T >= 0 /\ B - T - 1 >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ Q - T >= 0 /\ -Q - T >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ N - T >= 0 /\ M - T >= 0 /\ L - T >= 0 /\ K - T >= 0 /\ J - T >= 0 /\ A - T - 1 >= 0 /\ T >= 0 /\ B + T - 1 >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ Q + T >= 0 /\ -Q + T >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ N + T >= 0 /\ M + T >= 0 /\ L + T >= 0 /\ K + T >= 0 /\ J + T >= 0 /\ A + T - 1 >= 0 /\ A - B >= 0 /\ B - 1 >= 0 /\ S + B - 1 >= 0 /\ -S + B - 1 >= 0 /\ R + B - 1 >= 0 /\ -R + B - 1 >= 0 /\ Q + B - 1 >= 0 /\ -Q + B - 1 >= 0 /\ P + B - 1 >= 0 /\ -P + B - 1 >= 0 /\ O + B - 1 >= 0 /\ -O + B - 1 >= 0 /\ N + B - 1 >= 0 /\ M + B - 1 >= 0 /\ L + B - 1 >= 0 /\ K + B - 1 >= 0 /\ J + B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ Q - S >= 0 /\ -Q - S >= 0 /\ P - S >= 0 /\ -P - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ N - S >= 0 /\ M - S >= 0 /\ L - S >= 0 /\ K - S >= 0 /\ J - S >= 0 /\ A - S - 1 >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ Q + S >= 0 /\ -Q + S >= 0 /\ P + S >= 0 /\ -P + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ N + S >= 0 /\ M + S >= 0 /\ L + S >= 0 /\ K + S >= 0 /\ J + S >= 0 /\ A + S - 1 >= 0 /\ -R >= 0 /\ Q - R >= 0 /\ -Q - R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ N - R >= 0 /\ M - R >= 0 /\ L - R >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ A - R - 1 >= 0 /\ R >= 0 /\ Q + R >= 0 /\ -Q + R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ N + R >= 0 /\ M + R >= 0 /\ L + R >= 0 /\ K + R >= 0 /\ J + R >= 0 /\ A + R - 1 >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ O - Q >= 0 /\ -O - Q >= 0 /\ N - Q >= 0 /\ M - Q >= 0 /\ L - Q >= 0 /\ K - Q >= 0 /\ J - Q >= 0 /\ A - Q - 1 >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ O + Q >= 0 /\ -O + Q >= 0 /\ N + Q >= 0 /\ M + Q >= 0 /\ L + Q >= 0 /\ K + Q >= 0 /\ J + Q >= 0 /\ A + Q - 1 >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ N - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ K - P >= 0 /\ J - P >= 0 /\ A - P - 1 >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ N + P >= 0 /\ M + P >= 0 /\ L + P >= 0 /\ K + P >= 0 /\ J + P >= 0 /\ A + P - 1 >= 0 /\ -O >= 0 /\ N - O >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ A - O - 1 >= 0 /\ O >= 0 /\ N + O >= 0 /\ M + O >= 0 /\ L + O >= 0 /\ K + O >= 0 /\ J + O >= 0 /\ A + O - 1 >= 0 /\ N >= 0 /\ M + N >= 0 /\ L + N >= 0 /\ K + N >= 0 /\ J + N >= 0 /\ A + N - 1 >= 0 /\ M >= 0 /\ L + M >= 0 /\ K + M >= 0 /\ J + M >= 0 /\ A + M - 1 >= 0 /\ J - L >= 0 /\ L >= 0 /\ K + L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L - 1 >= 0 /\ K >= 0 /\ J + K >= 0 /\ A + K - 1 >= 0 /\ J >= 0 /\ A + J - 1 >= 0 /\ A - 1 >= 0 /\ C >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1) -> Com_1(f2(A, B, C, T + D + U + 1, V + E + W - 1, X + F + Z + B1, Y + G + A1, H, I, J, K, L, M, N, O, P, Q, R, S, 0, 0, 0, 0, 0, 0, 0, 0, 0, D1)) [ -I >= 0 /\ H - I >= 0 /\ -H - I >= 0 /\ G - I - 1 >= 0 /\ F - I >= 0 /\ E - I >= 0 /\ D - I >= 0 /\ C - I >= 0 /\ -C - I >= 0 /\ B1 - I >= 0 /\ -B1 - I >= 0 /\ A1 - I >= 0 /\ -A1 - I >= 0 /\ Z - I >= 0 /\ -Z - I >= 0 /\ Y - I >= 0 /\ -Y - I >= 0 /\ X - I >= 0 /\ -X - I >= 0 /\ W - I >= 0 /\ -W - I >= 0 /\ V - I >= 0 /\ -V - I >= 0 /\ U - I >= 0 /\ -U - I >= 0 /\ T - I >= 0 /\ -T - I >= 0 /\ B - I >= 0 /\ -B - I >= 0 /\ S - I >= 0 /\ -S - I >= 0 /\ R - I >= 0 /\ -R - I >= 0 /\ Q - I >= 0 /\ -Q - I >= 0 /\ P - I >= 0 /\ -P - I >= 0 /\ O - I >= 0 /\ -O - I >= 0 /\ N - I >= 0 /\ M - I >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ J - I >= 0 /\ A - I >= 0 /\ -A - I >= 0 /\ I >= 0 /\ H + I >= 0 /\ -H + I >= 0 /\ G + I - 1 >= 0 /\ F + I >= 0 /\ E + I >= 0 /\ D + I >= 0 /\ C + I >= 0 /\ -C + I >= 0 /\ B1 + I >= 0 /\ -B1 + I >= 0 /\ A1 + I >= 0 /\ -A1 + I >= 0 /\ Z + I >= 0 /\ -Z + I >= 0 /\ Y + I >= 0 /\ -Y + I >= 0 /\ X + I >= 0 /\ -X + I >= 0 /\ W + I >= 0 /\ -W + I >= 0 /\ V + I >= 0 /\ -V + I >= 0 /\ U + I >= 0 /\ -U + I >= 0 /\ T + I >= 0 /\ -T + I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ S + I >= 0 /\ -S + I >= 0 /\ R + I >= 0 /\ -R + I >= 0 /\ Q + I >= 0 /\ -Q + I >= 0 /\ P + I >= 0 /\ -P + I >= 0 /\ O + I >= 0 /\ -O + I >= 0 /\ N + I >= 0 /\ M + I >= 0 /\ L + I >= 0 /\ K + I >= 0 /\ J + I >= 0 /\ A + I >= 0 /\ -A + I >= 0 /\ -H >= 0 /\ G - H - 1 >= 0 /\ F - H >= 0 /\ E - H >= 0 /\ D - H >= 0 /\ C - H >= 0 /\ -C - H >= 0 /\ B1 - H >= 0 /\ -B1 - H >= 0 /\ A1 - H >= 0 /\ -A1 - H >= 0 /\ Z - H >= 0 /\ -Z - H >= 0 /\ Y - H >= 0 /\ -Y - H >= 0 /\ X - H >= 0 /\ -X - H >= 0 /\ W - H >= 0 /\ -W - H >= 0 /\ V - H >= 0 /\ -V - H >= 0 /\ U - H >= 0 /\ -U - H >= 0 /\ T - H >= 0 /\ -T - H >= 0 /\ B - H >= 0 /\ -B - H >= 0 /\ S - H >= 0 /\ -S - H >= 0 /\ R - H >= 0 /\ -R - H >= 0 /\ Q - H >= 0 /\ -Q - H >= 0 /\ P - H >= 0 /\ -P - H >= 0 /\ O - H >= 0 /\ -O - H >= 0 /\ N - H >= 0 /\ M - H >= 0 /\ L - H >= 0 /\ K - H >= 0 /\ J - H >= 0 /\ A - H >= 0 /\ -A - H >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ C + H >= 0 /\ -C + H >= 0 /\ B1 + H >= 0 /\ -B1 + H >= 0 /\ A1 + H >= 0 /\ -A1 + H >= 0 /\ Z + H >= 0 /\ -Z + H >= 0 /\ Y + H >= 0 /\ -Y + H >= 0 /\ X + H >= 0 /\ -X + H >= 0 /\ W + H >= 0 /\ -W + H >= 0 /\ V + H >= 0 /\ -V + H >= 0 /\ U + H >= 0 /\ -U + H >= 0 /\ T + H >= 0 /\ -T + H >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ S + H >= 0 /\ -S + H >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ Q + H >= 0 /\ -Q + H >= 0 /\ P + H >= 0 /\ -P + H >= 0 /\ O + H >= 0 /\ -O + H >= 0 /\ N + H >= 0 /\ M + H >= 0 /\ L + H >= 0 /\ K + H >= 0 /\ J + H >= 0 /\ A + H >= 0 /\ -A + H >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 1 >= 0 /\ -C + G - 1 >= 0 /\ B1 + G - 1 >= 0 /\ -B1 + G - 1 >= 0 /\ A1 + G - 1 >= 0 /\ -A1 + G - 1 >= 0 /\ Z + G - 1 >= 0 /\ -Z + G - 1 >= 0 /\ Y + G - 1 >= 0 /\ -Y + G - 1 >= 0 /\ X + G - 1 >= 0 /\ -X + G - 1 >= 0 /\ W + G - 1 >= 0 /\ -W + G - 1 >= 0 /\ V + G - 1 >= 0 /\ -V + G - 1 >= 0 /\ U + G - 1 >= 0 /\ -U + G - 1 >= 0 /\ T + G - 1 >= 0 /\ -T + G - 1 >= 0 /\ B + G - 1 >= 0 /\ -B + G - 1 >= 0 /\ S + G - 1 >= 0 /\ -S + G - 1 >= 0 /\ R + G - 1 >= 0 /\ -R + G - 1 >= 0 /\ Q + G - 1 >= 0 /\ -Q + G - 1 >= 0 /\ P + G - 1 >= 0 /\ -P + G - 1 >= 0 /\ O + G - 1 >= 0 /\ -O + G - 1 >= 0 /\ N + G - 1 >= 0 /\ M + G - 1 >= 0 /\ L + G - 1 >= 0 /\ K + G - 1 >= 0 /\ J + G - 1 >= 0 /\ A + G - 1 >= 0 /\ -A + G - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ C + F >= 0 /\ -C + F >= 0 /\ B1 + F >= 0 /\ -B1 + F >= 0 /\ A1 + F >= 0 /\ -A1 + F >= 0 /\ Z + F >= 0 /\ -Z + F >= 0 /\ Y + F >= 0 /\ -Y + F >= 0 /\ X + F >= 0 /\ -X + F >= 0 /\ W + F >= 0 /\ -W + F >= 0 /\ V + F >= 0 /\ -V + F >= 0 /\ U + F >= 0 /\ -U + F >= 0 /\ T + F >= 0 /\ -T + F >= 0 /\ B + F >= 0 /\ -B + F >= 0 /\ S + F >= 0 /\ -S + F >= 0 /\ R + F >= 0 /\ -R + F >= 0 /\ Q + F >= 0 /\ -Q + F >= 0 /\ P + F >= 0 /\ -P + F >= 0 /\ O + F >= 0 /\ -O + F >= 0 /\ N + F >= 0 /\ M + F >= 0 /\ L + F >= 0 /\ K + F >= 0 /\ J + F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B1 + E >= 0 /\ -B1 + E >= 0 /\ A1 + E >= 0 /\ -A1 + E >= 0 /\ Z + E >= 0 /\ -Z + E >= 0 /\ Y + E >= 0 /\ -Y + E >= 0 /\ X + E >= 0 /\ -X + E >= 0 /\ W + E >= 0 /\ -W + E >= 0 /\ V + E >= 0 /\ -V + E >= 0 /\ U + E >= 0 /\ -U + E >= 0 /\ T + E >= 0 /\ -T + E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ S + E >= 0 /\ -S + E >= 0 /\ R + E >= 0 /\ -R + E >= 0 /\ Q + E >= 0 /\ -Q + E >= 0 /\ P + E >= 0 /\ -P + E >= 0 /\ O + E >= 0 /\ -O + E >= 0 /\ N + E >= 0 /\ M + E >= 0 /\ L + E >= 0 /\ K + E >= 0 /\ J + E >= 0 /\ A + E >= 0 /\ -A + E >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B1 + D >= 0 /\ -B1 + D >= 0 /\ A1 + D >= 0 /\ -A1 + D >= 0 /\ Z + D >= 0 /\ -Z + D >= 0 /\ Y + D >= 0 /\ -Y + D >= 0 /\ X + D >= 0 /\ -X + D >= 0 /\ W + D >= 0 /\ -W + D >= 0 /\ V + D >= 0 /\ -V + D >= 0 /\ U + D >= 0 /\ -U + D >= 0 /\ T + D >= 0 /\ -T + D >= 0 /\ B + D >= 0 /\ -B + D >= 0 /\ S + D >= 0 /\ -S + D >= 0 /\ R + D >= 0 /\ -R + D >= 0 /\ Q + D >= 0 /\ -Q + D >= 0 /\ P + D >= 0 /\ -P + D >= 0 /\ O + D >= 0 /\ -O + D >= 0 /\ N + D >= 0 /\ M + D >= 0 /\ L + D >= 0 /\ K + D >= 0 /\ J + D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ -C >= 0 /\ B1 - C >= 0 /\ -B1 - C >= 0 /\ A1 - C >= 0 /\ -A1 - C >= 0 /\ Z - C >= 0 /\ -Z - C >= 0 /\ Y - C >= 0 /\ -Y - C >= 0 /\ X - C >= 0 /\ -X - C >= 0 /\ W - C >= 0 /\ -W - C >= 0 /\ V - C >= 0 /\ -V - C >= 0 /\ U - C >= 0 /\ -U - C >= 0 /\ T - C >= 0 /\ -T - C >= 0 /\ B - C >= 0 /\ -B - C >= 0 /\ S - C >= 0 /\ -S - C >= 0 /\ R - C >= 0 /\ -R - C >= 0 /\ Q - C >= 0 /\ -Q - C >= 0 /\ P - C >= 0 /\ -P - C >= 0 /\ O - C >= 0 /\ -O - C >= 0 /\ N - C >= 0 /\ M - C >= 0 /\ L - C >= 0 /\ K - C >= 0 /\ J - C >= 0 /\ A - C >= 0 /\ -A - C >= 0 /\ C >= 0 /\ B1 + C >= 0 /\ -B1 + C >= 0 /\ A1 + C >= 0 /\ -A1 + C >= 0 /\ Z + C >= 0 /\ -Z + C >= 0 /\ Y + C >= 0 /\ -Y + C >= 0 /\ X + C >= 0 /\ -X + C >= 0 /\ W + C >= 0 /\ -W + C >= 0 /\ V + C >= 0 /\ -V + C >= 0 /\ U + C >= 0 /\ -U + C >= 0 /\ T + C >= 0 /\ -T + C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ S + C >= 0 /\ -S + C >= 0 /\ R + C >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ P + C >= 0 /\ -P + C >= 0 /\ O + C >= 0 /\ -O + C >= 0 /\ N + C >= 0 /\ M + C >= 0 /\ L + C >= 0 /\ K + C >= 0 /\ J + C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ -B1 >= 0 /\ A1 - B1 >= 0 /\ -A1 - B1 >= 0 /\ Z - B1 >= 0 /\ -Z - B1 >= 0 /\ Y - B1 >= 0 /\ -Y - B1 >= 0 /\ X - B1 >= 0 /\ -X - B1 >= 0 /\ W - B1 >= 0 /\ -W - B1 >= 0 /\ V - B1 >= 0 /\ -V - B1 >= 0 /\ U - B1 >= 0 /\ -U - B1 >= 0 /\ T - B1 >= 0 /\ -T - B1 >= 0 /\ B - B1 >= 0 /\ -B - B1 >= 0 /\ S - B1 >= 0 /\ -S - B1 >= 0 /\ R - B1 >= 0 /\ -R - B1 >= 0 /\ Q - B1 >= 0 /\ -Q - B1 >= 0 /\ P - B1 >= 0 /\ -P - B1 >= 0 /\ O - B1 >= 0 /\ -O - B1 >= 0 /\ N - B1 >= 0 /\ M - B1 >= 0 /\ L - B1 >= 0 /\ K - B1 >= 0 /\ J - B1 >= 0 /\ A - B1 >= 0 /\ -A - B1 >= 0 /\ B1 >= 0 /\ A1 + B1 >= 0 /\ -A1 + B1 >= 0 /\ Z + B1 >= 0 /\ -Z + B1 >= 0 /\ Y + B1 >= 0 /\ -Y + B1 >= 0 /\ X + B1 >= 0 /\ -X + B1 >= 0 /\ W + B1 >= 0 /\ -W + B1 >= 0 /\ V + B1 >= 0 /\ -V + B1 >= 0 /\ U + B1 >= 0 /\ -U + B1 >= 0 /\ T + B1 >= 0 /\ -T + B1 >= 0 /\ B + B1 >= 0 /\ -B + B1 >= 0 /\ S + B1 >= 0 /\ -S + B1 >= 0 /\ R + B1 >= 0 /\ -R + B1 >= 0 /\ Q + B1 >= 0 /\ -Q + B1 >= 0 /\ P + B1 >= 0 /\ -P + B1 >= 0 /\ O + B1 >= 0 /\ -O + B1 >= 0 /\ N + B1 >= 0 /\ M + B1 >= 0 /\ L + B1 >= 0 /\ K + B1 >= 0 /\ J + B1 >= 0 /\ A + B1 >= 0 /\ -A + B1 >= 0 /\ -A1 >= 0 /\ Z - A1 >= 0 /\ -Z - A1 >= 0 /\ Y - A1 >= 0 /\ -Y - A1 >= 0 /\ X - A1 >= 0 /\ -X - A1 >= 0 /\ W - A1 >= 0 /\ -W - A1 >= 0 /\ V - A1 >= 0 /\ -V - A1 >= 0 /\ U - A1 >= 0 /\ -U - A1 >= 0 /\ T - A1 >= 0 /\ -T - A1 >= 0 /\ B - A1 >= 0 /\ -B - A1 >= 0 /\ S - A1 >= 0 /\ -S - A1 >= 0 /\ R - A1 >= 0 /\ -R - A1 >= 0 /\ Q - A1 >= 0 /\ -Q - A1 >= 0 /\ P - A1 >= 0 /\ -P - A1 >= 0 /\ O - A1 >= 0 /\ -O - A1 >= 0 /\ N - A1 >= 0 /\ M - A1 >= 0 /\ L - A1 >= 0 /\ K - A1 >= 0 /\ J - A1 >= 0 /\ A - A1 >= 0 /\ -A - A1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ -Z + A1 >= 0 /\ Y + A1 >= 0 /\ -Y + A1 >= 0 /\ X + A1 >= 0 /\ -X + A1 >= 0 /\ W + A1 >= 0 /\ -W + A1 >= 0 /\ V + A1 >= 0 /\ -V + A1 >= 0 /\ U + A1 >= 0 /\ -U + A1 >= 0 /\ T + A1 >= 0 /\ -T + A1 >= 0 /\ B + A1 >= 0 /\ -B + A1 >= 0 /\ S + A1 >= 0 /\ -S + A1 >= 0 /\ R + A1 >= 0 /\ -R + A1 >= 0 /\ Q + A1 >= 0 /\ -Q + A1 >= 0 /\ P + A1 >= 0 /\ -P + A1 >= 0 /\ O + A1 >= 0 /\ -O + A1 >= 0 /\ N + A1 >= 0 /\ M + A1 >= 0 /\ L + A1 >= 0 /\ K + A1 >= 0 /\ J + A1 >= 0 /\ A + A1 >= 0 /\ -A + A1 >= 0 /\ -Z >= 0 /\ Y - Z >= 0 /\ -Y - Z >= 0 /\ X - Z >= 0 /\ -X - Z >= 0 /\ W - Z >= 0 /\ -W - Z >= 0 /\ V - Z >= 0 /\ -V - Z >= 0 /\ U - Z >= 0 /\ -U - Z >= 0 /\ T - Z >= 0 /\ -T - Z >= 0 /\ B - Z >= 0 /\ -B - Z >= 0 /\ S - Z >= 0 /\ -S - Z >= 0 /\ R - Z >= 0 /\ -R - Z >= 0 /\ Q - Z >= 0 /\ -Q - Z >= 0 /\ P - Z >= 0 /\ -P - Z >= 0 /\ O - Z >= 0 /\ -O - Z >= 0 /\ N - Z >= 0 /\ M - Z >= 0 /\ L - Z >= 0 /\ K - Z >= 0 /\ J - Z >= 0 /\ A - Z >= 0 /\ -A - Z >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ -Y + Z >= 0 /\ X + Z >= 0 /\ -X + Z >= 0 /\ W + Z >= 0 /\ -W + Z >= 0 /\ V + Z >= 0 /\ -V + Z >= 0 /\ U + Z >= 0 /\ -U + Z >= 0 /\ T + Z >= 0 /\ -T + Z >= 0 /\ B + Z >= 0 /\ -B + Z >= 0 /\ S + Z >= 0 /\ -S + Z >= 0 /\ R + Z >= 0 /\ -R + Z >= 0 /\ Q + Z >= 0 /\ -Q + Z >= 0 /\ P + Z >= 0 /\ -P + Z >= 0 /\ O + Z >= 0 /\ -O + Z >= 0 /\ N + Z >= 0 /\ M + Z >= 0 /\ L + Z >= 0 /\ K + Z >= 0 /\ J + Z >= 0 /\ A + Z >= 0 /\ -A + Z >= 0 /\ -Y >= 0 /\ X - Y >= 0 /\ -X - Y >= 0 /\ W - Y >= 0 /\ -W - Y >= 0 /\ V - Y >= 0 /\ -V - Y >= 0 /\ U - Y >= 0 /\ -U - Y >= 0 /\ T - Y >= 0 /\ -T - Y >= 0 /\ B - Y >= 0 /\ -B - Y >= 0 /\ S - Y >= 0 /\ -S - Y >= 0 /\ R - Y >= 0 /\ -R - Y >= 0 /\ Q - Y >= 0 /\ -Q - Y >= 0 /\ P - Y >= 0 /\ -P - Y >= 0 /\ O - Y >= 0 /\ -O - Y >= 0 /\ N - Y >= 0 /\ M - Y >= 0 /\ L - Y >= 0 /\ K - Y >= 0 /\ J - Y >= 0 /\ A - Y >= 0 /\ -A - Y >= 0 /\ Y >= 0 /\ X + Y >= 0 /\ -X + Y >= 0 /\ W + Y >= 0 /\ -W + Y >= 0 /\ V + Y >= 0 /\ -V + Y >= 0 /\ U + Y >= 0 /\ -U + Y >= 0 /\ T + Y >= 0 /\ -T + Y >= 0 /\ B + Y >= 0 /\ -B + Y >= 0 /\ S + Y >= 0 /\ -S + Y >= 0 /\ R + Y >= 0 /\ -R + Y >= 0 /\ Q + Y >= 0 /\ -Q + Y >= 0 /\ P + Y >= 0 /\ -P + Y >= 0 /\ O + Y >= 0 /\ -O + Y >= 0 /\ N + Y >= 0 /\ M + Y >= 0 /\ L + Y >= 0 /\ K + Y >= 0 /\ J + Y >= 0 /\ A + Y >= 0 /\ -A + Y >= 0 /\ -X >= 0 /\ W - X >= 0 /\ -W - X >= 0 /\ V - X >= 0 /\ -V - X >= 0 /\ U - X >= 0 /\ -U - X >= 0 /\ T - X >= 0 /\ -T - X >= 0 /\ B - X >= 0 /\ -B - X >= 0 /\ S - X >= 0 /\ -S - X >= 0 /\ R - X >= 0 /\ -R - X >= 0 /\ Q - X >= 0 /\ -Q - X >= 0 /\ P - X >= 0 /\ -P - X >= 0 /\ O - X >= 0 /\ -O - X >= 0 /\ N - X >= 0 /\ M - X >= 0 /\ L - X >= 0 /\ K - X >= 0 /\ J - X >= 0 /\ A - X >= 0 /\ -A - X >= 0 /\ X >= 0 /\ W + X >= 0 /\ -W + X >= 0 /\ V + X >= 0 /\ -V + X >= 0 /\ U + X >= 0 /\ -U + X >= 0 /\ T + X >= 0 /\ -T + X >= 0 /\ B + X >= 0 /\ -B + X >= 0 /\ S + X >= 0 /\ -S + X >= 0 /\ R + X >= 0 /\ -R + X >= 0 /\ Q + X >= 0 /\ -Q + X >= 0 /\ P + X >= 0 /\ -P + X >= 0 /\ O + X >= 0 /\ -O + X >= 0 /\ N + X >= 0 /\ M + X >= 0 /\ L + X >= 0 /\ K + X >= 0 /\ J + X >= 0 /\ A + X >= 0 /\ -A + X >= 0 /\ -W >= 0 /\ V - W >= 0 /\ -V - W >= 0 /\ U - W >= 0 /\ -U - W >= 0 /\ T - W >= 0 /\ -T - W >= 0 /\ B - W >= 0 /\ -B - W >= 0 /\ S - W >= 0 /\ -S - W >= 0 /\ R - W >= 0 /\ -R - W >= 0 /\ Q - W >= 0 /\ -Q - W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ O - W >= 0 /\ -O - W >= 0 /\ N - W >= 0 /\ M - W >= 0 /\ L - W >= 0 /\ K - W >= 0 /\ J - W >= 0 /\ A - W >= 0 /\ -A - W >= 0 /\ W >= 0 /\ V + W >= 0 /\ -V + W >= 0 /\ U + W >= 0 /\ -U + W >= 0 /\ T + W >= 0 /\ -T + W >= 0 /\ B + W >= 0 /\ -B + W >= 0 /\ S + W >= 0 /\ -S + W >= 0 /\ R + W >= 0 /\ -R + W >= 0 /\ Q + W >= 0 /\ -Q + W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ O + W >= 0 /\ -O + W >= 0 /\ N + W >= 0 /\ M + W >= 0 /\ L + W >= 0 /\ K + W >= 0 /\ J + W >= 0 /\ A + W >= 0 /\ -A + W >= 0 /\ -V >= 0 /\ U - V >= 0 /\ -U - V >= 0 /\ T - V >= 0 /\ -T - V >= 0 /\ B - V >= 0 /\ -B - V >= 0 /\ S - V >= 0 /\ -S - V >= 0 /\ R - V >= 0 /\ -R - V >= 0 /\ Q - V >= 0 /\ -Q - V >= 0 /\ P - V >= 0 /\ -P - V >= 0 /\ O - V >= 0 /\ -O - V >= 0 /\ N - V >= 0 /\ M - V >= 0 /\ L - V >= 0 /\ K - V >= 0 /\ J - V >= 0 /\ A - V >= 0 /\ -A - V >= 0 /\ V >= 0 /\ U + V >= 0 /\ -U + V >= 0 /\ T + V >= 0 /\ -T + V >= 0 /\ B + V >= 0 /\ -B + V >= 0 /\ S + V >= 0 /\ -S + V >= 0 /\ R + V >= 0 /\ -R + V >= 0 /\ Q + V >= 0 /\ -Q + V >= 0 /\ P + V >= 0 /\ -P + V >= 0 /\ O + V >= 0 /\ -O + V >= 0 /\ N + V >= 0 /\ M + V >= 0 /\ L + V >= 0 /\ K + V >= 0 /\ J + V >= 0 /\ A + V >= 0 /\ -A + V >= 0 /\ -U >= 0 /\ T - U >= 0 /\ -T - U >= 0 /\ B - U >= 0 /\ -B - U >= 0 /\ S - U >= 0 /\ -S - U >= 0 /\ R - U >= 0 /\ -R - U >= 0 /\ Q - U >= 0 /\ -Q - U >= 0 /\ P - U >= 0 /\ -P - U >= 0 /\ O - U >= 0 /\ -O - U >= 0 /\ N - U >= 0 /\ M - U >= 0 /\ L - U >= 0 /\ K - U >= 0 /\ J - U >= 0 /\ A - U >= 0 /\ -A - U >= 0 /\ U >= 0 /\ T + U >= 0 /\ -T + U >= 0 /\ B + U >= 0 /\ -B + U >= 0 /\ S + U >= 0 /\ -S + U >= 0 /\ R + U >= 0 /\ -R + U >= 0 /\ Q + U >= 0 /\ -Q + U >= 0 /\ P + U >= 0 /\ -P + U >= 0 /\ O + U >= 0 /\ -O + U >= 0 /\ N + U >= 0 /\ M + U >= 0 /\ L + U >= 0 /\ K + U >= 0 /\ J + U >= 0 /\ A + U >= 0 /\ -A + U >= 0 /\ -T >= 0 /\ B - T >= 0 /\ -B - T >= 0 /\ S - T >= 0 /\ -S - T >= 0 /\ R - T >= 0 /\ -R - T >= 0 /\ Q - T >= 0 /\ -Q - T >= 0 /\ P - T >= 0 /\ -P - T >= 0 /\ O - T >= 0 /\ -O - T >= 0 /\ N - T >= 0 /\ M - T >= 0 /\ L - T >= 0 /\ K - T >= 0 /\ J - T >= 0 /\ A - T >= 0 /\ -A - T >= 0 /\ T >= 0 /\ B + T >= 0 /\ -B + T >= 0 /\ S + T >= 0 /\ -S + T >= 0 /\ R + T >= 0 /\ -R + T >= 0 /\ Q + T >= 0 /\ -Q + T >= 0 /\ P + T >= 0 /\ -P + T >= 0 /\ O + T >= 0 /\ -O + T >= 0 /\ N + T >= 0 /\ M + T >= 0 /\ L + T >= 0 /\ K + T >= 0 /\ J + T >= 0 /\ A + T >= 0 /\ -A + T >= 0 /\ -B >= 0 /\ S - B >= 0 /\ -S - B >= 0 /\ R - B >= 0 /\ -R - B >= 0 /\ Q - B >= 0 /\ -Q - B >= 0 /\ P - B >= 0 /\ -P - B >= 0 /\ O - B >= 0 /\ -O - B >= 0 /\ N - B >= 0 /\ M - B >= 0 /\ L - B >= 0 /\ K - B >= 0 /\ J - B >= 0 /\ A - B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ S + B >= 0 /\ -S + B >= 0 /\ R + B >= 0 /\ -R + B >= 0 /\ Q + B >= 0 /\ -Q + B >= 0 /\ P + B >= 0 /\ -P + B >= 0 /\ O + B >= 0 /\ -O + B >= 0 /\ N + B >= 0 /\ M + B >= 0 /\ L + B >= 0 /\ K + B >= 0 /\ J + B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ -S >= 0 /\ R - S >= 0 /\ -R - S >= 0 /\ Q - S >= 0 /\ -Q - S >= 0 /\ P - S >= 0 /\ -P - S >= 0 /\ O - S >= 0 /\ -O - S >= 0 /\ N - S >= 0 /\ M - S >= 0 /\ L - S >= 0 /\ K - S >= 0 /\ J - S >= 0 /\ A - S >= 0 /\ -A - S >= 0 /\ S >= 0 /\ R + S >= 0 /\ -R + S >= 0 /\ Q + S >= 0 /\ -Q + S >= 0 /\ P + S >= 0 /\ -P + S >= 0 /\ O + S >= 0 /\ -O + S >= 0 /\ N + S >= 0 /\ M + S >= 0 /\ L + S >= 0 /\ K + S >= 0 /\ J + S >= 0 /\ A + S >= 0 /\ -A + S >= 0 /\ -R >= 0 /\ Q - R >= 0 /\ -Q - R >= 0 /\ P - R >= 0 /\ -P - R >= 0 /\ O - R >= 0 /\ -O - R >= 0 /\ N - R >= 0 /\ M - R >= 0 /\ L - R >= 0 /\ K - R >= 0 /\ J - R >= 0 /\ A - R >= 0 /\ -A - R >= 0 /\ R >= 0 /\ Q + R >= 0 /\ -Q + R >= 0 /\ P + R >= 0 /\ -P + R >= 0 /\ O + R >= 0 /\ -O + R >= 0 /\ N + R >= 0 /\ M + R >= 0 /\ L + R >= 0 /\ K + R >= 0 /\ J + R >= 0 /\ A + R >= 0 /\ -A + R >= 0 /\ -Q >= 0 /\ P - Q >= 0 /\ -P - Q >= 0 /\ O - Q >= 0 /\ -O - Q >= 0 /\ N - Q >= 0 /\ M - Q >= 0 /\ L - Q >= 0 /\ K - Q >= 0 /\ J - Q >= 0 /\ A - Q >= 0 /\ -A - Q >= 0 /\ Q >= 0 /\ P + Q >= 0 /\ -P + Q >= 0 /\ O + Q >= 0 /\ -O + Q >= 0 /\ N + Q >= 0 /\ M + Q >= 0 /\ L + Q >= 0 /\ K + Q >= 0 /\ J + Q >= 0 /\ A + Q >= 0 /\ -A + Q >= 0 /\ -P >= 0 /\ O - P >= 0 /\ -O - P >= 0 /\ N - P >= 0 /\ M - P >= 0 /\ L - P >= 0 /\ K - P >= 0 /\ J - P >= 0 /\ A - P >= 0 /\ -A - P >= 0 /\ P >= 0 /\ O + P >= 0 /\ -O + P >= 0 /\ N + P >= 0 /\ M + P >= 0 /\ L + P >= 0 /\ K + P >= 0 /\ J + P >= 0 /\ A + P >= 0 /\ -A + P >= 0 /\ -O >= 0 /\ N - O >= 0 /\ M - O >= 0 /\ L - O >= 0 /\ K - O >= 0 /\ J - O >= 0 /\ A - O >= 0 /\ -A - O >= 0 /\ O >= 0 /\ N + O >= 0 /\ M + O >= 0 /\ L + O >= 0 /\ K + O >= 0 /\ J + O >= 0 /\ A + O >= 0 /\ -A + O >= 0 /\ N >= 0 /\ M + N >= 0 /\ L + N >= 0 /\ K + N >= 0 /\ J + N >= 0 /\ A + N >= 0 /\ -A + N >= 0 /\ M >= 0 /\ L + M >= 0 /\ K + M >= 0 /\ J + M >= 0 /\ A + M >= 0 /\ -A + M >= 0 /\ J - L >= 0 /\ L >= 0 /\ K + L >= 0 /\ J + L >= 0 /\ -J + L >= 0 /\ A + L >= 0 /\ -A + L >= 0 /\ K >= 0 /\ J + K >= 0 /\ A + K >= 0 /\ -A + K >= 0 /\ J >= 0 /\ A + J >= 0 /\ -A + J >= 0 /\ -A >= 0 /\ A >= 0 /\ G >= 1 /\ F >= C1 /\ C1 >= 1 /\ E >= C1 ]
)