(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start0)) (VAR A B C D E F G H I J K L M N O P) (RULES start(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl21(A, B, C, D, E, F, G, H, I, J, K, L, M, N, Q, P)) [ J - I >= 0 /\ -J + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ O - P >= 0 /\ -O + P >= 0 /\ M - N >= 0 /\ -M + N >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ A = B /\ C = D /\ E = F /\ G = H /\ I = J /\ K = L /\ M = N /\ O = P ] lbl121(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl123(A, B, C, D, E, F, A, H, I, J, K, L, M, N, O, P)) [ M - I + 1 >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ I - 2 >= 0 /\ G + I - 3 >= 0 /\ E + I - 2 >= 0 /\ -E + I - 1 >= 0 /\ O + I - 3 >= 0 /\ M + I - 3 >= 0 /\ -M + I - 1 >= 0 /\ L + I - 4 >= 0 /\ -L + I >= 0 /\ K + I - 4 >= 0 /\ -K + I >= 0 /\ O - G >= 0 /\ G - 1 >= 0 /\ E + G - 1 >= 0 /\ O + G - 2 >= 0 /\ M + G - 2 >= 0 /\ L + G - 3 >= 0 /\ K + G - 3 >= 0 /\ M - E >= 0 /\ L - E - 1 >= 0 /\ K - E - 1 >= 0 /\ E >= 0 /\ O + E - 1 >= 0 /\ M + E - 1 >= 0 /\ L + E - 2 >= 0 /\ K + E - 2 >= 0 /\ O - 1 >= 0 /\ M + O - 2 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ L - M - 1 >= 0 /\ K - M - 1 >= 0 /\ M - 1 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 1 >= 0 /\ K + M - 3 >= 0 /\ -K + M + 1 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ K - 2 >= 0 /\ G >= 2*A /\ 2*A + 1 >= G /\ 2*O + 1 >= L /\ O >= G /\ G >= 1 /\ L >= E + 1 /\ K = L /\ I = L /\ M + 1 = L ] lbl123(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(stop(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P)) [ M - I + 1 >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ I - 2 >= 0 /\ G + I - 2 >= 0 /\ E + I - 2 >= 0 /\ -E + I - 1 >= 0 /\ O + I - 3 >= 0 /\ M + I - 3 >= 0 /\ -M + I - 1 >= 0 /\ L + I - 4 >= 0 /\ -L + I >= 0 /\ K + I - 4 >= 0 /\ -K + I >= 0 /\ A + I - 2 >= 0 /\ A - G >= 0 /\ G >= 0 /\ E + G >= 0 /\ O + G - 1 >= 0 /\ M + G - 1 >= 0 /\ L + G - 2 >= 0 /\ K + G - 2 >= 0 /\ A + G >= 0 /\ -A + G >= 0 /\ M - E >= 0 /\ L - E - 1 >= 0 /\ K - E - 1 >= 0 /\ E >= 0 /\ O + E - 1 >= 0 /\ M + E - 1 >= 0 /\ L + E - 2 >= 0 /\ K + E - 2 >= 0 /\ A + E >= 0 /\ O - 1 >= 0 /\ M + O - 2 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ A + O - 1 >= 0 /\ L - M - 1 >= 0 /\ K - M - 1 >= 0 /\ M - 1 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 1 >= 0 /\ K + M - 3 >= 0 /\ -K + M + 1 >= 0 /\ A + M - 1 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ A + L - 2 >= 0 /\ K - 2 >= 0 /\ A + K - 2 >= 0 /\ A >= 0 /\ 2*O + 1 >= L /\ O >= 1 /\ L >= E + 1 /\ O >= 0 /\ G = 0 /\ K = L /\ I = L /\ M + 1 = L /\ A = 0 ] lbl123(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl71(A, B, Q, D, 0, F, G, H, 0, J, K, L, M, N, O, P)) [ M - I + 1 >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ I - 2 >= 0 /\ G + I - 2 >= 0 /\ E + I - 2 >= 0 /\ -E + I - 1 >= 0 /\ O + I - 3 >= 0 /\ M + I - 3 >= 0 /\ -M + I - 1 >= 0 /\ L + I - 4 >= 0 /\ -L + I >= 0 /\ K + I - 4 >= 0 /\ -K + I >= 0 /\ A + I - 2 >= 0 /\ A - G >= 0 /\ G >= 0 /\ E + G >= 0 /\ O + G - 1 >= 0 /\ M + G - 1 >= 0 /\ L + G - 2 >= 0 /\ K + G - 2 >= 0 /\ A + G >= 0 /\ -A + G >= 0 /\ M - E >= 0 /\ L - E - 1 >= 0 /\ K - E - 1 >= 0 /\ E >= 0 /\ O + E - 1 >= 0 /\ M + E - 1 >= 0 /\ L + E - 2 >= 0 /\ K + E - 2 >= 0 /\ A + E >= 0 /\ O - 1 >= 0 /\ M + O - 2 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ A + O - 1 >= 0 /\ L - M - 1 >= 0 /\ K - M - 1 >= 0 /\ M - 1 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 1 >= 0 /\ K + M - 3 >= 0 /\ -K + M + 1 >= 0 /\ A + M - 1 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ A + L - 2 >= 0 /\ K - 2 >= 0 /\ A + K - 2 >= 0 /\ A >= 0 /\ L >= 1 /\ A >= 1 /\ 2*O + 1 >= L /\ O >= 1 /\ L >= E + 1 /\ O >= 2*A /\ K = L /\ I = L /\ M + 1 = L /\ G = A ] lbl101(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl101(A, B, C, D, E - G, F, G, H, I, J, K, L, M, N, O, P)) [ L - I - 1 >= 0 /\ K - I - 1 >= 0 /\ I - 1 >= 0 /\ G + I - 2 >= 0 /\ -G + I >= 0 /\ E + I >= 0 /\ -E + I - 1 >= 0 /\ O + I - 2 >= 0 /\ L + I - 3 >= 0 /\ K + I - 3 >= 0 /\ O - G >= 0 /\ L - G - 1 >= 0 /\ K - G - 1 >= 0 /\ G - 1 >= 0 /\ E + G >= 0 /\ O + G - 2 >= 0 /\ L + G - 3 >= 0 /\ K + G - 3 >= 0 /\ L - E - 2 >= 0 /\ K - E - 2 >= 0 /\ O + E >= 0 /\ L + E - 1 >= 0 /\ K + E - 1 >= 0 /\ O - 1 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ K - 2 >= 0 /\ E >= G /\ I >= G + E /\ O >= G /\ L >= I + 1 /\ G >= 1 /\ 2*O + 1 >= L /\ E >= 0 /\ K = L ] lbl101(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl53(A, B, C, D, E, F, G, H, I + 1, J, K, L, I, N, O, P)) [ L - I - 1 >= 0 /\ K - I - 1 >= 0 /\ I - 1 >= 0 /\ G + I - 2 >= 0 /\ -G + I >= 0 /\ E + I >= 0 /\ -E + I - 1 >= 0 /\ O + I - 2 >= 0 /\ L + I - 3 >= 0 /\ K + I - 3 >= 0 /\ O - G >= 0 /\ L - G - 1 >= 0 /\ K - G - 1 >= 0 /\ G - 1 >= 0 /\ E + G >= 0 /\ O + G - 2 >= 0 /\ L + G - 3 >= 0 /\ K + G - 3 >= 0 /\ L - E - 2 >= 0 /\ K - E - 2 >= 0 /\ O + E >= 0 /\ L + E - 1 >= 0 /\ K + E - 1 >= 0 /\ O - 1 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ K - 2 >= 0 /\ I >= G + E /\ O >= G /\ L >= I + 1 /\ G >= 1 /\ 2*O + 1 >= L /\ E >= 0 /\ K = L ] lbl71(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl101(A, B, C, D, E - G, F, G, H, I, J, K, L, M, N, O, P)) [ E - I >= 0 /\ I >= 0 /\ G + I - 1 >= 0 /\ E + I >= 0 /\ -E + I >= 0 /\ O + I - 1 >= 0 /\ L + I - 2 >= 0 /\ K + I - 2 >= 0 /\ O - G >= 0 /\ G - 1 >= 0 /\ E + G - 1 >= 0 /\ O + G - 2 >= 0 /\ L + G - 3 >= 0 /\ K + G - 3 >= 0 /\ E >= 0 /\ O + E - 1 >= 0 /\ L + E - 2 >= 0 /\ K + E - 2 >= 0 /\ O - 1 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ K - 2 >= 0 /\ E >= G /\ 2*O + 1 >= L /\ O >= G /\ G >= 1 /\ L >= E + 1 /\ I = E /\ K = L ] lbl71(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl53(A, B, C, D, E, F, G, H, I + 1, J, K, L, I, N, O, P)) [ E - I >= 0 /\ I >= 0 /\ G + I - 1 >= 0 /\ E + I >= 0 /\ -E + I >= 0 /\ O + I - 1 >= 0 /\ L + I - 2 >= 0 /\ K + I - 2 >= 0 /\ O - G >= 0 /\ G - 1 >= 0 /\ E + G - 1 >= 0 /\ O + G - 2 >= 0 /\ L + G - 3 >= 0 /\ K + G - 3 >= 0 /\ E >= 0 /\ O + E - 1 >= 0 /\ L + E - 2 >= 0 /\ K + E - 2 >= 0 /\ O - 1 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ K - 2 >= 0 /\ 2*O + 1 >= L /\ O >= G /\ G >= 1 /\ L >= E + 1 /\ I = E /\ K = L ] lbl53(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl121(Q, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P)) [ M - I + 1 >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ I - 1 >= 0 /\ G + I - 2 >= 0 /\ E + I - 1 >= 0 /\ -E + I - 1 >= 0 /\ O + I - 2 >= 0 /\ M + I - 1 >= 0 /\ -M + I - 1 >= 0 /\ L + I - 3 >= 0 /\ K + I - 3 >= 0 /\ O - G >= 0 /\ G - 1 >= 0 /\ E + G - 1 >= 0 /\ O + G - 2 >= 0 /\ M + G - 1 >= 0 /\ L + G - 3 >= 0 /\ K + G - 3 >= 0 /\ M - E >= 0 /\ L - E - 1 >= 0 /\ K - E - 1 >= 0 /\ E >= 0 /\ O + E - 1 >= 0 /\ M + E >= 0 /\ L + E - 2 >= 0 /\ K + E - 2 >= 0 /\ O - 1 >= 0 /\ M + O - 1 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ L - M - 1 >= 0 /\ K - M - 1 >= 0 /\ M >= 0 /\ L + M - 2 >= 0 /\ K + M - 2 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ K - 2 >= 0 /\ L >= E + 1 /\ G >= 1 /\ O >= G /\ 2*O + 1 >= L /\ I = L /\ K = L /\ M + 1 = L ] lbl53(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl71(A, B, Q, D, I, F, G, H, I, J, K, L, M, N, O, P)) [ M - I + 1 >= 0 /\ L - I >= 0 /\ K - I >= 0 /\ I - 1 >= 0 /\ G + I - 2 >= 0 /\ E + I - 1 >= 0 /\ -E + I - 1 >= 0 /\ O + I - 2 >= 0 /\ M + I - 1 >= 0 /\ -M + I - 1 >= 0 /\ L + I - 3 >= 0 /\ K + I - 3 >= 0 /\ O - G >= 0 /\ G - 1 >= 0 /\ E + G - 1 >= 0 /\ O + G - 2 >= 0 /\ M + G - 1 >= 0 /\ L + G - 3 >= 0 /\ K + G - 3 >= 0 /\ M - E >= 0 /\ L - E - 1 >= 0 /\ K - E - 1 >= 0 /\ E >= 0 /\ O + E - 1 >= 0 /\ M + E >= 0 /\ L + E - 2 >= 0 /\ K + E - 2 >= 0 /\ O - 1 >= 0 /\ M + O - 1 >= 0 /\ L + O - 3 >= 0 /\ K + O - 3 >= 0 /\ L - M - 1 >= 0 /\ K - M - 1 >= 0 /\ M >= 0 /\ L + M - 2 >= 0 /\ K + M - 2 >= 0 /\ K - L >= 0 /\ L - 2 >= 0 /\ K + L - 4 >= 0 /\ -K + L >= 0 /\ K - 2 >= 0 /\ L >= M + 2 /\ L >= M + 1 /\ M >= E /\ G >= 1 /\ O >= G /\ 2*O + 1 >= L /\ I = M + 1 /\ K = L ] lbl21(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(stop(A, B, C, D, E, F, O, H, I, J, K, L, M, N, O, P)) [ J - I >= 0 /\ -J + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ M - N >= 0 /\ -M + N >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ L >= 2*O /\ 0 >= O /\ 2*O + 1 >= L /\ M = N /\ A = B /\ C = D /\ E = F /\ G = H /\ I = J /\ K = L ] lbl21(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(lbl71(A, B, Q, D, 0, F, O, H, 0, J, K, L, M, N, O, P)) [ J - I >= 0 /\ -J + I >= 0 /\ G - H >= 0 /\ -G + H >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ M - N >= 0 /\ -M + N >= 0 /\ K - L >= 0 /\ -K + L >= 0 /\ L >= 2*O /\ O >= 1 /\ 2*O + 1 >= L /\ M = N /\ A = B /\ C = D /\ E = F /\ G = H /\ I = J /\ K = L ] start0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P) -> Com_1(start(B, B, D, D, F, F, H, H, J, J, L, L, N, N, P, P)) )