(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalEx5start)) (VAR A B C D E) (RULES evalEx5start(A, B, C, D, E) -> Com_1(evalEx5entryin(A, B, C, D, E)) evalEx5entryin(A, B, C, D, E) -> Com_1(evalEx5bb6in(0, A, C, D, E)) evalEx5bb6in(A, B, C, D, E) -> Com_1(evalEx5bb3in(A, B, 0, B, E)) [ A >= 0 /\ B >= A + 1 ] evalEx5bb6in(A, B, C, D, E) -> Com_1(evalEx5returnin(A, B, C, D, E)) [ A >= 0 /\ A >= B ] evalEx5bb3in(A, B, C, D, E) -> Com_1(evalEx5bb1in(A, B, C, D, E)) [ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ 0 >= F + 1 ] evalEx5bb3in(A, B, C, D, E) -> Com_1(evalEx5bb1in(A, B, C, D, E)) [ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ F >= 1 ] evalEx5bb3in(A, B, C, D, E) -> Com_1(evalEx5bb4in(A, B, C, D, E)) [ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ] evalEx5bb1in(A, B, C, D, E) -> Com_1(evalEx5bb2in(A, B, C, D, D - 1)) [ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ 0 >= F + 1 ] evalEx5bb1in(A, B, C, D, E) -> Com_1(evalEx5bb2in(A, B, C, D, D - 1)) [ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ F >= 1 ] evalEx5bb1in(A, B, C, D, E) -> Com_1(evalEx5bb3in(A, B, C, D, E)) [ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ] evalEx5bb2in(A, B, C, D, E) -> Com_1(evalEx5bb3in(A, B, 1, E, E)) [ D - E - 1 >= 0 /\ B - E - 1 >= 0 /\ -D + E + 1 >= 0 /\ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ] evalEx5bb4in(A, B, C, D, E) -> Com_1(evalEx5bb6in(A + 1, D, C, D, E)) [ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ C = 0 ] evalEx5bb4in(A, B, C, D, E) -> Com_1(evalEx5bb6in(A, D, C, D, E)) [ B - D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ C >= 1 ] evalEx5returnin(A, B, C, D, E) -> Com_1(evalEx5stop(A, B, C, D, E)) [ A - B >= 0 /\ A >= 0 ] )