(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalrealheapsortstep1start)) (VAR A B C) (RULES evalrealheapsortstep1start(A, B, C) -> Com_1(evalrealheapsortstep1entryin(A, B, C)) evalrealheapsortstep1entryin(A, B, C) -> Com_1(evalrealheapsortstep1returnin(A, B, C)) [ 2 >= A ] evalrealheapsortstep1entryin(A, B, C) -> Com_1(evalrealheapsortstep1bb6in(A, 1, C)) [ A >= 3 ] evalrealheapsortstep1returnin(A, B, C) -> Com_1(evalrealheapsortstep1stop(A, B, C)) evalrealheapsortstep1bb6in(A, B, C) -> Com_1(evalrealheapsortstep1bb3in(A, B, B)) [ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ A >= B + 1 ] evalrealheapsortstep1bb3in(A, B, C) -> Com_1(evalrealheapsortstep1bb4in(A, B, C)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ C >= 1 ] evalrealheapsortstep1bb3in(A, B, C) -> Com_1(evalrealheapsortstep1bb5in(A, B, C)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ 0 >= C ] evalrealheapsortstep1bb4in(A, B, C) -> Com_1(evalrealheapsortstep1bb5in(A, B, C)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ C >= 0 /\ D >= 0 /\ C + 1 >= 2*D /\ 2*D >= C ] evalrealheapsortstep1bb4in(A, B, C) -> Com_1(evalrealheapsortstep1bb2in(A, B, C)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ C >= 0 /\ D >= 0 /\ C + 1 >= 2*D /\ 2*D >= C ] evalrealheapsortstep1bb5in(A, B, C) -> Com_1(evalrealheapsortstep1bb6in(A, B + 1, C)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 ] evalrealheapsortstep1bb6in(A, B, C) -> Com_1(evalrealheapsortstep1returnin(A, B, C)) [ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ B >= A ] evalrealheapsortstep1bb2in(A, B, C) -> Com_1(evalrealheapsortstep1bb3in(A, B, D - 1)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 4 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ C >= 0 /\ E >= 0 /\ C + 1 >= 2*E /\ 2*E >= C /\ F >= 0 /\ C + 1 >= 2*F /\ 2*F >= C /\ D >= 0 /\ C + 1 >= 2*D /\ 2*D >= C ] )