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

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

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

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

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

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

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

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

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

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

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

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

Solved cost expressions of evalfstart(A,B,C,D): 
evalfstart(A,B,C,D):[35]: 4  with precondition: [1>=B] 
evalfstart(A,B,C,D):[36]: 9/2*B+3/2+max([5/2*B+ -5/2, (9/2*B+2)* (1/2*B+ -1/2)])+4  with precondition: [B>=2] 
Maximum cost of evalfstart(A,B,C,D): max([4,9/2*B+3/2+max([5/2*B+ -5/2, (9/2*B+2)* (1/2*B+ -1/2)])+4]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 15 ms.
Invariants computed in 45 ms.
----Backward Invariants 21 ms.
----Transitive Invariants 7 ms.
Refinement performed in 37 ms.
Termination proved in 17 ms.
Upper bounds computed in 109 ms.
----Phase cost structures 51 ms.
--------Equation cost structures 40 ms.
--------Inductive compression(1) 6 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 52 ms.
----Solving cost expressions 2 ms.

Compressed phase information: 1 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 250 ms.