warning: Ignored call to evalrealheapsortstep1stop/3 in equation evalrealheapsortstep1returnin/3 
Inferred cost of evalrealheapsortstep1bb3in(A,B,C,D,E,F,G): 
evalrealheapsortstep1bb3in(A,B,C,D,E,F,G):[21]: 1
  with precondition: [D=1,B=C,A=E,B=F,B=G,B>=1,A>=B+1] 

evalrealheapsortstep1bb3in(A,B,C,D,E,F,G):[22]: 2
  with precondition: [D=0,B=C,A=E,B=F,B=G,B>=1,A>=B+1] 

evalrealheapsortstep1bb3in(A,B,C,D,E,F,G):[23]: 1
  with precondition: [D=0,B=C,A=E,B=F,B=G,0>=B,A>=B+1] 

evalrealheapsortstep1bb3in(A,B,C,D,E,F,G):[[20],21]: 1+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*F,it1=<-1*G+1*B,it1=<-1*G+1*F,it1=<1*A+ -1,it1=<1*C+ -1*G,it1=<1*E+ -1,it1=<-1*G+1*A+ -1,it1=<-1*G+1*E+ -1
  with precondition: [D=1,A=E,B=F,G>=1,C>=2*G+1,A>=B+1,B>=C] 

evalrealheapsortstep1bb3in(A,B,C,D,E,F,G):[[20],22]: 2+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*F,it1=<-1*G+1*B,it1=<-1*G+1*F,it1=<1*A+ -1,it1=<1*C+ -1*G,it1=<1*E+ -1,it1=<-1*G+1*A+ -1,it1=<-1*G+1*E+ -1
  with precondition: [D=0,A=E,B=F,G>=1,C>=2*G+1,A>=B+1,B>=C] 

evalrealheapsortstep1bb3in(A,B,C,D,E,F,G):[[20],23]: 1+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*F,it1=<-1*G+1*B,it1=<-1*G+1*F,it1=<1*A+ -1,it1=<1*C+ -1*G,it1=<1*E+ -1,it1=<-1*G+1*A+ -1,it1=<-1*G+1*E+ -1
  with precondition: [D=0,A=E,B=F,0>=G,C>=1,2*G+1>=0,A>=B+1,B>=C] 

Inferred cost of evalrealheapsortstep1bb6in(A,B,C,D,E,F,G): 
evalrealheapsortstep1bb6in(A,B,C,D,E,F,G):[29]: 2
  with precondition: [B=1,D=1,A>=3] 

evalrealheapsortstep1bb6in(A,B,C,D,E,F,G):[[25,27,28],29]: 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: [D=1,B>=1,A>=B+2] 

evalrealheapsortstep1bb6in(A,B,C,D,E,F,G):[[25,27,28],30]: 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: [D=1,A>=4,B>=1,A>=B+2] 

evalrealheapsortstep1bb6in(A,B,C,D,E,F,G):[[25,27,28],31]: 1+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that:it1+it2+it4=<1*A+ -1*B,it1+it2+it4=<1*E+ -1,it1+it2+it4=<1*E+ -1*B,it1+it2+it4=<1*F+ -1
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1/2,it5=<1*A+ -1
  with precondition: [D=0,A=E,A=F,A>=3,B>=1,2*G+1>=0,A>=B+1,A>=G+1] 

Inferred cost of evalrealheapsortstep1returnin(A,B,C): 
evalrealheapsortstep1returnin(A,B,C):[33]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalrealheapsortstep1bb6in(A,B,C): 
loop_cont_evalrealheapsortstep1bb6in(A,B,C):[35]: 1
  with precondition: [] 

Inferred cost of evalrealheapsortstep1entryin(A,B,C): 
evalrealheapsortstep1entryin(A,B,C):[37]: 2
  with precondition: [2>=A] 

evalrealheapsortstep1entryin(A,B,C):[38]: 3+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that: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] 

evalrealheapsortstep1entryin(A,B,C):[39]: 3
  with precondition: [A>=3] 

evalrealheapsortstep1entryin(A,B,C):[40]: 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] 

evalrealheapsortstep1entryin(A,B,C):[41]: 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] 

Inferred cost of evalrealheapsortstep1start(A,B,C): 
evalrealheapsortstep1start(A,B,C):[43]: 3
  with precondition: [2>=A] 

evalrealheapsortstep1start(A,B,C):[44]: 4+it1*(4)+it2*(4+it3*(3))+it4*(3+it5*(3))
  Such that: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] 

evalrealheapsortstep1start(A,B,C):[45]: 4
  with precondition: [A>=3] 

evalrealheapsortstep1start(A,B,C):[46]: 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] 

evalrealheapsortstep1start(A,B,C):[47]: 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] 

Solved cost expressions of evalrealheapsortstep1start(A,B,C): 
evalrealheapsortstep1start(A,B,C):[43]: 3  with precondition: [2>=A] 
evalrealheapsortstep1start(A,B,C):[44]: max([4*A+ -4, (1*A+ -1)* (3*A), (3*A+ -2)* (1*A+ -1)])+4  with precondition: [A>=3] 
evalrealheapsortstep1start(A,B,C):[45]: 4  with precondition: [A>=3] 
evalrealheapsortstep1start(A,B,C):[46]: max([4*A+ -8, (1*A+ -2)* (3*A), (3*A+ -2)* (1*A+ -2)])+4  with precondition: [A>=3] 
evalrealheapsortstep1start(A,B,C):[47]: 3*A+ -6+max([4*A+ -8, (1*A+ -2)* (3*A), (3*A+ -2)* (1*A+ -2)])+4  with precondition: [A>=4] 
Maximum cost of evalrealheapsortstep1start(A,B,C): max([4,max([4*A+ -8, (1*A+ -2)* (3*A), (3*A+ -2)* (1*A+ -2)])+4,max([4*A+ -4, (1*A+ -1)* (3*A), (3*A+ -2)* (1*A+ -1)])+4,3*A+ -6+max([4*A+ -8, (1*A+ -2)* (3*A), (3*A+ -2)* (1*A+ -2)])+4]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 15 ms.
Invariants computed in 52 ms.
----Backward Invariants 28 ms.
----Transitive Invariants 6 ms.
Refinement performed in 39 ms.
Termination proved in 13 ms.
Upper bounds computed in 135 ms.
----Phase cost structures 79 ms.
--------Equation cost structures 57 ms.
--------Inductive compression(1) 2 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 47 ms.
----Solving cost expressions 4 ms.

Compressed phase information: 4 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 288 ms.