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