(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalfstart)) (VAR A B C D E) (RULES evalfstart(A, B, C, D, E) -> Com_1(evalfentryin(A, B, C, D, E)) evalfentryin(A, B, C, D, E) -> Com_1(evalfbb7in(B, B, 0, D, E)) evalfbb7in(A, B, C, D, E) -> Com_1(evalfbbin(A, B, C, D, E)) [ C + 1 >= 0 /\ -A + B >= 0 /\ A >= 0 /\ C >= 0 ] evalfbb7in(A, B, C, D, E) -> Com_1(evalfreturnin(A, B, C, D, E)) [ C + 1 >= 0 /\ -A + B >= 0 /\ 0 >= A + 1 ] evalfbb7in(A, B, C, D, E) -> Com_1(evalfreturnin(A, B, C, D, E)) [ C + 1 >= 0 /\ -A + B >= 0 /\ 0 >= C + 1 ] evalfbbin(A, B, C, D, E) -> Com_1(evalfbb3in(A, B, C, C, E)) [ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ 0 >= F + 1 ] evalfbbin(A, B, C, D, E) -> Com_1(evalfbb3in(A, B, C, C, E)) [ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ F >= 1 ] evalfbbin(A, B, C, D, E) -> Com_1(evalfbb6in(A, B, C, A, C)) [ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 ] evalfbb3in(A, B, C, D, E) -> Com_1(evalfbb5in(A, B, C, D, E)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ D >= B + 1 ] evalfbb3in(A, B, C, D, E) -> Com_1(evalfbb4in(A, B, C, D, E)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ B >= D ] evalfbb4in(A, B, C, D, E) -> Com_1(evalfbb2in(A, B, C, D, E)) [ B - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ 0 >= F + 1 ] evalfbb4in(A, B, C, D, E) -> Com_1(evalfbb2in(A, B, C, D, E)) [ B - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ F >= 1 ] evalfbb4in(A, B, C, D, E) -> Com_1(evalfbb5in(A, B, C, D, E)) [ B - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 ] evalfbb2in(A, B, C, D, E) -> Com_1(evalfbb3in(A, B, C, D + 1, E)) [ B - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 ] evalfbb5in(A, B, C, D, E) -> Com_1(evalfbb6in(A, B, C, A - 1, D)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 ] evalfbb6in(A, B, C, D, E) -> Com_1(evalfbb7in(D, B, E - 1, D, E)) [ E >= 0 /\ D + E + 1 >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E >= 0 /\ A + E >= 0 /\ B - D >= 0 /\ A - D >= 0 /\ D + 1 >= 0 /\ C + D + 1 >= 0 /\ B + D + 1 >= 0 /\ A + D + 1 >= 0 /\ -A + D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 ] evalfreturnin(A, B, C, D, E) -> Com_1(evalfstop(A, B, C, D, E)) [ C + 1 >= 0 /\ -A + B >= 0 ] )