(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalNestedMultipleDepstart))
(VAR A B C D E)
(RULES
  evalNestedMultipleDepstart(A, B, C, D, E) -> Com_1(evalNestedMultipleDepentryin(A, B, C, D, E))
  evalNestedMultipleDepentryin(A, B, C, D, E) -> Com_1(evalNestedMultipleDepbb3in(0, B, C, D, E))
  evalNestedMultipleDepbb3in(A, B, C, D, E) -> Com_1(evalNestedMultipleDepbbin(A, B, C, D, E)) [ A >= 0 /\ B >= A + 1 ]
  evalNestedMultipleDepbb3in(A, B, C, D, E) -> Com_1(evalNestedMultipleDepreturnin(A, B, C, D, E)) [ A >= 0 /\ A >= B ]
  evalNestedMultipleDepbbin(A, B, C, D, E) -> Com_1(evalNestedMultipleDepbb2in(A, B, A + 1, 0, E)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ]
  evalNestedMultipleDepbb2in(A, B, C, D, E) -> Com_1(evalNestedMultipleDepbb1in(A, B, C, D, E)) [ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ A - C + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ E >= D + 1 ]
  evalNestedMultipleDepbb2in(A, B, C, D, E) -> Com_1(evalNestedMultipleDepbb3in(C, B, C, D, E)) [ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ A - C + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ D >= E ]
  evalNestedMultipleDepbb1in(A, B, C, D, E) -> Com_1(evalNestedMultipleDepbb2in(A, B, C, D + 1, E)) [ E - 1 >= 0 /\ D + E - 1 >= 0 /\ -D + E - 1 >= 0 /\ C + E - 2 >= 0 /\ B + E - 2 >= 0 /\ A + E - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ A - C + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ]
  evalNestedMultipleDepreturnin(A, B, C, D, E) -> Com_1(evalNestedMultipleDepstop(A, B, C, D, E)) [ A - B >= 0 /\ A >= 0 ]
)