(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalrealheapsortstep2start))
(VAR A B C D)
(RULES
  evalrealheapsortstep2start(A, B, C, D) -> Com_1(evalrealheapsortstep2entryin(A, B, C, D))
  evalrealheapsortstep2entryin(A, B, C, D) -> Com_1(evalrealheapsortstep2returnin(A, B, C, D)) [ 2 >= A ]
  evalrealheapsortstep2entryin(A, B, C, D) -> Com_1(evalrealheapsortstep2bbin(A, B, C, D)) [ A >= 3 ]
  evalrealheapsortstep2returnin(A, B, C, D) -> Com_1(evalrealheapsortstep2stop(A, B, C, D))
  evalrealheapsortstep2bbin(A, B, C, D) -> Com_1(evalrealheapsortstep2bb11in(A, 0, C, D)) [ A - 3 >= 0 ]
  evalrealheapsortstep2bb11in(A, B, C, D) -> Com_1(evalrealheapsortstep2returnin(A, B, C, D)) [ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 /\ B + 1 >= A ]
  evalrealheapsortstep2bb11in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb1in(A, B, C, D)) [ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 /\ A >= B + 2 ]
  evalrealheapsortstep2bb1in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb9in(A, B, 0, D)) [ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 ]
  evalrealheapsortstep2bb9in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb10in(A, B, C, D)) [ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 /\ 2*C + B + 2 >= A ]
  evalrealheapsortstep2bb9in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb2in(A, B, C, D)) [ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 /\ A >= B + 2*C + 3 ]
  evalrealheapsortstep2bb10in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb11in(A, B + 1, C, D)) [ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 ]
  evalrealheapsortstep2bb2in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb3in(A, B, C, D)) [ A - C - 3 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 /\ A >= B + 2*C + 4 ]
  evalrealheapsortstep2bb2in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb4in(A, B, C, D)) [ A - C - 3 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 /\ A = 2*C + B + 3 ]
  evalrealheapsortstep2bb3in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb5in(A, B, C, D)) [ A - C - 4 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 4 >= 0 /\ A - B - 4 >= 0 /\ B >= 0 /\ A + B - 4 >= 0 /\ A - 4 >= 0 ]
  evalrealheapsortstep2bb3in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb4in(A, B, C, D)) [ A - C - 4 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 4 >= 0 /\ A - B - 4 >= 0 /\ B >= 0 /\ A + B - 4 >= 0 /\ A - 4 >= 0 ]
  evalrealheapsortstep2bb4in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb6in(A, B, C, 2*C + 1)) [ A - C - 3 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 ]
  evalrealheapsortstep2bb6in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb9in(A, B, A, D)) [ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 4 >= 0 /\ A - C - 3 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 ]
  evalrealheapsortstep2bb6in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb7in(A, B, C, D)) [ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 4 >= 0 /\ A - C - 3 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 ]
  evalrealheapsortstep2bb5in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb6in(A, B, C, 2*C + 2)) [ A - C - 4 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 4 >= 0 /\ A - B - 4 >= 0 /\ B >= 0 /\ A + B - 4 >= 0 /\ A - 4 >= 0 ]
  evalrealheapsortstep2bb7in(A, B, C, D) -> Com_1(evalrealheapsortstep2bb9in(A, B, D, D)) [ D - 1 >= 0 /\ C + D - 1 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 4 >= 0 /\ A - C - 3 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 3 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 3 >= 0 ]
)