(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start0)) (VAR A B C D E F) (RULES start(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E, F)) [ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ 0 >= A + 1 /\ B = C /\ D = E /\ F = A ] start(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E, F)) [ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 0 /\ C >= E + 1 /\ B = C /\ D = E /\ F = A ] start(A, B, C, D, E, F) -> Com_1(lbl91(A, B, C, D - F - 1, E, F)) [ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 0 /\ E >= C /\ B = C /\ D = E /\ F = A ] start(A, B, C, D, E, F) -> Com_1(lbl101(A, F + B + 1, C, D, E, F)) [ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 0 /\ E >= C /\ B = C /\ D = E /\ F = A ] lbl91(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E, F)) [ A - F >= 0 /\ F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ -D + E - 1 >= 0 /\ -C + E >= 0 /\ -B + E >= 0 /\ B - C >= 0 /\ A >= 0 /\ B >= D + 1 /\ B >= C /\ A + D + 1 >= B /\ E >= A + D + 1 /\ F = A ] lbl91(A, B, C, D, E, F) -> Com_1(lbl91(A, B, C, D - F - 1, E, F)) [ A - F >= 0 /\ F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ -D + E - 1 >= 0 /\ -C + E >= 0 /\ -B + E >= 0 /\ B - C >= 0 /\ A >= 0 /\ D >= B /\ B >= C /\ A + D + 1 >= B /\ E >= A + D + 1 /\ F = A ] lbl91(A, B, C, D, E, F) -> Com_1(lbl101(A, F + B + 1, C, D, E, F)) [ A - F >= 0 /\ F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ -D + E - 1 >= 0 /\ -C + E >= 0 /\ -B + E >= 0 /\ B - C >= 0 /\ A >= 0 /\ D >= B /\ B >= C /\ A + D + 1 >= B /\ E >= A + D + 1 /\ F = A ] lbl101(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E, F)) [ A - F >= 0 /\ F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ -D + E >= 0 /\ -C + E >= 0 /\ -C + D >= 0 /\ B - C - 1 >= 0 /\ A >= 0 /\ B >= D + 1 /\ E >= D /\ B >= A + C + 1 /\ A + D + 1 >= B /\ F = A ] lbl101(A, B, C, D, E, F) -> Com_1(lbl91(A, B, C, D - F - 1, E, F)) [ A - F >= 0 /\ F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ -D + E >= 0 /\ -C + E >= 0 /\ -C + D >= 0 /\ B - C - 1 >= 0 /\ A >= 0 /\ D >= B /\ E >= D /\ B >= A + C + 1 /\ A + D + 1 >= B /\ F = A ] lbl101(A, B, C, D, E, F) -> Com_1(lbl101(A, F + B + 1, C, D, E, F)) [ A - F >= 0 /\ F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ -D + E >= 0 /\ -C + E >= 0 /\ -C + D >= 0 /\ B - C - 1 >= 0 /\ A >= 0 /\ D >= B /\ E >= D /\ B >= A + C + 1 /\ A + D + 1 >= B /\ F = A ] start0(A, B, C, D, E, F) -> Com_1(start(A, C, C, E, E, A)) )