warning: Ignored call to evalinsertsortstop/4 in equation evalinsertsortreturnin/4 
Inferred cost of evalinsertsortbb2in(A,B,C,D,E,F,G,H,I): 
evalinsertsortbb2in(A,B,C,D,E,F,G,H,I):[20]: 2
  with precondition: [E=0,H=C,A=D+1,A=F,B=G,A=I+1,A>=1,B>=A+1] 

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

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

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

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

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

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

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

evalinsertsortbb5in(A,B,C,D,E,F,G,H,I):[[24,26,27],28]: 3+it1*(5)+it2*(5+it3*(3))+it4*(4+it5*(3))
  Such that:it1+it2+it4=<1*B+ -2,it1+it2+it4=<1*B+ -1,it1+it2+it4=<1*B+ -1*A,it1+it2+it4=<-1*A+1*B+ -1
            it3=<1*B+ -1,it3=<1*B+ -2
            it5=<1*B+ -1
  with precondition: [E=1,A>=1,B>=A+2] 

evalinsertsortbb5in(A,B,C,D,E,F,G,H,I):[[24,26,27],29]: 3+it1*(3)+it2*(5)+it3*(5+it4*(3))+it5*(4+it6*(3))
  Such that:it1=<1*B+ -2,it1=<1*B+ -1,it2+it3+it5=<1*B+ -2,it2+it3+it5=<1*B+ -1,it2+it3+it5=<1*B+ -1*A,it2+it3+it5=<-1*A+1*B+ -1
            it4=<1*B+ -1,it4=<1*B+ -2
            it6=<1*B+ -1
  with precondition: [E=1,A>=1,B>=A+2] 

evalinsertsortbb5in(A,B,C,D,E,F,G,H,I):[[24,26,27],30]: 1+it1*(5)+it2*(5+it3*(3))+it4*(4+it5*(3))
  Such that:it1+it2+it4=<1*B+ -1,it1+it2+it4=<1*F+ -1,it1+it2+it4=<1*G+ -1,it1+it2+it4=<1*G+ -1*A
            it3=<1*B+ -1,it3=<1*B+ -2
            it5=<1*B+ -1
  with precondition: [E=0,G=B,G=F,A>=1,I+1>=0,G>=A+1,G>=I+2] 

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

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

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

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

evalinsertsortentryin(A,B,C,D):[38]: 4
  with precondition: [B>=2] 

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

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

Inferred cost of evalinsertsortstart(A,B,C,D): 
evalinsertsortstart(A,B,C,D):[42]: 4
  with precondition: [1>=B] 

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

evalinsertsortstart(A,B,C,D):[44]: 5
  with precondition: [B>=2] 

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

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

Solved cost expressions of evalinsertsortstart(A,B,C,D): 
evalinsertsortstart(A,B,C,D):[42]: 4  with precondition: [1>=B] 
evalinsertsortstart(A,B,C,D):[43]: max([5*B+ -5, (3*B+ -1)* (1*B+ -1), (3*B+1)* (1*B+ -1)])+4  with precondition: [B>=2] 
evalinsertsortstart(A,B,C,D):[44]: 5  with precondition: [B>=2] 
evalinsertsortstart(A,B,C,D):[45]: max([5*B+ -10, (3*B+ -1)* (1*B+ -2), (3*B+1)* (1*B+ -2)])+5  with precondition: [B>=3] 
evalinsertsortstart(A,B,C,D):[46]: 3*B+ -6+max([5*B+ -10, (3*B+ -1)* (1*B+ -2), (3*B+1)* (1*B+ -2)])+5  with precondition: [B>=3] 
Maximum cost of evalinsertsortstart(A,B,C,D): max([5,max([5*B+ -10, (3*B+ -1)* (1*B+ -2), (3*B+1)* (1*B+ -2)])+5,max([5*B+ -5, (3*B+ -1)* (1*B+ -1), (3*B+1)* (1*B+ -1)])+4,3*B+ -6+max([5*B+ -10, (3*B+ -1)* (1*B+ -2), (3*B+1)* (1*B+ -2)])+5]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 17 ms.
Invariants computed in 56 ms.
----Backward Invariants 32 ms.
----Transitive Invariants 6 ms.
Refinement performed in 46 ms.
Termination proved in 14 ms.
Upper bounds computed in 120 ms.
----Phase cost structures 59 ms.
--------Equation cost structures 45 ms.
--------Inductive compression(1) 2 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 50 ms.
----Solving cost expressions 3 ms.

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