warning: Ignored call to end/4 in equation eval1/4 
warning: Ignored call to loop_cont_eval5/4 in equation loop_cont_eval3/4 
Inferred cost of eval3(A,B,C,D,E,F,G,H,I): 
eval3(A,B,C,D,E,F,G,H,I):[[21],22]: 1+it1*(1)
  Such that:it1=<1*H+ -1,it1=<-1/11*A+101/11,it1=<-1/11*G+1/11*F,it1=<-1/11*G+101/11,it1=<-1/11*G+111/11,it1=<1/11*F+ -1/11*A,it1=<-1/11*B+ -1*C+112/11,it1=<-1/11*F+1*H+90/11,it1=<-1/11*G+ -1*C+112/11,it1=<1/11*F+ -1/11*B+ -1*C+1,it1=<1/11*F+ -1/11*G+ -1*C+1
  with precondition: [E=0,B=G,D=I,B+11*C=A+11,B+11*H=F+11,111>=F,F>=101,F>=A+11,A>=B] 

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

eval5(A,B,C,D,E,F,G,H,I):[[25,26,27,28,29],24,30]: 2+it1*(4)+it2*(4)
  Such that:it1=<1*C+ -2,it1=<1*C+ -1,it1=<nat(-1*A+9*C+102)*max([1/9,1/9,1/9])+min([1/9*A+ -110/9,1/9*F+1*C+ -118/9,1/9*F+10/9*C+ -121/9]),it2=<9*C+ -1*A+102,it2=<9*C+1*I+ -1*A+2
  with precondition: [E=1,H=1,I+10=F,B=G,C>=2,I>=91,I+9*C+2>=A,I+10*C>=A+1] 

eval5(A,B,C,D,E,F,G,H,I):[[25,26,27,28,29],30]: 0+it1*(4)+it2*(4)
  Such that:it1=<1*C+ -1,it1=<1*C+ -1*H,it1=<nat(-1*A+9*C+102)*max([1/9,1/9,1/9])+min([1/9*A+ -110/9,-1*H+1/9*F+1*C+ -110/9,-10/9*H+1/9*F+10/9*C+ -37/3]),it2=<9*C+ -1*A+102,it2=<9*C+1*F+ -1*A+ -9*H
  with precondition: [E=1,B=G,D=I,C>=2,H>=1,C>=H] 

eval5(A,B,C,D,E,F,G,H,I):[24,30]: 2
  with precondition: [C=2,E=1,H=1,A=F+10,B=G,A=I+20,A>=111] 

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

loop_cont_eval3(A,B,C,D):[33]: 2+it1*(4)+it2*(4)
  Such that:it1=<1*C+ -2,it1=<1*C+ -1,it1=<nat(-1*A+9*C+102)*max([1/9,1/9,1/9])+min([1/9*A+ -110/9,inf,inf]),it2=<9*C+ -1*A+102
  with precondition: [C>=2] 

loop_cont_eval3(A,B,C,D):[34]: 0+it1*(4)+it2*(4)
  Such that:it1=<1*C+ -1,it1=<nat(-1*A+9*C+102)*max([1/9,1/9,1/9])+min([1/9*A+ -110/9,inf,inf]),it2=<9*C+ -1*A+102
  with precondition: [C>=2] 

loop_cont_eval3(A,B,C,D):[35]: 2
  with precondition: [C=2,A>=111] 

Inferred cost of eval1(A,B,C,D): 
eval1(A,B,C,D):[37]: 1
  with precondition: [C=1,B=A,B>=101] 

eval1(A,B,C,D):[38]: 2+it1*(1)
  Such that:it1=<-1/11*A+101/11,it1=<-1/11*A+111/11,it1=<-1/11*B+101/11,it1=<-1/11*B+111/11
  with precondition: [C=1,B=A,100>=B] 

eval1(A,B,C,D):[39]: 4+it1*(1)+it2*(4)+it3*(4)
  Such that:it1=<-1/11*A+101/11,it1=<-1/11*A+111/11,it1=<-1/11*B+101/11,it1=<-1/11*B+111/11,it2=<nat(min([-1*A+109,-1*B+109,-9/11*A+1019/11,-9/11*B+1019/11]))*max([1/9,1/9,1/9])+min([1/9,inf,inf]),it2=<-1/11*A+100/11,it2=<-1/11*A+111/11,it2=<-1/11*B+100/11,it2=<-1/11*B+111/11,it3=<-1*A+109,it3=<-1*B+109,it3=<-9/11*A+1019/11,it3=<-9/11*B+1019/11
  with precondition: [C=1,B=A,100>=B] 

eval1(A,B,C,D):[40]: 2+it1*(1)+it2*(4)+it3*(4)
  Such that:it1=<-1/11*A+101/11,it1=<-1/11*A+111/11,it1=<-1/11*B+101/11,it1=<-1/11*B+111/11,it2=<nat(min([-1*A+109,-1*B+109,-9/11*A+1019/11,-9/11*B+1019/11]))*max([1/9,1/9,1/9])+min([1/9,inf,inf]),it2=<-1/11*A+111/11,it2=<-1/11*B+111/11,it3=<-1*A+109,it3=<-1*B+109,it3=<-9/11*A+1019/11,it3=<-9/11*B+1019/11
  with precondition: [C=1,B=A,100>=B] 

eval1(A,B,C,D):[41]: 4+it1*(1)
  Such that:it1=<1,it1=<1/11
  with precondition: [A=100,B=100,C=1] 

Inferred cost of eval0(A,B,C,D): 
eval0(A,B,C,D):[43]: 2
  with precondition: [B>=101] 

eval0(A,B,C,D):[44]: 3+it1*(1)
  Such that:it1=<-1/11*B+101/11,it1=<-1/11*B+111/11
  with precondition: [100>=B] 

eval0(A,B,C,D):[45]: 5+it1*(1)+it2*(4)+it3*(4)
  Such that:it1=<-1/11*B+101/11,it1=<-1/11*B+111/11,it2=<nat(min([-1*B+109,-1*B+109,-9/11*B+1019/11,-9/11*B+1019/11]))*max([1/9,1/9,1/9])+min([1/9,inf,inf]),it2=<-1/11*B+100/11,it2=<-1/11*B+111/11,it3=<-1*B+109,it3=<-9/11*B+1019/11
  with precondition: [100>=B] 

eval0(A,B,C,D):[46]: 3+it1*(1)+it2*(4)+it3*(4)
  Such that:it1=<-1/11*B+101/11,it1=<-1/11*B+111/11,it2=<nat(min([-1*B+109,-1*B+109,-9/11*B+1019/11,-9/11*B+1019/11]))*max([1/9,1/9,1/9])+min([1/9,inf,inf]),it2=<-1/11*B+111/11,it3=<-1*B+109,it3=<-9/11*B+1019/11
  with precondition: [100>=B] 

eval0(A,B,C,D):[47]: 5+it1*(1)
  Such that:it1=<1,it1=<1/11
  with precondition: [B=100] 

Solved cost expressions of eval0(A,B,C,D): 
eval0(A,B,C,D):[43]: 2  with precondition: [B>=101] 
eval0(A,B,C,D):[44]: -1/11*B+134/11  with precondition: [100>=B] 
eval0(A,B,C,D):[45]: -1/11*B+101/11+nat(min([-1/11*B+100/11,1/9+1/9*nat(min([-9/11*B+1019/11,-1*B+109]))]))*4+nat(min([-9/11*B+1019/11,-1*B+109]))*4+5  with precondition: [100>=B] 
eval0(A,B,C,D):[46]: -1/11*B+101/11+nat(min([-1/11*B+111/11,1/9+1/9*nat(min([-9/11*B+1019/11,-1*B+109]))]))*4+nat(min([-9/11*B+1019/11,-1*B+109]))*4+3  with precondition: [100>=B] 
eval0(A,B,C,D):[47]: 56/11  with precondition: [B=100] 
Maximum cost of eval0(A,B,C,D): max([56/11,-1/11*B+134/11,-1/11*B+101/11+nat(min([-1/11*B+100/11,1/9+1/9*nat(min([-9/11*B+1019/11,-1*B+109]))]))*4+nat(min([-9/11*B+1019/11,-1*B+109]))*4+5,-1/11*B+101/11+nat(min([-1/11*B+111/11,1/9+1/9*nat(min([-9/11*B+1019/11,-1*B+109]))]))*4+nat(min([-9/11*B+1019/11,-1*B+109]))*4+3]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 30 ms.
Invariants computed in 54 ms.
----Backward Invariants 27 ms.
----Transitive Invariants 7 ms.
Refinement performed in 69 ms.
Termination proved in 18 ms.
Upper bounds computed in 256 ms.
----Phase cost structures 198 ms.
--------Equation cost structures 192 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 46 ms.
----Solving cost expressions 4 ms.

Compressed phase information: 3 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 460 ms.