(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalrealheapsortstep1start)) (VAR A B C D E F) (RULES evalrealheapsortstep1start(A,B,C) -> Com_1(evalrealheapsortstep1entryin(A,B,C)) evalrealheapsortstep1entryin(A,B,C) -> Com_1(evalrealheapsortstep1bb6in(A,1,C)) :|: A >= 3 evalrealheapsortstep1entryin(A,B,C) -> Com_1(evalrealheapsortstep1returnin(A,B,C)) :|: 2 >= A evalrealheapsortstep1bb6in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,B)) :|: A >= 1 + B evalrealheapsortstep1bb6in(A,B,C) -> Com_1(evalrealheapsortstep1returnin(A,B,C)) :|: B >= A evalrealheapsortstep1bb3in(A,B,C) -> Com_1(evalrealheapsortstep1bb5in(A,B,C)) :|: 0 >= C evalrealheapsortstep1bb3in(A,B,C) -> Com_1(evalrealheapsortstep1bb4in(A,B,C)) :|: C >= 1 evalrealheapsortstep1bb4in(A,B,C) -> Com_1(evalrealheapsortstep1bb2in(A,B,C)) :|: C + 1 = 0 evalrealheapsortstep1bb4in(A,B,C) -> Com_1(evalrealheapsortstep1bb2in(A,B,C)) :|: C >= 0 && D >= 0 && C + 1 >= 2*D && 2*D >= C evalrealheapsortstep1bb4in(A,B,C) -> Com_1(evalrealheapsortstep1bb2in(A,B,C)) :|: 0 >= C + 2 && 0 >= D && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb4in(A,B,C) -> Com_1(evalrealheapsortstep1bb5in(A,B,C)) :|: C + 1 = 0 evalrealheapsortstep1bb4in(A,B,C) -> Com_1(evalrealheapsortstep1bb5in(A,B,C)) :|: C >= 0 && D >= 0 && C + 1 >= 2*D && 2*D >= C evalrealheapsortstep1bb4in(A,B,C) -> Com_1(evalrealheapsortstep1bb5in(A,B,C)) :|: 0 >= C + 2 && 0 >= D && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: C + 1 = 0 evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && C + 1 = 0 evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && 0 >= D && C + 1 = 0 && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: 0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && C + 1 = 0 evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && C + 1 = 0 evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && 0 >= D && C + 1 = 0 && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: 0 >= 1 && 0 >= D && C + 1 = 0 && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && 0 >= E && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && C + 1 = 0 && 2*E >= C + 1 && 2 + C >= 2*E evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && 0 >= E && 0 >= D && C + 1 = 0 && 2*E >= C + 1 && 2 + C >= 2*E && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: 0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && C + 1 = 0 evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && C + 1 = 0 evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && 0 >= D && C + 1 = 0 && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: 0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && C + 1 = 0 evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 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 evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: C >= 0 && E >= 0 && C + 1 >= 2*E && 2*E >= C && F >= 0 && C + 1 >= 2*F && 2*F >= C && 0 >= C + 2 && 0 >= D && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: 0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 0 >= E && C + 1 = 0 && 2*E >= C + 1 && 2 + C >= 2*E evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: C >= 0 && E >= 0 && C + 1 >= 2*E && 2*E >= C && 0 >= C + 2 && 0 >= F && D >= 0 && C + 1 >= 2*D && 2*D >= C && 2*F >= C + 1 && 2 + C >= 2*F evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: C >= 0 && E >= 0 && C + 1 >= 2*E && 2*E >= C && 0 >= C + 2 && 0 >= F && 0 >= D && 2*F >= C + 1 && 2 + C >= 2*F && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: 0 >= 1 && 0 >= D && C + 1 = 0 && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && 0 >= E && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && C + 1 = 0 && 2*E >= C + 1 && 2 + C >= 2*E evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= 1 && 0 >= E && 0 >= D && C + 1 = 0 && 2*E >= C + 1 && 2 + C >= 2*E && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: 0 >= 1 && 0 >= D && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && C + 1 = 0 && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= C + 2 && 0 >= E && C >= 0 && F >= 0 && C + 1 >= 2*F && 2*F >= C && D >= 0 && C + 1 >= 2*D && 2*D >= C && 2*E >= C + 1 && 2 + C >= 2*E evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= C + 2 && 0 >= E && C >= 0 && F >= 0 && C + 1 >= 2*F && 2*F >= C && 0 >= D && 2*E >= C + 1 && 2 + C >= 2*E && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,-1)) :|: 0 >= 1 && 0 >= D && 0 >= E && C + 1 = 0 && 2*D >= C + 1 && 2 + C >= 2*D && 2*E >= C + 1 && 2 + C >= 2*E evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= C + 2 && 0 >= E && 0 >= F && C >= 0 && D >= 0 && C + 1 >= 2*D && 2*D >= C && 2*E >= C + 1 && 2 + C >= 2*E && 2*F >= C + 1 && 2 + C >= 2*F evalrealheapsortstep1bb2in(A,B,C) -> Com_1(evalrealheapsortstep1bb3in(A,B,D - 1)) :|: 0 >= C + 2 && 0 >= E && 0 >= F && 0 >= D && 2*E >= C + 1 && 2 + C >= 2*E && 2*F >= C + 1 && 2 + C >= 2*F && 2*D >= C + 1 && 2 + C >= 2*D evalrealheapsortstep1bb5in(A,B,C) -> Com_1(evalrealheapsortstep1bb6in(A,B + 1,C)) evalrealheapsortstep1returnin(A,B,C) -> Com_1(evalrealheapsortstep1stop(A,B,C)) )