warning: Ignored call to loop_cont_l2/4 in equation loop_cont_l1/4 
Inferred cost of l1(A,B,C,D,E,F,G,H,I): 
l1(A,B,C,D,E,F,G,H,I):[19]: 1
  with precondition: [A=0,E=0,F=0,H=0,I=D,B=G,0>=B] 

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

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

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

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

Inferred cost of l2(A,B,C,D,E,F,G,H,I): 
l2(A,B,C,D,E,F,G,H,I):[26]: 1
  with precondition: [E=1,C>=1] 

l2(A,B,C,D,E,F,G,H,I):[27]: 1+it1*(1)
  Such that:it1=<1*C
  with precondition: [E=1,C>=1] 

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

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

l2(A,B,C,D,E,F,G,H,I):[[25],27]: 1+it1*(1)+it2*(2+it3*(1))
  Such that:it1+it2=<1*C,it2=<1*C
            it3=<1*C
  with precondition: [E=1,C>=2] 

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

Inferred cost of loop_cont_l1(A,B,C,D): 
loop_cont_l1(A,B,C,D):[30]: 1
  with precondition: [C>=1] 

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

loop_cont_l1(A,B,C,D):[32]: 0
  with precondition: [] 

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

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

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

Inferred cost of l0(A,B,C,D): 
l0(A,B,C,D):[37]: 2
  with precondition: [0>=B] 

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

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

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

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

l0(A,B,C,D):[42]: 3+it1*(1)+it2*(1)+it3*(2+it4*(1))
  Such that:it1=<1*B,it2+it3=<1*B,it3=<1*B
            it4=<1*B
  with precondition: [B>=2] 

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

Solved cost expressions of l0(A,B,C,D): 
l0(A,B,C,D):[37]: 2  with precondition: [0>=B] 
l0(A,B,C,D):[38]: 1*B+3  with precondition: [B>=1] 
l0(A,B,C,D):[39]: 2*B+3  with precondition: [B>=1] 
l0(A,B,C,D):[40]: 1*B+2  with precondition: [B>=1] 
l0(A,B,C,D):[41]: (1*B+2)* (1*B+ -1)+1*B+3  with precondition: [B>=2] 
l0(A,B,C,D):[42]: 1*B+max([1*B, (1*B+2)* (1*B)])+3  with precondition: [B>=2] 
l0(A,B,C,D):[43]: (1*B+2)* (1*B)+1*B+2  with precondition: [B>=1] 
Maximum cost of l0(A,B,C,D): max([2*B+3,2,1*B+3,1*B+max([1*B, (1*B+2)* (1*B)])+3, (1*B+2)* (1*B)+1*B+2, (1*B+2)* (1*B+ -1)+1*B+3]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 9 ms.
Invariants computed in 44 ms.
----Backward Invariants 22 ms.
----Transitive Invariants 6 ms.
Refinement performed in 40 ms.
Termination proved in 12 ms.
Upper bounds computed in 69 ms.
----Phase cost structures 30 ms.
--------Equation cost structures 26 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 30 ms.
----Solving cost expressions 2 ms.

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