warning: Ignored call to evalrealheapsortstep2stop/4 in equation evalrealheapsortstep2returnin/4 
Inferred cost of evalrealheapsortstep2bb9in(A,B,C,D,E,F,G,H,I): 
evalrealheapsortstep2bb9in(A,B,C,D,E,F,G,H,I):[31]: 1
  with precondition: [C=0,E=0,H=0,A=B+2,I=D,A=F,A=G+2] 

evalrealheapsortstep2bb9in(A,B,C,D,E,F,G,H,I):[[26,27,28,29,30],25,31]: 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] 

evalrealheapsortstep2bb9in(A,B,C,D,E,F,G,H,I):[[26,27,28,29,30],31]: 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] 

evalrealheapsortstep2bb9in(A,B,C,D,E,F,G,H,I):[[26,27,28,29,30],32]...: inf
  with precondition: [1>=E,E>=0,A>=B+2,A>=2*C+B+3] 

evalrealheapsortstep2bb9in(A,B,C,D,E,F,G,H,I):[25,31]: 6
  with precondition: [C=0,E=0,H=1,I=1,A=B+3,A=F,A=G+3] 

Inferred cost of evalrealheapsortstep2bb11in(A,B,C,D,E,F,G,H,I): 
evalrealheapsortstep2bb11in(A,B,C,D,E,F,G,H,I):[38]...: inf
  with precondition: [B=0,1>=E,A>=3,E>=0] 

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

evalrealheapsortstep2bb11in(A,B,C,D,E,F,G,H,I):[[34,35],33,37]: 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] 

evalrealheapsortstep2bb11in(A,B,C,D,E,F,G,H,I):[[34,35],36,33,37]: 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] 

evalrealheapsortstep2bb11in(A,B,C,D,E,F,G,H,I):[[34,35],38]...: inf
  with precondition: [1>=E,B>=0,E>=0,A>=B+4] 

evalrealheapsortstep2bb11in(A,B,C,D,E,F,G,H,I):[[34,35],39]...: inf
  with precondition: [E=1,B>=0,A>=B+4] 

evalrealheapsortstep2bb11in(A,B,C,D,E,F,G,H,I):[36,33,37]: 14
  with precondition: [A=3,B=0,E=0,F=3,G=2,H=0,I=1] 

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

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

Inferred cost of evalrealheapsortstep2bbin(A,B,C,D): 
evalrealheapsortstep2bbin(A,B,C,D):[45]: 7+it1*(inf)
  Such that:it1=<1*A+ -2
  with precondition: [A>=3] 

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

evalrealheapsortstep2bbin(A,B,C,D):[47]: 16
  with precondition: [A=3] 

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

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

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

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

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

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

Inferred cost of evalrealheapsortstep2entryin(A,B,C,D): 
evalrealheapsortstep2entryin(A,B,C,D):[55]: 8+it1*(inf)
  Such that:it1=<1*A+ -2
  with precondition: [A>=3] 

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

evalrealheapsortstep2entryin(A,B,C,D):[57]: 17
  with precondition: [A=3] 

evalrealheapsortstep2entryin(A,B,C,D):[58]: 2
  with precondition: [2>=A] 

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

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

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

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

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

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

Inferred cost of evalrealheapsortstep2start(A,B,C,D): 
evalrealheapsortstep2start(A,B,C,D):[66]: 9+it1*(inf)
  Such that:it1=<1*A+ -2
  with precondition: [A>=3] 

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

evalrealheapsortstep2start(A,B,C,D):[68]: 18
  with precondition: [A=3] 

evalrealheapsortstep2start(A,B,C,D):[69]: 3
  with precondition: [2>=A] 

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

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

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

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

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

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

Solved cost expressions of evalrealheapsortstep2start(A,B,C,D): 
evalrealheapsortstep2start(A,B,C,D):[66]: inf  with precondition: [A>=3] 
evalrealheapsortstep2start(A,B,C,D):[67]: inf  with precondition: [A>=4] 
evalrealheapsortstep2start(A,B,C,D):[68]: 18  with precondition: [A=3] 
evalrealheapsortstep2start(A,B,C,D):[69]: 3  with precondition: [2>=A] 
evalrealheapsortstep2start(A,B,C,D):[70]...: inf  with precondition: [A>=3] 
evalrealheapsortstep2start(A,B,C,D):[71]...: inf  with precondition: [A>=4] 
evalrealheapsortstep2start(A,B,C,D):[72]...: inf  with precondition: [A>=3] 
evalrealheapsortstep2start(A,B,C,D):[73]...: inf  with precondition: [A>=3] 
evalrealheapsortstep2start(A,B,C,D):[74]...: inf  with precondition: [A>=4] 
evalrealheapsortstep2start(A,B,C,D):[75]...: inf  with precondition: [A>=4] 
Maximum cost of evalrealheapsortstep2start(A,B,C,D): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 38 ms.
Invariants computed in 108 ms.
----Backward Invariants 59 ms.
----Transitive Invariants 8 ms.
Refinement performed in 81 ms.
Termination proved in 13 ms.
Upper bounds computed in 100 ms.
----Phase cost structures 33 ms.
--------Equation cost structures 32 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 58 ms.
----Solving cost expressions 1 ms.

Compressed phase information: 5 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 379 ms.