warning: Ignored call to f19/4 in equation f15/4 
warning: Ignored call to f19/4 in equation f15/4 
warning: Ignored call to f19/4 in equation f15/4 
Inferred cost of f6(A,B,C,D,E,F,G,H,I): 
f6(A,B,C,D,E,F,G,H,I):[20]: 0
  with precondition: [A=0,B=0,E=1,F=0,G=0,H=C,I=D] 

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

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

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

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

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

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

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

f15(A,B,C,D):[25]: 1
  with precondition: [C>=A] 

f15(A,B,C,D):[26]: 1
  with precondition: [A>=C+2] 

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

loop_cont_f6(A,B,C,D):[29]: 1
  with precondition: [C>=A] 

loop_cont_f6(A,B,C,D):[30]: 1
  with precondition: [A>=C+2] 

Inferred cost of f0(A,B,C,D): 
f0(A,B,C,D):[32]: 3
  with precondition: [C+1=0] 

f0(A,B,C,D):[33]: 3
  with precondition: [0>=C+2] 

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

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

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

f0(A,B,C,D):[37]: 1
  with precondition: [] 

f0(A,B,C,D):[38]: 2
  with precondition: [C=0] 

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

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

Solved cost expressions of f0(A,B,C,D): 
f0(A,B,C,D):[32]: 3  with precondition: [C+1=0] 
f0(A,B,C,D):[33]: 3  with precondition: [0>=C+2] 
f0(A,B,C,D):[34]: 1*C+3  with precondition: [C>=1] 
f0(A,B,C,D):[35]: 1*C+3  with precondition: [C>=1] 
f0(A,B,C,D):[36]: 1*C+3  with precondition: [C>=2] 
f0(A,B,C,D):[37]: 1  with precondition: [] 
f0(A,B,C,D):[38]: 2  with precondition: [C=0] 
f0(A,B,C,D):[39]: 1*C+1  with precondition: [C>=1] 
f0(A,B,C,D):[40]: 1*C+2  with precondition: [C>=2] 
Maximum cost of f0(A,B,C,D): max([1*C+3,3]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 6 ms.
Invariants computed in 42 ms.
----Backward Invariants 28 ms.
----Transitive Invariants 2 ms.
Refinement performed in 36 ms.
Termination proved in 7 ms.
Upper bounds computed in 95 ms.
----Phase cost structures 22 ms.
--------Equation cost structures 21 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 63 ms.
----Solving cost expressions 1 ms.

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