warning: Ignored call to f13/14 in equation f300/14 
warning: Ignored call to loop_cont_f11/14 in equation loop_cont_f16/14 
Inferred cost of f16(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,B1,C1): 
f16(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,B1,C1):[18]: 1
  with precondition: [F=2,G=1,O=0,U=2,V=1,P=A,H=I,H=J,C1=N,E=T,H=W,H=X,H=Y,H=A1,H=B1,E>=0,R>=1] 

f16(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,B1,C1):[19]: 0
  with precondition: [G=1,O=1,V=1,P=A,Q=B,R=C,S=D,T=E,H=I,H=J,Z=K,A1=L,B1=M,C1=N,F=U,H=W,H=X,H=Y,F>=2] 

f16(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,B1,C1):[20]: 1
  with precondition: [F=2,G=1,O=0,U=2,V=1,P=A,H=I,H=J,C1=N,E=T,H=W,H=X,H=Y,H=A1,H=B1,0>=R+1,E>=0] 

f16(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,B1,C1):[[17],18]: 1+it1*(1)
  Such that:it1=<1*U+ -2,it1=<1*V+ -1,it1=<1*F+ -1*G+ -1,it1=<1*U+ -1*G+ -1
  with precondition: [O=0,H=I,H=J,A=P,E=T,F=U,F=V+1,W=X,W=Y,W=A1,W=B1,N=C1,E>=0,G>=1,R>=1,F>=G+2] 

f16(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,B1,C1):[[17],19]: 0+it1*(1)
  Such that:it1=<1*F+ -2,it1=<1*U+ -2,it1=<1*V+ -1,it1=<1*V+ -1*G,it1=<1*F+ -1*G+ -1,it1=<1*U+ -1*G+ -1
  with precondition: [O=1,H=I,H=J,A=P,B=Q,C=R,D=S,E=T,F=U,W=X,W=Y,K=Z,L=A1,M=B1,N=C1,E>=0,G>=1,V>=G+1,F>=V+1] 

f16(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,B1,C1):[[17],20]: 1+it1*(1)
  Such that:it1=<1*U+ -2,it1=<1*V+ -1,it1=<1*F+ -1*G+ -1,it1=<1*U+ -1*G+ -1
  with precondition: [O=0,H=I,H=J,A=P,E=T,F=U,F=V+1,W=X,W=Y,W=A1,W=B1,N=C1,0>=R+1,E>=0,G>=1,F>=G+2] 

Inferred cost of f11(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,B1,C1): 
f11(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,B1,C1):[24]: 1
  with precondition: [B=0,O=1,Q=0,R=C,S=D,T=E,U=F,V=G,W=H,X=I,Y=J,A1=L,B1=M,C1=N,A=P,A>=0] 

f11(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,B1,C1):[[22,23],24]: inf
  with precondition: [O=1,Q=0,A=P,E=T,F=U,G=V,H=W,I=X,J=Y,L=A1,M=B1,N=C1,A>=0] 

f11(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,B1,C1):[[22,23],25]...: inf
  with precondition: [1>=O,A>=0,O>=0] 

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

loop_cont_f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[27]: inf
  with precondition: [A>=0] 

loop_cont_f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[28]...: inf
  with precondition: [A>=0] 

loop_cont_f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[29]...: inf
  with precondition: [A>=0] 

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

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[32]: 3
  with precondition: [F=2,A>=0,E>=0] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[33]: inf
  with precondition: [F=2,A>=0,E>=0] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[34]: 3
  with precondition: [F=2,A>=0,E>=0] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[35]: inf
  with precondition: [F=2,A>=0,E>=0] 

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

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[37]: inf
  with precondition: [A>=0,E>=0,F>=3] 

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

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[39]: inf
  with precondition: [A>=0,E>=0,F>=3] 

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

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

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[42]...: inf
  with precondition: [F=2,A>=0,E>=0] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[43]...: inf
  with precondition: [F=2,A>=0,E>=0] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[44]...: inf
  with precondition: [F=2,A>=0,E>=0] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[45]...: inf
  with precondition: [F=2,A>=0,E>=0] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[46]...: inf
  with precondition: [A>=0,E>=0,F>=3] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[47]...: inf
  with precondition: [A>=0,E>=0,F>=3] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[48]...: inf
  with precondition: [A>=0,E>=0,F>=3] 

f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[49]...: inf
  with precondition: [A>=0,E>=0,F>=3] 

Solved cost expressions of f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N): 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[31]: 1  with precondition: [1>=F] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[32]: 3  with precondition: [F=2,A>=0,E>=0] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[33]: inf  with precondition: [F=2,A>=0,E>=0] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[34]: 3  with precondition: [F=2,A>=0,E>=0] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[35]: inf  with precondition: [F=2,A>=0,E>=0] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[36]: 1*F+1  with precondition: [A>=0,E>=0,F>=3] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[37]: inf  with precondition: [A>=0,E>=0,F>=3] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[38]: 1*F+1  with precondition: [A>=0,E>=0,F>=3] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[39]: inf  with precondition: [A>=0,E>=0,F>=3] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[40]: 1  with precondition: [F>=2] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[41]: 1*F+ -1  with precondition: [E>=0,F>=3] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[42]...: inf  with precondition: [F=2,A>=0,E>=0] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[43]...: inf  with precondition: [F=2,A>=0,E>=0] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[44]...: inf  with precondition: [F=2,A>=0,E>=0] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[45]...: inf  with precondition: [F=2,A>=0,E>=0] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[46]...: inf  with precondition: [A>=0,E>=0,F>=3] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[47]...: inf  with precondition: [A>=0,E>=0,F>=3] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[48]...: inf  with precondition: [A>=0,E>=0,F>=3] 
f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[49]...: inf  with precondition: [A>=0,E>=0,F>=3] 
Maximum cost of f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 26 ms.
Invariants computed in 124 ms.
----Backward Invariants 70 ms.
----Transitive Invariants 17 ms.
Refinement performed in 140 ms.
Termination proved in 37 ms.
Upper bounds computed in 118 ms.
----Phase cost structures 54 ms.
--------Equation cost structures 50 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 54 ms.
----Solving cost expressions 1 ms.

Compressed phase information: 3 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 501 ms.