warning: Ignored call to evalrealheapsortstop/4 in equation evalrealheapsortreturnin/4 
Inferred cost of evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I): 
evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I):[38]: 1
  with precondition: [E=1,B=C,I=D,A=F,B=G,B=H,B>=1,A>=B+1] 

evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I):[39]: 2
  with precondition: [E=0,B=C,I=D,A=F,B=G,B=H,B>=1,A>=B+1] 

evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I):[40]: 1
  with precondition: [E=0,B=C,I=D,A=F,B=G,B=H,0>=B,A>=B+1] 

evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I):[[37],38]: 1+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*G,it1=<-1*H+1*B,it1=<-1*H+1*G,it1=<1*A+ -1,it1=<1*C+ -1*H,it1=<1*F+ -1,it1=<-1*H+1*A+ -1,it1=<-1*H+1*F+ -1
  with precondition: [E=1,A=F,B=G,D=I,H>=1,C>=2*H+1,A>=B+1,B>=C] 

evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I):[[37],39]: 2+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*G,it1=<-1*H+1*B,it1=<-1*H+1*G,it1=<1*A+ -1,it1=<1*C+ -1*H,it1=<1*F+ -1,it1=<-1*H+1*A+ -1,it1=<-1*H+1*F+ -1
  with precondition: [E=0,A=F,B=G,D=I,H>=1,C>=2*H+1,A>=B+1,B>=C] 

evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I):[[37],40]: 1+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*G,it1=<-1*H+1*B,it1=<-1*H+1*G,it1=<1*A+ -1,it1=<1*C+ -1*H,it1=<1*F+ -1,it1=<-1*H+1*A+ -1,it1=<-1*H+1*F+ -1
  with precondition: [E=0,A=F,B=G,D=I,0>=H,C>=1,2*H+1>=0,A>=B+1,B>=C] 

Inferred cost of evalrealheapsortbb6in(A,B,C,D,E,F,G,H,I): 
evalrealheapsortbb6in(A,B,C,D,E,F,G,H,I):[46]: 2
  with precondition: [B=1,E=1,A>=3] 

evalrealheapsortbb6in(A,B,C,D,E,F,G,H,I):[[42,44,45],46]: 2+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that:it1+it2+it4=<1*A+ -1*B,it1+it2+it4=<-1*B+1*A+ -1
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [E=1,B>=1,A>=B+2] 

evalrealheapsortbb6in(A,B,C,D,E,F,G,H,I):[[42,44,45],47]: 2+it1*(3)+it2*(4)+it3*(4+it4*(3))+it5*(3+it6*(3))
  Such that:it1=<1*A+ -2,it1=<1*A+ -1,it2+it3+it5=<1*A+ -1*B,it2+it3+it5=<-1*B+1*A+ -1
            it4=<1*A+ -1,it4=<1*A+ -2
            it6=<1*A+ -1/2,it6=<1*A+ -1
  with precondition: [E=1,A>=4,B>=1,A>=B+2] 

evalrealheapsortbb6in(A,B,C,D,E,F,G,H,I):[[42,44,45],48]: 1+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that:it1+it2+it4=<1*A+ -1*B,it1+it2+it4=<1*F+ -1,it1+it2+it4=<1*F+ -1*B,it1+it2+it4=<1*G+ -1
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [E=0,A=F,A=G,D=I,A>=3,B>=1,2*H+1>=0,A>=B+1,A>=H+1] 

Inferred cost of evalrealheapsortreturnin(A,B,C,D): 
evalrealheapsortreturnin(A,B,C,D):[50]: 1
  with precondition: [] 

Inferred cost of evalrealheapsortbb16in(A,B,C,D,E,F,G,H,I): 
evalrealheapsortbb16in(A,B,C,D,E,F,G,H,I):[58]: 1
  with precondition: [C=0,E=0,H=0,A=B+2,I=D,A=F,A=G+2] 

evalrealheapsortbb16in(A,B,C,D,E,F,G,H,I):[[53,54,55,56,57],52,58]: inf
  with precondition: [E=0,G=B,A=F,A=G+H+2,A=G+I+2,A>=G+2,A>=2*C+G+3] 

evalrealheapsortbb16in(A,B,C,D,E,F,G,H,I):[[53,54,55,56,57],58]: inf
  with precondition: [E=0,A=F,B=G,A>=B+2,A>=2*C+B+3,B+2*H+2>=A,A>=B+I+2] 

evalrealheapsortbb16in(A,B,C,D,E,F,G,H,I):[[53,54,55,56,57],59]...: inf
  with precondition: [1>=E,E>=0,A>=B+2,A>=2*C+B+3] 

evalrealheapsortbb16in(A,B,C,D,E,F,G,H,I):[52,58]: 6
  with precondition: [C=0,E=0,H=1,I=1,A=B+3,A=F,A=G+3] 

Inferred cost of evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I): 
evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[64]: 1
  with precondition: [B=0,E=0,G=0,H=C,I=D,A=F,1>=A] 

evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[65]...: inf
  with precondition: [B=0,1>=E,A>=3,E>=0] 

evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[66]...: inf
  with precondition: [B=0,E=1,A>=3] 

evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[[61,62],60,64]: 5+it1*(inf)
  Such that:it1=<1*F+ -2,it1=<1*G+ -1,it1=<1*A+ -1*B+ -2,it1=<1*F+ -1*B+ -2
  with precondition: [E=0,H=0,A=F,A=G+1,1>=I,B>=0,A>=B+3] 

evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[[61,62],63,60,64]: 14+it1*(inf)
  Such that:it1=<1*F+ -3,it1=<1*F+ -2,it1=<1*G+ -2,it1=<1*G+ -1,it1=<1*A+ -1*B+ -3,it1=<1*A+ -1*B+ -2,it1=<1*F+ -1*B+ -3,it1=<1*F+ -1*B+ -2
  with precondition: [E=0,H=0,I=1,A=F,A=G+1,B>=0,A>=B+4] 

evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[[61,62],65]...: inf
  with precondition: [1>=E,B>=0,E>=0,A>=B+4] 

evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[[61,62],66]...: inf
  with precondition: [E=1,B>=0,A>=B+4] 

evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[60,64]: 5
  with precondition: [A=2,B=0,E=0,F=2,G=1,H=0,D=I] 

evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I):[63,60,64]: 14
  with precondition: [A=3,B=0,E=0,F=3,G=2,H=0,I=1] 

Inferred cost of loop_cont_evalrealheapsortbb18in(A,B,C,D): 
loop_cont_evalrealheapsortbb18in(A,B,C,D):[68]: 1
  with precondition: [] 

Inferred cost of evalrealheapsortbb7in(A,B,C,D): 
evalrealheapsortbb7in(A,B,C,D):[70]: 3
  with precondition: [1>=A] 

evalrealheapsortbb7in(A,B,C,D):[71]: 7+it1*(inf)
  Such that:it1=<1*A+ -2
  with precondition: [A>=3] 

evalrealheapsortbb7in(A,B,C,D):[72]: 16+it1*(inf)
  Such that:it1=<1*A+ -3,it1=<1*A+ -2
  with precondition: [A>=4] 

evalrealheapsortbb7in(A,B,C,D):[73]: 7
  with precondition: [A=2] 

evalrealheapsortbb7in(A,B,C,D):[74]: 16
  with precondition: [A=3] 

evalrealheapsortbb7in(A,B,C,D):[75]...: inf
  with precondition: [A>=3] 

evalrealheapsortbb7in(A,B,C,D):[76]...: inf
  with precondition: [A>=4] 

evalrealheapsortbb7in(A,B,C,D):[77]...: inf
  with precondition: [A>=3] 

evalrealheapsortbb7in(A,B,C,D):[78]...: inf
  with precondition: [A>=3] 

evalrealheapsortbb7in(A,B,C,D):[79]...: inf
  with precondition: [A>=4] 

evalrealheapsortbb7in(A,B,C,D):[80]...: inf
  with precondition: [A>=4] 

Inferred cost of loop_cont_evalrealheapsortbb6in(A,B,C,D): 
loop_cont_evalrealheapsortbb6in(A,B,C,D):[82]: 3
  with precondition: [1>=A] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[83]: 7+it1*(inf)
  Such that:it1=<1*A+ -2
  with precondition: [A>=3] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[84]: 16+it1*(inf)
  Such that:it1=<1*A+ -3,it1=<1*A+ -2
  with precondition: [A>=4] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[85]: 7
  with precondition: [A=2] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[86]: 16
  with precondition: [A=3] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[87]...: inf
  with precondition: [A>=3] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[88]...: inf
  with precondition: [A>=4] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[89]...: inf
  with precondition: [A>=3] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[90]...: inf
  with precondition: [A>=3] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[91]...: inf
  with precondition: [A>=4] 

loop_cont_evalrealheapsortbb6in(A,B,C,D):[92]...: inf
  with precondition: [A>=4] 

Inferred cost of evalrealheapsortentryin(A,B,C,D): 
evalrealheapsortentryin(A,B,C,D):[94]: 2
  with precondition: [2>=A] 

evalrealheapsortentryin(A,B,C,D):[95]: 9+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))+it6*(inf)
  Such that:it1+it2+it4=<1*A+ -1,it6=<1*A+ -2
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [A>=3] 

evalrealheapsortentryin(A,B,C,D):[96]: 18+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))+it6*(inf)
  Such that:it1+it2+it4=<1*A+ -1,it6=<1*A+ -3,it6=<1*A+ -2
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [A>=4] 

evalrealheapsortentryin(A,B,C,D):[97]: 18+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that:it1+it2+it4=<2
            it3=<2,it3=<1
            it5=<5/2,it5=<2
  with precondition: [A=3] 

evalrealheapsortentryin(A,B,C,D):[98]: 3
  with precondition: [A>=3] 

evalrealheapsortentryin(A,B,C,D):[99]: 3+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that:it1+it2+it4=<1*A+ -2,it1+it2+it4=<1*A+ -1
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [A>=3] 

evalrealheapsortentryin(A,B,C,D):[100]: 3+it1*(3)+it2*(4)+it3*(4+it4*(3))+it5*(3+it6*(3))
  Such that:it1=<1*A+ -2,it1=<1*A+ -1,it2+it3+it5=<1*A+ -2,it2+it3+it5=<1*A+ -1
            it4=<1*A+ -1,it4=<1*A+ -2
            it6=<1*A+ -1/2,it6=<1*A+ -1
  with precondition: [A>=4] 

evalrealheapsortentryin(A,B,C,D):[101]...: inf
  with precondition: [A>=3] 

evalrealheapsortentryin(A,B,C,D):[102]...: inf
  with precondition: [A>=4] 

evalrealheapsortentryin(A,B,C,D):[103]...: inf
  with precondition: [A>=3] 

evalrealheapsortentryin(A,B,C,D):[104]...: inf
  with precondition: [A>=3] 

evalrealheapsortentryin(A,B,C,D):[105]...: inf
  with precondition: [A>=4] 

evalrealheapsortentryin(A,B,C,D):[106]...: inf
  with precondition: [A>=4] 

Inferred cost of evalrealheapsortstart(A,B,C,D): 
evalrealheapsortstart(A,B,C,D):[108]: 3
  with precondition: [2>=A] 

evalrealheapsortstart(A,B,C,D):[109]: 10+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))+it6*(inf)
  Such that:it1+it2+it4=<1*A+ -1,it6=<1*A+ -2
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [A>=3] 

evalrealheapsortstart(A,B,C,D):[110]: 19+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))+it6*(inf)
  Such that:it1+it2+it4=<1*A+ -1,it6=<1*A+ -3,it6=<1*A+ -2
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [A>=4] 

evalrealheapsortstart(A,B,C,D):[111]: 19+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that:it1+it2+it4=<2
            it3=<2,it3=<1
            it5=<5/2,it5=<2
  with precondition: [A=3] 

evalrealheapsortstart(A,B,C,D):[112]: 4
  with precondition: [A>=3] 

evalrealheapsortstart(A,B,C,D):[113]: 4+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that:it1+it2+it4=<1*A+ -2,it1+it2+it4=<1*A+ -1
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [A>=3] 

evalrealheapsortstart(A,B,C,D):[114]: 4+it1*(3)+it2*(4)+it3*(4+it4*(3))+it5*(3+it6*(3))
  Such that:it1=<1*A+ -2,it1=<1*A+ -1,it2+it3+it5=<1*A+ -2,it2+it3+it5=<1*A+ -1
            it4=<1*A+ -1,it4=<1*A+ -2
            it6=<1*A+ -1/2,it6=<1*A+ -1
  with precondition: [A>=4] 

evalrealheapsortstart(A,B,C,D):[115]...: inf
  with precondition: [A>=3] 

evalrealheapsortstart(A,B,C,D):[116]...: inf
  with precondition: [A>=4] 

evalrealheapsortstart(A,B,C,D):[117]...: inf
  with precondition: [A>=3] 

evalrealheapsortstart(A,B,C,D):[118]...: inf
  with precondition: [A>=3] 

evalrealheapsortstart(A,B,C,D):[119]...: inf
  with precondition: [A>=4] 

evalrealheapsortstart(A,B,C,D):[120]...: inf
  with precondition: [A>=4] 

Solved cost expressions of evalrealheapsortstart(A,B,C,D): 
evalrealheapsortstart(A,B,C,D):[108]: 3  with precondition: [2>=A] 
evalrealheapsortstart(A,B,C,D):[109]: inf  with precondition: [A>=3] 
evalrealheapsortstart(A,B,C,D):[110]: inf  with precondition: [A>=4] 
evalrealheapsortstart(A,B,C,D):[111]: 37  with precondition: [A=3] 
evalrealheapsortstart(A,B,C,D):[112]: 4  with precondition: [A>=3] 
evalrealheapsortstart(A,B,C,D):[113]: max([4*A+ -8, (1*A+ -2)* (3*A), (3*A+ -2)* (1*A+ -2)])+4  with precondition: [A>=3] 
evalrealheapsortstart(A,B,C,D):[114]: 3*A+ -6+max([4*A+ -8, (1*A+ -2)* (3*A), (3*A+ -2)* (1*A+ -2)])+4  with precondition: [A>=4] 
evalrealheapsortstart(A,B,C,D):[115]...: inf  with precondition: [A>=3] 
evalrealheapsortstart(A,B,C,D):[116]...: inf  with precondition: [A>=4] 
evalrealheapsortstart(A,B,C,D):[117]...: inf  with precondition: [A>=3] 
evalrealheapsortstart(A,B,C,D):[118]...: inf  with precondition: [A>=3] 
evalrealheapsortstart(A,B,C,D):[119]...: inf  with precondition: [A>=4] 
evalrealheapsortstart(A,B,C,D):[120]...: inf  with precondition: [A>=4] 
Maximum cost of evalrealheapsortstart(A,B,C,D): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 52 ms.
Invariants computed in 173 ms.
----Backward Invariants 95 ms.
----Transitive Invariants 14 ms.
Refinement performed in 138 ms.
Termination proved in 28 ms.
Upper bounds computed in 288 ms.
----Phase cost structures 156 ms.
--------Equation cost structures 126 ms.
--------Inductive compression(1) 2 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 116 ms.
----Solving cost expressions 5 ms.

Compressed phase information: 9 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 753 ms.