(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalaxstart)) (VAR A B C) (RULES evalaxstart(A, B, C) -> Com_1(evalaxentryin(A, B, C)) evalaxentryin(A, B, C) -> Com_1(evalaxbbin(0, B, C)) evalaxbbin(A, B, C) -> Com_1(evalaxbb2in(A, 0, C)) [ A >= 0 ] evalaxbb2in(A, B, C) -> Com_1(evalaxbb3in(A, B, C)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B + 1 >= C ] evalaxbb2in(A, B, C) -> Com_1(evalaxbb1in(A, B, C)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= B + 2 ] evalaxbb3in(A, B, C) -> Com_1(evalaxreturnin(A, B, C)) [ B - C + 1 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A + 2 >= C ] evalaxbb3in(A, B, C) -> Com_1(evalaxbbin(A + 1, B, C)) [ B - C + 1 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B + 1 >= C /\ C >= A + 3 ] evalaxbb1in(A, B, C) -> Com_1(evalaxbb2in(A, B + 1, C)) [ C - 2 >= 0 /\ B + C - 2 >= 0 /\ -B + C - 2 >= 0 /\ A + C - 2 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 ] evalaxreturnin(A, B, C) -> Com_1(evalaxstop(A, B, C)) [ B - C + 1 >= 0 /\ A - C + 2 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 ] )