warning: Ignored call to f7/5 in equation f0/5 
warning: Ignored call to f7/5 in equation f0/5 
warning: Ignored call to loop_cont_f23/5 in equation loop_cont_f15/5 
Inferred cost of f15(A,B,C,D,E,F,G,H,I,J,K): 
f15(A,B,C,D,E,F,G,H,I,J,K):[21]: 2
  with precondition: [B=0,F=0,H+1=0,K=0,A=C,J=D,A=G,A=I,100>=A,A>=1] 

f15(A,B,C,D,E,F,G,H,I,J,K):[24]: 0
  with precondition: [B=0,F=1,H=0,A=C,J=D,K=E,A=G,A=I,100>=A,A>=1] 

f15(A,B,C,D,E,F,G,H,I,J,K):[[19],21]: 2+it1*(2)
  Such that:it1=<99,it1=<100,it1=<1*A,it1=<1*C,it1=<1*G,it1=<1*I,it1=<-1*B+100,it1=<1*A+ -1,it1=<1*C+ -1,it1=<1*G+ -1,it1=<1*H+1,it1=<1*I+ -1,it1=<1*I+ -1*B,it1=<1*H+ -1*B+1
  with precondition: [F=0,K=0,A=C,A=G,A=I,D=J,100>=A,B>=0,H>=B,A>=H+2] 

f15(A,B,C,D,E,F,G,H,I,J,K):[[19],23]: 1+it1*(2)
  Such that:it1=<100,it1=<1*A,it1=<1*C,it1=<1*G,it1=<1*I,it1=<-1*B+100,it1=<1*H+1,it1=<1*I+ -1*B
  with precondition: [F=0,K=0,A=C,A=G,A=H+1,A=I,D=J,100>=A,B>=0,A>=B+1] 

f15(A,B,C,D,E,F,G,H,I,J,K):[[19],24]: 0+it1*(2)
  Such that:it1=<100,it1=<1*A,it1=<1*C,it1=<1*G,it1=<1*H,it1=<1*I,it1=<-1*B+100,it1=<1*H+ -1*B,it1=<1*I+ -1*B
  with precondition: [F=1,I=A,I=C,I=G,D=J,E=K,100>=I,B>=0,H>=B+1,I>=H] 

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

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

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

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

Inferred cost of f0(A,B,C,D,E): 
f0(A,B,C,D,E):[32]: 1
  with precondition: [] 

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

f0(A,B,C,D,E):[34]: 4
  with precondition: [] 

f0(A,B,C,D,E):[35]: 4+it1*(2)
  Such that:it1=<1,it1=<99,it1=<100
  with precondition: [] 

f0(A,B,C,D,E):[36]: 4+it1*(2)+it2*(1)
  Such that:it1=<99,it1=<100,it2=<98
  with precondition: [] 

f0(A,B,C,D,E):[37]: 3+it1*(2)
  Such that:it1=<1,it1=<100
  with precondition: [] 

f0(A,B,C,D,E):[38]: 3+it1*(2)+it2*(1)
  Such that:it1=<100,it2=<99
  with precondition: [] 

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

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

Solved cost expressions of f0(A,B,C,D,E): 
f0(A,B,C,D,E):[32]: 1  with precondition: [] 
f0(A,B,C,D,E):[33]: 1  with precondition: [] 
f0(A,B,C,D,E):[34]: 4  with precondition: [] 
f0(A,B,C,D,E):[35]: 6  with precondition: [] 
f0(A,B,C,D,E):[36]: 300  with precondition: [] 
f0(A,B,C,D,E):[37]: 5  with precondition: [] 
f0(A,B,C,D,E):[38]: 302  with precondition: [] 
f0(A,B,C,D,E):[39]: 1  with precondition: [] 
f0(A,B,C,D,E):[40]: 201  with precondition: [] 
Maximum cost of f0(A,B,C,D,E): 302 
Asymptotic class: constant 
Time statistics: 
Partial evaluation computed in 14 ms.
Invariants computed in 40 ms.
----Backward Invariants 23 ms.
----Transitive Invariants 4 ms.
Refinement performed in 41 ms.
Termination proved in 11 ms.
Upper bounds computed in 92 ms.
----Phase cost structures 41 ms.
--------Equation cost structures 39 ms.
--------Inductive compression(1) 1 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 47 ms.
----Solving cost expressions 1 ms.

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