warning: Ignored call to loop_cont_f16/7 in equation loop_cont_f9/7 
Inferred cost of f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): 
f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[23]: 1
  with precondition: [A=0,B=0,C=0,H=0,I=0,J=0,K=0,L=0,M=E,N=F,O=G] 

f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[24]: 0
  with precondition: [A=0,B=0,H=1,I=0,J=0,K=C,L=D,M=E,N=F,O=G] 

f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[19,20],21]: 2+it1*(2)
  Such that:it1=<10,it1=<-1*A+10,it1=<-1*B+10
  with precondition: [H=0,I=0,J=10,A=B,K=L,E=M,F=N,G=O,9>=A,0>=K+1,A>=0] 

f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[19,20],22]: 2+it1*(2)
  Such that:it1=<10,it1=<-1*A+10,it1=<-1*B+10
  with precondition: [H=0,I=0,J=10,A=B,K=L,E=M,F=N,G=O,9>=A,A>=0,K>=1] 

f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[19,20],23]: 1+it1*(2)
  Such that:it1=<10,it1=<1*J,it1=<-1*A+10,it1=<-1*B+10,it1=<1*J+ -1*A,it1=<1*J+ -1*B
  with precondition: [H=0,I=0,K=0,L=0,A=B,E=M,F=N,G=O,10>=J,A>=0,J>=A+1] 

f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[19,20],24]: 0+it1*(2)
  Such that:it1=<10,it1=<1*I,it1=<1*J,it1=<-1*A+10,it1=<-1*B+10,it1=<1*J+ -1*A,it1=<1*J+ -1*B
  with precondition: [H=1,A=B,J=I,E=M,F=N,G=O,10>=J,A>=0,J>=A+1] 

Inferred cost of f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): 
f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[28]: 1
  with precondition: [H=1,J=B,K=C,L=D,M=E,N=F,O=G,A=I,A>=10] 

f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[29]: 1
  with precondition: [H=1,N=0,O=0,J=B,K=C,L=D,A=I,A=M,9>=A] 

f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[26,27],28]: 1+it1*(1)
  Such that:it1=<-1*A+10
  with precondition: [H=1,I=10,M=9,B=J,C=K,D=L,N=O,9>=A] 

f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[26,27],29]: 1+it1*(1)
  Such that:it1=<-1*A+10,it1=<1*I+ -1*A
  with precondition: [H=1,N=0,O=0,M=I,B=J,C=K,D=L,9>=M,M>=A+1] 

Inferred cost of loop_cont_f9(A,B,C,D,E,F,G): 
loop_cont_f9(A,B,C,D,E,F,G):[31]: 1
  with precondition: [A>=10] 

loop_cont_f9(A,B,C,D,E,F,G):[32]: 1
  with precondition: [9>=A] 

loop_cont_f9(A,B,C,D,E,F,G):[33]: 1+it1*(1)
  Such that:it1=<-1*A+10
  with precondition: [9>=A] 

loop_cont_f9(A,B,C,D,E,F,G):[34]: 1+it1*(1)
  Such that:it1=<-1*A+9,it1=<-1*A+10
  with precondition: [8>=A] 

Inferred cost of f0(A,B,C,D,E,F,G): 
f0(A,B,C,D,E,F,G):[36]: 3
  with precondition: [] 

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

f0(A,B,C,D,E,F,G):[38]: 3+it1*(1)
  Such that:it1=<9,it1=<10
  with precondition: [] 

f0(A,B,C,D,E,F,G):[39]: 4+it1*(2)
  Such that:it1=<10
  with precondition: [] 

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

f0(A,B,C,D,E,F,G):[41]: 4+it1*(2)+it2*(1)
  Such that:it1=<10,it2=<9,it2=<10
  with precondition: [] 

f0(A,B,C,D,E,F,G):[42]: 4+it1*(2)
  Such that:it1=<10
  with precondition: [] 

f0(A,B,C,D,E,F,G):[43]: 4+it1*(2)+it2*(1)
  Such that:it1=<10,it2=<10
  with precondition: [] 

f0(A,B,C,D,E,F,G):[44]: 4+it1*(2)+it2*(1)
  Such that:it1=<10,it2=<9,it2=<10
  with precondition: [] 

f0(A,B,C,D,E,F,G):[45]: 3+it1*(2)
  Such that:it1=<10
  with precondition: [] 

f0(A,B,C,D,E,F,G):[46]: 3+it1*(2)+it2*(1)
  Such that:it1=<10,it2=<10
  with precondition: [] 

f0(A,B,C,D,E,F,G):[47]: 3+it1*(2)+it2*(1)
  Such that:it1=<10,it2=<9,it2=<10
  with precondition: [] 

f0(A,B,C,D,E,F,G):[48]: 1
  with precondition: [] 

f0(A,B,C,D,E,F,G):[49]: 1+it1*(2)
  Such that:it1=<10
  with precondition: [] 

Solved cost expressions of f0(A,B,C,D,E,F,G): 
f0(A,B,C,D,E,F,G):[36]: 3  with precondition: [] 
f0(A,B,C,D,E,F,G):[37]: 13  with precondition: [] 
f0(A,B,C,D,E,F,G):[38]: 12  with precondition: [] 
f0(A,B,C,D,E,F,G):[39]: 24  with precondition: [] 
f0(A,B,C,D,E,F,G):[40]: 34  with precondition: [] 
f0(A,B,C,D,E,F,G):[41]: 33  with precondition: [] 
f0(A,B,C,D,E,F,G):[42]: 24  with precondition: [] 
f0(A,B,C,D,E,F,G):[43]: 34  with precondition: [] 
f0(A,B,C,D,E,F,G):[44]: 33  with precondition: [] 
f0(A,B,C,D,E,F,G):[45]: 23  with precondition: [] 
f0(A,B,C,D,E,F,G):[46]: 33  with precondition: [] 
f0(A,B,C,D,E,F,G):[47]: 32  with precondition: [] 
f0(A,B,C,D,E,F,G):[48]: 1  with precondition: [] 
f0(A,B,C,D,E,F,G):[49]: 21  with precondition: [] 
Maximum cost of f0(A,B,C,D,E,F,G): 34 
Asymptotic class: constant 
Time statistics: 
Partial evaluation computed in 21 ms.
Invariants computed in 75 ms.
----Backward Invariants 45 ms.
----Transitive Invariants 7 ms.
Refinement performed in 78 ms.
Termination proved in 21 ms.
Upper bounds computed in 97 ms.
----Phase cost structures 39 ms.
--------Equation cost structures 36 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 49 ms.
----Solving cost expressions 1 ms.

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