(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalfstart)) (VAR A B C D E F G) (RULES evalfstart(A, B, C, D, E, F, G) -> Com_1(evalfentryin(A, B, C, D, E, F, G)) evalfentryin(A, B, C, D, E, F, G) -> Com_1(evalfbb10in(B, C, D, A, E, F, G)) evalfbb10in(A, B, C, D, E, F, G) -> Com_1(evalfbb8in(A, B, C, D, 1, F, G)) [ D >= 1 ] evalfbb10in(A, B, C, D, E, F, G) -> Com_1(evalfreturnin(A, B, C, D, E, F, G)) [ 0 >= D ] evalfbb8in(A, B, C, D, E, F, G) -> Com_1(evalfbb6in(A, B, C, D, E, D, G)) [ E - 1 >= 0 /\ D + E - 2 >= 0 /\ D - 1 >= 0 /\ A >= E ] evalfbb8in(A, B, C, D, E, F, G) -> Com_1(evalfbb9in(A, B, C, D, E, F, G)) [ E - 1 >= 0 /\ D + E - 2 >= 0 /\ D - 1 >= 0 /\ E >= A + 1 ] evalfbb6in(A, B, C, D, E, F, G) -> Com_1(evalfbb4in(A, B, C, D, E, F, C)) [ F - 1 >= 0 /\ E + F - 2 >= 0 /\ D + F - 2 >= 0 /\ -D + F >= 0 /\ A + F - 2 >= 0 /\ A - E >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ A + E - 2 >= 0 /\ D - 1 >= 0 /\ A + D - 2 >= 0 /\ A - 1 >= 0 /\ B >= F ] evalfbb6in(A, B, C, D, E, F, G) -> Com_1(evalfbb7in(A, B, C, D, E, F, G)) [ F - 1 >= 0 /\ E + F - 2 >= 0 /\ D + F - 2 >= 0 /\ -D + F >= 0 /\ A + F - 2 >= 0 /\ A - E >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ A + E - 2 >= 0 /\ D - 1 >= 0 /\ A + D - 2 >= 0 /\ A - 1 >= 0 /\ F >= B + 1 ] evalfbb4in(A, B, C, D, E, F, G) -> Com_1(evalfbb3in(A, B, C, D, E, F, G)) [ C - G >= 0 /\ B - F >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ D + F - 2 >= 0 /\ -D + F >= 0 /\ B + F - 2 >= 0 /\ A + F - 2 >= 0 /\ A - E >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ B + E - 2 >= 0 /\ A + E - 2 >= 0 /\ B - D >= 0 /\ D - 1 >= 0 /\ B + D - 2 >= 0 /\ A + D - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ E >= G ] evalfbb4in(A, B, C, D, E, F, G) -> Com_1(evalfbb5in(A, B, C, D, E, F, G)) [ C - G >= 0 /\ B - F >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ D + F - 2 >= 0 /\ -D + F >= 0 /\ B + F - 2 >= 0 /\ A + F - 2 >= 0 /\ A - E >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ B + E - 2 >= 0 /\ A + E - 2 >= 0 /\ B - D >= 0 /\ D - 1 >= 0 /\ B + D - 2 >= 0 /\ A + D - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ G >= E + 1 ] evalfbb3in(A, B, C, D, E, F, G) -> Com_1(evalfbb4in(A, B, C, D, E, F, G - 1)) [ E - G >= 0 /\ C - G >= 0 /\ A - G >= 0 /\ B - F >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ D + F - 2 >= 0 /\ -D + F >= 0 /\ B + F - 2 >= 0 /\ A + F - 2 >= 0 /\ A - E >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ B + E - 2 >= 0 /\ A + E - 2 >= 0 /\ B - D >= 0 /\ D - 1 >= 0 /\ B + D - 2 >= 0 /\ A + D - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 ] evalfbb5in(A, B, C, D, E, F, G) -> Com_1(evalfbb6in(A, B, C, D, E, F + 1, G)) [ C - G >= 0 /\ G - 2 >= 0 /\ F + G - 3 >= 0 /\ E + G - 3 >= 0 /\ -E + G - 1 >= 0 /\ D + G - 3 >= 0 /\ C + G - 4 >= 0 /\ B + G - 3 >= 0 /\ A + G - 3 >= 0 /\ B - F >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ D + F - 2 >= 0 /\ -D + F >= 0 /\ C + F - 3 >= 0 /\ B + F - 2 >= 0 /\ A + F - 2 >= 0 /\ C - E - 1 >= 0 /\ A - E >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 3 >= 0 /\ B + E - 2 >= 0 /\ A + E - 2 >= 0 /\ B - D >= 0 /\ D - 1 >= 0 /\ C + D - 3 >= 0 /\ B + D - 2 >= 0 /\ A + D - 2 >= 0 /\ C - 2 >= 0 /\ B + C - 3 >= 0 /\ A + C - 3 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 ] evalfbb7in(A, B, C, D, E, F, G) -> Com_1(evalfbb8in(A, B, C, D, E + 1, F, G)) [ F - 1 >= 0 /\ E + F - 2 >= 0 /\ D + F - 2 >= 0 /\ -D + F >= 0 /\ -B + F - 1 >= 0 /\ A + F - 2 >= 0 /\ A - E >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ A + E - 2 >= 0 /\ D - 1 >= 0 /\ A + D - 2 >= 0 /\ A - 1 >= 0 ] evalfbb9in(A, B, C, D, E, F, G) -> Com_1(evalfbb10in(A, B, C, D - 1, E, F, G)) [ E - 1 >= 0 /\ D + E - 2 >= 0 /\ -A + E - 1 >= 0 /\ D - 1 >= 0 ] evalfreturnin(A, B, C, D, E, F, G) -> Com_1(evalfstop(A, B, C, D, E, F, G)) [ -D >= 0 ] )