(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start0)) (VAR A B C D E F) (RULES start(A, B, C, D, E, F) -> Com_1(lbl71(A, B, 1, D, 0, F)) [ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ A >= 2 /\ B = A /\ C = D /\ E = F ] start(A, B, C, D, E, F) -> Com_1(stop(A, B, 0, D, 1, F)) [ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ 1 >= A /\ B = A /\ C = D /\ E = F ] lbl71(A, B, C, D, E, F) -> Com_1(lbl71(A, B, C + 1, D, E, F)) [ B - E - 2 >= 0 /\ A - E - 2 >= 0 /\ E >= 0 /\ C + E - 1 >= 0 /\ B + E - 2 >= 0 /\ A + E - 2 >= 0 /\ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ A + C - 3 >= 0 /\ A - B >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ -A + B >= 0 /\ A - 2 >= 0 /\ A >= C + 2 /\ A >= C + 1 /\ A >= E + 2 /\ C >= 1 /\ B = A ] lbl71(A, B, C, D, E, F) -> Com_1(cut(A, B, C, D, E + 1, F)) [ B - E - 2 >= 0 /\ A - E - 2 >= 0 /\ E >= 0 /\ C + E - 1 >= 0 /\ B + E - 2 >= 0 /\ A + E - 2 >= 0 /\ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ A + C - 3 >= 0 /\ A - B >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ -A + B >= 0 /\ A - 2 >= 0 /\ A >= E + 3 /\ A >= E + 2 /\ A >= 2 /\ C + 1 = A /\ B = A ] lbl71(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E + 1, F)) [ B - E - 2 >= 0 /\ A - E - 2 >= 0 /\ E >= 0 /\ C + E - 1 >= 0 /\ B + E - 2 >= 0 /\ A + E - 2 >= 0 /\ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ A + C - 3 >= 0 /\ A - B >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ -A + B >= 0 /\ A - 2 >= 0 /\ A >= 2 /\ E + 2 = A /\ C + 1 = A /\ B = A ] cut(A, B, C, D, E, F) -> Com_1(lbl71(A, B, 1, D, E, F)) [ C - E - 1 >= 0 /\ B - E - 2 >= 0 /\ A - E - 2 >= 0 /\ E - 1 >= 0 /\ C + E - 3 >= 0 /\ B + E - 4 >= 0 /\ A + E - 4 >= 0 /\ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C - 2 >= 0 /\ B + C - 5 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 1 >= 0 /\ A - B >= 0 /\ B - 3 >= 0 /\ A + B - 6 >= 0 /\ -A + B >= 0 /\ A - 3 >= 0 /\ A >= 2 /\ A >= E + 2 /\ E >= 1 /\ C + 1 = A /\ B = A ] start0(A, B, C, D, E, F) -> Com_1(start(A, A, D, D, F, F)) )