warning: Ignored call to loop_cont_f8/13 in equation f15/13 
warning: Ignored call to loop_cont_f1/13 in equation f13/13 
warning: Ignored call to loop_cont_f1/13 in equation f12/13 
warning: Ignored call to loop_cont_f1/13 in equation f10/13 
Warning: the following predicates are never called:[f10/13,f12/13,f12/27,f13/13]
Inferred cost of f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): 
f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[15]: 2
  with precondition: [H=0,J=0,K=0,N=0,V=1,X=1,Y=1,R=D,B+1=E,U=G,W=I,Z=L,A+1=O,B+1=P,B+1=S,M=A1,M>=5,B>=A+1] 

f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[[13],16]...: inf
  with precondition: [H=0,J=0,K=0,4>=M,1>=N,N>=0,B>=A+1,E>=B+1] 

f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[[14],15]: 2+it1*(2)
  Such that:it1=<-1*A+1*S+ -2,it1=<-1*O+1*E+ -1,it1=<-1*O+1*S+ -1,it1=<1*S+ -1*B+ -1
  with precondition: [H=0,J=0,K=0,N=0,V=1,X=1,Y=1,S=E,A+1=O,S=P,D=R,I=W,L=Z,M=A1,M>=5,B>=A+1,S>=B+2] 

Inferred cost of f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1): 
f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[20]: 1
  with precondition: [N=1,R=D,S=E,T=F,U=G,V=H,W=I,X=J,Y=K,Z=L,A1=M,A=O,B=P,A>=B] 

f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[21]...: inf
  with precondition: [4>=M,1>=N,N>=0,B>=A+1,E>=B+1] 

f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[22]...: inf
  with precondition: [N=1,4>=M,B>=A+1,E>=B+1] 

f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[[17],20]: 1+it1*(1)
  Such that:it1=<1*B+ -1*A
  with precondition: [N=1,P=B,P=O,D=R,E=S,F=T,G=U,H=V,I=W,J=X,K=Y,L=Z,M=A1,P>=A+1,P>=E] 

f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[18,[17],20]: 4+it1*(1)
  Such that:it1=<1*E+ -1*A+ -1
  with precondition: [N=1,V=1,X=1,Y=1,O=B+1,O=E,O=P,D=R,O=S,I=W,L=Z,M=A1,M>=5,O>=A+2] 

f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1):[19,[17],20]: 4+it1*(1)+it2*(2)
  Such that:it1=<1*O+ -1*A+ -1,it2=<-1*A+1*S+ -2,it2=<1*O+ -1*A+ -2,it2=<1*S+ -1*B+ -1
  with precondition: [N=1,V=1,X=1,Y=1,E=O,E=P,D=R,E=S,I=W,L=Z,M=A1,M>=5,B>=A+1,E>=B+2] 

Inferred cost of f15(A,B,C,D,E,F,G,H,I,J,K,L,M): 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[24]: 2
  with precondition: [A>=B] 

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

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

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

f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[28]...: inf
  with precondition: [4>=M,B>=A+1,E>=B+1] 

f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[29]...: inf
  with precondition: [4>=M,B>=A+1,E>=B+1] 

f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[30]...: inf
  with precondition: [4>=M,B>=A+1,E>=B+1] 

Solved cost expressions of f15(A,B,C,D,E,F,G,H,I,J,K,L,M): 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[24]: 2  with precondition: [A>=B] 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[25]: -1*A+1*B+2  with precondition: [B>=A+1,B>=E] 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[26]: -1*A+1*B+5  with precondition: [E=B+1,M>=5,E>=A+2] 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[27]: -1*A+ -2*B+3*E+2  with precondition: [M>=5,B>=A+1,E>=B+2] 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[28]...: inf  with precondition: [4>=M,B>=A+1,E>=B+1] 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[29]...: inf  with precondition: [4>=M,B>=A+1,E>=B+1] 
f15(A,B,C,D,E,F,G,H,I,J,K,L,M):[30]...: inf  with precondition: [4>=M,B>=A+1,E>=B+1] 
Maximum cost of f15(A,B,C,D,E,F,G,H,I,J,K,L,M): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 37 ms.
Invariants computed in 154 ms.
----Backward Invariants 62 ms.
----Transitive Invariants 21 ms.
Refinement performed in 127 ms.
Termination proved in 49 ms.
Upper bounds computed in 143 ms.
----Phase cost structures 36 ms.
--------Equation cost structures 32 ms.
--------Inductive compression(1) 1 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 99 ms.
----Solving cost expressions 2 ms.

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