(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start0)) (VAR A B C D E F G H I J K L M N O P Q R S T) (RULES start(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(stop(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ H - I >= 0 /\ -H + I >= 0 /\ F - G >= 0 /\ -F + G >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A - T >= 0 /\ -A + T >= 0 /\ R - S >= 0 /\ -R + S >= 0 /\ P - Q >= 0 /\ -P + Q >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ 2 >= A /\ B = C /\ D = E /\ F = G /\ H = I /\ J = K /\ L = M /\ N = O /\ P = Q /\ R = S /\ T = A ] start(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl71(A, B, C, D, E, F, G, H, I, U, K, L, M, N, O, 1, Q, 1, S, T)) [ H - I >= 0 /\ -H + I >= 0 /\ F - G >= 0 /\ -F + G >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A - T >= 0 /\ -A + T >= 0 /\ R - S >= 0 /\ -R + S >= 0 /\ P - Q >= 0 /\ -P + Q >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ J - K >= 0 /\ -J + K >= 0 /\ A >= 3 /\ B = C /\ D = E /\ F = G /\ H = I /\ J = K /\ L = M /\ N = O /\ P = Q /\ R = S /\ T = A ] lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl133(A, B, C, D, E, F, G, H, I, J, K, P, M, N, O, P + 1, Q, R, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ R + T - 4 >= 0 /\ P + T - 3 >= 0 /\ -P + T - 3 >= 0 /\ N + T - 4 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ R + B - 3 >= 0 /\ P + B - 2 >= 0 /\ -P + B - 2 >= 0 /\ N + B - 3 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ R - 1 >= 0 /\ P + R - 1 >= 0 /\ N + R - 2 >= 0 /\ A + R - 4 >= 0 /\ A - P - 3 >= 0 /\ P >= 0 /\ N + P - 1 >= 0 /\ A + P - 3 >= 0 /\ N - 1 >= 0 /\ A + N - 4 >= 0 /\ A - 3 >= 0 /\ 2*N + P + 2 >= A /\ N >= 1 /\ A >= 2*N + P /\ A >= N + P + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ R = N /\ T = A ] lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl281(A, B, C, D, E, F, G, H, I, J, K, L, M, 2*R + 1, O, P, Q, T, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ R + T - 4 >= 0 /\ P + T - 3 >= 0 /\ -P + T - 3 >= 0 /\ N + T - 4 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ R + B - 3 >= 0 /\ P + B - 2 >= 0 /\ -P + B - 2 >= 0 /\ N + B - 3 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ R - 1 >= 0 /\ P + R - 1 >= 0 /\ N + R - 2 >= 0 /\ A + R - 4 >= 0 /\ A - P - 3 >= 0 /\ P >= 0 /\ N + P - 1 >= 0 /\ A + P - 3 >= 0 /\ N - 1 >= 0 /\ A + N - 4 >= 0 /\ A - 3 >= 0 /\ A >= 2*N + P + 3 /\ N >= 1 /\ A >= 2*N + P /\ A >= N + P + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ R = N /\ T = A ] lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, 2*R + 1, O, P, Q, 2*R + 1, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ R + T - 4 >= 0 /\ P + T - 3 >= 0 /\ -P + T - 3 >= 0 /\ N + T - 4 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ R + B - 3 >= 0 /\ P + B - 2 >= 0 /\ -P + B - 2 >= 0 /\ N + B - 3 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ R - 1 >= 0 /\ P + R - 1 >= 0 /\ N + R - 2 >= 0 /\ A + R - 4 >= 0 /\ A - P - 3 >= 0 /\ P >= 0 /\ N + P - 1 >= 0 /\ A + P - 3 >= 0 /\ N - 1 >= 0 /\ A + N - 4 >= 0 /\ A - 3 >= 0 /\ A >= 2*N + P + 3 /\ N >= 1 /\ A >= 2*N + P /\ A >= N + P + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ R = N /\ T = A ] lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl281(A, B, C, D, E, F, G, H, I, J, K, L, M, 2*R + 2, O, P, Q, T, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ R + T - 4 >= 0 /\ P + T - 3 >= 0 /\ -P + T - 3 >= 0 /\ N + T - 4 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ R + B - 3 >= 0 /\ P + B - 2 >= 0 /\ -P + B - 2 >= 0 /\ N + B - 3 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ R - 1 >= 0 /\ P + R - 1 >= 0 /\ N + R - 2 >= 0 /\ A + R - 4 >= 0 /\ A - P - 3 >= 0 /\ P >= 0 /\ N + P - 1 >= 0 /\ A + P - 3 >= 0 /\ N - 1 >= 0 /\ A + N - 4 >= 0 /\ A - 3 >= 0 /\ A >= 2*N + P + 4 /\ N >= 1 /\ A >= 2*N + P /\ A >= N + P + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ R = N /\ T = A ] lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, 2*R + 2, O, P, Q, 2*R + 2, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ R + T - 4 >= 0 /\ P + T - 3 >= 0 /\ -P + T - 3 >= 0 /\ N + T - 4 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ R + B - 3 >= 0 /\ P + B - 2 >= 0 /\ -P + B - 2 >= 0 /\ N + B - 3 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ R - 1 >= 0 /\ P + R - 1 >= 0 /\ N + R - 2 >= 0 /\ A + R - 4 >= 0 /\ A - P - 3 >= 0 /\ P >= 0 /\ N + P - 1 >= 0 /\ A + P - 3 >= 0 /\ N - 1 >= 0 /\ A + N - 4 >= 0 /\ A - 3 >= 0 /\ A >= 2*N + P + 4 /\ N >= 1 /\ A >= 2*N + P /\ A >= N + P + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ R = N /\ T = A ] lbl281(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl133(A, B, C, D, E, F, G, H, I, J, K, P, M, N, O, P + 1, Q, R, S, T)) [ B - T + 1 >= 0 /\ R - T >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ R + T - 6 >= 0 /\ -R + T >= 0 /\ P + T - 3 >= 0 /\ -P + T - 3 >= 0 /\ N + T - 4 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ R + B - 5 >= 0 /\ -R + B + 1 >= 0 /\ P + B - 2 >= 0 /\ -P + B - 2 >= 0 /\ N + B - 3 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ A - R >= 0 /\ R - 3 >= 0 /\ P + R - 3 >= 0 /\ -P + R - 3 >= 0 /\ N + R - 4 >= 0 /\ A + R - 6 >= 0 /\ -A + R >= 0 /\ A - P - 3 >= 0 /\ P >= 0 /\ N + P - 1 >= 0 /\ A + P - 3 >= 0 /\ N - 1 >= 0 /\ A + N - 4 >= 0 /\ A - 3 >= 0 /\ A + P + 2 >= 0 /\ N >= 1 /\ A >= P + N + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ T = A /\ R = A ] lbl133(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(stop(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ -R + T >= 0 /\ P + T - 4 >= 0 /\ -N + T - 2 >= 0 /\ L + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ -R + B + 1 >= 0 /\ P + B - 3 >= 0 /\ -N + B - 1 >= 0 /\ L + B - 2 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ A - R >= 0 /\ L - P + 1 >= 0 /\ P - 1 >= 0 /\ N + P - 2 >= 0 /\ L + P - 1 >= 0 /\ -L + P - 1 >= 0 /\ A + P - 4 >= 0 /\ A - N - 2 >= 0 /\ L + N - 1 >= 0 /\ L >= 0 /\ A + L - 3 >= 0 /\ A - 3 >= 0 /\ L + 2 >= A /\ R + L + N + 2 >= A /\ R >= N /\ L + N >= 1 /\ A >= L + N + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ P = L + 1 /\ T = A ] lbl133(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl133(A, B, C, D, E, F, G, H, I, J, K, P, M, 0, O, P + 1, Q, 0, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ -R + T >= 0 /\ P + T - 4 >= 0 /\ -N + T - 2 >= 0 /\ L + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ -R + B + 1 >= 0 /\ P + B - 3 >= 0 /\ -N + B - 1 >= 0 /\ L + B - 2 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ A - R >= 0 /\ L - P + 1 >= 0 /\ P - 1 >= 0 /\ N + P - 2 >= 0 /\ L + P - 1 >= 0 /\ -L + P - 1 >= 0 /\ A + P - 4 >= 0 /\ A - N - 2 >= 0 /\ L + N - 1 >= 0 /\ L >= 0 /\ A + L - 3 >= 0 /\ A - 3 >= 0 /\ R + N >= 1 /\ R >= N /\ A + N >= 4 /\ A >= 3 /\ 1 >= N /\ B >= 2*J + 1 /\ B + 1 >= A /\ T = A /\ P + 2 = A /\ L + 3 = A ] lbl133(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl281(A, B, C, D, E, F, G, H, I, J, K, L, M, 1, O, P, Q, T, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ -R + T >= 0 /\ P + T - 4 >= 0 /\ -N + T - 2 >= 0 /\ L + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ -R + B + 1 >= 0 /\ P + B - 3 >= 0 /\ -N + B - 1 >= 0 /\ L + B - 2 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ A - R >= 0 /\ L - P + 1 >= 0 /\ P - 1 >= 0 /\ N + P - 2 >= 0 /\ L + P - 1 >= 0 /\ -L + P - 1 >= 0 /\ A + P - 4 >= 0 /\ A - N - 2 >= 0 /\ L + N - 1 >= 0 /\ L >= 0 /\ A + L - 3 >= 0 /\ A - 3 >= 0 /\ A >= L + 4 /\ R + L + N + 2 >= A /\ R >= N /\ L + N >= 1 /\ A >= L + N + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ P = L + 1 /\ T = A ] lbl133(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, 1, O, P, Q, 1, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ -R + T >= 0 /\ P + T - 4 >= 0 /\ -N + T - 2 >= 0 /\ L + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ -R + B + 1 >= 0 /\ P + B - 3 >= 0 /\ -N + B - 1 >= 0 /\ L + B - 2 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ A - R >= 0 /\ L - P + 1 >= 0 /\ P - 1 >= 0 /\ N + P - 2 >= 0 /\ L + P - 1 >= 0 /\ -L + P - 1 >= 0 /\ A + P - 4 >= 0 /\ A - N - 2 >= 0 /\ L + N - 1 >= 0 /\ L >= 0 /\ A + L - 3 >= 0 /\ A - 3 >= 0 /\ A >= L + 4 /\ R + L + N + 2 >= A /\ R >= N /\ L + N >= 1 /\ A >= L + N + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ P = L + 1 /\ T = A ] lbl133(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl281(A, B, C, D, E, F, G, H, I, J, K, L, M, 2, O, P, Q, T, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ -R + T >= 0 /\ P + T - 4 >= 0 /\ -N + T - 2 >= 0 /\ L + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ -R + B + 1 >= 0 /\ P + B - 3 >= 0 /\ -N + B - 1 >= 0 /\ L + B - 2 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ A - R >= 0 /\ L - P + 1 >= 0 /\ P - 1 >= 0 /\ N + P - 2 >= 0 /\ L + P - 1 >= 0 /\ -L + P - 1 >= 0 /\ A + P - 4 >= 0 /\ A - N - 2 >= 0 /\ L + N - 1 >= 0 /\ L >= 0 /\ A + L - 3 >= 0 /\ A - 3 >= 0 /\ A >= L + 5 /\ R + L + N + 2 >= A /\ R >= N /\ L + N >= 1 /\ A >= L + N + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ P = L + 1 /\ T = A ] lbl133(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, 2, O, P, Q, 2, S, T)) [ B - T + 1 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 5 >= 0 /\ -R + T >= 0 /\ P + T - 4 >= 0 /\ -N + T - 2 >= 0 /\ L + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ B - 2 >= 0 /\ -R + B + 1 >= 0 /\ P + B - 3 >= 0 /\ -N + B - 1 >= 0 /\ L + B - 2 >= 0 /\ A + B - 5 >= 0 /\ -A + B + 1 >= 0 /\ A - R >= 0 /\ L - P + 1 >= 0 /\ P - 1 >= 0 /\ N + P - 2 >= 0 /\ L + P - 1 >= 0 /\ -L + P - 1 >= 0 /\ A + P - 4 >= 0 /\ A - N - 2 >= 0 /\ L + N - 1 >= 0 /\ L >= 0 /\ A + L - 3 >= 0 /\ A - 3 >= 0 /\ A >= L + 5 /\ R + L + N + 2 >= A /\ R >= N /\ L + N >= 1 /\ A >= L + N + 2 /\ B >= 2*J + 1 /\ B + 1 >= A /\ P = L + 1 /\ T = A ] lbl71(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl101(A, B, C, U, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ A - T >= 0 /\ T - 3 >= 0 /\ P + T - 4 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - R >= 0 /\ P - 1 >= 0 /\ A + P - 4 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ A - 3 >= 0 /\ R >= 1 /\ R >= 2*J + 1 /\ 2*J + 2 >= R /\ P >= 1 /\ A >= 3 /\ P >= R /\ T = A /\ N = O /\ L = M ] lbl71(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl43(A, P, C, D, E, F, G, H, I, J, K, L, M, N, O, P + 1, Q, R, S, T)) [ A - T >= 0 /\ T - 3 >= 0 /\ P + T - 4 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - R >= 0 /\ P - 1 >= 0 /\ A + P - 4 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ A - 3 >= 0 /\ R >= 2*J + 1 /\ 2*J + 2 >= R /\ P >= 1 /\ A >= 3 /\ P >= R /\ T = A /\ N = O /\ L = M ] lbl121(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl123(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, H, S, T)) [ F >= 0 /\ D + F >= 0 /\ T + F - 3 >= 0 /\ R + F - 1 >= 0 /\ P + F - 1 >= 0 /\ J + F >= 0 /\ A + F - 3 >= 0 /\ R - D - 1 >= 0 /\ P - D - 1 >= 0 /\ D >= 0 /\ T + D - 3 >= 0 /\ R + D - 1 >= 0 /\ P + D - 1 >= 0 /\ J + D >= 0 /\ A + D - 3 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ R + T - 4 >= 0 /\ P + T - 4 >= 0 /\ J + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - R >= 0 /\ R - 1 >= 0 /\ P + R - 2 >= 0 /\ J + R - 1 >= 0 /\ -J + R - 1 >= 0 /\ A + R - 4 >= 0 /\ P - 1 >= 0 /\ J + P - 1 >= 0 /\ -J + P - 1 >= 0 /\ A + P - 4 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ J >= 0 /\ A + J - 3 >= 0 /\ A - 3 >= 0 /\ R >= 2*H + 1 /\ 2*H + 2 >= R /\ A >= 3 /\ R >= 1 /\ R >= 2*D + 1 /\ R >= 2*F + 1 /\ R >= 2*J + 1 /\ P >= R /\ 2*J + 2 >= R /\ 2*F + 2 >= R /\ 2*D + 2 >= R /\ L = M /\ N = O /\ T = A ] lbl123(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl71(A, B, C, D, E, F, G, H, I, U, K, L, M, N, O, P, Q, R, S, T)) [ R - H >= 0 /\ H >= 0 /\ F + H >= 0 /\ D + H >= 0 /\ T + H - 3 >= 0 /\ R + H >= 0 /\ -R + H >= 0 /\ P + H - 1 >= 0 /\ J + H >= 0 /\ A + H - 3 >= 0 /\ P - F - 1 >= 0 /\ F >= 0 /\ D + F >= 0 /\ T + F - 3 >= 0 /\ R + F >= 0 /\ P + F - 1 >= 0 /\ J + F >= 0 /\ A + F - 3 >= 0 /\ P - D - 1 >= 0 /\ D >= 0 /\ T + D - 3 >= 0 /\ R + D >= 0 /\ P + D - 1 >= 0 /\ J + D >= 0 /\ A + D - 3 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ R + T - 3 >= 0 /\ P + T - 4 >= 0 /\ J + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ R >= 0 /\ P + R - 1 >= 0 /\ J + R >= 0 /\ A + R - 3 >= 0 /\ P - 1 >= 0 /\ J + P - 1 >= 0 /\ -J + P - 1 >= 0 /\ A + P - 4 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ J >= 0 /\ A + J - 3 >= 0 /\ A - 3 >= 0 /\ 2*H + 1 >= 0 /\ P >= 1 /\ 2*F + 1 >= 0 /\ 2*J + 1 >= 0 /\ 2*D + 1 >= 0 /\ P >= 2*J + 1 /\ P >= 2*F + 1 /\ P >= 2*D + 1 /\ P >= 2*H + 1 /\ 2*D + 1 >= 2*F /\ 2*H + 1 >= 2*J /\ 2*H + 1 >= 2*D /\ 2*H + 1 >= 2*F /\ 2*J + 1 >= 2*D /\ 2*J + 1 >= 2*F /\ 2*D + 1 >= 2*J /\ 2*D + 1 >= 2*H /\ 2*F + 1 >= 2*D /\ 2*F + 1 >= 2*J /\ 2*F + 1 >= 2*H /\ 2*J + 1 >= 2*H /\ A >= 3 /\ R = H /\ L = M /\ T = A /\ N = O ] lbl111(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl121(A, B, C, D, E, F, G, U, I, J, K, L, M, N, O, P, Q, R, S, T)) [ D >= 0 /\ T + D - 3 >= 0 /\ R + D - 1 >= 0 /\ P + D - 1 >= 0 /\ J + D >= 0 /\ A + D - 3 >= 0 /\ A - T >= 0 /\ T - 3 >= 0 /\ R + T - 4 >= 0 /\ P + T - 4 >= 0 /\ J + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - R >= 0 /\ R - 1 >= 0 /\ P + R - 2 >= 0 /\ J + R - 1 >= 0 /\ -J + R - 1 >= 0 /\ A + R - 4 >= 0 /\ P - 1 >= 0 /\ J + P - 1 >= 0 /\ -J + P - 1 >= 0 /\ A + P - 4 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ J >= 0 /\ A + J - 3 >= 0 /\ A - 3 >= 0 /\ R >= 2*F + 1 /\ 2*F + 2 >= R /\ A >= 3 /\ R >= 1 /\ R >= 2*D + 1 /\ R >= 2*J + 1 /\ P >= R /\ 2*J + 2 >= R /\ 2*D + 2 >= R /\ L = M /\ N = O /\ T = A ] lbl101(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl111(A, B, C, D, E, U, G, H, I, J, K, L, M, N, O, P, Q, R, S, T)) [ A - T >= 0 /\ T - 3 >= 0 /\ R + T - 4 >= 0 /\ P + T - 4 >= 0 /\ J + T - 3 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - R >= 0 /\ R - 1 >= 0 /\ P + R - 2 >= 0 /\ J + R - 1 >= 0 /\ A + R - 4 >= 0 /\ P - 1 >= 0 /\ J + P - 1 >= 0 /\ A + P - 4 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ J >= 0 /\ A + J - 3 >= 0 /\ A - 3 >= 0 /\ R >= 2*D + 1 /\ 2*D + 2 >= R /\ A >= 3 /\ R >= 1 /\ R >= 2*J + 1 /\ P >= R /\ 2*J + 2 >= R /\ L = M /\ N = O /\ T = A ] lbl43(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl71(A, B, C, D, E, F, G, H, I, U, K, L, M, N, O, P, Q, P, S, T)) [ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 4 >= 0 /\ P + T - 5 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - B - 1 >= 0 /\ B - 1 >= 0 /\ -R + B >= 0 /\ P + B - 3 >= 0 /\ -P + B + 1 >= 0 /\ A + B - 4 >= 0 /\ P - R - 1 >= 0 /\ P - 2 >= 0 /\ A + P - 5 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ A - 3 >= 0 /\ A >= B + 2 /\ A >= 3 /\ R >= 2*J + 1 /\ B >= 1 /\ 2*J + 2 >= R /\ B >= R /\ P = B + 1 /\ L = M /\ N = O /\ T = A ] lbl43(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl281(A, B, C, D, E, F, G, H, I, J, K, L, M, 1, O, 0, Q, T, S, T)) [ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 4 >= 0 /\ P + T - 5 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - B - 1 >= 0 /\ B - 1 >= 0 /\ -R + B >= 0 /\ P + B - 3 >= 0 /\ -P + B + 1 >= 0 /\ A + B - 4 >= 0 /\ P - R - 1 >= 0 /\ P - 2 >= 0 /\ A + P - 5 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ A - 3 >= 0 /\ A >= 3 /\ B + 1 >= A /\ R >= 2*J + 1 /\ B >= 1 /\ 2*J + 2 >= R /\ B >= R /\ P = B + 1 /\ L = M /\ N = O /\ T = A ] lbl43(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, 1, O, 0, Q, 1, S, T)) [ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 4 >= 0 /\ P + T - 5 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - B - 1 >= 0 /\ B - 1 >= 0 /\ -R + B >= 0 /\ P + B - 3 >= 0 /\ -P + B + 1 >= 0 /\ A + B - 4 >= 0 /\ P - R - 1 >= 0 /\ P - 2 >= 0 /\ A + P - 5 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ A - 3 >= 0 /\ A >= 3 /\ B + 1 >= A /\ R >= 2*J + 1 /\ B >= 1 /\ 2*J + 2 >= R /\ B >= R /\ P = B + 1 /\ L = M /\ N = O /\ T = A ] lbl43(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl281(A, B, C, D, E, F, G, H, I, J, K, L, M, 2, O, 0, Q, T, S, T)) [ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 4 >= 0 /\ P + T - 5 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - B - 1 >= 0 /\ B - 1 >= 0 /\ -R + B >= 0 /\ P + B - 3 >= 0 /\ -P + B + 1 >= 0 /\ A + B - 4 >= 0 /\ P - R - 1 >= 0 /\ P - 2 >= 0 /\ A + P - 5 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ A - 3 >= 0 /\ A >= 4 /\ B + 1 >= A /\ A >= 3 /\ R >= 2*J + 1 /\ B >= 1 /\ 2*J + 2 >= R /\ B >= R /\ P = B + 1 /\ L = M /\ N = O /\ T = A ] lbl43(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(lbl271(A, B, C, D, E, F, G, H, I, J, K, L, M, 2, O, 0, Q, 2, S, T)) [ A - T >= 0 /\ T - 3 >= 0 /\ B + T - 4 >= 0 /\ P + T - 5 >= 0 /\ A + T - 6 >= 0 /\ -A + T >= 0 /\ P - B - 1 >= 0 /\ B - 1 >= 0 /\ -R + B >= 0 /\ P + B - 3 >= 0 /\ -P + B + 1 >= 0 /\ A + B - 4 >= 0 /\ P - R - 1 >= 0 /\ P - 2 >= 0 /\ A + P - 5 >= 0 /\ N - O >= 0 /\ -N + O >= 0 /\ L - M >= 0 /\ -L + M >= 0 /\ A - 3 >= 0 /\ A >= 4 /\ B + 1 >= A /\ A >= 3 /\ R >= 2*J + 1 /\ B >= 1 /\ 2*J + 2 >= R /\ B >= R /\ P = B + 1 /\ L = M /\ N = O /\ T = A ] start0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T) -> Com_1(start(A, C, C, E, E, G, G, I, I, K, K, M, M, O, O, Q, Q, S, S, A)) )