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

evalfbb3in(A,B,C,D,E,F,G,H,I):[[15,16],17]: 2+it1*(4)+it2*(4)
  Such that:it1=<nat(min([1*G,1*B+ -1*D,1*G+ -1*D]))*min([1*A,1*F,1*B+ -1,1*G+ -1])+min([1*F,1*A+ -1*C,1*B+ -1,1*F+ -1*C,1*G+ -1]),it1=<nat(min([1*G,1*B+ -1*D,1*G+ -1*D]))*min([1*B+ -1,1*G+ -1])+min([1*B+ -1,1*G+ -1,1*G+ -1*C+ -1]),it2=<1*G,it2=<1*I,it2=<1*B+ -1,it2=<1*B+ -1*D,it2=<1*G+ -1,it2=<1*G+ -1*D,it2=<1*I+ -1*D,it2=<nat(min([1*G,1*B+ -1*D,1*G+ -1*D]))*min([1*A,1*F,1*B+ -1,1*G+ -1])+min([1*F,1*A+ -1*C,1*B+ -1,1*F+ -1*C,1*G+ -1])+1*C
  with precondition: [E=0,A=F,B=G,A>=1,C>=0,D>=0,B>=A+1,I>=D,A>=H,B>=I+1,H+I>=D+1] 

evalfbb3in(A,B,C,D,E,F,G,H,I):[[15,16],18]: 1+it1*(4)+it2*(4)
  Such that:it1=<nat(min([1*G,1*I,1*B+ -1*D,1*G+ -1*D]))*min([1*A,1*F,1*B+ -1,1*G+ -1,1*I+ -1])+min([1*F,1*A+ -1*C,1*B+ -1,1*F+ -1*C,1*G+ -1,1*I+ -1]),it1=<nat(min([1*G,1*I,1*B+ -1*D,1*G+ -1*D]))*min([1*B+ -1,1*G+ -1,1*I+ -1])+min([1*B+ -1,1*G+ -1,1*I+ -1,1*G+ -1*C+ -1]),it2=<1*G,it2=<1*I,it2=<1*B+ -1*D,it2=<1*G+ -1*D,it2=<1*I+ -1*D,it2=<-1*H+2*G+ -2,it2=<nat(min([1*G,1*I,1*B+ -1*D,1*G+ -1*D]))*min([1*A,1*F,1*B+ -1,1*G+ -1,1*I+ -1])+min([1*F,1*A+ -1*C,1*B+ -1,1*F+ -1*C,1*G+ -1,1*I+ -1])+1*C,it2=<-1*H+1*A+1*B+ -1,it2=<-1*H+1*B+1*F+ -1,it2=<-1*H+1*F+1*G+ -1
  with precondition: [E=0,H=0,A=F,B=G,B=I,A>=1,C>=0,D>=0,B>=A+1,B>=D+1] 

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

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

Inferred cost of evalfentryin(A,B,C,D): 
evalfentryin(A,B,C,D):[24]: 4
  with precondition: [A>=1,B>=A+1] 

evalfentryin(A,B,C,D):[25]: 4+it1*(4)+it2*(4)
  Such that:it1=<nat(min([1*B,1*B,1*B]))*min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1])+min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,min([1*A,1*B+ -1]),1*B+ -1]),it1=<nat(min([1*B,1*B,1*B]))*min([1*B+ -1,1*B+ -1])+min([1*B+ -1,1*B+ -1,1*B+ -1]),it2=<1*B,it2=<1*B+ -1,it2=<nat(min([1*B,1*B,1*B]))*min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1])+min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,min([1*A,1*B+ -1]),1*B+ -1])
  with precondition: [A>=1,B>=A+1] 

evalfentryin(A,B,C,D):[26]: 3+it1*(4)+it2*(4)
  Such that:it1=<nat(min([1*B,1*B,1*B,1*B]))*min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1,1*B+ -1])+min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1]),it1=<nat(min([1*B,1*B,1*B,1*B]))*min([1*B+ -1,1*B+ -1,1*B+ -1])+min([1*B+ -1,1*B+ -1,1*B+ -1,1*B+ -1]),it2=<1*B,it2=<2*B+ -2,it2=<nat(min([1*B,1*B,1*B,1*B]))*min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1,1*B+ -1])+min([min([1*A,1*B+ -1]),min([1*A,1*B+ -1]),1*B+ -1,min([1*A,1*B+ -1]),1*B+ -1,1*B+ -1]),it2=<1*A+1*B+ -1
  with precondition: [A>=1,B>=A+1] 

Inferred cost of evalfstart(A,B,C,D): 
evalfstart(A,B,C,D):[28]: 5
  with precondition: [A>=1,B>=A+1] 

evalfstart(A,B,C,D):[29]: 5+it1*(4)+it2*(4)
  Such that:it1=<nat(min([1*B,1*B,1*B]))*min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1])+min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1]),it1=<nat(min([1*B,1*B,1*B]))*min([1*B+ -1,1*B+ -1])+min([1*B+ -1,1*B+ -1,1*B+ -1]),it2=<1*B,it2=<1*B+ -1,it2=<nat(min([1*B,1*B,1*B]))*min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1])+min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1])
  with precondition: [A>=1,B>=A+1] 

evalfstart(A,B,C,D):[30]: 4+it1*(4)+it2*(4)
  Such that:it1=<nat(min([1*B,1*B,1*B,1*B]))*min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1,1*B+ -1])+min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1]),it1=<nat(min([1*B,1*B,1*B,1*B]))*min([1*B+ -1,1*B+ -1,1*B+ -1])+min([1*B+ -1,1*B+ -1,1*B+ -1,1*B+ -1]),it2=<1*B,it2=<2*B+ -2,it2=<nat(min([1*B,1*B,1*B,1*B]))*min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1,1*B+ -1])+min([min([min([1*A,1*B+ -1]),1*B+ -1]),min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,min([min([1*A,1*B+ -1]),1*B+ -1]),1*B+ -1,1*B+ -1]),it2=<1*A+1*B+ -1
  with precondition: [A>=1,B>=A+1] 

Solved cost expressions of evalfstart(A,B,C,D): 
evalfstart(A,B,C,D):[28]: 5  with precondition: [A>=1,B>=A+1] 
evalfstart(A,B,C,D):[29]: nat(min([1*B* (1*A)+1*A,1*B+ -1+ (1*B+ -1)* (1*B)]))*4+nat(min([1*B+ -1,1*B* (1*A)+1*A]))*4+5  with precondition: [A>=1,B>=A+1] 
evalfstart(A,B,C,D):[30]: nat(min([1*B* (1*A)+1*A,1*B+ -1+ (1*B+ -1)* (1*B)]))*4+nat(min([1*B,1*B* (1*A)+1*A]))*4+4  with precondition: [A>=1,B>=A+1] 
Maximum cost of evalfstart(A,B,C,D): max([5,nat(min([1*B* (1*A)+1*A,1*B+ -1+ (1*B+ -1)* (1*B)]))*4+nat(min([1*B,1*B* (1*A)+1*A]))*4+4,nat(min([1*B* (1*A)+1*A,1*B+ -1+ (1*B+ -1)* (1*B)]))*4+nat(min([1*B+ -1,1*B* (1*A)+1*A]))*4+5]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 13 ms.
Invariants computed in 31 ms.
----Backward Invariants 16 ms.
----Transitive Invariants 4 ms.
Refinement performed in 25 ms.
Termination proved in 9 ms.
Upper bounds computed in 195 ms.
----Phase cost structures 89 ms.
--------Equation cost structures 85 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 93 ms.
----Solving cost expressions 7 ms.

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