warning: Ignored call to f4/24 in equation f3/24 
warning: Ignored call to f4/24 in equation f9/24 
warning: Ignored call to f4/24 in equation f9/24 
warning: Ignored call to loop_cont_f10/24 in equation f9/24 
warning: Ignored call to loop_cont_f10/24 in equation f9/24 
warning: Ignored call to loop_cont_f10/24 in equation f9/24 
warning: Ignored call to loop_cont_f10/24 in equation f9/24 
warning: Ignored call to loop_cont_f10/24 in equation loop_cont_f1/24 
Warning: the following predicates are never called:[f9/24]
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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): 
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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[20]: 0
  with precondition: [B=2,Y=1,A1=2,K=C,C1=D,D1=E,E1=F,F1=G,G1=H,H1=I,I1=J,K1=L,L1=M,M1=N,N1=O,O1=P,P1=Q,Q1=R,R1=S,S1=T,T1=U,U1=V,V1=W,W1=X,A=Z,K=B1,K=J1,A>=2] 

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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[21]: 1
  with precondition: [A=2,B=2,Y=0,O1=0,Q1=0,K=C,C1=D,D1=E,E1=F,F1=G,G1=H,H1=I,I1=J,K1=L,L1=M,U1=V,V1=W,W1=X,U+1=A1,K=B1,K=J1,K=M1,U=N1,K=P1,K=R1,K=S1,U=T1,K>=1,Z>=2] 

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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[22]: 1
  with precondition: [A=2,B=2,Y=0,O1=0,Q1=0,K=C,C1=D,D1=E,E1=F,F1=G,G1=H,H1=I,I1=J,K1=L,L1=M,U1=V,V1=W,W1=X,U+1=A1,K=B1,K=J1,K=M1,U=N1,K=P1,K=R1,K=S1,U=T1,0>=K+1,Z>=2] 

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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[19],20]: 0+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*A+ -1*B,it1=<1*Z+ -2,it1=<1*Z+ -1*B,it1=<1*A1+ -2,it1=<1*L1+ -1,it1=<1*L1+ -1*B+1
  with precondition: [Y=1,C=K,A=Z,B1=J1,A1=L1+1,N=M1,O=N1,P=O1,Q=P1,R=Q1,S=R1,T=S1,U=T1,V=U1,W=V1,X=W1,B>=2,A1>=B+1,A>=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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[19],21]: 1+it1*(1)
  Such that:it1=<1*A+ -1*B,it1=<1*L1+ -1,it1=<1*L1+ -1*B+1
  with precondition: [Y=0,O1=0,Q1=0,C=K,U+1=A1,M1=B1,M1=J1,A=L1+1,U=N1,M1=P1,M1=R1,M1=S1,U=T1,V=U1,W=V1,X=W1,B>=2,Z>=2,M1>=1,A>=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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[19],22]: 1+it1*(1)
  Such that:it1=<1*A+ -1*B,it1=<1*L1+ -1,it1=<1*L1+ -1*B+1
  with precondition: [Y=0,O1=0,Q1=0,C=K,U+1=A1,M1=B1,M1=J1,A=L1+1,U=N1,M1=P1,M1=R1,M1=S1,U=T1,V=U1,W=V1,X=W1,0>=M1+1,B>=2,Z>=2,A>=B+1] 

Inferred cost of f10(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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1): 
f10(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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[28]: 1
  with precondition: [Y=1,A1=B,B1=C,C1=D,D1=E,E1=F,F1=G,G1=H,I1=J,J1=K,K1=L,L1=M,P=N,N1=O,U1=V,V1=W,W1=X,U=T1,U>=0,Z>=2] 

f10(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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1):[[24,25,26,27],28]: 1+it1*(1)
  Such that:it1=<1*U+1,it1=<1*U+ -1*T1
  with precondition: [N=0,P=0,Y=1,D=C1,E=D1,F=E1,G=F1,H=G1,J=I1,B1=J1,L=K1,M=L1,O=N1,V1=T1,X=W1,Z>=2,A1>=2,V1>=0,U>=V1+1] 

Inferred cost of loop_cont_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): 
loop_cont_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):[30]: 1
  with precondition: [P=N,U>=0] 

loop_cont_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):[31]: 1+it1*(1)
  Such that:it1=<1*U,it1=<1*U+1
  with precondition: [N=0,P=0,U>=1] 

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

f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[34]: 1
  with precondition: [A>=2] 

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

Solved cost expressions of f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X): 
f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[33]: 1  with precondition: [0>=A] 
f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[34]: 1  with precondition: [A>=2] 
f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X):[35]: 1*A+ -1  with precondition: [A>=3] 
Maximum cost of f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X): max([1*A+ -1,1]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 72 ms.
Invariants computed in 285 ms.
----Backward Invariants 128 ms.
----Transitive Invariants 56 ms.
Refinement performed in 372 ms.
Termination proved in 163 ms.
Upper bounds computed in 129 ms.
----Phase cost structures 36 ms.
--------Equation cost structures 31 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 84 ms.
----Solving cost expressions 0 ms.

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