(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalinsertsortstart))
(VAR A B C D)
(RULES
  evalinsertsortstart(A, B, C, D) -> Com_1(evalinsertsortentryin(A, B, C, D))
  evalinsertsortentryin(A, B, C, D) -> Com_1(evalinsertsortbb5in(1, B, C, D))
  evalinsertsortbb5in(A, B, C, D) -> Com_1(evalinsertsortbbin(A, B, C, D)) [ A - 1 >= 0 /\ B >= A + 1 ]
  evalinsertsortbb5in(A, B, C, D) -> Com_1(evalinsertsortreturnin(A, B, C, D)) [ A - 1 >= 0 /\ A >= B ]
  evalinsertsortbbin(A, B, C, D) -> Com_1(evalinsertsortbb2in(A, B, E, A - 1)) [ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 ]
  evalinsertsortbb2in(A, B, C, D) -> Com_1(evalinsertsortbb4in(A, B, C, D)) [ B - D - 2 >= 0 /\ A - D - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 /\ 0 >= D + 1 ]
  evalinsertsortbb2in(A, B, C, D) -> Com_1(evalinsertsortbb3in(A, B, C, D)) [ B - D - 2 >= 0 /\ A - D - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 /\ D >= 0 ]
  evalinsertsortbb3in(A, B, C, D) -> Com_1(evalinsertsortbb1in(A, B, C, D)) [ B - D - 2 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ B + D - 2 >= 0 /\ A + D - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 /\ E >= C + 1 ]
  evalinsertsortbb3in(A, B, C, D) -> Com_1(evalinsertsortbb4in(A, B, C, D)) [ B - D - 2 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ B + D - 2 >= 0 /\ A + D - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 /\ C >= E ]
  evalinsertsortbb1in(A, B, C, D) -> Com_1(evalinsertsortbb2in(A, B, C, D - 1)) [ B - D - 2 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ B + D - 2 >= 0 /\ A + D - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 ]
  evalinsertsortbb4in(A, B, C, D) -> Com_1(evalinsertsortbb5in(A + 1, B, C, D)) [ B - D - 2 >= 0 /\ A - D - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 ]
  evalinsertsortreturnin(A, B, C, D) -> Com_1(evalinsertsortstop(A, B, C, D)) [ A - B >= 0 /\ A - 1 >= 0 ]
)