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

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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1): 
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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1):[28]: 1
  with precondition: [Z=1,A1=A,B1=B,C1=C,D1=D,E1=E,F1=F,G1=G,J=H,I1=I,L1=L,S1=S,T1=T,U1=U,V1=V,W1=W,X1=X,Y1=Y,R=R1,R>=0,K1>=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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1):[[24,25,26,27],28]: 1+it1*(1)
  Such that:it1=<1*R+1,it1=<1*R+ -1*R1
  with precondition: [H=0,J=0,Z=1,A=A1,B=B1,C=C1,D=D1,E=E1,F=F1,G=G1,I=I1,T1=R1,U=U1,V=V1,W=W1,X=X1,Y=Y1,K1>=2,T1>=0,R>=T1+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,Y): 
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,Y):[30]: 1
  with precondition: [J=H,R>=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,Y):[31]: 1+it1*(1)
  Such that:it1=<1*R,it1=<1*R+1
  with precondition: [H=0,J=0,R>=1] 

Inferred cost of f9(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): 
f9(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):[33]: 1
  with precondition: [] 

f9(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):[34]: 1
  with precondition: [] 

f9(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):[35]: inf
  with precondition: [] 

Solved cost expressions of f9(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): 
f9(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):[33]: 1  with precondition: [] 
f9(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):[34]: 1  with precondition: [] 
f9(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):[35]: inf  with precondition: [] 
Maximum cost of f9(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): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 70 ms.
Invariants computed in 285 ms.
----Backward Invariants 126 ms.
----Transitive Invariants 58 ms.
Refinement performed in 382 ms.
Termination proved in 186 ms.
Upper bounds computed in 151 ms.
----Phase cost structures 36 ms.
--------Equation cost structures 33 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 108 ms.
----Solving cost expressions 0 ms.

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