(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1 C1 D1 E1 F1 G1 H1 I1 J1 K1 L1 M1 N1 O1 P1)
(RULES
  f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f422(3, 43690, 3, Q1, 0, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1))
  f422(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f422(A, B, Q1, R1, E + 1, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ E >= 0 /\ B + E - 43690 >= 0 /\ -B + E + 43690 >= 0 /\ A + E - 3 >= 0 /\ -A + E + 3 >= 0 /\ -B + 43690 >= 0 /\ A - B + 43687 >= 0 /\ -A - B + 43693 >= 0 /\ B - 43690 >= 0 /\ A + B - 43693 >= 0 /\ -A + B - 43687 >= 0 /\ -A + 3 >= 0 /\ A - 3 >= 0 /\ 149 >= E ]
  f437(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f441(A, B, C, D, E, F, 0, 0, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ F >= 0 /\ E + F - 150 >= 0 /\ B + F - 43690 >= 0 /\ -B + F + 43690 >= 0 /\ E - 150 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ B - 43690 >= 0 /\ 49 >= F ]
  f441(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f441(A, B, C, D, E, F, Q1, H + 1, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ H >= 0 /\ F + H >= 0 /\ E + H - 150 >= 0 /\ B + H - 43690 >= 0 /\ -B + H + 43690 >= 0 /\ F >= 0 /\ E + F - 150 >= 0 /\ B + F - 43690 >= 0 /\ -B + F + 43690 >= 0 /\ E - 150 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ B - 43690 >= 0 /\ 49 >= H ]
  f455(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f461(A, B, C, D, E, F, G, H, I, 0, 0, Q1, 0, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I >= 0 /\ F + I - 50 >= 0 /\ E + I - 150 >= 0 /\ B + I - 43690 >= 0 /\ -B + I + 43690 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ B + F - 43740 >= 0 /\ -B + F + 43640 >= 0 /\ E - 150 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ B - 43690 >= 0 /\ 99 >= I ]
  f461(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f461(A, B, C, D, E, F, G, H, I, Q1, R1, S1, M + 2, T1, U1, V1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I >= 0 /\ F + I - 50 >= 0 /\ E + I - 150 >= 0 /\ B + I - 43690 >= 0 /\ -B + I + 43690 >= 0 /\ M + I >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ B + F - 43740 >= 0 /\ -B + F + 43640 >= 0 /\ M + F - 50 >= 0 /\ E - 150 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ M + E - 150 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ M - B + 43690 >= 0 /\ B - 43690 >= 0 /\ M + B - 43690 >= 0 /\ M >= 0 /\ 31 >= M ]
  f485(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f485(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q - 1, Q1, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ B + I - 43790 >= 0 /\ -B + I + 43590 >= 0 /\ -Q + I - 2 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ B + F - 43740 >= 0 /\ -B + F + 43640 >= 0 /\ -Q + F + 48 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ -Q + E - 52 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ B - N1 - 43590 >= 0 /\ -B - N1 + 43790 >= 0 /\ -Q - N1 + 198 >= 0 /\ N1 - 100 >= 0 /\ B + N1 - 43790 >= 0 /\ -B + N1 + 43590 >= 0 /\ -Q + N1 - 2 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ -Q - B + 43788 >= 0 /\ B - 43690 >= 0 /\ -Q + B - 43592 >= 0 /\ -Q + 98 >= 0 /\ Q >= 0 ]
  f501(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f501(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S + 1, Q1, R1, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ S + I - 100 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ S + F - 50 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ S + E - 150 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ S - N1 + 100 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ S + N1 - 100 >= 0 /\ -Q + N1 - 101 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S >= 0 /\ -Q + S - 1 >= 0 /\ -Q - 1 >= 0 /\ 49 >= S ]
  f526(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f526(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W + 1, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ K1 + I - 101 >= 0 /\ -K1 + I - 99 >= 0 /\ H1 + I - 101 >= 0 /\ -H1 + I - 99 >= 0 /\ W + I - 102 >= 0 /\ V + I - 117 >= 0 /\ -V + I - 83 >= 0 /\ S + I - 150 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ K1 + F - 51 >= 0 /\ -K1 + F - 49 >= 0 /\ H1 + F - 51 >= 0 /\ -H1 + F - 49 >= 0 /\ W + F - 52 >= 0 /\ V + F - 67 >= 0 /\ -V + F - 33 >= 0 /\ S + F - 100 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ K1 + E - 151 >= 0 /\ -K1 + E - 149 >= 0 /\ H1 + E - 151 >= 0 /\ -H1 + E - 149 >= 0 /\ W + E - 152 >= 0 /\ V + E - 167 >= 0 /\ -V + E - 133 >= 0 /\ S + E - 200 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ J1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -J1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ J1 - O1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -J1 + O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ K1 - N1 + 99 >= 0 /\ -K1 - N1 + 101 >= 0 /\ H1 - N1 + 99 >= 0 /\ -H1 - N1 + 101 >= 0 /\ W - N1 + 98 >= 0 /\ V - N1 + 83 >= 0 /\ -V - N1 + 117 >= 0 /\ S - N1 + 50 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ K1 + N1 - 101 >= 0 /\ -K1 + N1 - 99 >= 0 /\ H1 + N1 - 101 >= 0 /\ -H1 + N1 - 99 >= 0 /\ W + N1 - 102 >= 0 /\ V + N1 - 117 >= 0 /\ -V + N1 - 83 >= 0 /\ S + N1 - 150 >= 0 /\ -Q + N1 - 101 >= 0 /\ G1 - M1 >= 0 /\ E1 - M1 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -G1 + M1 >= 0 /\ -E1 + M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ -K1 + 1 >= 0 /\ H1 - K1 >= 0 /\ -H1 - K1 + 2 >= 0 /\ W - K1 - 1 >= 0 /\ V - K1 - 16 >= 0 /\ -V - K1 + 18 >= 0 /\ S - K1 - 49 >= 0 /\ -Q - K1 >= 0 /\ K1 - 1 >= 0 /\ H1 + K1 - 2 >= 0 /\ -H1 + K1 >= 0 /\ W + K1 - 3 >= 0 /\ V + K1 - 18 >= 0 /\ -V + K1 + 16 >= 0 /\ S + K1 - 51 >= 0 /\ -Q + K1 - 2 >= 0 /\ C - J1 >= 0 /\ A - J1 >= 0 /\ -C + J1 >= 0 /\ -A + J1 >= 0 /\ -H1 + 1 >= 0 /\ W - H1 - 1 >= 0 /\ V - H1 - 16 >= 0 /\ -V - H1 + 18 >= 0 /\ S - H1 - 49 >= 0 /\ -Q - H1 >= 0 /\ H1 - 1 >= 0 /\ W + H1 - 3 >= 0 /\ V + H1 - 18 >= 0 /\ -V + H1 + 16 >= 0 /\ S + H1 - 51 >= 0 /\ -Q + H1 - 2 >= 0 /\ E1 - G1 >= 0 /\ B - G1 >= 0 /\ R - G1 >= 0 /\ -E1 + G1 >= 0 /\ -B + G1 >= 0 /\ -R + G1 >= 0 /\ B - E1 >= 0 /\ R - E1 >= 0 /\ -B + E1 >= 0 /\ -R + E1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ W - 2 >= 0 /\ V + W - 19 >= 0 /\ -V + W + 15 >= 0 /\ S + W - 52 >= 0 /\ -Q + W - 3 >= 0 /\ -V + 17 >= 0 /\ S - V - 33 >= 0 /\ -Q - V + 16 >= 0 /\ V - 17 >= 0 /\ S + V - 67 >= 0 /\ -Q + V - 18 >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S - 50 >= 0 /\ -Q + S - 51 >= 0 /\ -Q - 1 >= 0 /\ V >= W ]
  f540(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f543(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, 0, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ K1 + I - 101 >= 0 /\ -K1 + I - 99 >= 0 /\ H1 + I - 101 >= 0 /\ -H1 + I - 99 >= 0 /\ -C1 + I - 92 >= 0 /\ B1 + I - 113 >= 0 /\ A1 + I - 100 >= 0 /\ X + I - 101 >= 0 /\ W + I - 118 >= 0 /\ V + I - 117 >= 0 /\ -V + I - 83 >= 0 /\ S + I - 150 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ K1 + F - 51 >= 0 /\ -K1 + F - 49 >= 0 /\ H1 + F - 51 >= 0 /\ -H1 + F - 49 >= 0 /\ -C1 + F - 42 >= 0 /\ B1 + F - 63 >= 0 /\ A1 + F - 50 >= 0 /\ X + F - 51 >= 0 /\ W + F - 68 >= 0 /\ V + F - 67 >= 0 /\ -V + F - 33 >= 0 /\ S + F - 100 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ K1 + E - 151 >= 0 /\ -K1 + E - 149 >= 0 /\ H1 + E - 151 >= 0 /\ -H1 + E - 149 >= 0 /\ -C1 + E - 142 >= 0 /\ B1 + E - 163 >= 0 /\ A1 + E - 150 >= 0 /\ X + E - 151 >= 0 /\ W + E - 168 >= 0 /\ V + E - 167 >= 0 /\ -V + E - 133 >= 0 /\ S + E - 200 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ J1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -J1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ J1 - O1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -J1 + O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ K1 - N1 + 99 >= 0 /\ -K1 - N1 + 101 >= 0 /\ H1 - N1 + 99 >= 0 /\ -H1 - N1 + 101 >= 0 /\ -C1 - N1 + 108 >= 0 /\ B1 - N1 + 87 >= 0 /\ A1 - N1 + 100 >= 0 /\ X - N1 + 99 >= 0 /\ W - N1 + 82 >= 0 /\ V - N1 + 83 >= 0 /\ -V - N1 + 117 >= 0 /\ S - N1 + 50 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ K1 + N1 - 101 >= 0 /\ -K1 + N1 - 99 >= 0 /\ H1 + N1 - 101 >= 0 /\ -H1 + N1 - 99 >= 0 /\ -C1 + N1 - 92 >= 0 /\ B1 + N1 - 113 >= 0 /\ A1 + N1 - 100 >= 0 /\ X + N1 - 101 >= 0 /\ W + N1 - 118 >= 0 /\ V + N1 - 117 >= 0 /\ -V + N1 - 83 >= 0 /\ S + N1 - 150 >= 0 /\ -Q + N1 - 101 >= 0 /\ G1 - M1 >= 0 /\ F1 - M1 >= 0 /\ E1 - M1 >= 0 /\ D1 - M1 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -G1 + M1 >= 0 /\ -F1 + M1 >= 0 /\ -E1 + M1 >= 0 /\ -D1 + M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ -K1 + 1 >= 0 /\ H1 - K1 >= 0 /\ -H1 - K1 + 2 >= 0 /\ -C1 - K1 + 9 >= 0 /\ B1 - K1 - 12 >= 0 /\ A1 - K1 + 1 >= 0 /\ X - K1 >= 0 /\ W - K1 - 17 >= 0 /\ V - K1 - 16 >= 0 /\ -V - K1 + 18 >= 0 /\ S - K1 - 49 >= 0 /\ -Q - K1 >= 0 /\ K1 - 1 >= 0 /\ H1 + K1 - 2 >= 0 /\ -H1 + K1 >= 0 /\ -C1 + K1 + 7 >= 0 /\ B1 + K1 - 14 >= 0 /\ A1 + K1 - 1 >= 0 /\ X + K1 - 2 >= 0 /\ W + K1 - 19 >= 0 /\ V + K1 - 18 >= 0 /\ -V + K1 + 16 >= 0 /\ S + K1 - 51 >= 0 /\ -Q + K1 - 2 >= 0 /\ C - J1 >= 0 /\ A - J1 >= 0 /\ -C + J1 >= 0 /\ -A + J1 >= 0 /\ -H1 + 1 >= 0 /\ -C1 - H1 + 9 >= 0 /\ B1 - H1 - 12 >= 0 /\ A1 - H1 + 1 >= 0 /\ X - H1 >= 0 /\ W - H1 - 17 >= 0 /\ V - H1 - 16 >= 0 /\ -V - H1 + 18 >= 0 /\ S - H1 - 49 >= 0 /\ -Q - H1 >= 0 /\ H1 - 1 >= 0 /\ -C1 + H1 + 7 >= 0 /\ B1 + H1 - 14 >= 0 /\ A1 + H1 - 1 >= 0 /\ X + H1 - 2 >= 0 /\ W + H1 - 19 >= 0 /\ V + H1 - 18 >= 0 /\ -V + H1 + 16 >= 0 /\ S + H1 - 51 >= 0 /\ -Q + H1 - 2 >= 0 /\ F1 - G1 >= 0 /\ E1 - G1 >= 0 /\ D1 - G1 >= 0 /\ B - G1 >= 0 /\ R - G1 >= 0 /\ -F1 + G1 >= 0 /\ -E1 + G1 >= 0 /\ -D1 + G1 >= 0 /\ -B + G1 >= 0 /\ -R + G1 >= 0 /\ E1 - F1 >= 0 /\ D1 - F1 >= 0 /\ B - F1 >= 0 /\ R - F1 >= 0 /\ -E1 + F1 >= 0 /\ -D1 + F1 >= 0 /\ -B + F1 >= 0 /\ -R + F1 >= 0 /\ D1 - E1 >= 0 /\ B - E1 >= 0 /\ R - E1 >= 0 /\ -D1 + E1 >= 0 /\ -B + E1 >= 0 /\ -R + E1 >= 0 /\ B - D1 >= 0 /\ R - D1 >= 0 /\ -B + D1 >= 0 /\ -R + D1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -C1 + 8 >= 0 /\ B1 - C1 - 5 >= 0 /\ -B1 - C1 + 21 >= 0 /\ A1 - C1 + 8 >= 0 /\ -A1 - C1 + 8 >= 0 /\ X - C1 + 7 >= 0 /\ -X - C1 + 9 >= 0 /\ W - C1 - 10 >= 0 /\ V - C1 - 9 >= 0 /\ -V - C1 + 25 >= 0 /\ S - C1 - 42 >= 0 /\ -Q - C1 + 7 >= 0 /\ X + C1 - 9 >= 0 /\ A1 - B1 + 13 >= 0 /\ X - B1 + 12 >= 0 /\ B1 - 13 >= 0 /\ A1 + B1 - 13 >= 0 /\ -A1 + B1 - 13 >= 0 /\ X + B1 - 14 >= 0 /\ W + B1 - 31 >= 0 /\ V + B1 - 30 >= 0 /\ -V + B1 + 4 >= 0 /\ S + B1 - 63 >= 0 /\ -Q + B1 - 14 >= 0 /\ X - A1 - 1 >= 0 /\ A1 >= 0 /\ X + A1 - 1 >= 0 /\ W + A1 - 18 >= 0 /\ V + A1 - 17 >= 0 /\ -V + A1 + 17 >= 0 /\ S + A1 - 50 >= 0 /\ -Q + A1 - 1 >= 0 /\ X - 1 >= 0 /\ W + X - 19 >= 0 /\ V + X - 18 >= 0 /\ -V + X + 16 >= 0 /\ S + X - 51 >= 0 /\ -Q + X - 2 >= 0 /\ W - 18 >= 0 /\ V + W - 35 >= 0 /\ -V + W - 1 >= 0 /\ S + W - 68 >= 0 /\ -Q + W - 19 >= 0 /\ -V + 17 >= 0 /\ S - V - 33 >= 0 /\ -Q - V + 16 >= 0 /\ V - 17 >= 0 /\ S + V - 67 >= 0 /\ -Q + V - 18 >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S - 50 >= 0 /\ -Q + S - 51 >= 0 /\ -Q - 1 >= 0 /\ 8 >= X ]
  f543(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f546(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, 0, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ K1 + I - 101 >= 0 /\ -K1 + I - 99 >= 0 /\ H1 + I - 101 >= 0 /\ -H1 + I - 99 >= 0 /\ -C1 + I - 92 >= 0 /\ B1 + I - 113 >= 0 /\ A1 + I - 100 >= 0 /\ Y + I - 100 >= 0 /\ X + I - 101 >= 0 /\ W + I - 118 >= 0 /\ V + I - 117 >= 0 /\ -V + I - 83 >= 0 /\ S + I - 150 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ K1 + F - 51 >= 0 /\ -K1 + F - 49 >= 0 /\ H1 + F - 51 >= 0 /\ -H1 + F - 49 >= 0 /\ -C1 + F - 42 >= 0 /\ B1 + F - 63 >= 0 /\ A1 + F - 50 >= 0 /\ Y + F - 50 >= 0 /\ X + F - 51 >= 0 /\ W + F - 68 >= 0 /\ V + F - 67 >= 0 /\ -V + F - 33 >= 0 /\ S + F - 100 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ K1 + E - 151 >= 0 /\ -K1 + E - 149 >= 0 /\ H1 + E - 151 >= 0 /\ -H1 + E - 149 >= 0 /\ -C1 + E - 142 >= 0 /\ B1 + E - 163 >= 0 /\ A1 + E - 150 >= 0 /\ Y + E - 150 >= 0 /\ X + E - 151 >= 0 /\ W + E - 168 >= 0 /\ V + E - 167 >= 0 /\ -V + E - 133 >= 0 /\ S + E - 200 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ J1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -J1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ J1 - O1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -J1 + O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ K1 - N1 + 99 >= 0 /\ -K1 - N1 + 101 >= 0 /\ H1 - N1 + 99 >= 0 /\ -H1 - N1 + 101 >= 0 /\ -C1 - N1 + 108 >= 0 /\ B1 - N1 + 87 >= 0 /\ A1 - N1 + 100 >= 0 /\ Y - N1 + 100 >= 0 /\ X - N1 + 99 >= 0 /\ W - N1 + 82 >= 0 /\ V - N1 + 83 >= 0 /\ -V - N1 + 117 >= 0 /\ S - N1 + 50 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ K1 + N1 - 101 >= 0 /\ -K1 + N1 - 99 >= 0 /\ H1 + N1 - 101 >= 0 /\ -H1 + N1 - 99 >= 0 /\ -C1 + N1 - 92 >= 0 /\ B1 + N1 - 113 >= 0 /\ A1 + N1 - 100 >= 0 /\ Y + N1 - 100 >= 0 /\ X + N1 - 101 >= 0 /\ W + N1 - 118 >= 0 /\ V + N1 - 117 >= 0 /\ -V + N1 - 83 >= 0 /\ S + N1 - 150 >= 0 /\ -Q + N1 - 101 >= 0 /\ G1 - M1 >= 0 /\ F1 - M1 >= 0 /\ E1 - M1 >= 0 /\ D1 - M1 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -G1 + M1 >= 0 /\ -F1 + M1 >= 0 /\ -E1 + M1 >= 0 /\ -D1 + M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ -K1 + 1 >= 0 /\ H1 - K1 >= 0 /\ -H1 - K1 + 2 >= 0 /\ -C1 - K1 + 9 >= 0 /\ B1 - K1 - 12 >= 0 /\ A1 - K1 + 1 >= 0 /\ Y - K1 + 1 >= 0 /\ X - K1 >= 0 /\ W - K1 - 17 >= 0 /\ V - K1 - 16 >= 0 /\ -V - K1 + 18 >= 0 /\ S - K1 - 49 >= 0 /\ -Q - K1 >= 0 /\ K1 - 1 >= 0 /\ H1 + K1 - 2 >= 0 /\ -H1 + K1 >= 0 /\ -C1 + K1 + 7 >= 0 /\ B1 + K1 - 14 >= 0 /\ A1 + K1 - 1 >= 0 /\ Y + K1 - 1 >= 0 /\ X + K1 - 2 >= 0 /\ W + K1 - 19 >= 0 /\ V + K1 - 18 >= 0 /\ -V + K1 + 16 >= 0 /\ S + K1 - 51 >= 0 /\ -Q + K1 - 2 >= 0 /\ C - J1 >= 0 /\ A - J1 >= 0 /\ -C + J1 >= 0 /\ -A + J1 >= 0 /\ -H1 + 1 >= 0 /\ -C1 - H1 + 9 >= 0 /\ B1 - H1 - 12 >= 0 /\ A1 - H1 + 1 >= 0 /\ Y - H1 + 1 >= 0 /\ X - H1 >= 0 /\ W - H1 - 17 >= 0 /\ V - H1 - 16 >= 0 /\ -V - H1 + 18 >= 0 /\ S - H1 - 49 >= 0 /\ -Q - H1 >= 0 /\ H1 - 1 >= 0 /\ -C1 + H1 + 7 >= 0 /\ B1 + H1 - 14 >= 0 /\ A1 + H1 - 1 >= 0 /\ Y + H1 - 1 >= 0 /\ X + H1 - 2 >= 0 /\ W + H1 - 19 >= 0 /\ V + H1 - 18 >= 0 /\ -V + H1 + 16 >= 0 /\ S + H1 - 51 >= 0 /\ -Q + H1 - 2 >= 0 /\ F1 - G1 >= 0 /\ E1 - G1 >= 0 /\ D1 - G1 >= 0 /\ B - G1 >= 0 /\ R - G1 >= 0 /\ -F1 + G1 >= 0 /\ -E1 + G1 >= 0 /\ -D1 + G1 >= 0 /\ -B + G1 >= 0 /\ -R + G1 >= 0 /\ E1 - F1 >= 0 /\ D1 - F1 >= 0 /\ B - F1 >= 0 /\ R - F1 >= 0 /\ -E1 + F1 >= 0 /\ -D1 + F1 >= 0 /\ -B + F1 >= 0 /\ -R + F1 >= 0 /\ D1 - E1 >= 0 /\ B - E1 >= 0 /\ R - E1 >= 0 /\ -D1 + E1 >= 0 /\ -B + E1 >= 0 /\ -R + E1 >= 0 /\ B - D1 >= 0 /\ R - D1 >= 0 /\ -B + D1 >= 0 /\ -R + D1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -C1 + 8 >= 0 /\ B1 - C1 - 5 >= 0 /\ -B1 - C1 + 21 >= 0 /\ A1 - C1 + 8 >= 0 /\ -A1 - C1 + 8 >= 0 /\ Y - C1 + 8 >= 0 /\ X - C1 + 7 >= 0 /\ -X - C1 + 9 >= 0 /\ W - C1 - 10 >= 0 /\ V - C1 - 9 >= 0 /\ -V - C1 + 25 >= 0 /\ S - C1 - 42 >= 0 /\ -Q - C1 + 7 >= 0 /\ X + C1 - 9 >= 0 /\ A1 - B1 + 13 >= 0 /\ X - B1 + 12 >= 0 /\ B1 - 13 >= 0 /\ A1 + B1 - 13 >= 0 /\ -A1 + B1 - 13 >= 0 /\ Y + B1 - 13 >= 0 /\ X + B1 - 14 >= 0 /\ W + B1 - 31 >= 0 /\ V + B1 - 30 >= 0 /\ -V + B1 + 4 >= 0 /\ S + B1 - 63 >= 0 /\ -Q + B1 - 14 >= 0 /\ X - A1 - 1 >= 0 /\ A1 >= 0 /\ Y + A1 >= 0 /\ X + A1 - 1 >= 0 /\ W + A1 - 18 >= 0 /\ V + A1 - 17 >= 0 /\ -V + A1 + 17 >= 0 /\ S + A1 - 50 >= 0 /\ -Q + A1 - 1 >= 0 /\ Y >= 0 /\ X + Y - 1 >= 0 /\ W + Y - 18 >= 0 /\ V + Y - 17 >= 0 /\ -V + Y + 17 >= 0 /\ S + Y - 50 >= 0 /\ -Q + Y - 1 >= 0 /\ X - 1 >= 0 /\ W + X - 19 >= 0 /\ V + X - 18 >= 0 /\ -V + X + 16 >= 0 /\ S + X - 51 >= 0 /\ -Q + X - 2 >= 0 /\ W - 18 >= 0 /\ V + W - 35 >= 0 /\ -V + W - 1 >= 0 /\ S + W - 68 >= 0 /\ -Q + W - 19 >= 0 /\ -V + 17 >= 0 /\ S - V - 33 >= 0 /\ -Q - V + 16 >= 0 /\ V - 17 >= 0 /\ S + V - 67 >= 0 /\ -Q + V - 18 >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S - 50 >= 0 /\ -Q + S - 51 >= 0 /\ -Q - 1 >= 0 /\ 7 >= Y ]
  f546(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f546(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 + 1, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ K1 + I - 101 >= 0 /\ -K1 + I - 99 >= 0 /\ H1 + I - 101 >= 0 /\ -H1 + I - 99 >= 0 /\ -C1 + I - 92 >= 0 /\ B1 + I - 113 >= 0 /\ A1 + I - 100 >= 0 /\ Z + I - 100 >= 0 /\ Y + I - 100 >= 0 /\ X + I - 101 >= 0 /\ W + I - 118 >= 0 /\ V + I - 117 >= 0 /\ -V + I - 83 >= 0 /\ S + I - 150 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ K1 + F - 51 >= 0 /\ -K1 + F - 49 >= 0 /\ H1 + F - 51 >= 0 /\ -H1 + F - 49 >= 0 /\ -C1 + F - 42 >= 0 /\ B1 + F - 63 >= 0 /\ A1 + F - 50 >= 0 /\ Z + F - 50 >= 0 /\ Y + F - 50 >= 0 /\ X + F - 51 >= 0 /\ W + F - 68 >= 0 /\ V + F - 67 >= 0 /\ -V + F - 33 >= 0 /\ S + F - 100 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ K1 + E - 151 >= 0 /\ -K1 + E - 149 >= 0 /\ H1 + E - 151 >= 0 /\ -H1 + E - 149 >= 0 /\ -C1 + E - 142 >= 0 /\ B1 + E - 163 >= 0 /\ A1 + E - 150 >= 0 /\ Z + E - 150 >= 0 /\ Y + E - 150 >= 0 /\ X + E - 151 >= 0 /\ W + E - 168 >= 0 /\ V + E - 167 >= 0 /\ -V + E - 133 >= 0 /\ S + E - 200 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ J1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -J1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ J1 - O1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -J1 + O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ K1 - N1 + 99 >= 0 /\ -K1 - N1 + 101 >= 0 /\ H1 - N1 + 99 >= 0 /\ -H1 - N1 + 101 >= 0 /\ -C1 - N1 + 108 >= 0 /\ B1 - N1 + 87 >= 0 /\ A1 - N1 + 100 >= 0 /\ Z - N1 + 100 >= 0 /\ Y - N1 + 100 >= 0 /\ X - N1 + 99 >= 0 /\ W - N1 + 82 >= 0 /\ V - N1 + 83 >= 0 /\ -V - N1 + 117 >= 0 /\ S - N1 + 50 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ K1 + N1 - 101 >= 0 /\ -K1 + N1 - 99 >= 0 /\ H1 + N1 - 101 >= 0 /\ -H1 + N1 - 99 >= 0 /\ -C1 + N1 - 92 >= 0 /\ B1 + N1 - 113 >= 0 /\ A1 + N1 - 100 >= 0 /\ Z + N1 - 100 >= 0 /\ Y + N1 - 100 >= 0 /\ X + N1 - 101 >= 0 /\ W + N1 - 118 >= 0 /\ V + N1 - 117 >= 0 /\ -V + N1 - 83 >= 0 /\ S + N1 - 150 >= 0 /\ -Q + N1 - 101 >= 0 /\ G1 - M1 >= 0 /\ F1 - M1 >= 0 /\ E1 - M1 >= 0 /\ D1 - M1 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -G1 + M1 >= 0 /\ -F1 + M1 >= 0 /\ -E1 + M1 >= 0 /\ -D1 + M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ -K1 + 1 >= 0 /\ H1 - K1 >= 0 /\ -H1 - K1 + 2 >= 0 /\ -C1 - K1 + 9 >= 0 /\ B1 - K1 - 12 >= 0 /\ A1 - K1 + 1 >= 0 /\ Z - K1 + 1 >= 0 /\ Y - K1 + 1 >= 0 /\ X - K1 >= 0 /\ W - K1 - 17 >= 0 /\ V - K1 - 16 >= 0 /\ -V - K1 + 18 >= 0 /\ S - K1 - 49 >= 0 /\ -Q - K1 >= 0 /\ K1 - 1 >= 0 /\ H1 + K1 - 2 >= 0 /\ -H1 + K1 >= 0 /\ -C1 + K1 + 7 >= 0 /\ B1 + K1 - 14 >= 0 /\ A1 + K1 - 1 >= 0 /\ Z + K1 - 1 >= 0 /\ Y + K1 - 1 >= 0 /\ X + K1 - 2 >= 0 /\ W + K1 - 19 >= 0 /\ V + K1 - 18 >= 0 /\ -V + K1 + 16 >= 0 /\ S + K1 - 51 >= 0 /\ -Q + K1 - 2 >= 0 /\ C - J1 >= 0 /\ A - J1 >= 0 /\ -C + J1 >= 0 /\ -A + J1 >= 0 /\ -H1 + 1 >= 0 /\ -C1 - H1 + 9 >= 0 /\ B1 - H1 - 12 >= 0 /\ A1 - H1 + 1 >= 0 /\ Z - H1 + 1 >= 0 /\ Y - H1 + 1 >= 0 /\ X - H1 >= 0 /\ W - H1 - 17 >= 0 /\ V - H1 - 16 >= 0 /\ -V - H1 + 18 >= 0 /\ S - H1 - 49 >= 0 /\ -Q - H1 >= 0 /\ H1 - 1 >= 0 /\ -C1 + H1 + 7 >= 0 /\ B1 + H1 - 14 >= 0 /\ A1 + H1 - 1 >= 0 /\ Z + H1 - 1 >= 0 /\ Y + H1 - 1 >= 0 /\ X + H1 - 2 >= 0 /\ W + H1 - 19 >= 0 /\ V + H1 - 18 >= 0 /\ -V + H1 + 16 >= 0 /\ S + H1 - 51 >= 0 /\ -Q + H1 - 2 >= 0 /\ F1 - G1 >= 0 /\ E1 - G1 >= 0 /\ D1 - G1 >= 0 /\ B - G1 >= 0 /\ R - G1 >= 0 /\ -F1 + G1 >= 0 /\ -E1 + G1 >= 0 /\ -D1 + G1 >= 0 /\ -B + G1 >= 0 /\ -R + G1 >= 0 /\ E1 - F1 >= 0 /\ D1 - F1 >= 0 /\ B - F1 >= 0 /\ R - F1 >= 0 /\ -E1 + F1 >= 0 /\ -D1 + F1 >= 0 /\ -B + F1 >= 0 /\ -R + F1 >= 0 /\ D1 - E1 >= 0 /\ B - E1 >= 0 /\ R - E1 >= 0 /\ -D1 + E1 >= 0 /\ -B + E1 >= 0 /\ -R + E1 >= 0 /\ B - D1 >= 0 /\ R - D1 >= 0 /\ -B + D1 >= 0 /\ -R + D1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -C1 + 8 >= 0 /\ B1 - C1 - 5 >= 0 /\ -B1 - C1 + 21 >= 0 /\ A1 - C1 + 8 >= 0 /\ -A1 - C1 + 8 >= 0 /\ Z - C1 + 8 >= 0 /\ Y - C1 + 8 >= 0 /\ X - C1 + 7 >= 0 /\ -X - C1 + 9 >= 0 /\ W - C1 - 10 >= 0 /\ V - C1 - 9 >= 0 /\ -V - C1 + 25 >= 0 /\ S - C1 - 42 >= 0 /\ -Q - C1 + 7 >= 0 /\ X + C1 - 9 >= 0 /\ A1 - B1 + 13 >= 0 /\ X - B1 + 12 >= 0 /\ B1 - 13 >= 0 /\ A1 + B1 - 13 >= 0 /\ -A1 + B1 - 13 >= 0 /\ Z + B1 - 13 >= 0 /\ Y + B1 - 13 >= 0 /\ X + B1 - 14 >= 0 /\ W + B1 - 31 >= 0 /\ V + B1 - 30 >= 0 /\ -V + B1 + 4 >= 0 /\ S + B1 - 63 >= 0 /\ -Q + B1 - 14 >= 0 /\ X - A1 - 1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ Y + A1 >= 0 /\ X + A1 - 1 >= 0 /\ W + A1 - 18 >= 0 /\ V + A1 - 17 >= 0 /\ -V + A1 + 17 >= 0 /\ S + A1 - 50 >= 0 /\ -Q + A1 - 1 >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ X + Z - 1 >= 0 /\ W + Z - 18 >= 0 /\ V + Z - 17 >= 0 /\ -V + Z + 17 >= 0 /\ S + Z - 50 >= 0 /\ -Q + Z - 1 >= 0 /\ Y >= 0 /\ X + Y - 1 >= 0 /\ W + Y - 18 >= 0 /\ V + Y - 17 >= 0 /\ -V + Y + 17 >= 0 /\ S + Y - 50 >= 0 /\ -Q + Y - 1 >= 0 /\ X - 1 >= 0 /\ W + X - 19 >= 0 /\ V + X - 18 >= 0 /\ -V + X + 16 >= 0 /\ S + X - 51 >= 0 /\ -Q + X - 2 >= 0 /\ W - 18 >= 0 /\ V + W - 35 >= 0 /\ -V + W - 1 >= 0 /\ S + W - 68 >= 0 /\ -Q + W - 19 >= 0 /\ -V + 17 >= 0 /\ S - V - 33 >= 0 /\ -Q - V + 16 >= 0 /\ V - 17 >= 0 /\ S + V - 67 >= 0 /\ -Q + V - 18 >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S - 50 >= 0 /\ -Q + S - 51 >= 0 /\ -Q - 1 >= 0 /\ 3 >= Z ]
  f546(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f543(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 + 1, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ K1 + I - 101 >= 0 /\ -K1 + I - 99 >= 0 /\ H1 + I - 101 >= 0 /\ -H1 + I - 99 >= 0 /\ -C1 + I - 92 >= 0 /\ B1 + I - 113 >= 0 /\ A1 + I - 100 >= 0 /\ Z + I - 100 >= 0 /\ Y + I - 100 >= 0 /\ X + I - 101 >= 0 /\ W + I - 118 >= 0 /\ V + I - 117 >= 0 /\ -V + I - 83 >= 0 /\ S + I - 150 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ K1 + F - 51 >= 0 /\ -K1 + F - 49 >= 0 /\ H1 + F - 51 >= 0 /\ -H1 + F - 49 >= 0 /\ -C1 + F - 42 >= 0 /\ B1 + F - 63 >= 0 /\ A1 + F - 50 >= 0 /\ Z + F - 50 >= 0 /\ Y + F - 50 >= 0 /\ X + F - 51 >= 0 /\ W + F - 68 >= 0 /\ V + F - 67 >= 0 /\ -V + F - 33 >= 0 /\ S + F - 100 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ K1 + E - 151 >= 0 /\ -K1 + E - 149 >= 0 /\ H1 + E - 151 >= 0 /\ -H1 + E - 149 >= 0 /\ -C1 + E - 142 >= 0 /\ B1 + E - 163 >= 0 /\ A1 + E - 150 >= 0 /\ Z + E - 150 >= 0 /\ Y + E - 150 >= 0 /\ X + E - 151 >= 0 /\ W + E - 168 >= 0 /\ V + E - 167 >= 0 /\ -V + E - 133 >= 0 /\ S + E - 200 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ J1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -J1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ J1 - O1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -J1 + O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ K1 - N1 + 99 >= 0 /\ -K1 - N1 + 101 >= 0 /\ H1 - N1 + 99 >= 0 /\ -H1 - N1 + 101 >= 0 /\ -C1 - N1 + 108 >= 0 /\ B1 - N1 + 87 >= 0 /\ A1 - N1 + 100 >= 0 /\ Z - N1 + 100 >= 0 /\ Y - N1 + 100 >= 0 /\ X - N1 + 99 >= 0 /\ W - N1 + 82 >= 0 /\ V - N1 + 83 >= 0 /\ -V - N1 + 117 >= 0 /\ S - N1 + 50 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ K1 + N1 - 101 >= 0 /\ -K1 + N1 - 99 >= 0 /\ H1 + N1 - 101 >= 0 /\ -H1 + N1 - 99 >= 0 /\ -C1 + N1 - 92 >= 0 /\ B1 + N1 - 113 >= 0 /\ A1 + N1 - 100 >= 0 /\ Z + N1 - 100 >= 0 /\ Y + N1 - 100 >= 0 /\ X + N1 - 101 >= 0 /\ W + N1 - 118 >= 0 /\ V + N1 - 117 >= 0 /\ -V + N1 - 83 >= 0 /\ S + N1 - 150 >= 0 /\ -Q + N1 - 101 >= 0 /\ G1 - M1 >= 0 /\ F1 - M1 >= 0 /\ E1 - M1 >= 0 /\ D1 - M1 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -G1 + M1 >= 0 /\ -F1 + M1 >= 0 /\ -E1 + M1 >= 0 /\ -D1 + M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ -K1 + 1 >= 0 /\ H1 - K1 >= 0 /\ -H1 - K1 + 2 >= 0 /\ -C1 - K1 + 9 >= 0 /\ B1 - K1 - 12 >= 0 /\ A1 - K1 + 1 >= 0 /\ Z - K1 + 1 >= 0 /\ Y - K1 + 1 >= 0 /\ X - K1 >= 0 /\ W - K1 - 17 >= 0 /\ V - K1 - 16 >= 0 /\ -V - K1 + 18 >= 0 /\ S - K1 - 49 >= 0 /\ -Q - K1 >= 0 /\ K1 - 1 >= 0 /\ H1 + K1 - 2 >= 0 /\ -H1 + K1 >= 0 /\ -C1 + K1 + 7 >= 0 /\ B1 + K1 - 14 >= 0 /\ A1 + K1 - 1 >= 0 /\ Z + K1 - 1 >= 0 /\ Y + K1 - 1 >= 0 /\ X + K1 - 2 >= 0 /\ W + K1 - 19 >= 0 /\ V + K1 - 18 >= 0 /\ -V + K1 + 16 >= 0 /\ S + K1 - 51 >= 0 /\ -Q + K1 - 2 >= 0 /\ C - J1 >= 0 /\ A - J1 >= 0 /\ -C + J1 >= 0 /\ -A + J1 >= 0 /\ -H1 + 1 >= 0 /\ -C1 - H1 + 9 >= 0 /\ B1 - H1 - 12 >= 0 /\ A1 - H1 + 1 >= 0 /\ Z - H1 + 1 >= 0 /\ Y - H1 + 1 >= 0 /\ X - H1 >= 0 /\ W - H1 - 17 >= 0 /\ V - H1 - 16 >= 0 /\ -V - H1 + 18 >= 0 /\ S - H1 - 49 >= 0 /\ -Q - H1 >= 0 /\ H1 - 1 >= 0 /\ -C1 + H1 + 7 >= 0 /\ B1 + H1 - 14 >= 0 /\ A1 + H1 - 1 >= 0 /\ Z + H1 - 1 >= 0 /\ Y + H1 - 1 >= 0 /\ X + H1 - 2 >= 0 /\ W + H1 - 19 >= 0 /\ V + H1 - 18 >= 0 /\ -V + H1 + 16 >= 0 /\ S + H1 - 51 >= 0 /\ -Q + H1 - 2 >= 0 /\ F1 - G1 >= 0 /\ E1 - G1 >= 0 /\ D1 - G1 >= 0 /\ B - G1 >= 0 /\ R - G1 >= 0 /\ -F1 + G1 >= 0 /\ -E1 + G1 >= 0 /\ -D1 + G1 >= 0 /\ -B + G1 >= 0 /\ -R + G1 >= 0 /\ E1 - F1 >= 0 /\ D1 - F1 >= 0 /\ B - F1 >= 0 /\ R - F1 >= 0 /\ -E1 + F1 >= 0 /\ -D1 + F1 >= 0 /\ -B + F1 >= 0 /\ -R + F1 >= 0 /\ D1 - E1 >= 0 /\ B - E1 >= 0 /\ R - E1 >= 0 /\ -D1 + E1 >= 0 /\ -B + E1 >= 0 /\ -R + E1 >= 0 /\ B - D1 >= 0 /\ R - D1 >= 0 /\ -B + D1 >= 0 /\ -R + D1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -C1 + 8 >= 0 /\ B1 - C1 - 5 >= 0 /\ -B1 - C1 + 21 >= 0 /\ A1 - C1 + 8 >= 0 /\ -A1 - C1 + 8 >= 0 /\ Z - C1 + 8 >= 0 /\ Y - C1 + 8 >= 0 /\ X - C1 + 7 >= 0 /\ -X - C1 + 9 >= 0 /\ W - C1 - 10 >= 0 /\ V - C1 - 9 >= 0 /\ -V - C1 + 25 >= 0 /\ S - C1 - 42 >= 0 /\ -Q - C1 + 7 >= 0 /\ X + C1 - 9 >= 0 /\ A1 - B1 + 13 >= 0 /\ X - B1 + 12 >= 0 /\ B1 - 13 >= 0 /\ A1 + B1 - 13 >= 0 /\ -A1 + B1 - 13 >= 0 /\ Z + B1 - 13 >= 0 /\ Y + B1 - 13 >= 0 /\ X + B1 - 14 >= 0 /\ W + B1 - 31 >= 0 /\ V + B1 - 30 >= 0 /\ -V + B1 + 4 >= 0 /\ S + B1 - 63 >= 0 /\ -Q + B1 - 14 >= 0 /\ X - A1 - 1 >= 0 /\ A1 >= 0 /\ Z + A1 >= 0 /\ Y + A1 >= 0 /\ X + A1 - 1 >= 0 /\ W + A1 - 18 >= 0 /\ V + A1 - 17 >= 0 /\ -V + A1 + 17 >= 0 /\ S + A1 - 50 >= 0 /\ -Q + A1 - 1 >= 0 /\ Z >= 0 /\ Y + Z >= 0 /\ X + Z - 1 >= 0 /\ W + Z - 18 >= 0 /\ V + Z - 17 >= 0 /\ -V + Z + 17 >= 0 /\ S + Z - 50 >= 0 /\ -Q + Z - 1 >= 0 /\ Y >= 0 /\ X + Y - 1 >= 0 /\ W + Y - 18 >= 0 /\ V + Y - 17 >= 0 /\ -V + Y + 17 >= 0 /\ S + Y - 50 >= 0 /\ -Q + Y - 1 >= 0 /\ X - 1 >= 0 /\ W + X - 19 >= 0 /\ V + X - 18 >= 0 /\ -V + X + 16 >= 0 /\ S + X - 51 >= 0 /\ -Q + X - 2 >= 0 /\ W - 18 >= 0 /\ V + W - 35 >= 0 /\ -V + W - 1 >= 0 /\ S + W - 68 >= 0 /\ -Q + W - 19 >= 0 /\ -V + 17 >= 0 /\ S - V - 33 >= 0 /\ -Q - V + 16 >= 0 /\ V - 17 >= 0 /\ S + V - 67 >= 0 /\ -Q + V - 18 >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S - 50 >= 0 /\ -Q + S - 51 >= 0 /\ -Q - 1 >= 0 /\ Z >= 4 ]
  f543(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f540(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X + 7, Y, Z, A1 + 3, B1 + 3, C1 - 7, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ K1 + I - 101 >= 0 /\ -K1 + I - 99 >= 0 /\ H1 + I - 101 >= 0 /\ -H1 + I - 99 >= 0 /\ -C1 + I - 92 >= 0 /\ B1 + I - 113 >= 0 /\ A1 + I - 100 >= 0 /\ Y + I - 100 >= 0 /\ X + I - 101 >= 0 /\ W + I - 118 >= 0 /\ V + I - 117 >= 0 /\ -V + I - 83 >= 0 /\ S + I - 150 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ K1 + F - 51 >= 0 /\ -K1 + F - 49 >= 0 /\ H1 + F - 51 >= 0 /\ -H1 + F - 49 >= 0 /\ -C1 + F - 42 >= 0 /\ B1 + F - 63 >= 0 /\ A1 + F - 50 >= 0 /\ Y + F - 50 >= 0 /\ X + F - 51 >= 0 /\ W + F - 68 >= 0 /\ V + F - 67 >= 0 /\ -V + F - 33 >= 0 /\ S + F - 100 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ K1 + E - 151 >= 0 /\ -K1 + E - 149 >= 0 /\ H1 + E - 151 >= 0 /\ -H1 + E - 149 >= 0 /\ -C1 + E - 142 >= 0 /\ B1 + E - 163 >= 0 /\ A1 + E - 150 >= 0 /\ Y + E - 150 >= 0 /\ X + E - 151 >= 0 /\ W + E - 168 >= 0 /\ V + E - 167 >= 0 /\ -V + E - 133 >= 0 /\ S + E - 200 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ J1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -J1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ J1 - O1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -J1 + O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ K1 - N1 + 99 >= 0 /\ -K1 - N1 + 101 >= 0 /\ H1 - N1 + 99 >= 0 /\ -H1 - N1 + 101 >= 0 /\ -C1 - N1 + 108 >= 0 /\ B1 - N1 + 87 >= 0 /\ A1 - N1 + 100 >= 0 /\ Y - N1 + 100 >= 0 /\ X - N1 + 99 >= 0 /\ W - N1 + 82 >= 0 /\ V - N1 + 83 >= 0 /\ -V - N1 + 117 >= 0 /\ S - N1 + 50 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ K1 + N1 - 101 >= 0 /\ -K1 + N1 - 99 >= 0 /\ H1 + N1 - 101 >= 0 /\ -H1 + N1 - 99 >= 0 /\ -C1 + N1 - 92 >= 0 /\ B1 + N1 - 113 >= 0 /\ A1 + N1 - 100 >= 0 /\ Y + N1 - 100 >= 0 /\ X + N1 - 101 >= 0 /\ W + N1 - 118 >= 0 /\ V + N1 - 117 >= 0 /\ -V + N1 - 83 >= 0 /\ S + N1 - 150 >= 0 /\ -Q + N1 - 101 >= 0 /\ G1 - M1 >= 0 /\ F1 - M1 >= 0 /\ E1 - M1 >= 0 /\ D1 - M1 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -G1 + M1 >= 0 /\ -F1 + M1 >= 0 /\ -E1 + M1 >= 0 /\ -D1 + M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ -K1 + 1 >= 0 /\ H1 - K1 >= 0 /\ -H1 - K1 + 2 >= 0 /\ -C1 - K1 + 9 >= 0 /\ B1 - K1 - 12 >= 0 /\ A1 - K1 + 1 >= 0 /\ Y - K1 + 1 >= 0 /\ X - K1 >= 0 /\ W - K1 - 17 >= 0 /\ V - K1 - 16 >= 0 /\ -V - K1 + 18 >= 0 /\ S - K1 - 49 >= 0 /\ -Q - K1 >= 0 /\ K1 - 1 >= 0 /\ H1 + K1 - 2 >= 0 /\ -H1 + K1 >= 0 /\ -C1 + K1 + 7 >= 0 /\ B1 + K1 - 14 >= 0 /\ A1 + K1 - 1 >= 0 /\ Y + K1 - 1 >= 0 /\ X + K1 - 2 >= 0 /\ W + K1 - 19 >= 0 /\ V + K1 - 18 >= 0 /\ -V + K1 + 16 >= 0 /\ S + K1 - 51 >= 0 /\ -Q + K1 - 2 >= 0 /\ C - J1 >= 0 /\ A - J1 >= 0 /\ -C + J1 >= 0 /\ -A + J1 >= 0 /\ -H1 + 1 >= 0 /\ -C1 - H1 + 9 >= 0 /\ B1 - H1 - 12 >= 0 /\ A1 - H1 + 1 >= 0 /\ Y - H1 + 1 >= 0 /\ X - H1 >= 0 /\ W - H1 - 17 >= 0 /\ V - H1 - 16 >= 0 /\ -V - H1 + 18 >= 0 /\ S - H1 - 49 >= 0 /\ -Q - H1 >= 0 /\ H1 - 1 >= 0 /\ -C1 + H1 + 7 >= 0 /\ B1 + H1 - 14 >= 0 /\ A1 + H1 - 1 >= 0 /\ Y + H1 - 1 >= 0 /\ X + H1 - 2 >= 0 /\ W + H1 - 19 >= 0 /\ V + H1 - 18 >= 0 /\ -V + H1 + 16 >= 0 /\ S + H1 - 51 >= 0 /\ -Q + H1 - 2 >= 0 /\ F1 - G1 >= 0 /\ E1 - G1 >= 0 /\ D1 - G1 >= 0 /\ B - G1 >= 0 /\ R - G1 >= 0 /\ -F1 + G1 >= 0 /\ -E1 + G1 >= 0 /\ -D1 + G1 >= 0 /\ -B + G1 >= 0 /\ -R + G1 >= 0 /\ E1 - F1 >= 0 /\ D1 - F1 >= 0 /\ B - F1 >= 0 /\ R - F1 >= 0 /\ -E1 + F1 >= 0 /\ -D1 + F1 >= 0 /\ -B + F1 >= 0 /\ -R + F1 >= 0 /\ D1 - E1 >= 0 /\ B - E1 >= 0 /\ R - E1 >= 0 /\ -D1 + E1 >= 0 /\ -B + E1 >= 0 /\ -R + E1 >= 0 /\ B - D1 >= 0 /\ R - D1 >= 0 /\ -B + D1 >= 0 /\ -R + D1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -C1 + 8 >= 0 /\ B1 - C1 - 5 >= 0 /\ -B1 - C1 + 21 >= 0 /\ A1 - C1 + 8 >= 0 /\ -A1 - C1 + 8 >= 0 /\ Y - C1 + 8 >= 0 /\ X - C1 + 7 >= 0 /\ -X - C1 + 9 >= 0 /\ W - C1 - 10 >= 0 /\ V - C1 - 9 >= 0 /\ -V - C1 + 25 >= 0 /\ S - C1 - 42 >= 0 /\ -Q - C1 + 7 >= 0 /\ X + C1 - 9 >= 0 /\ A1 - B1 + 13 >= 0 /\ X - B1 + 12 >= 0 /\ B1 - 13 >= 0 /\ A1 + B1 - 13 >= 0 /\ -A1 + B1 - 13 >= 0 /\ Y + B1 - 13 >= 0 /\ X + B1 - 14 >= 0 /\ W + B1 - 31 >= 0 /\ V + B1 - 30 >= 0 /\ -V + B1 + 4 >= 0 /\ S + B1 - 63 >= 0 /\ -Q + B1 - 14 >= 0 /\ X - A1 - 1 >= 0 /\ A1 >= 0 /\ Y + A1 >= 0 /\ X + A1 - 1 >= 0 /\ W + A1 - 18 >= 0 /\ V + A1 - 17 >= 0 /\ -V + A1 + 17 >= 0 /\ S + A1 - 50 >= 0 /\ -Q + A1 - 1 >= 0 /\ Y >= 0 /\ X + Y - 1 >= 0 /\ W + Y - 18 >= 0 /\ V + Y - 17 >= 0 /\ -V + Y + 17 >= 0 /\ S + Y - 50 >= 0 /\ -Q + Y - 1 >= 0 /\ X - 1 >= 0 /\ W + X - 19 >= 0 /\ V + X - 18 >= 0 /\ -V + X + 16 >= 0 /\ S + X - 51 >= 0 /\ -Q + X - 2 >= 0 /\ W - 18 >= 0 /\ V + W - 35 >= 0 /\ -V + W - 1 >= 0 /\ S + W - 68 >= 0 /\ -Q + W - 19 >= 0 /\ -V + 17 >= 0 /\ S - V - 33 >= 0 /\ -Q - V + 16 >= 0 /\ V - 17 >= 0 /\ S + V - 67 >= 0 /\ -Q + V - 18 >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S - 50 >= 0 /\ -Q + S - 51 >= 0 /\ -Q - 1 >= 0 /\ Y >= 8 ]
  f540(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f584(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ K1 + I - 101 >= 0 /\ -K1 + I - 99 >= 0 /\ H1 + I - 101 >= 0 /\ -H1 + I - 99 >= 0 /\ -C1 + I - 92 >= 0 /\ B1 + I - 113 >= 0 /\ A1 + I - 100 >= 0 /\ X + I - 101 >= 0 /\ W + I - 118 >= 0 /\ V + I - 117 >= 0 /\ -V + I - 83 >= 0 /\ S + I - 150 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ K1 + F - 51 >= 0 /\ -K1 + F - 49 >= 0 /\ H1 + F - 51 >= 0 /\ -H1 + F - 49 >= 0 /\ -C1 + F - 42 >= 0 /\ B1 + F - 63 >= 0 /\ A1 + F - 50 >= 0 /\ X + F - 51 >= 0 /\ W + F - 68 >= 0 /\ V + F - 67 >= 0 /\ -V + F - 33 >= 0 /\ S + F - 100 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ K1 + E - 151 >= 0 /\ -K1 + E - 149 >= 0 /\ H1 + E - 151 >= 0 /\ -H1 + E - 149 >= 0 /\ -C1 + E - 142 >= 0 /\ B1 + E - 163 >= 0 /\ A1 + E - 150 >= 0 /\ X + E - 151 >= 0 /\ W + E - 168 >= 0 /\ V + E - 167 >= 0 /\ -V + E - 133 >= 0 /\ S + E - 200 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ J1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -J1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ J1 - O1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -J1 + O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ K1 - N1 + 99 >= 0 /\ -K1 - N1 + 101 >= 0 /\ H1 - N1 + 99 >= 0 /\ -H1 - N1 + 101 >= 0 /\ -C1 - N1 + 108 >= 0 /\ B1 - N1 + 87 >= 0 /\ A1 - N1 + 100 >= 0 /\ X - N1 + 99 >= 0 /\ W - N1 + 82 >= 0 /\ V - N1 + 83 >= 0 /\ -V - N1 + 117 >= 0 /\ S - N1 + 50 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ K1 + N1 - 101 >= 0 /\ -K1 + N1 - 99 >= 0 /\ H1 + N1 - 101 >= 0 /\ -H1 + N1 - 99 >= 0 /\ -C1 + N1 - 92 >= 0 /\ B1 + N1 - 113 >= 0 /\ A1 + N1 - 100 >= 0 /\ X + N1 - 101 >= 0 /\ W + N1 - 118 >= 0 /\ V + N1 - 117 >= 0 /\ -V + N1 - 83 >= 0 /\ S + N1 - 150 >= 0 /\ -Q + N1 - 101 >= 0 /\ G1 - M1 >= 0 /\ F1 - M1 >= 0 /\ E1 - M1 >= 0 /\ D1 - M1 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -G1 + M1 >= 0 /\ -F1 + M1 >= 0 /\ -E1 + M1 >= 0 /\ -D1 + M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ -K1 + 1 >= 0 /\ H1 - K1 >= 0 /\ -H1 - K1 + 2 >= 0 /\ -C1 - K1 + 9 >= 0 /\ B1 - K1 - 12 >= 0 /\ A1 - K1 + 1 >= 0 /\ X - K1 >= 0 /\ W - K1 - 17 >= 0 /\ V - K1 - 16 >= 0 /\ -V - K1 + 18 >= 0 /\ S - K1 - 49 >= 0 /\ -Q - K1 >= 0 /\ K1 - 1 >= 0 /\ H1 + K1 - 2 >= 0 /\ -H1 + K1 >= 0 /\ -C1 + K1 + 7 >= 0 /\ B1 + K1 - 14 >= 0 /\ A1 + K1 - 1 >= 0 /\ X + K1 - 2 >= 0 /\ W + K1 - 19 >= 0 /\ V + K1 - 18 >= 0 /\ -V + K1 + 16 >= 0 /\ S + K1 - 51 >= 0 /\ -Q + K1 - 2 >= 0 /\ C - J1 >= 0 /\ A - J1 >= 0 /\ -C + J1 >= 0 /\ -A + J1 >= 0 /\ -H1 + 1 >= 0 /\ -C1 - H1 + 9 >= 0 /\ B1 - H1 - 12 >= 0 /\ A1 - H1 + 1 >= 0 /\ X - H1 >= 0 /\ W - H1 - 17 >= 0 /\ V - H1 - 16 >= 0 /\ -V - H1 + 18 >= 0 /\ S - H1 - 49 >= 0 /\ -Q - H1 >= 0 /\ H1 - 1 >= 0 /\ -C1 + H1 + 7 >= 0 /\ B1 + H1 - 14 >= 0 /\ A1 + H1 - 1 >= 0 /\ X + H1 - 2 >= 0 /\ W + H1 - 19 >= 0 /\ V + H1 - 18 >= 0 /\ -V + H1 + 16 >= 0 /\ S + H1 - 51 >= 0 /\ -Q + H1 - 2 >= 0 /\ F1 - G1 >= 0 /\ E1 - G1 >= 0 /\ D1 - G1 >= 0 /\ B - G1 >= 0 /\ R - G1 >= 0 /\ -F1 + G1 >= 0 /\ -E1 + G1 >= 0 /\ -D1 + G1 >= 0 /\ -B + G1 >= 0 /\ -R + G1 >= 0 /\ E1 - F1 >= 0 /\ D1 - F1 >= 0 /\ B - F1 >= 0 /\ R - F1 >= 0 /\ -E1 + F1 >= 0 /\ -D1 + F1 >= 0 /\ -B + F1 >= 0 /\ -R + F1 >= 0 /\ D1 - E1 >= 0 /\ B - E1 >= 0 /\ R - E1 >= 0 /\ -D1 + E1 >= 0 /\ -B + E1 >= 0 /\ -R + E1 >= 0 /\ B - D1 >= 0 /\ R - D1 >= 0 /\ -B + D1 >= 0 /\ -R + D1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -C1 + 8 >= 0 /\ B1 - C1 - 5 >= 0 /\ -B1 - C1 + 21 >= 0 /\ A1 - C1 + 8 >= 0 /\ -A1 - C1 + 8 >= 0 /\ X - C1 + 7 >= 0 /\ -X - C1 + 9 >= 0 /\ W - C1 - 10 >= 0 /\ V - C1 - 9 >= 0 /\ -V - C1 + 25 >= 0 /\ S - C1 - 42 >= 0 /\ -Q - C1 + 7 >= 0 /\ X + C1 - 9 >= 0 /\ A1 - B1 + 13 >= 0 /\ X - B1 + 12 >= 0 /\ B1 - 13 >= 0 /\ A1 + B1 - 13 >= 0 /\ -A1 + B1 - 13 >= 0 /\ X + B1 - 14 >= 0 /\ W + B1 - 31 >= 0 /\ V + B1 - 30 >= 0 /\ -V + B1 + 4 >= 0 /\ S + B1 - 63 >= 0 /\ -Q + B1 - 14 >= 0 /\ X - A1 - 1 >= 0 /\ A1 >= 0 /\ X + A1 - 1 >= 0 /\ W + A1 - 18 >= 0 /\ V + A1 - 17 >= 0 /\ -V + A1 + 17 >= 0 /\ S + A1 - 50 >= 0 /\ -Q + A1 - 1 >= 0 /\ X - 1 >= 0 /\ W + X - 19 >= 0 /\ V + X - 18 >= 0 /\ -V + X + 16 >= 0 /\ S + X - 51 >= 0 /\ -Q + X - 2 >= 0 /\ W - 18 >= 0 /\ V + W - 35 >= 0 /\ -V + W - 1 >= 0 /\ S + W - 68 >= 0 /\ -Q + W - 19 >= 0 /\ -V + 17 >= 0 /\ S - V - 33 >= 0 /\ -Q - V + 16 >= 0 /\ V - 17 >= 0 /\ S + V - 67 >= 0 /\ -Q + V - 18 >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S - 50 >= 0 /\ -Q + S - 51 >= 0 /\ -Q - 1 >= 0 /\ X >= 9 ]
  f526(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f540(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, 1, Y, Z, 0, 13, 8, E1, E1, E1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ K1 + I - 101 >= 0 /\ -K1 + I - 99 >= 0 /\ H1 + I - 101 >= 0 /\ -H1 + I - 99 >= 0 /\ W + I - 102 >= 0 /\ V + I - 117 >= 0 /\ -V + I - 83 >= 0 /\ S + I - 150 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ K1 + F - 51 >= 0 /\ -K1 + F - 49 >= 0 /\ H1 + F - 51 >= 0 /\ -H1 + F - 49 >= 0 /\ W + F - 52 >= 0 /\ V + F - 67 >= 0 /\ -V + F - 33 >= 0 /\ S + F - 100 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ K1 + E - 151 >= 0 /\ -K1 + E - 149 >= 0 /\ H1 + E - 151 >= 0 /\ -H1 + E - 149 >= 0 /\ W + E - 152 >= 0 /\ V + E - 167 >= 0 /\ -V + E - 133 >= 0 /\ S + E - 200 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ J1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -J1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ J1 - O1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -J1 + O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ K1 - N1 + 99 >= 0 /\ -K1 - N1 + 101 >= 0 /\ H1 - N1 + 99 >= 0 /\ -H1 - N1 + 101 >= 0 /\ W - N1 + 98 >= 0 /\ V - N1 + 83 >= 0 /\ -V - N1 + 117 >= 0 /\ S - N1 + 50 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ K1 + N1 - 101 >= 0 /\ -K1 + N1 - 99 >= 0 /\ H1 + N1 - 101 >= 0 /\ -H1 + N1 - 99 >= 0 /\ W + N1 - 102 >= 0 /\ V + N1 - 117 >= 0 /\ -V + N1 - 83 >= 0 /\ S + N1 - 150 >= 0 /\ -Q + N1 - 101 >= 0 /\ G1 - M1 >= 0 /\ E1 - M1 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -G1 + M1 >= 0 /\ -E1 + M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ -K1 + 1 >= 0 /\ H1 - K1 >= 0 /\ -H1 - K1 + 2 >= 0 /\ W - K1 - 1 >= 0 /\ V - K1 - 16 >= 0 /\ -V - K1 + 18 >= 0 /\ S - K1 - 49 >= 0 /\ -Q - K1 >= 0 /\ K1 - 1 >= 0 /\ H1 + K1 - 2 >= 0 /\ -H1 + K1 >= 0 /\ W + K1 - 3 >= 0 /\ V + K1 - 18 >= 0 /\ -V + K1 + 16 >= 0 /\ S + K1 - 51 >= 0 /\ -Q + K1 - 2 >= 0 /\ C - J1 >= 0 /\ A - J1 >= 0 /\ -C + J1 >= 0 /\ -A + J1 >= 0 /\ -H1 + 1 >= 0 /\ W - H1 - 1 >= 0 /\ V - H1 - 16 >= 0 /\ -V - H1 + 18 >= 0 /\ S - H1 - 49 >= 0 /\ -Q - H1 >= 0 /\ H1 - 1 >= 0 /\ W + H1 - 3 >= 0 /\ V + H1 - 18 >= 0 /\ -V + H1 + 16 >= 0 /\ S + H1 - 51 >= 0 /\ -Q + H1 - 2 >= 0 /\ E1 - G1 >= 0 /\ B - G1 >= 0 /\ R - G1 >= 0 /\ -E1 + G1 >= 0 /\ -B + G1 >= 0 /\ -R + G1 >= 0 /\ B - E1 >= 0 /\ R - E1 >= 0 /\ -B + E1 >= 0 /\ -R + E1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ W - 2 >= 0 /\ V + W - 19 >= 0 /\ -V + W + 15 >= 0 /\ S + W - 52 >= 0 /\ -Q + W - 3 >= 0 /\ -V + 17 >= 0 /\ S - V - 33 >= 0 /\ -Q - V + 16 >= 0 /\ V - 17 >= 0 /\ S + V - 67 >= 0 /\ -Q + V - 18 >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S - 50 >= 0 /\ -Q + S - 51 >= 0 /\ -Q - 1 >= 0 /\ W >= V + 1 ]
  f501(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f526(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, 17, 2, X, Y, Z, A1, B1, C1, D1, B, F1, B, 1, Q1, A, 1, R1, M1, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ S + I - 100 >= 0 /\ -Q + I - 101 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ S + F - 50 >= 0 /\ -Q + F - 51 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ S + E - 150 >= 0 /\ -Q + E - 151 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ S - N1 + 100 >= 0 /\ -Q - N1 + 99 >= 0 /\ N1 - 100 >= 0 /\ S + N1 - 100 >= 0 /\ -Q + N1 - 101 >= 0 /\ B - M1 >= 0 /\ R - M1 >= 0 /\ -B + M1 >= 0 /\ -R + M1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ R - B >= 0 /\ -R + B >= 0 /\ S >= 0 /\ -Q + S - 1 >= 0 /\ -Q - 1 >= 0 /\ S >= 50 ]
  f485(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f501(A, R, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, 0, Q1, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, R, N1, O1, P1)) [ I - 100 >= 0 /\ F + I - 150 >= 0 /\ E + I - 250 >= 0 /\ N1 + I - 200 >= 0 /\ -N1 + I >= 0 /\ B + I - 43790 >= 0 /\ -B + I + 43590 >= 0 /\ -Q + I - 2 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ N1 + F - 150 >= 0 /\ -N1 + F + 50 >= 0 /\ B + F - 43740 >= 0 /\ -B + F + 43640 >= 0 /\ -Q + F + 48 >= 0 /\ E - 150 >= 0 /\ N1 + E - 250 >= 0 /\ -N1 + E - 50 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ -Q + E - 52 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ -N1 + 100 >= 0 /\ B - N1 - 43590 >= 0 /\ -B - N1 + 43790 >= 0 /\ -Q - N1 + 198 >= 0 /\ N1 - 100 >= 0 /\ B + N1 - 43790 >= 0 /\ -B + N1 + 43590 >= 0 /\ -Q + N1 - 2 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ -Q - B + 43788 >= 0 /\ B - 43690 >= 0 /\ -Q + B - 43592 >= 0 /\ -Q + 98 >= 0 /\ 0 >= Q + 1 ]
  f461(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f455(A, B, C, D, E, F, G, H, I + 2, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ I >= 0 /\ F + I - 50 >= 0 /\ E + I - 150 >= 0 /\ B + I - 43690 >= 0 /\ -B + I + 43690 >= 0 /\ M + I >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ B + F - 43740 >= 0 /\ -B + F + 43640 >= 0 /\ M + F - 50 >= 0 /\ E - 150 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ M + E - 150 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ M - B + 43690 >= 0 /\ B - 43690 >= 0 /\ M + B - 43690 >= 0 /\ M >= 0 /\ M >= 32 ]
  f455(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f485(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 98, Q1, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, 100, O1, P1)) [ I >= 0 /\ F + I - 50 >= 0 /\ E + I - 150 >= 0 /\ B + I - 43690 >= 0 /\ -B + I + 43690 >= 0 /\ F - 50 >= 0 /\ E + F - 200 >= 0 /\ B + F - 43740 >= 0 /\ -B + F + 43640 >= 0 /\ E - 150 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ B - 43690 >= 0 /\ I >= 100 ]
  f441(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f437(A, B, C, D, E, F + 1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ H >= 0 /\ F + H >= 0 /\ E + H - 150 >= 0 /\ B + H - 43690 >= 0 /\ -B + H + 43690 >= 0 /\ F >= 0 /\ E + F - 150 >= 0 /\ B + F - 43690 >= 0 /\ -B + F + 43690 >= 0 /\ E - 150 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ B - 43690 >= 0 /\ H >= 50 ]
  f437(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f455(A, B, C, D, E, F, G, H, 0, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1)) [ F >= 0 /\ E + F - 150 >= 0 /\ B + F - 43690 >= 0 /\ -B + F + 43690 >= 0 /\ E - 150 >= 0 /\ B + E - 43840 >= 0 /\ -B + E + 43540 >= 0 /\ O1 - P1 >= 0 /\ C - P1 >= 0 /\ A - P1 >= 0 /\ -O1 + P1 >= 0 /\ -C + P1 >= 0 /\ -A + P1 >= 0 /\ C - O1 >= 0 /\ A - O1 >= 0 /\ -C + O1 >= 0 /\ -A + O1 >= 0 /\ A - C >= 0 /\ -A + C >= 0 /\ -B + 43690 >= 0 /\ B - 43690 >= 0 /\ F >= 50 ]
  f422(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1) -> Com_1(f437(C, B, C, D, E, 0, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, C, C)) [ E >= 0 /\ B + E - 43690 >= 0 /\ -B + E + 43690 >= 0 /\ A + E - 3 >= 0 /\ -A + E + 3 >= 0 /\ -B + 43690 >= 0 /\ A - B + 43687 >= 0 /\ -A - B + 43693 >= 0 /\ B - 43690 >= 0 /\ A + B - 43693 >= 0 /\ -A + B - 43687 >= 0 /\ -A + 3 >= 0 /\ A - 3 >= 0 /\ E >= 150 ]
)