(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalEx4start))
(VAR A B C D)
(RULES
  evalEx4start(A, B, C, D) -> Com_1(evalEx4entryin(A, B, C, D))
  evalEx4entryin(A, B, C, D) -> Com_1(evalEx4bb4in(1, A, C, D))
  evalEx4bb4in(A, B, C, D) -> Com_1(evalEx4bb2in(A, B, 0, B)) [ A = 1 ]
  evalEx4bb4in(A, B, C, D) -> Com_1(evalEx4returnin(A, B, C, D)) [ 0 >= A ]
  evalEx4bb4in(A, B, C, D) -> Com_1(evalEx4returnin(A, B, C, D)) [ A >= 2 ]
  evalEx4bb2in(A, B, C, D) -> Com_1(evalEx4bb4in(C, D, C, D)) [ B - D >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 0 >= D ]
  evalEx4bb2in(A, B, C, D) -> Com_1(evalEx4bb3in(A, B, C, D)) [ B - D >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ D >= 1 ]
  evalEx4bb3in(A, B, C, D) -> Com_1(evalEx4bb1in(A, B, C, D)) [ B - D >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 0 >= E + 1 ]
  evalEx4bb3in(A, B, C, D) -> Com_1(evalEx4bb1in(A, B, C, D)) [ B - D >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ E >= 1 ]
  evalEx4bb3in(A, B, C, D) -> Com_1(evalEx4bb4in(C, D, C, D)) [ B - D >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 ]
  evalEx4bb1in(A, B, C, D) -> Com_1(evalEx4bb2in(A, B, 1, D - 1)) [ B - D >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 2 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ -A + C + 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 ]
  evalEx4returnin(A, B, C, D) -> Com_1(evalEx4stop(A, B, C, D))
)