warning: Ignored call to loop_cont_f23/7 in equation loop_cont_f12/7 
Inferred cost of f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[27]: 1
  with precondition: [E=0,H=0,M=0,J=B,K=C,N=F,O=G,A=I,D+1=L,0>=A,A>=D+1] 

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

Inferred cost of f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O): 
f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[30],31]: 1+it1*(2+it2*(1))
  Such that:it1=<2,it1=<-1*D+2
            it2=<2
  with precondition: [A=2,H=0,I=2,L=0,M=2,B=J,C=K,F=N,G=O,1>=D,D>=0] 

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

f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[33],34]: 1+it1*(1)
  Such that:it1=<1*I,it1=<1*N,it1=<1*A+ -1*F,it1=<1*N+ -1*F
  with precondition: [H=0,A=I,B=J,C=K,D=L,E+1=M,A=N,G=O,F>=0,A>=E+1,A>=F+1] 

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

f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[37],38]: 1+it1*(2+it2*(1))
  Such that:it1=<1*I,it1=<1*M,it1=<1*N,it1=<1*A+ -1*E,it1=<1*N+ -1*E
            it2=<1*A
  with precondition: [H=0,A=I,B=J,C=K,D+1=L,A=M,A=N,G=O,E>=0,A>=D+1,A>=E+1] 

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

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

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

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

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],42]: 1+it1*(2+it2*(2+it3*(1)))
  Such that:it1=<1*A+ -1*D,it1=<1*I+ -1*D
            it2=<1*A
            it3=<1*A
  with precondition: [H=1,O=0,M=A,M=I,B=J,C=K,M=L,M=N,M>=1,M>=D+1] 

f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O):[[41],43]: 1+it1*(2+it2*(2+it3*(1)))
  Such that:it1=<1*A+ -1*D,it1=<1*I+ -1*D
            it2=<1*A
            it3=<1*A
  with precondition: [H=1,O=1,L=A,L=I,B=J,C=K,L=M,L=N,L>=1,L>=D+1] 

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

loop_cont_f12(A,B,C,D,E,F,G):[46]: 1
  with precondition: [D>=A] 

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

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

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

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

Inferred cost of f0(A,B,C,D,E,F,G): 
f0(A,B,C,D,E,F,G):[52]: 3+it1*(2+it2*(1))+it3*(2+it4*(2+it5*(1)))
  Such that:it1=<2,it3=<2
            it2=<2
            it4=<2
            it5=<2
  with precondition: [] 

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

Solved cost expressions of f0(A,B,C,D,E,F,G): 
f0(A,B,C,D,E,F,G):[52]: 31  with precondition: [] 
f0(A,B,C,D,E,F,G):[53]: 31  with precondition: [] 
Maximum cost of f0(A,B,C,D,E,F,G): 31 
Asymptotic class: constant 
Time statistics: 
Partial evaluation computed in 31 ms.
Invariants computed in 134 ms.
----Backward Invariants 57 ms.
----Transitive Invariants 24 ms.
Refinement performed in 104 ms.
Termination proved in 62 ms.
Upper bounds computed in 148 ms.
----Phase cost structures 63 ms.
--------Equation cost structures 52 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 81 ms.
----Solving cost expressions 0 ms.

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