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

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

f4(A,B,C,D,E,F,G,H,I):[[20,22],21,[16,18],26]: 4+it1*(3)+it2*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*G,it1=<1*H,it1=<1*I,it1=<1*C+ -1,it1=<1*D+ -1,it1=<1*H+ -1,it2=<-1*B+1*H,it2=<-1*G+1*H,it2=<-1*I+1*H,it2=<1*C+ -1*D+1,it2=<1*H+ -1*D+1
  with precondition: [E=1,B=G,C=H,B=I,B>=1,D>=B+1,C>=D] 

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

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

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

f4(A,B,C,D,E,F,G,H,I):[[20,22],23,[16,18],26]: 4+it1*(3)+it2*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*G,it1=<1*H,it1=<1*I,it1=<1*C+ -1,it1=<1*D+ -1,it1=<1*H+ -1,it2=<-1*B+1*H,it2=<-1*G+1*H,it2=<-1*I+1*H,it2=<1*C+ -1*D+1,it2=<1*H+ -1*D+1
  with precondition: [E=1,B=G,C=H,B=I,B>=1,D>=B+1,C>=D] 

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

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

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

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

f4(A,B,C,D,E,F,G,H,I):[21,[16,18],26]: 4+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*G,it1=<1*H,it1=<1*I,it1=<1*D+ -1
  with precondition: [E=1,B=C,B+1=D,B=G,B=H,B=I,B>=1] 

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

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

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

f4(A,B,C,D,E,F,G,H,I):[23,[16,18],26]: 4+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*G,it1=<1*H,it1=<1*I,it1=<1*D+ -1
  with precondition: [E=1,B=C,B+1=D,B=G,B=H,B=I,B>=1] 

f4(A,B,C,D,E,F,G,H,I):[23,24]: 5
  with precondition: [E=1,F=0,I=0,B=C,B+1=D,B=G,B=H,B>=1] 

f4(A,B,C,D,E,F,G,H,I):[23,26]: 4
  with precondition: [B=0,C=0,D=1,E=1,G=0,H=0,I=0,F>=1] 

Inferred cost of f0(A,B,C,D): 
f0(A,B,C,D):[28]: 3
  with precondition: [B>=0,C>=B] 

f0(A,B,C,D):[29]: 6+it1*(3)+it2*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*B+ -1,it1=<1*C+ -2,it1=<1*C+ -1,it2=<1*C+ -2,it2=<1*C+ -1*B
  with precondition: [B>=2,C>=B+1] 

f0(A,B,C,D):[30]: 5+it1*(3)+it2*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*C+ -1,it2=<1*C+ -1,it2=<1*C+ -1*B
  with precondition: [B>=1,C>=B+1] 

f0(A,B,C,D):[31]: 6+it1*(3)
  Such that:it1=<1*C+ -1,it1=<1*C+ -1*B
  with precondition: [B>=1,C>=B+1] 

f0(A,B,C,D):[32]: 5+it1*(3)
  Such that:it1=<1*C
  with precondition: [B=0,C>=1] 

f0(A,B,C,D):[33]: 6+it1*(3)+it2*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*B+ -1,it1=<1*C+ -2,it1=<1*C+ -1,it2=<1*C+ -2,it2=<1*C+ -1*B
  with precondition: [B>=2,C>=B+1] 

f0(A,B,C,D):[34]: 5+it1*(3)+it2*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*C+ -1,it2=<1*C+ -1,it2=<1*C+ -1*B
  with precondition: [B>=1,C>=B+1] 

f0(A,B,C,D):[35]: 6+it1*(3)
  Such that:it1=<1*C+ -1,it1=<1*C+ -1*B
  with precondition: [B>=1,C>=B+1] 

f0(A,B,C,D):[36]: 5+it1*(3)
  Such that:it1=<1*C
  with precondition: [B=0,C>=1] 

f0(A,B,C,D):[37]: 3+it1*(3)
  Such that:it1=<1*C,it1=<-1*B+1*C,it1=<1*C+ -1*B
  with precondition: [B>=0,C>=B+1] 

f0(A,B,C,D):[38]: 6+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*B+ -1,it1=<1*C+ -1
  with precondition: [B=C,B>=2] 

f0(A,B,C,D):[39]: 5+it1*(3)
  Such that:it1=<1*B,it1=<1*C
  with precondition: [B=C,B>=1] 

f0(A,B,C,D):[40]: 6
  with precondition: [B=C,B>=1] 

f0(A,B,C,D):[41]: 5
  with precondition: [B=0,C=0] 

f0(A,B,C,D):[42]: 6+it1*(3)
  Such that:it1=<1*B,it1=<1*C,it1=<1*B+ -1,it1=<1*C+ -1
  with precondition: [B=C,B>=2] 

f0(A,B,C,D):[43]: 5+it1*(3)
  Such that:it1=<1*B,it1=<1*C
  with precondition: [B=C,B>=1] 

f0(A,B,C,D):[44]: 6
  with precondition: [B=C,B>=1] 

f0(A,B,C,D):[45]: 5
  with precondition: [B=0,C=0] 

Solved cost expressions of f0(A,B,C,D): 
f0(A,B,C,D):[28]: 3  with precondition: [B>=0,C>=B] 
f0(A,B,C,D):[29]: 3*C+3  with precondition: [B>=2,C>=B+1] 
f0(A,B,C,D):[30]: 3*C+5  with precondition: [B>=1,C>=B+1] 
f0(A,B,C,D):[31]: -3*B+3*C+6  with precondition: [B>=1,C>=B+1] 
f0(A,B,C,D):[32]: 3*C+5  with precondition: [B=0,C>=1] 
f0(A,B,C,D):[33]: 3*C+3  with precondition: [B>=2,C>=B+1] 
f0(A,B,C,D):[34]: 3*C+5  with precondition: [B>=1,C>=B+1] 
f0(A,B,C,D):[35]: -3*B+3*C+6  with precondition: [B>=1,C>=B+1] 
f0(A,B,C,D):[36]: 3*C+5  with precondition: [B=0,C>=1] 
f0(A,B,C,D):[37]: -3*B+3*C+3  with precondition: [B>=0,C>=B+1] 
f0(A,B,C,D):[38]: 3*B+3  with precondition: [B=C,B>=2] 
f0(A,B,C,D):[39]: 3*B+5  with precondition: [B=C,B>=1] 
f0(A,B,C,D):[40]: 6  with precondition: [B=C,B>=1] 
f0(A,B,C,D):[41]: 5  with precondition: [B=0,C=0] 
f0(A,B,C,D):[42]: 3*B+3  with precondition: [B=C,B>=2] 
f0(A,B,C,D):[43]: 3*B+5  with precondition: [B=C,B>=1] 
f0(A,B,C,D):[44]: 6  with precondition: [B=C,B>=1] 
f0(A,B,C,D):[45]: 5  with precondition: [B=0,C=0] 
Maximum cost of f0(A,B,C,D): max([-3*B+3*C+6,3*C+5,3*B+5,6]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 27 ms.
Invariants computed in 191 ms.
----Backward Invariants 108 ms.
----Transitive Invariants 5 ms.
Refinement performed in 92 ms.
Termination proved in 13 ms.
Upper bounds computed in 696 ms.
----Phase cost structures 101 ms.
--------Equation cost structures 96 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 576 ms.
----Solving cost expressions 6 ms.

Compressed phase information: 27 
Compressed Chains: 0 
Compressed invariants: 2 
Total analysis performed in 1049 ms.