Inferring Expected Runtimes Using Sizes

KoAT2 Proof WORST_CASE( ?, (1+Arg_0)*max([18, 6*Arg_0])+(2*(1+max([1+4*Arg_0, 13]))+Arg_0)*max([2*Arg_0, 6])+(3+max([1+4*Arg_0, 13]))*max([2*Arg_0, 6])+2*(1+Arg_0)+2*(1+Arg_0)*(1+Arg_0)+2*(1+Arg_0)*Arg_0+2*(1+Arg_0)*max([12, 4*Arg_0])+2*(2+2*(1+max([1+4*Arg_0, 13])))*max([2*Arg_0, 6])+2*Arg_0+24+3*max([3*Arg_0, 9])+6*(1+Arg_0)*(1+max([2*Arg_0, 6]))+max([1+4*Arg_0, 13])+max([2*Arg_0, 6]) {O(n^2)})

Initial Complexity Problem (after preprocessing)

Start:evalrealheapsortstart
Program_Vars:Arg_0, Arg_1, Arg_2, Arg_3
Temp_Vars:E, F, G
Locations:evalrealheapsortbb10in, evalrealheapsortbb11in, evalrealheapsortbb12in, evalrealheapsortbb13in, evalrealheapsortbb14in, evalrealheapsortbb16in, evalrealheapsortbb17in, evalrealheapsortbb18in, evalrealheapsortbb2in, evalrealheapsortbb3in, evalrealheapsortbb4in, evalrealheapsortbb5in, evalrealheapsortbb6in, evalrealheapsortbb7in, evalrealheapsortbb8in, evalrealheapsortbb9in, evalrealheapsortentryin, evalrealheapsortreturnin, evalrealheapsortstart, evalrealheapsortstop
Transitions:
evalrealheapsortstart(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortentryin(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_3<=0 && 0<=Arg_3
evalrealheapsortbb6in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb3in(Arg_0,Arg_1,Arg_1,Arg_3) :|: 1+Arg_1<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb6in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb7in(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_0<=Arg_1 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb3in(Arg_0,Arg_1,Arg_2,Arg_3) -> 1/2:evalrealheapsortbb5in(Arg_0,Arg_1,Arg_2,Arg_3) :+: 1/2:evalrealheapsortbb2in(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_2<=0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb3in(Arg_0,Arg_1,Arg_2,Arg_3) -> 1/2:evalrealheapsortbb3in(Arg_0,Arg_1,Arg_2,Arg_3) :+: 1/2:evalrealheapsortbb4in(Arg_0,Arg_1,Arg_2,Arg_3) :|: 1<=Arg_2 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb4in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb2in(Arg_0,Arg_1,Arg_2,Arg_3) :|: 0<=Arg_2 && 0<=E && 2*E<=Arg_2+1 && Arg_2<=2*E && Arg_3<=0 && 1+Arg_3<=Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 1<=Arg_2 && 2<=Arg_1+Arg_2 && 4<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 1<=Arg_2 && 2<=Arg_1+Arg_2 && 4<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 1<=Arg_2 && 2<=Arg_1+Arg_2 && 4<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb4in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb5in(Arg_0,Arg_1,Arg_2,Arg_3) :|: 0<=Arg_2 && 0<=E && 2*E<=Arg_2+1 && Arg_2<=2*E && Arg_3<=0 && 1+Arg_3<=Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 1<=Arg_2 && 2<=Arg_1+Arg_2 && 4<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 1<=Arg_2 && 2<=Arg_1+Arg_2 && 4<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 1<=Arg_2 && 2<=Arg_1+Arg_2 && 4<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb2in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb3in(Arg_0,Arg_1,-1,Arg_3) :|: Arg_2+1<=0 && 0<=1+Arg_2 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb2in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb3in(Arg_0,Arg_1,E-1,Arg_3) :|: 0<=Arg_2 && 0<=F && 2*F<=Arg_2+1 && Arg_2<=2*F && 0<=G && 2*G<=Arg_2+1 && Arg_2<=2*G && 0<=E && 2*E<=Arg_2+1 && Arg_2<=2*E && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb5in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb6in(Arg_0,Arg_1+1,Arg_2,Arg_3) :|: Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && Arg_3<=1+Arg_2 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 0<=1+Arg_2+Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_2<=Arg_1 && 1+Arg_2<=Arg_0 && 0<=1+Arg_2 && 0<=Arg_1+Arg_2 && 2<=Arg_0+Arg_2 && 1+Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb18in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb8in(Arg_0,Arg_1,Arg_2,Arg_3) :|: 2+Arg_1<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb18in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortreturnin(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_0<=Arg_1+1 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb16in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb9in(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_1+3+2*Arg_2<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb16in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb17in(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_0<=2*Arg_2+2+Arg_1 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb11in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb13in(Arg_0,Arg_1,Arg_2,2*Arg_2+1) :|: 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb12in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb13in(Arg_0,Arg_1,Arg_2,2*Arg_2+2) :|: 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 4+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 4<=Arg_0+Arg_2 && 4+Arg_1<=Arg_0 && 0<=Arg_1 && 4<=Arg_0+Arg_1 && 4<=Arg_0
evalrealheapsortbb13in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb14in(Arg_0,Arg_1,Arg_2,Arg_3) :|: 1<=Arg_3 && 1<=Arg_2+Arg_3 && 1+Arg_2<=Arg_3 && 1<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 1<=Arg_3 && 1<=Arg_2+Arg_3 && 1+Arg_2<=Arg_3 && 1<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 1<=Arg_3 && 1<=Arg_2+Arg_3 && 1+Arg_2<=Arg_3 && 1<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb13in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb16in(Arg_0,Arg_1,Arg_0,Arg_3) :|: 1<=Arg_3 && 1<=Arg_2+Arg_3 && 1+Arg_2<=Arg_3 && 1<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 1<=Arg_3 && 1<=Arg_2+Arg_3 && 1+Arg_2<=Arg_3 && 1<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 1<=Arg_3 && 1<=Arg_2+Arg_3 && 1+Arg_2<=Arg_3 && 1<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb14in(Arg_0,Arg_1,Arg_2,Arg_3) -> evalrealheapsortbb16in(Arg_0,Arg_1,Arg_3,Arg_3) :|: 1<=Arg_3 && 1<=Arg_2+Arg_3 && 1+Arg_2<=Arg_3 && 1<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 1<=Arg_3 && 1<=Arg_2+Arg_3 && 1+Arg_2<=Arg_3 && 1<=Arg_1+Arg_3 && 4<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 0<=Arg_1
evalrealheapsortbb16in(Arg_0,Arg_1,Arg_2,Arg_3) -{2}> evalrealheapsortbb18in(Arg_0,Arg_1+1,Arg_2,Arg_3) :|: Arg_0<=2*Arg_2+2+Arg_1 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb6in(Arg_0,Arg_1,Arg_2,Arg_3) -{2}> evalrealheapsortbb18in(Arg_0,0,Arg_2,Arg_3) :|: Arg_0<=Arg_1 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 3+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 3<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 3<=Arg_1 && 6<=Arg_0+Arg_1 && Arg_0<=Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_3<=0 && 1+Arg_3<=Arg_1 && 3+Arg_3<=Arg_0 && 0<=Arg_3 && 1<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && Arg_1<=Arg_0 && 1<=Arg_1 && 4<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb18in(Arg_0,Arg_1,Arg_2,Arg_3) -{2}> evalrealheapsortbb16in(Arg_0,Arg_1,0,Arg_3) :|: 2+Arg_1<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb16in(Arg_0,Arg_1,Arg_2,Arg_3) -{2}> evalrealheapsortbb11in(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_1+3+2*Arg_2<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_0<=2*Arg_2+3+Arg_1 && 2*Arg_2+3+Arg_1<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb16in(Arg_0,Arg_1,Arg_2,Arg_3) -{2}> evalrealheapsortbb10in(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_1+3+2*Arg_2<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_1+4+2*Arg_2<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortstart(Arg_0,Arg_1,Arg_2,Arg_3) -{2}> evalrealheapsortbb6in(Arg_0,1,Arg_2,Arg_3) :|: Arg_3<=0 && 0<=Arg_3 && 3<=Arg_0 && Arg_3<=0 && 0<=Arg_3
evalrealheapsortstart(Arg_0,Arg_1,Arg_2,Arg_3) -{2}> evalrealheapsortreturnin(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_3<=0 && 0<=Arg_3 && Arg_0<=2 && Arg_3<=0 && 0<=Arg_3
evalrealheapsortbb18in(Arg_0,Arg_1,Arg_2,Arg_3) -{2}> evalrealheapsortstop(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_0<=Arg_1+1 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 1+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortstart(Arg_0,Arg_1,Arg_2,Arg_3) -{3}> evalrealheapsortstop(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_3<=0 && 0<=Arg_3 && Arg_0<=2 && Arg_3<=0 && 0<=Arg_3 && 0<=Arg_3
evalrealheapsortbb16in(Arg_0,Arg_1,Arg_2,Arg_3) -{3}> evalrealheapsortbb11in(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_1+3+2*Arg_2<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_1+4+2*Arg_2<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0
evalrealheapsortbb16in(Arg_0,Arg_1,Arg_2,Arg_3) -{3}> evalrealheapsortbb12in(Arg_0,Arg_1,Arg_2,Arg_3) :|: Arg_1+3+2*Arg_2<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && Arg_1+4+2*Arg_2<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 3+Arg_2<=Arg_0 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 3+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0 && 0<=Arg_3 && 0<=Arg_2+Arg_3 && 0<=Arg_1+Arg_3 && 3<=Arg_0+Arg_3 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && 3<=Arg_0+Arg_2 && 2+Arg_1<=Arg_0 && 0<=Arg_1 && 3<=Arg_0+Arg_1 && 3<=Arg_0

G evalrealheapsortbb10in evalrealheapsortbb10in evalrealheapsortbb11in evalrealheapsortbb11in evalrealheapsortbb13in evalrealheapsortbb13in evalrealheapsortbb11in->evalrealheapsortbb13in t₅₄ ∈ g₅₂ η (Arg_3) = 2*Arg_2+1 evalrealheapsortbb12in evalrealheapsortbb12in evalrealheapsortbb12in->evalrealheapsortbb13in t₅₅ ∈ g₅₃ η (Arg_3) = 2*Arg_2+2 evalrealheapsortbb14in evalrealheapsortbb14in evalrealheapsortbb13in->evalrealheapsortbb14in t₅₆ ∈ g₅₄ evalrealheapsortbb16in evalrealheapsortbb16in evalrealheapsortbb13in->evalrealheapsortbb16in t₅₇ ∈ g₅₅ η (Arg_2) = Arg_0 evalrealheapsortbb14in->evalrealheapsortbb16in t₅₈ ∈ g₅₆ η (Arg_2) = Arg_3 evalrealheapsortbb16in->evalrealheapsortbb10in t₆₅ ∈ g₆₃ τ = Arg_1+3+2*Arg_2<=Arg_0 && Arg_1+4+2*Arg_2<=Arg_0 {2} evalrealheapsortbb16in->evalrealheapsortbb11in t₆₄ ∈ g₆₂ τ = Arg_1+3+2*Arg_2<=Arg_0 && Arg_0<=2*Arg_2+3+Arg_1 && 2*Arg_2+3+Arg_1<=Arg_0 {2} evalrealheapsortbb16in->evalrealheapsortbb11in t₇₁ ∈ g₆₉ τ = Arg_1+3+2*Arg_2<=Arg_0 && Arg_1+4+2*Arg_2<=Arg_0 {3} evalrealheapsortbb16in->evalrealheapsortbb12in t₇₂ ∈ g₇₀ τ = Arg_1+3+2*Arg_2<=Arg_0 && Arg_1+4+2*Arg_2<=Arg_0 {3} evalrealheapsortbb17in evalrealheapsortbb17in evalrealheapsortbb16in->evalrealheapsortbb17in t₄₈ ∈ g₄₆ τ = Arg_0<=2*Arg_2+2+Arg_1 evalrealheapsortbb18in evalrealheapsortbb18in evalrealheapsortbb16in->evalrealheapsortbb18in t₆₁ ∈ g₅₉ η (Arg_1) = Arg_1+1 τ = Arg_0<=2*Arg_2+2+Arg_1 {2} evalrealheapsortbb9in evalrealheapsortbb9in evalrealheapsortbb16in->evalrealheapsortbb9in t₄₇ ∈ g₄₅ τ = Arg_1+3+2*Arg_2<=Arg_0 evalrealheapsortbb18in->evalrealheapsortbb16in t₆₃ ∈ g₆₁ η (Arg_2) = 0 τ = 2+Arg_1<=Arg_0 {2} evalrealheapsortbb8in evalrealheapsortbb8in evalrealheapsortbb18in->evalrealheapsortbb8in t₄₄ ∈ g₄₂ τ = 2+Arg_1<=Arg_0 evalrealheapsortreturnin evalrealheapsortreturnin evalrealheapsortbb18in->evalrealheapsortreturnin t₄₅ ∈ g₄₃ τ = Arg_0<=Arg_1+1 evalrealheapsortstop evalrealheapsortstop evalrealheapsortbb18in->evalrealheapsortstop t₆₉ ∈ g₆₇ τ = Arg_0<=Arg_1+1 {2} evalrealheapsortbb2in evalrealheapsortbb2in evalrealheapsortbb3in evalrealheapsortbb3in evalrealheapsortbb2in->evalrealheapsortbb3in t₁₅ ∈ g₁₃ η (Arg_2) = -1 τ = Arg_2+1<=0 && 0<=1+Arg_2 evalrealheapsortbb2in->evalrealheapsortbb3in t₂₈ ∈ g₂₆ η (Arg_2) = E-1 τ = 0<=Arg_2 && 0<=F && 2*F<=Arg_2+1 && Arg_2<=2*F && 0<=G && 2*G<=Arg_2+1 && Arg_2<=2*G && 0<=E && 2*E<=Arg_2+1 && Arg_2<=2*E evalrealheapsortbb3in->evalrealheapsortbb2in t₆ ∈ g₅ p = 1/2 τ = Arg_2<=0 evalrealheapsortbb3in->evalrealheapsortbb3in t₇ ∈ g₆ p = 1/2 τ = 1<=Arg_2 evalrealheapsortbb4in evalrealheapsortbb4in evalrealheapsortbb3in->evalrealheapsortbb4in t₈ ∈ g₆ p = 1/2 τ = 1<=Arg_2 evalrealheapsortbb5in evalrealheapsortbb5in evalrealheapsortbb3in->evalrealheapsortbb5in t₅ ∈ g₅ p = 1/2 τ = Arg_2<=0 evalrealheapsortbb4in->evalrealheapsortbb2in t₁₀ ∈ g₈ τ = 0<=Arg_2 && 0<=E && 2*E<=Arg_2+1 && Arg_2<=2*E evalrealheapsortbb4in->evalrealheapsortbb5in t₁₃ ∈ g₁₁ τ = 0<=Arg_2 && 0<=E && 2*E<=Arg_2+1 && Arg_2<=2*E evalrealheapsortbb6in evalrealheapsortbb6in evalrealheapsortbb5in->evalrealheapsortbb6in t₄₂ ∈ g₄₀ η (Arg_1) = Arg_1+1 evalrealheapsortbb6in->evalrealheapsortbb18in t₆₂ ∈ g₆₀ η (Arg_1) = 0 τ = Arg_0<=Arg_1 {2} evalrealheapsortbb6in->evalrealheapsortbb3in t₃ ∈ g₃ η (Arg_2) = Arg_1 τ = 1+Arg_1<=Arg_0 evalrealheapsortbb7in evalrealheapsortbb7in evalrealheapsortbb6in->evalrealheapsortbb7in t₄ ∈ g₄ τ = Arg_0<=Arg_1 evalrealheapsortentryin evalrealheapsortentryin evalrealheapsortstart evalrealheapsortstart evalrealheapsortstart->evalrealheapsortbb6in t₆₇ ∈ g₆₅ η (Arg_1) = 1 τ = Arg_3<=0 && 0<=Arg_3 && 3<=Arg_0 {2} evalrealheapsortstart->evalrealheapsortentryin t₀ ∈ g₀ τ = Arg_3<=0 && 0<=Arg_3 evalrealheapsortstart->evalrealheapsortreturnin t₆₈ ∈ g₆₆ τ = Arg_3<=0 && 0<=Arg_3 && Arg_0<=2 {2} evalrealheapsortstart->evalrealheapsortstop t₇₀ ∈ g₆₈ τ = Arg_3<=0 && 0<=Arg_3 && Arg_0<=2 {3}

Timebounds:

Overall timebound:inf {Infinity}
54,52: evalrealheapsortbb11in->evalrealheapsortbb13in: max([0, 1+Arg_0])*max([0, Arg_0]) {O(n^2)}
55,53: evalrealheapsortbb12in->evalrealheapsortbb13in: max([0, 1+Arg_0])*max([0, Arg_0]) {O(n^2)}
56,54: evalrealheapsortbb13in->evalrealheapsortbb14in: max([0, 1+Arg_0])*max([12, 4*Arg_0]) {O(n^2)}
57,55: evalrealheapsortbb13in->evalrealheapsortbb16in: max([0, 1+Arg_0])*max([18, 6*Arg_0]) {O(n^2)}
58,56: evalrealheapsortbb14in->evalrealheapsortbb16in: max([0, 1+Arg_0])*max([12, 4*Arg_0]) {O(n^2)}
47,45: evalrealheapsortbb16in->evalrealheapsortbb9in: 1 {O(1)}
48,46: evalrealheapsortbb16in->evalrealheapsortbb17in: 1 {O(1)}
61,59: evalrealheapsortbb16in->evalrealheapsortbb18in: max([3*Arg_0, 9]) {O(n)}
64,62: evalrealheapsortbb16in->evalrealheapsortbb11in: max([0, 1+Arg_0])*max([0, 1+Arg_0]) {O(n^2)}
65,63: evalrealheapsortbb16in->evalrealheapsortbb10in: 1 {O(1)}
71,69: evalrealheapsortbb16in->evalrealheapsortbb11in: (1+max([2*Arg_0, 6]))*max([0, 1+Arg_0]) {O(n^2)}
72,70: evalrealheapsortbb16in->evalrealheapsortbb12in: (1+max([2*Arg_0, 6]))*max([0, 1+Arg_0]) {O(n^2)}
44,42: evalrealheapsortbb18in->evalrealheapsortbb8in: 1 {O(1)}
45,43: evalrealheapsortbb18in->evalrealheapsortreturnin: 1 {O(1)}
63,61: evalrealheapsortbb18in->evalrealheapsortbb16in: max([0, 1+Arg_0]) {O(n)}
69,67: evalrealheapsortbb18in->evalrealheapsortstop: 1 {O(1)}
15,13: evalrealheapsortbb2in->evalrealheapsortbb3in: inf {Infinity}
28,26: evalrealheapsortbb2in->evalrealheapsortbb3in: max([0, Arg_0+max([2, 2*(1+max([(-1)+max([12, 4*Arg_0]), 0]))])])*max([2*Arg_0, 6]) {O(n^2)}
5,5: evalrealheapsortbb3in->evalrealheapsortbb5in: max([(-2)+max([2*Arg_0, 6]), 0]) {O(n)}
6,5: evalrealheapsortbb3in->evalrealheapsortbb2in: inf {Infinity}
7,6: evalrealheapsortbb3in->evalrealheapsortbb3in: inf {Infinity}
8,6: evalrealheapsortbb3in->evalrealheapsortbb4in: max([2*Arg_0, 6])*max([2+2*(1+max([(-1)+max([12, 4*Arg_0]), 0])), 4]) {O(n^2)}
10,8: evalrealheapsortbb4in->evalrealheapsortbb2in: max([2*Arg_0, 6])*max([2+2*(1+max([(-1)+max([12, 4*Arg_0]), 0])), 4]) {O(n^2)}
13,11: evalrealheapsortbb4in->evalrealheapsortbb5in: max([(-3)+max([3*Arg_0, 9]), 0]) {O(n)}
42,40: evalrealheapsortbb5in->evalrealheapsortbb6in: max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
3,3: evalrealheapsortbb6in->evalrealheapsortbb3in: max([2*Arg_0, 6]) {O(n)}
4,4: evalrealheapsortbb6in->evalrealheapsortbb7in: 1 {O(1)}
62,60: evalrealheapsortbb6in->evalrealheapsortbb18in: 1 {O(1)}
0,0: evalrealheapsortstart->evalrealheapsortentryin: 1 {O(1)}
67,65: evalrealheapsortstart->evalrealheapsortbb6in: 1 {O(1)}
68,66: evalrealheapsortstart->evalrealheapsortreturnin: 1 {O(1)}
70,68: evalrealheapsortstart->evalrealheapsortstop: 1 {O(1)}

Expected Timebounds:

Overall expected timebound: (1+Arg_0)*(1+Arg_0)+(1+Arg_0)*max([18, 6*Arg_0])+(2*(1+max([1+4*Arg_0, 13]))+Arg_0)*max([2*Arg_0, 6])+(3+max([1+4*Arg_0, 13]))*max([2*Arg_0, 6])+18+2*(1+Arg_0)*(1+max([2*Arg_0, 6]))+2*(1+Arg_0)*Arg_0+2*(1+Arg_0)*max([12, 4*Arg_0])+2*(2+2*(1+max([1+4*Arg_0, 13])))*max([2*Arg_0, 6])+2*max([3*Arg_0, 9])+3*Arg_0+max([1+4*Arg_0, 13])+max([2*Arg_0, 6]) {O(n^2)}
0: evalrealheapsortstart->[1:evalrealheapsortentryin]: 1 {O(1)}
3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in]: max([2*Arg_0, 6]) {O(n)}
4: evalrealheapsortbb6in->[1:evalrealheapsortbb7in]: 1 {O(1)}
5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in]: 2+2*Arg_0 {O(n)}
6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in]: (2+2*(1+max([1+4*Arg_0, 13])))*max([2*Arg_0, 6]) {O(n^2)}
8: evalrealheapsortbb4in->[1:evalrealheapsortbb2in]: (2+2*(1+max([1+4*Arg_0, 13])))*max([2*Arg_0, 6]) {O(n^2)}
11: evalrealheapsortbb4in->[1:evalrealheapsortbb5in]: 3+max([3*Arg_0, 9]) {O(n)}
13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in]: (3+max([1+4*Arg_0, 13]))*max([2*Arg_0, 6]) {O(n^2)}
26: evalrealheapsortbb2in->[1:evalrealheapsortbb3in]: (2*(1+max([1+4*Arg_0, 13]))+Arg_0)*max([2*Arg_0, 6]) {O(n^2)}
40: evalrealheapsortbb5in->[1:evalrealheapsortbb6in]: max([1+4*Arg_0, 13]) {O(n)}
42: evalrealheapsortbb18in->[1:evalrealheapsortbb8in]: 1 {O(1)}
43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin]: 1 {O(1)}
45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in]: 1 {O(1)}
46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in]: 1 {O(1)}
52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in]: (1+Arg_0)*Arg_0 {O(n^2)}
53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in]: (1+Arg_0)*Arg_0 {O(n^2)}
54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in]: (1+Arg_0)*max([12, 4*Arg_0]) {O(n^2)}
55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in]: (1+Arg_0)*max([18, 6*Arg_0]) {O(n^2)}
56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in]: (1+Arg_0)*max([12, 4*Arg_0]) {O(n^2)}
59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in]: max([3*Arg_0, 9]) {O(n)}
60: evalrealheapsortbb6in->[1:evalrealheapsortbb18in]: 1 {O(1)}
61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in]: 1+Arg_0 {O(n)}
62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in]: (1+Arg_0)*(1+Arg_0) {O(n^2)}
63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in]: 1 {O(1)}
65: evalrealheapsortstart->[1:evalrealheapsortbb6in]: 1 {O(1)}
66: evalrealheapsortstart->[1:evalrealheapsortreturnin]: 1 {O(1)}
67: evalrealheapsortbb18in->[1:evalrealheapsortstop]: 1 {O(1)}
68: evalrealheapsortstart->[1:evalrealheapsortstop]: 1 {O(1)}
69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in]: (1+Arg_0)*(1+max([2*Arg_0, 6])) {O(n^2)}
70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in]: (1+Arg_0)*(1+max([2*Arg_0, 6])) {O(n^2)}

Costbounds:

Overall costbound: inf {Infinity}
54,52: evalrealheapsortbb11in->evalrealheapsortbb13in: inf {Infinity}
55,53: evalrealheapsortbb12in->evalrealheapsortbb13in: inf {Infinity}
56,54: evalrealheapsortbb13in->evalrealheapsortbb14in: inf {Infinity}
57,55: evalrealheapsortbb13in->evalrealheapsortbb16in: inf {Infinity}
58,56: evalrealheapsortbb14in->evalrealheapsortbb16in: inf {Infinity}
47,45: evalrealheapsortbb16in->evalrealheapsortbb9in: inf {Infinity}
48,46: evalrealheapsortbb16in->evalrealheapsortbb17in: inf {Infinity}
61,59: evalrealheapsortbb16in->evalrealheapsortbb18in: inf {Infinity}
64,62: evalrealheapsortbb16in->evalrealheapsortbb11in: inf {Infinity}
65,63: evalrealheapsortbb16in->evalrealheapsortbb10in: inf {Infinity}
71,69: evalrealheapsortbb16in->evalrealheapsortbb11in: inf {Infinity}
72,70: evalrealheapsortbb16in->evalrealheapsortbb12in: inf {Infinity}
44,42: evalrealheapsortbb18in->evalrealheapsortbb8in: inf {Infinity}
45,43: evalrealheapsortbb18in->evalrealheapsortreturnin: inf {Infinity}
63,61: evalrealheapsortbb18in->evalrealheapsortbb16in: inf {Infinity}
69,67: evalrealheapsortbb18in->evalrealheapsortstop: inf {Infinity}
15,13: evalrealheapsortbb2in->evalrealheapsortbb3in: inf {Infinity}
28,26: evalrealheapsortbb2in->evalrealheapsortbb3in: inf {Infinity}
5,5: evalrealheapsortbb3in->evalrealheapsortbb5in: inf {Infinity}
6,5: evalrealheapsortbb3in->evalrealheapsortbb2in: inf {Infinity}
7,6: evalrealheapsortbb3in->evalrealheapsortbb3in: inf {Infinity}
8,6: evalrealheapsortbb3in->evalrealheapsortbb4in: inf {Infinity}
10,8: evalrealheapsortbb4in->evalrealheapsortbb2in: inf {Infinity}
13,11: evalrealheapsortbb4in->evalrealheapsortbb5in: inf {Infinity}
42,40: evalrealheapsortbb5in->evalrealheapsortbb6in: inf {Infinity}
3,3: evalrealheapsortbb6in->evalrealheapsortbb3in: inf {Infinity}
4,4: evalrealheapsortbb6in->evalrealheapsortbb7in: inf {Infinity}
62,60: evalrealheapsortbb6in->evalrealheapsortbb18in: inf {Infinity}
0,0: evalrealheapsortstart->evalrealheapsortentryin: inf {Infinity}
67,65: evalrealheapsortstart->evalrealheapsortbb6in: inf {Infinity}
68,66: evalrealheapsortstart->evalrealheapsortreturnin: inf {Infinity}
70,68: evalrealheapsortstart->evalrealheapsortstop: inf {Infinity}

Expected Costbounds:

Overall expected costbound: (1+Arg_0)*max([18, 6*Arg_0])+(2*(1+max([1+4*Arg_0, 13]))+Arg_0)*max([2*Arg_0, 6])+(3+max([1+4*Arg_0, 13]))*max([2*Arg_0, 6])+2*(1+Arg_0)+2*(1+Arg_0)*(1+Arg_0)+2*(1+Arg_0)*Arg_0+2*(1+Arg_0)*max([12, 4*Arg_0])+2*(2+2*(1+max([1+4*Arg_0, 13])))*max([2*Arg_0, 6])+2*Arg_0+24+3*max([3*Arg_0, 9])+6*(1+Arg_0)*(1+max([2*Arg_0, 6]))+max([1+4*Arg_0, 13])+max([2*Arg_0, 6]) {O(n^2)}
0: evalrealheapsortstart->[1:evalrealheapsortentryin]: 1 {O(1)}
3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in]: max([2*Arg_0, 6]) {O(n)}
4: evalrealheapsortbb6in->[1:evalrealheapsortbb7in]: 1 {O(1)}
5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in]: 2+2*Arg_0 {O(n)}
6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in]: (2+2*(1+max([1+4*Arg_0, 13])))*max([2*Arg_0, 6]) {O(n^2)}
8: evalrealheapsortbb4in->[1:evalrealheapsortbb2in]: (2+2*(1+max([1+4*Arg_0, 13])))*max([2*Arg_0, 6]) {O(n^2)}
11: evalrealheapsortbb4in->[1:evalrealheapsortbb5in]: 3+max([3*Arg_0, 9]) {O(n)}
13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in]: (3+max([1+4*Arg_0, 13]))*max([2*Arg_0, 6]) {O(n^2)}
26: evalrealheapsortbb2in->[1:evalrealheapsortbb3in]: (2*(1+max([1+4*Arg_0, 13]))+Arg_0)*max([2*Arg_0, 6]) {O(n^2)}
40: evalrealheapsortbb5in->[1:evalrealheapsortbb6in]: max([1+4*Arg_0, 13]) {O(n)}
42: evalrealheapsortbb18in->[1:evalrealheapsortbb8in]: 1 {O(1)}
43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin]: 1 {O(1)}
45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in]: 1 {O(1)}
46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in]: 1 {O(1)}
52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in]: (1+Arg_0)*Arg_0 {O(n^2)}
53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in]: (1+Arg_0)*Arg_0 {O(n^2)}
54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in]: (1+Arg_0)*max([12, 4*Arg_0]) {O(n^2)}
55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in]: (1+Arg_0)*max([18, 6*Arg_0]) {O(n^2)}
56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in]: (1+Arg_0)*max([12, 4*Arg_0]) {O(n^2)}
59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in]: 2*max([3*Arg_0, 9]) {O(n)}
60: evalrealheapsortbb6in->[1:evalrealheapsortbb18in]: 2 {O(1)}
61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in]: 2*(1+Arg_0) {O(n)}
62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in]: 2*(1+Arg_0)*(1+Arg_0) {O(n^2)}
63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in]: 2 {O(1)}
65: evalrealheapsortstart->[1:evalrealheapsortbb6in]: 2 {O(1)}
66: evalrealheapsortstart->[1:evalrealheapsortreturnin]: 2 {O(1)}
67: evalrealheapsortbb18in->[1:evalrealheapsortstop]: 2 {O(1)}
68: evalrealheapsortstart->[1:evalrealheapsortstop]: 3 {O(1)}
69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in]: 3*(1+Arg_0)*(1+max([2*Arg_0, 6])) {O(n^2)}
70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in]: 3*(1+Arg_0)*(1+max([2*Arg_0, 6])) {O(n^2)}

Sizebounds:

54,52: evalrealheapsortbb11in->evalrealheapsortbb13in, Arg_0: Arg_0 {O(n)}
54,52: evalrealheapsortbb11in->evalrealheapsortbb13in, Arg_1: max([3*Arg_0, 9]) {O(n)}
54,52: evalrealheapsortbb11in->evalrealheapsortbb13in, Arg_2: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
54,52: evalrealheapsortbb11in->evalrealheapsortbb13in, Arg_3: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
55,53: evalrealheapsortbb12in->evalrealheapsortbb13in, Arg_0: Arg_0 {O(n)}
55,53: evalrealheapsortbb12in->evalrealheapsortbb13in, Arg_1: max([3*Arg_0, 9]) {O(n)}
55,53: evalrealheapsortbb12in->evalrealheapsortbb13in, Arg_2: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
55,53: evalrealheapsortbb12in->evalrealheapsortbb13in, Arg_3: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
56,54: evalrealheapsortbb13in->evalrealheapsortbb14in, Arg_0: Arg_0 {O(n)}
56,54: evalrealheapsortbb13in->evalrealheapsortbb14in, Arg_1: max([3*Arg_0, 9]) {O(n)}
56,54: evalrealheapsortbb13in->evalrealheapsortbb14in, Arg_2: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
56,54: evalrealheapsortbb13in->evalrealheapsortbb14in, Arg_3: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
57,55: evalrealheapsortbb13in->evalrealheapsortbb16in, Arg_0: Arg_0 {O(n)}
57,55: evalrealheapsortbb13in->evalrealheapsortbb16in, Arg_1: max([3*Arg_0, 9]) {O(n)}
57,55: evalrealheapsortbb13in->evalrealheapsortbb16in, Arg_2: Arg_0 {O(n)}
57,55: evalrealheapsortbb13in->evalrealheapsortbb16in, Arg_3: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
58,56: evalrealheapsortbb14in->evalrealheapsortbb16in, Arg_0: Arg_0 {O(n)}
58,56: evalrealheapsortbb14in->evalrealheapsortbb16in, Arg_1: max([3*Arg_0, 9]) {O(n)}
58,56: evalrealheapsortbb14in->evalrealheapsortbb16in, Arg_2: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
58,56: evalrealheapsortbb14in->evalrealheapsortbb16in, Arg_3: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
47,45: evalrealheapsortbb16in->evalrealheapsortbb9in, Arg_0: Arg_0 {O(n)}
47,45: evalrealheapsortbb16in->evalrealheapsortbb9in, Arg_1: max([3*Arg_0, 9]) {O(n)}
47,45: evalrealheapsortbb16in->evalrealheapsortbb9in, Arg_2: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
47,45: evalrealheapsortbb16in->evalrealheapsortbb9in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
48,46: evalrealheapsortbb16in->evalrealheapsortbb17in, Arg_0: Arg_0 {O(n)}
48,46: evalrealheapsortbb16in->evalrealheapsortbb17in, Arg_1: max([3*Arg_0, 9]) {O(n)}
48,46: evalrealheapsortbb16in->evalrealheapsortbb17in, Arg_2: max([max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]), Arg_0]) {O(EXP)}
48,46: evalrealheapsortbb16in->evalrealheapsortbb17in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
61,59: evalrealheapsortbb16in->evalrealheapsortbb18in, Arg_0: Arg_0 {O(n)}
61,59: evalrealheapsortbb16in->evalrealheapsortbb18in, Arg_1: max([3*Arg_0, 9]) {O(n)}
61,59: evalrealheapsortbb16in->evalrealheapsortbb18in, Arg_2: max([max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]), Arg_0]) {O(EXP)}
61,59: evalrealheapsortbb16in->evalrealheapsortbb18in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
64,62: evalrealheapsortbb16in->evalrealheapsortbb11in, Arg_0: Arg_0 {O(n)}
64,62: evalrealheapsortbb16in->evalrealheapsortbb11in, Arg_1: max([3*Arg_0, 9]) {O(n)}
64,62: evalrealheapsortbb16in->evalrealheapsortbb11in, Arg_2: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
64,62: evalrealheapsortbb16in->evalrealheapsortbb11in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
65,63: evalrealheapsortbb16in->evalrealheapsortbb10in, Arg_0: Arg_0 {O(n)}
65,63: evalrealheapsortbb16in->evalrealheapsortbb10in, Arg_1: max([3*Arg_0, 9]) {O(n)}
65,63: evalrealheapsortbb16in->evalrealheapsortbb10in, Arg_2: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
65,63: evalrealheapsortbb16in->evalrealheapsortbb10in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
71,69: evalrealheapsortbb16in->evalrealheapsortbb11in, Arg_0: Arg_0 {O(n)}
71,69: evalrealheapsortbb16in->evalrealheapsortbb11in, Arg_1: max([3*Arg_0, 9]) {O(n)}
71,69: evalrealheapsortbb16in->evalrealheapsortbb11in, Arg_2: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
71,69: evalrealheapsortbb16in->evalrealheapsortbb11in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
72,70: evalrealheapsortbb16in->evalrealheapsortbb12in, Arg_0: Arg_0 {O(n)}
72,70: evalrealheapsortbb16in->evalrealheapsortbb12in, Arg_1: max([3*Arg_0, 9]) {O(n)}
72,70: evalrealheapsortbb16in->evalrealheapsortbb12in, Arg_2: 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0]) {O(EXP)}
72,70: evalrealheapsortbb16in->evalrealheapsortbb12in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
44,42: evalrealheapsortbb18in->evalrealheapsortbb8in, Arg_0: Arg_0 {O(n)}
44,42: evalrealheapsortbb18in->evalrealheapsortbb8in, Arg_1: max([3*Arg_0, 9]) {O(n)}
44,42: evalrealheapsortbb18in->evalrealheapsortbb8in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
45,43: evalrealheapsortbb18in->evalrealheapsortreturnin, Arg_0: Arg_0 {O(n)}
45,43: evalrealheapsortbb18in->evalrealheapsortreturnin, Arg_1: max([3*Arg_0, 9]) {O(n)}
45,43: evalrealheapsortbb18in->evalrealheapsortreturnin, Arg_2: max([max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]), Arg_0]) {O(EXP)}
45,43: evalrealheapsortbb18in->evalrealheapsortreturnin, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
63,61: evalrealheapsortbb18in->evalrealheapsortbb16in, Arg_0: Arg_0 {O(n)}
63,61: evalrealheapsortbb18in->evalrealheapsortbb16in, Arg_1: max([3*Arg_0, 9]) {O(n)}
63,61: evalrealheapsortbb18in->evalrealheapsortbb16in, Arg_2: 0 {O(1)}
63,61: evalrealheapsortbb18in->evalrealheapsortbb16in, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
69,67: evalrealheapsortbb18in->evalrealheapsortstop, Arg_0: Arg_0 {O(n)}
69,67: evalrealheapsortbb18in->evalrealheapsortstop, Arg_1: max([3*Arg_0, 9]) {O(n)}
69,67: evalrealheapsortbb18in->evalrealheapsortstop, Arg_2: max([max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]), Arg_0]) {O(EXP)}
69,67: evalrealheapsortbb18in->evalrealheapsortstop, Arg_3: max([0, 2*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*2^(max([0, 1+Arg_0])*max([0, Arg_0]))*max([0, 1+Arg_0])*max([0, Arg_0])]) {O(EXP)}
15,13: evalrealheapsortbb2in->evalrealheapsortbb3in, Arg_0: Arg_0 {O(n)}
15,13: evalrealheapsortbb2in->evalrealheapsortbb3in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
15,13: evalrealheapsortbb2in->evalrealheapsortbb3in, Arg_2: (-1) {O(1)}
15,13: evalrealheapsortbb2in->evalrealheapsortbb3in, Arg_3: 0 {O(1)}
28,26: evalrealheapsortbb2in->evalrealheapsortbb3in, Arg_0: Arg_0 {O(n)}
28,26: evalrealheapsortbb2in->evalrealheapsortbb3in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
28,26: evalrealheapsortbb2in->evalrealheapsortbb3in, Arg_3: 0 {O(1)}
5,5: evalrealheapsortbb3in->evalrealheapsortbb5in, Arg_0: Arg_0 {O(n)}
5,5: evalrealheapsortbb3in->evalrealheapsortbb5in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
5,5: evalrealheapsortbb3in->evalrealheapsortbb5in, Arg_2: 0 {O(1)}
5,5: evalrealheapsortbb3in->evalrealheapsortbb5in, Arg_3: 0 {O(1)}
6,5: evalrealheapsortbb3in->evalrealheapsortbb2in, Arg_0: Arg_0 {O(n)}
6,5: evalrealheapsortbb3in->evalrealheapsortbb2in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
6,5: evalrealheapsortbb3in->evalrealheapsortbb2in, Arg_2: 0 {O(1)}
6,5: evalrealheapsortbb3in->evalrealheapsortbb2in, Arg_3: 0 {O(1)}
7,6: evalrealheapsortbb3in->evalrealheapsortbb3in, Arg_0: Arg_0 {O(n)}
7,6: evalrealheapsortbb3in->evalrealheapsortbb3in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
7,6: evalrealheapsortbb3in->evalrealheapsortbb3in, Arg_3: 0 {O(1)}
8,6: evalrealheapsortbb3in->evalrealheapsortbb4in, Arg_0: Arg_0 {O(n)}
8,6: evalrealheapsortbb3in->evalrealheapsortbb4in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
8,6: evalrealheapsortbb3in->evalrealheapsortbb4in, Arg_3: 0 {O(1)}
10,8: evalrealheapsortbb4in->evalrealheapsortbb2in, Arg_0: Arg_0 {O(n)}
10,8: evalrealheapsortbb4in->evalrealheapsortbb2in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
10,8: evalrealheapsortbb4in->evalrealheapsortbb2in, Arg_3: 0 {O(1)}
13,11: evalrealheapsortbb4in->evalrealheapsortbb5in, Arg_0: Arg_0 {O(n)}
13,11: evalrealheapsortbb4in->evalrealheapsortbb5in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
13,11: evalrealheapsortbb4in->evalrealheapsortbb5in, Arg_3: 0 {O(1)}
42,40: evalrealheapsortbb5in->evalrealheapsortbb6in, Arg_0: Arg_0 {O(n)}
42,40: evalrealheapsortbb5in->evalrealheapsortbb6in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
42,40: evalrealheapsortbb5in->evalrealheapsortbb6in, Arg_3: 0 {O(1)}
3,3: evalrealheapsortbb6in->evalrealheapsortbb3in, Arg_0: Arg_0 {O(n)}
3,3: evalrealheapsortbb6in->evalrealheapsortbb3in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
3,3: evalrealheapsortbb6in->evalrealheapsortbb3in, Arg_2: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
3,3: evalrealheapsortbb6in->evalrealheapsortbb3in, Arg_3: 0 {O(1)}
4,4: evalrealheapsortbb6in->evalrealheapsortbb7in, Arg_0: Arg_0 {O(n)}
4,4: evalrealheapsortbb6in->evalrealheapsortbb7in, Arg_1: 1+max([(-1)+max([12, 4*Arg_0]), 0]) {O(n)}
4,4: evalrealheapsortbb6in->evalrealheapsortbb7in, Arg_3: 0 {O(1)}
62,60: evalrealheapsortbb6in->evalrealheapsortbb18in, Arg_0: Arg_0 {O(n)}
62,60: evalrealheapsortbb6in->evalrealheapsortbb18in, Arg_1: 0 {O(1)}
62,60: evalrealheapsortbb6in->evalrealheapsortbb18in, Arg_3: 0 {O(1)}
0,0: evalrealheapsortstart->evalrealheapsortentryin, Arg_0: Arg_0 {O(n)}
0,0: evalrealheapsortstart->evalrealheapsortentryin, Arg_1: Arg_1 {O(n)}
0,0: evalrealheapsortstart->evalrealheapsortentryin, Arg_2: Arg_2 {O(n)}
0,0: evalrealheapsortstart->evalrealheapsortentryin, Arg_3: 0 {O(1)}
67,65: evalrealheapsortstart->evalrealheapsortbb6in, Arg_0: Arg_0 {O(n)}
67,65: evalrealheapsortstart->evalrealheapsortbb6in, Arg_1: 1 {O(1)}
67,65: evalrealheapsortstart->evalrealheapsortbb6in, Arg_2: Arg_2 {O(n)}
67,65: evalrealheapsortstart->evalrealheapsortbb6in, Arg_3: 0 {O(1)}
68,66: evalrealheapsortstart->evalrealheapsortreturnin, Arg_0: 2 {O(1)}
68,66: evalrealheapsortstart->evalrealheapsortreturnin, Arg_1: Arg_1 {O(n)}
68,66: evalrealheapsortstart->evalrealheapsortreturnin, Arg_2: Arg_2 {O(n)}
68,66: evalrealheapsortstart->evalrealheapsortreturnin, Arg_3: 0 {O(1)}
70,68: evalrealheapsortstart->evalrealheapsortstop, Arg_0: 2 {O(1)}
70,68: evalrealheapsortstart->evalrealheapsortstop, Arg_1: Arg_1 {O(n)}
70,68: evalrealheapsortstart->evalrealheapsortstop, Arg_2: Arg_2 {O(n)}
70,68: evalrealheapsortstart->evalrealheapsortstop, Arg_3: 0 {O(1)}

ExpSizeBounds:

(0: evalrealheapsortstart->[1:evalrealheapsortentryin], evalrealheapsortentryin), E: E {O(n)}
(0: evalrealheapsortstart->[1:evalrealheapsortentryin], evalrealheapsortentryin), F: F {O(n)}
(0: evalrealheapsortstart->[1:evalrealheapsortentryin], evalrealheapsortentryin), G: G {O(n)}
(0: evalrealheapsortstart->[1:evalrealheapsortentryin], evalrealheapsortentryin), Arg_0: Arg_0 {O(n)}
(0: evalrealheapsortstart->[1:evalrealheapsortentryin], evalrealheapsortentryin), Arg_1: Arg_1 {O(n)}
(0: evalrealheapsortstart->[1:evalrealheapsortentryin], evalrealheapsortentryin), Arg_2: Arg_2 {O(n)}
(0: evalrealheapsortstart->[1:evalrealheapsortentryin], evalrealheapsortentryin), Arg_3: 0 {O(1)}
(3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), E: E {O(n)}
(3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), F: F {O(n)}
(3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), G: G {O(n)}
(3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_0: Arg_0 {O(n)}
(3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_2: 1+max([1+4*Arg_0, 13]) {O(n)}
(3: evalrealheapsortbb6in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_3: 0 {O(1)}
(4: evalrealheapsortbb6in->[1:evalrealheapsortbb7in], evalrealheapsortbb7in), E: E {O(n)}
(4: evalrealheapsortbb6in->[1:evalrealheapsortbb7in], evalrealheapsortbb7in), F: F {O(n)}
(4: evalrealheapsortbb6in->[1:evalrealheapsortbb7in], evalrealheapsortbb7in), G: G {O(n)}
(4: evalrealheapsortbb6in->[1:evalrealheapsortbb7in], evalrealheapsortbb7in), Arg_0: Arg_0 {O(n)}
(4: evalrealheapsortbb6in->[1:evalrealheapsortbb7in], evalrealheapsortbb7in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(4: evalrealheapsortbb6in->[1:evalrealheapsortbb7in], evalrealheapsortbb7in), Arg_3: 0 {O(1)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb2in), E: E {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb2in), F: F {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb2in), G: G {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb2in), Arg_0: Arg_0 {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb2in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb2in), Arg_2: 1/2 {O(1)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb2in), Arg_3: 0 {O(1)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb5in), E: E {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb5in), F: F {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb5in), G: G {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb5in), Arg_0: Arg_0 {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb5in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb5in), Arg_2: 1/2 {O(1)}
(5: evalrealheapsortbb3in->[1/2:evalrealheapsortbb5in; 1/2:evalrealheapsortbb2in], evalrealheapsortbb5in), Arg_3: 0 {O(1)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb3in), E: E {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb3in), F: F {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb3in), G: G {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb3in), Arg_0: Arg_0 {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb3in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb3in), Arg_3: 0 {O(1)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb4in), E: E {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb4in), F: F {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb4in), G: G {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb4in), Arg_0: Arg_0 {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb4in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(6: evalrealheapsortbb3in->[1/2:evalrealheapsortbb3in; 1/2:evalrealheapsortbb4in], evalrealheapsortbb4in), Arg_3: 0 {O(1)}
(8: evalrealheapsortbb4in->[1:evalrealheapsortbb2in], evalrealheapsortbb2in), E: E {O(n)}
(8: evalrealheapsortbb4in->[1:evalrealheapsortbb2in], evalrealheapsortbb2in), F: F {O(n)}
(8: evalrealheapsortbb4in->[1:evalrealheapsortbb2in], evalrealheapsortbb2in), G: G {O(n)}
(8: evalrealheapsortbb4in->[1:evalrealheapsortbb2in], evalrealheapsortbb2in), Arg_0: Arg_0 {O(n)}
(8: evalrealheapsortbb4in->[1:evalrealheapsortbb2in], evalrealheapsortbb2in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(8: evalrealheapsortbb4in->[1:evalrealheapsortbb2in], evalrealheapsortbb2in), Arg_3: 0 {O(1)}
(11: evalrealheapsortbb4in->[1:evalrealheapsortbb5in], evalrealheapsortbb5in), E: E {O(n)}
(11: evalrealheapsortbb4in->[1:evalrealheapsortbb5in], evalrealheapsortbb5in), F: F {O(n)}
(11: evalrealheapsortbb4in->[1:evalrealheapsortbb5in], evalrealheapsortbb5in), G: G {O(n)}
(11: evalrealheapsortbb4in->[1:evalrealheapsortbb5in], evalrealheapsortbb5in), Arg_0: Arg_0 {O(n)}
(11: evalrealheapsortbb4in->[1:evalrealheapsortbb5in], evalrealheapsortbb5in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(11: evalrealheapsortbb4in->[1:evalrealheapsortbb5in], evalrealheapsortbb5in), Arg_3: 0 {O(1)}
(13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), E: E {O(n)}
(13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), F: F {O(n)}
(13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), G: G {O(n)}
(13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_0: Arg_0 {O(n)}
(13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_2: 1 {O(1)}
(13: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_3: 0 {O(1)}
(26: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), E: E {O(n)}
(26: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), F: F {O(n)}
(26: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), G: G {O(n)}
(26: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_0: Arg_0 {O(n)}
(26: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(26: evalrealheapsortbb2in->[1:evalrealheapsortbb3in], evalrealheapsortbb3in), Arg_3: 0 {O(1)}
(40: evalrealheapsortbb5in->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), E: E {O(n)}
(40: evalrealheapsortbb5in->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), F: F {O(n)}
(40: evalrealheapsortbb5in->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), G: G {O(n)}
(40: evalrealheapsortbb5in->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), Arg_0: Arg_0 {O(n)}
(40: evalrealheapsortbb5in->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), Arg_1: 1+max([1+4*Arg_0, 13]) {O(n)}
(40: evalrealheapsortbb5in->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), Arg_3: 0 {O(1)}
(42: evalrealheapsortbb18in->[1:evalrealheapsortbb8in], evalrealheapsortbb8in), E: 2*E {O(n)}
(42: evalrealheapsortbb18in->[1:evalrealheapsortbb8in], evalrealheapsortbb8in), F: 2*F {O(n)}
(42: evalrealheapsortbb18in->[1:evalrealheapsortbb8in], evalrealheapsortbb8in), G: 2*G {O(n)}
(42: evalrealheapsortbb18in->[1:evalrealheapsortbb8in], evalrealheapsortbb8in), Arg_0: Arg_0 {O(n)}
(42: evalrealheapsortbb18in->[1:evalrealheapsortbb8in], evalrealheapsortbb8in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(42: evalrealheapsortbb18in->[1:evalrealheapsortbb8in], evalrealheapsortbb8in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), E: E {O(n)}
(43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), F: F {O(n)}
(43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), G: G {O(n)}
(43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), Arg_0: Arg_0 {O(n)}
(43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), Arg_1: max([3*Arg_0, 9]) {O(n)}
(43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), Arg_2: max([2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0, Arg_0]) {O(EXP)}
(43: evalrealheapsortbb18in->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in], evalrealheapsortbb9in), E: 2*E {O(n)}
(45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in], evalrealheapsortbb9in), F: 2*F {O(n)}
(45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in], evalrealheapsortbb9in), G: 2*G {O(n)}
(45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in], evalrealheapsortbb9in), Arg_0: Arg_0 {O(n)}
(45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in], evalrealheapsortbb9in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in], evalrealheapsortbb9in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(45: evalrealheapsortbb16in->[1:evalrealheapsortbb9in], evalrealheapsortbb9in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in], evalrealheapsortbb17in), E: 3*E {O(n)}
(46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in], evalrealheapsortbb17in), F: 3*F {O(n)}
(46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in], evalrealheapsortbb17in), G: 3*G {O(n)}
(46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in], evalrealheapsortbb17in), Arg_0: Arg_0 {O(n)}
(46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in], evalrealheapsortbb17in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in], evalrealheapsortbb17in), Arg_2: max([2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0, Arg_0]) {O(EXP)}
(46: evalrealheapsortbb16in->[1:evalrealheapsortbb17in], evalrealheapsortbb17in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), E: E {O(n)}
(52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), F: F {O(n)}
(52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), G: G {O(n)}
(52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), Arg_0: Arg_0 {O(n)}
(52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(52: evalrealheapsortbb11in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), Arg_3: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), E: E {O(n)}
(53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), F: F {O(n)}
(53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), G: G {O(n)}
(53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), Arg_0: Arg_0 {O(n)}
(53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(53: evalrealheapsortbb12in->[1:evalrealheapsortbb13in], evalrealheapsortbb13in), Arg_3: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in], evalrealheapsortbb14in), E: E {O(n)}
(54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in], evalrealheapsortbb14in), F: F {O(n)}
(54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in], evalrealheapsortbb14in), G: G {O(n)}
(54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in], evalrealheapsortbb14in), Arg_0: Arg_0 {O(n)}
(54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in], evalrealheapsortbb14in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in], evalrealheapsortbb14in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(54: evalrealheapsortbb13in->[1:evalrealheapsortbb14in], evalrealheapsortbb14in), Arg_3: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), E: E {O(n)}
(55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), F: F {O(n)}
(55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), G: G {O(n)}
(55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_0: Arg_0 {O(n)}
(55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_2: Arg_0 {O(n)}
(55: evalrealheapsortbb13in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_3: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), E: E {O(n)}
(56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), F: F {O(n)}
(56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), G: G {O(n)}
(56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_0: Arg_0 {O(n)}
(56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(56: evalrealheapsortbb14in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_3: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), E: E {O(n)}
(59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), F: F {O(n)}
(59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), G: G {O(n)}
(59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), Arg_0: Arg_0 {O(n)}
(59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), Arg_2: max([2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0, Arg_0]) {O(EXP)}
(59: evalrealheapsortbb16in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(60: evalrealheapsortbb6in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), E: E {O(n)}
(60: evalrealheapsortbb6in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), F: F {O(n)}
(60: evalrealheapsortbb6in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), G: G {O(n)}
(60: evalrealheapsortbb6in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), Arg_0: Arg_0 {O(n)}
(60: evalrealheapsortbb6in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), Arg_1: 0 {O(1)}
(60: evalrealheapsortbb6in->[1:evalrealheapsortbb18in], evalrealheapsortbb18in), Arg_3: 0 {O(1)}
(61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), E: E {O(n)}
(61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), F: F {O(n)}
(61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), G: G {O(n)}
(61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_0: Arg_0 {O(n)}
(61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_2: 0 {O(1)}
(61: evalrealheapsortbb18in->[1:evalrealheapsortbb16in], evalrealheapsortbb16in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), E: E {O(n)}
(62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), F: F {O(n)}
(62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), G: G {O(n)}
(62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), Arg_0: Arg_0 {O(n)}
(62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(62: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in], evalrealheapsortbb10in), E: 2*E {O(n)}
(63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in], evalrealheapsortbb10in), F: 2*F {O(n)}
(63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in], evalrealheapsortbb10in), G: 2*G {O(n)}
(63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in], evalrealheapsortbb10in), Arg_0: Arg_0 {O(n)}
(63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in], evalrealheapsortbb10in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in], evalrealheapsortbb10in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(63: evalrealheapsortbb16in->[1:evalrealheapsortbb10in], evalrealheapsortbb10in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(65: evalrealheapsortstart->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), E: E {O(n)}
(65: evalrealheapsortstart->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), F: F {O(n)}
(65: evalrealheapsortstart->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), G: G {O(n)}
(65: evalrealheapsortstart->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), Arg_0: Arg_0 {O(n)}
(65: evalrealheapsortstart->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), Arg_1: 1 {O(1)}
(65: evalrealheapsortstart->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), Arg_2: Arg_2 {O(n)}
(65: evalrealheapsortstart->[1:evalrealheapsortbb6in], evalrealheapsortbb6in), Arg_3: 0 {O(1)}
(66: evalrealheapsortstart->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), E: E {O(n)}
(66: evalrealheapsortstart->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), F: F {O(n)}
(66: evalrealheapsortstart->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), G: G {O(n)}
(66: evalrealheapsortstart->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), Arg_0: Arg_0 {O(n)}
(66: evalrealheapsortstart->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), Arg_1: Arg_1 {O(n)}
(66: evalrealheapsortstart->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), Arg_2: Arg_2 {O(n)}
(66: evalrealheapsortstart->[1:evalrealheapsortreturnin], evalrealheapsortreturnin), Arg_3: 0 {O(1)}
(67: evalrealheapsortbb18in->[1:evalrealheapsortstop], evalrealheapsortstop), E: E {O(n)}
(67: evalrealheapsortbb18in->[1:evalrealheapsortstop], evalrealheapsortstop), F: F {O(n)}
(67: evalrealheapsortbb18in->[1:evalrealheapsortstop], evalrealheapsortstop), G: G {O(n)}
(67: evalrealheapsortbb18in->[1:evalrealheapsortstop], evalrealheapsortstop), Arg_0: Arg_0 {O(n)}
(67: evalrealheapsortbb18in->[1:evalrealheapsortstop], evalrealheapsortstop), Arg_1: max([3*Arg_0, 9]) {O(n)}
(67: evalrealheapsortbb18in->[1:evalrealheapsortstop], evalrealheapsortstop), Arg_2: max([2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0, Arg_0]) {O(EXP)}
(67: evalrealheapsortbb18in->[1:evalrealheapsortstop], evalrealheapsortstop), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(68: evalrealheapsortstart->[1:evalrealheapsortstop], evalrealheapsortstop), E: E {O(n)}
(68: evalrealheapsortstart->[1:evalrealheapsortstop], evalrealheapsortstop), F: F {O(n)}
(68: evalrealheapsortstart->[1:evalrealheapsortstop], evalrealheapsortstop), G: G {O(n)}
(68: evalrealheapsortstart->[1:evalrealheapsortstop], evalrealheapsortstop), Arg_0: Arg_0 {O(n)}
(68: evalrealheapsortstart->[1:evalrealheapsortstop], evalrealheapsortstop), Arg_1: Arg_1 {O(n)}
(68: evalrealheapsortstart->[1:evalrealheapsortstop], evalrealheapsortstop), Arg_2: Arg_2 {O(n)}
(68: evalrealheapsortstart->[1:evalrealheapsortstop], evalrealheapsortstop), Arg_3: 0 {O(1)}
(69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), E: E {O(n)}
(69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), F: F {O(n)}
(69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), G: G {O(n)}
(69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), Arg_0: Arg_0 {O(n)}
(69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(69: evalrealheapsortbb16in->[1:evalrealheapsortbb11in], evalrealheapsortbb11in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}
(70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in], evalrealheapsortbb12in), E: E {O(n)}
(70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in], evalrealheapsortbb12in), F: F {O(n)}
(70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in], evalrealheapsortbb12in), G: G {O(n)}
(70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in], evalrealheapsortbb12in), Arg_0: Arg_0 {O(n)}
(70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in], evalrealheapsortbb12in), Arg_1: max([3*Arg_0, 9]) {O(n)}
(70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in], evalrealheapsortbb12in), Arg_2: 2*(1+Arg_0)*Arg_0*abs(2^((1+Arg_0)*Arg_0))*abs(2^((1+Arg_0)*Arg_0)) {O(EXP)}
(70: evalrealheapsortbb16in->[1:evalrealheapsortbb12in], evalrealheapsortbb12in), Arg_3: max([0, 2*(1+Arg_0)*2^((1+Arg_0)*Arg_0)*2^((1+Arg_0)*Arg_0)*Arg_0]) {O(EXP)}