warning: Ignored call to loop_cont_f4/5 in equation loop_cont_f3/5 
Inferred cost of f1(A,B,C,D,E,F,G,H,I,J,K): 
f1(A,B,C,D,E,F,G,H,I,J,K):[26]: 1
  with precondition: [F=0,J=D,K=E,A=G,B=H,B=I,B>=A] 

f1(A,B,C,D,E,F,G,H,I,J,K):[[25],26]: 1+it1*(1)
  Such that:it1=<1*A+ -1*B,it1=<1*I+ -1*B
  with precondition: [F=0,A=G,A=H,A=I,D=J,E=K,A>=B+1] 

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

f2(A,B,C,D,E,F,G,H,I,J,K):[[28],29]: 1+it1*(1)
  Such that:it1=<1*C
  with precondition: [F=0,I=0,J=0,A=G,B=H,E=K,C>=1] 

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

f3(A,B,C,D,E,F,G,H,I,J,K):[[31],32]: 1+it1*(1)
  Such that:it1=<1*A+ -1*D,it1=<1*K+ -1*D
  with precondition: [F=0,A=G,B=H,C=I,A=J,A=K,A>=D+1] 

Inferred cost of f4(A,B,C,D,E,F,G,H,I,J,K): 
f4(A,B,C,D,E,F,G,H,I,J,K):[35]: 0
  with precondition: [F=1,G=A,H=B,I=C,J=D,K=E] 

f4(A,B,C,D,E,F,G,H,I,J,K):[[34],35]: 0+it1*(1)
  Such that:it1=<1*E,it1=<1*E+ -1*K
  with precondition: [F=1,A=G,B=H,C=I,D=J,K>=0,E>=K+1] 

Inferred cost of loop_cont_f3(A,B,C,D,E): 
loop_cont_f3(A,B,C,D,E):[37]: 0
  with precondition: [] 

loop_cont_f3(A,B,C,D,E):[38]: 0+it1*(1)
  Such that:it1=<1*E
  with precondition: [E>=1] 

Inferred cost of loop_cont_f2(A,B,C,D,E): 
loop_cont_f2(A,B,C,D,E):[40]: 1
  with precondition: [D>=A] 

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

loop_cont_f2(A,B,C,D,E):[42]: 1+it1*(1)
  Such that:it1=<1*A+ -1*D
  with precondition: [A>=D+1] 

loop_cont_f2(A,B,C,D,E):[43]: 1+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -1*D,it2=<1*A
  with precondition: [A>=1,A>=D+1] 

Inferred cost of loop_cont_f1(A,B,C,D,E): 
loop_cont_f1(A,B,C,D,E):[45]: 2
  with precondition: [0>=C,C>=A] 

loop_cont_f1(A,B,C,D,E):[46]: 2+it1*(1)
  Such that:it1=<1*A+ -1*C
  with precondition: [0>=C,A>=C+1] 

loop_cont_f1(A,B,C,D,E):[47]: 2+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -1*C,it2=<1*A
  with precondition: [0>=C,A>=1] 

loop_cont_f1(A,B,C,D,E):[48]: 2+it1*(1)
  Such that:it1=<1*C
  with precondition: [0>=A,C>=1] 

loop_cont_f1(A,B,C,D,E):[49]: 2+it1*(1)+it2*(1)
  Such that:it1=<1*C,it2=<1*A
  with precondition: [A>=1,C>=1] 

loop_cont_f1(A,B,C,D,E):[50]: 2+it1*(1)+it2*(1)+it3*(1)
  Such that:it1=<1*C,it2=<1*A,it3=<1*A
  with precondition: [A>=1,C>=1] 

Inferred cost of f0(A,B,C,D,E): 
f0(A,B,C,D,E):[52]: 4
  with precondition: [0>=B,B>=A] 

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

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

f0(A,B,C,D,E):[55]: 4+it1*(1)+it2*(1)+it3*(1)
  Such that:it1=<1*B,it2=<1*A,it2=<1*B,it3=<1*A,it3=<1*B
  with precondition: [A>=1,B>=A] 

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

f0(A,B,C,D,E):[57]: 4+it1*(1)+it2*(1)+it3*(1)
  Such that:it1=<1*A+ -1*B,it2=<1*A,it3=<1*A
  with precondition: [A>=1,A>=B+1] 

f0(A,B,C,D,E):[58]: 4+it1*(1)+it2*(1)+it3*(1)+it4*(1)
  Such that:it1=<1*A+ -1*B,it2=<1*A,it3=<1*A,it4=<1*A
  with precondition: [A>=1,A>=B+1] 

Solved cost expressions of f0(A,B,C,D,E): 
f0(A,B,C,D,E):[52]: 4  with precondition: [0>=B,B>=A] 
f0(A,B,C,D,E):[53]: 1*B+4  with precondition: [0>=A,B>=1] 
f0(A,B,C,D,E):[54]: 1*A+1*B+4  with precondition: [A>=1,B>=A] 
f0(A,B,C,D,E):[55]: 2*A+1*B+4  with precondition: [A>=1,B>=A] 
f0(A,B,C,D,E):[56]: 1*A+ -1*B+4  with precondition: [0>=A,A>=B+1] 
f0(A,B,C,D,E):[57]: 3*A+ -1*B+4  with precondition: [A>=1,A>=B+1] 
f0(A,B,C,D,E):[58]: 4*A+ -1*B+4  with precondition: [A>=1,A>=B+1] 
Maximum cost of f0(A,B,C,D,E): max([4*A+ -1*B+4,2*A+1*B+4,1*A+ -1*B+4,4,1*B+4,1*A+1*B+4,3*A+ -1*B+4]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 13 ms.
Invariants computed in 50 ms.
----Backward Invariants 24 ms.
----Transitive Invariants 9 ms.
Refinement performed in 59 ms.
Termination proved in 17 ms.
Upper bounds computed in 84 ms.
----Phase cost structures 49 ms.
--------Equation cost structures 45 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 24 ms.
----Solving cost expressions 3 ms.

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