(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalndloopstart)) (VAR A) (RULES evalndloopstart(A) -> Com_1(evalndloopentryin(A)) evalndloopentryin(A) -> Com_1(evalndloopbbin(0)) evalndloopbbin(A) -> Com_1(evalndloopbbin(B)) [ A >= 0 /\ A + 2 >= B /\ B >= A + 1 /\ 9 >= B ] evalndloopbbin(A) -> Com_1(evalndloopreturnin(A)) [ A >= 0 /\ B >= A + 3 ] evalndloopbbin(A) -> Com_1(evalndloopreturnin(A)) [ A >= 0 /\ A >= B ] evalndloopbbin(A) -> Com_1(evalndloopreturnin(A)) [ A >= 0 /\ B >= 10 ] evalndloopreturnin(A) -> Com_1(evalndloopstop(A)) [ A >= 0 ] )