(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, F, 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(lbl121(A, 1, C, F - 1, E, F)) [ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 0 /\ 1 >= A /\ B = C /\ D = E /\ F = A ] start(A, B, C, D, E, F) -> Com_1(lbl101(A, 2, C, F, E, F)) [ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 2 /\ B = C /\ D = E /\ F = A ] lbl121(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E, F)) [ A - F >= 0 /\ F >= 0 /\ D + F + 1 >= 0 /\ -D + F - 1 >= 0 /\ B + F - 1 >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ B - D - 1 >= 0 /\ A - D - 1 >= 0 /\ D + 1 >= 0 /\ B + D >= 0 /\ A + D + 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ A >= 0 /\ B >= 0 /\ B >= 1 /\ D + 1 = 0 /\ F = A ] lbl121(A, B, C, D, E, F) -> Com_1(lbl121(A, 1, C, D - 1, E, F)) [ A - F >= 0 /\ F >= 0 /\ D + F + 1 >= 0 /\ -D + F - 1 >= 0 /\ B + F - 1 >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ B - D - 1 >= 0 /\ A - D - 1 >= 0 /\ D + 1 >= 0 /\ B + D >= 0 /\ A + D + 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ A >= 0 /\ D >= 0 /\ 1 >= D /\ A >= D + 1 /\ B >= D + 1 /\ B >= 1 /\ F = A ] lbl121(A, B, C, D, E, F) -> Com_1(lbl101(A, 2, C, D, E, F)) [ A - F >= 0 /\ F >= 0 /\ D + F + 1 >= 0 /\ -D + F - 1 >= 0 /\ B + F - 1 >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ B - D - 1 >= 0 /\ A - D - 1 >= 0 /\ D + 1 >= 0 /\ B + D >= 0 /\ A + D + 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ A >= 0 /\ D >= 2 /\ A >= D + 1 /\ B >= D + 1 /\ B >= 1 /\ F = A ] lbl101(A, B, C, D, E, F) -> Com_1(lbl101(A, 2*B, C, D, E, F)) [ A - F >= 0 /\ F - 2 >= 0 /\ D + F - 4 >= 0 /\ -D + F >= 0 /\ B + F - 4 >= 0 /\ A + F - 4 >= 0 /\ -A + F >= 0 /\ A - D >= 0 /\ D - 2 >= 0 /\ B + D - 4 >= 0 /\ A + D - 4 >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ A - 2 >= 0 /\ D >= B + 1 /\ B >= 2 /\ 2*D >= B + 2 /\ A >= D /\ F = A ] lbl101(A, B, C, D, E, F) -> Com_1(lbl121(A, B, C, D - 1, E, F)) [ A - F >= 0 /\ F - 2 >= 0 /\ D + F - 4 >= 0 /\ -D + F >= 0 /\ B + F - 4 >= 0 /\ A + F - 4 >= 0 /\ -A + F >= 0 /\ A - D >= 0 /\ D - 2 >= 0 /\ B + D - 4 >= 0 /\ A + D - 4 >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ A - 2 >= 0 /\ B >= D /\ B >= 2 /\ 2*D >= B + 2 /\ A >= D /\ F = A ] start0(A, B, C, D, E, F) -> Com_1(start(A, C, C, E, E, A)) )