(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalfstart)) (VAR A B C D E) (RULES evalfstart(A,B,C,D) -> Com_1(evalfentryin(A,B,C,D)) evalfentryin(A,B,C,D) -> Com_1(evalfbb5in(B,B,C,D)) evalfbb5in(A,B,C,D) -> Com_1(evalfbbin(A,B,C,D)) :|: B >= 2 evalfbb5in(A,B,C,D) -> Com_1(evalfreturnin(A,B,C,D)) :|: 1 >= B evalfbbin(A,B,C,D) -> Com_1(evalfbb2in(A,B,B - 1,A + B - 1)) evalfbb2in(A,B,C,D) -> Com_1(evalfbb4in(A,B,C,D)) :|: C >= D + 1 evalfbb2in(A,B,C,D) -> Com_1(evalfbb3in(A,B,C,D)) :|: D >= C evalfbb3in(A,B,C,D) -> Com_1(evalfbb1in(A,B,C,D)) :|: 0 >= E + 1 evalfbb3in(A,B,C,D) -> Com_1(evalfbb1in(A,B,C,D)) :|: E >= 1 evalfbb3in(A,B,C,D) -> Com_1(evalfbb4in(A,B,C,D)) evalfbb1in(A,B,C,D) -> Com_1(evalfbb2in(A,B,C,D - 1)) evalfbb4in(A,B,C,D) -> Com_1(evalfbb5in(D - C + 1,C - 1,C,D)) evalfreturnin(A,B,C,D) -> Com_1(evalfstop(A,B,C,D)) )