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