(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(evalfbb5in(0, 0, 0, D, E, F, G))
  evalfbb5in(A, B, C, D, E, F, G) -> Com_1(evalfreturnin(A, B, C, D, E, F, G)) [ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= D ]
  evalfbb5in(A, B, C, D, E, F, G) -> Com_1(evalfbbin(A, B, C, D, C + 1, F, G)) [ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ D >= C + 1 ]
  evalfbbin(A, B, C, D, E, F, G) -> Com_1(evalfbb1in(A, B, C, D, E, B, G)) [ D - E >= 0 /\ C - E + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ 0 >= H + 1 ]
  evalfbbin(A, B, C, D, E, F, G) -> Com_1(evalfbb1in(A, B, C, D, E, B, G)) [ D - E >= 0 /\ C - E + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ H >= 1 ]
  evalfbbin(A, B, C, D, E, F, G) -> Com_1(evalfbb3in(A, B, C, D, E, A, G)) [ D - E >= 0 /\ C - E + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 ]
  evalfbb1in(A, B, C, D, E, F, G) -> Com_1(evalfbb5in(A, F + 1, E, D, E, F, G)) [ F >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F >= 0 /\ B + F >= 0 /\ -B + F >= 0 /\ A + F >= 0 /\ D - E >= 0 /\ C - E + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ F >= G ]
  evalfbb1in(A, B, C, D, E, F, G) -> Com_1(evalfbb1in(A, B, C, D, E, F + 1, G)) [ F >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F >= 0 /\ B + F >= 0 /\ -B + F >= 0 /\ A + F >= 0 /\ D - E >= 0 /\ C - E + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ G >= F + 1 ]
  evalfbb3in(A, B, C, D, E, F, G) -> Com_1(evalfbb5in(F + 1, B, E, D, E, F, G)) [ F >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F >= 0 /\ B + F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ C - E + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ F >= G ]
  evalfbb3in(A, B, C, D, E, F, G) -> Com_1(evalfbb3in(A, B, C, D, E, F + 1, G)) [ F >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ C + F >= 0 /\ B + F >= 0 /\ A + F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ C - E + 1 >= 0 /\ E - 1 >= 0 /\ D + E - 2 >= 0 /\ C + E - 1 >= 0 /\ -C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ G >= F + 1 ]
  evalfreturnin(A, B, C, D, E, F, G) -> Com_1(evalfstop(A, B, C, D, E, F, G)) [ C - D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 ]
)