warning: Ignored call to f10/50 in equation f9/50 
warning: Ignored call to f10/50 in equation f9/50 
warning: Ignored call to f10/50 in equation f7/50 
warning: Ignored call to loop_cont_f8/50 in equation f7/50 
warning: Ignored call to loop_cont_f8/50 in equation f13/50 
warning: Ignored call to loop_cont_f8/50 in equation loop_cont_f116/50 
Warning: the following predicates are never called:[f12/50,f13/50,f7/50]
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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3): 
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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[25]: 1
  with precondition: [A=2,B=2,C=0,P=0,Q=2,T1=2,Y1=0,Z1=2,B2=0,O2=0,S3=2,C2=D,D2=E,F2=G,G2=H,H2=I,I2=J,J2=K,K2=L,L2=M,M2=N,N2=O,R=T,R=W,A3=B1,B3=C1,C3=D1,D3=E1,E3=F1,F3=G1,G3=H1,H3=I1,I3=J1,J3=K1,K3=L1,L3=M1,M3=N1,N3=O1,O3=P1,P3=Q1,Q3=R1,R3=S1,T3=U1,U3=V1,V3=W1,W3=X1,Y2=A2,F=E2,R=T2,R=U2,F>=2,Z2>=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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[26]: 0
  with precondition: [B=2,P=0,T1=2,Y1=1,A2=2,O2=0,S3=2,B2=C,C2=D,D2=E,E2=F,F2=G,G2=H,H2=I,I2=J,J2=K,K2=L,L2=M,M2=N,N2=O,A=Q,R2=S,R=T,T2=U,U2=V,R=W,W2=X,X2=Y,Y2=Z,Z2=A1,A3=B1,B3=C1,C3=D1,D3=E1,E3=F1,F3=G1,G3=H1,H3=I1,I3=J1,J3=K1,K3=L1,L3=M1,M3=N1,N3=O1,O3=P1,P3=Q1,Q3=R1,R3=S1,T3=U1,U3=V1,V3=W1,W3=X1,A=Z1,A=P2,R=Q2,R=S2,R=V2,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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[[24],25]: 1+it1*(1)
  Such that:it1=<1*A+ -1*B,it1=<1*F+ -2,it1=<1*Q+ -2,it1=<1*Z1+ -2,it1=<1*Z1+ -1*B,it1=<1*E2+ -2,it1=<1*Z2+ -2
  with precondition: [C=0,P=0,T1=2,Y1=0,B2=0,O2=0,S3=2,A=Q,R=T,A=Z1,D=C2,E=D2,F=E2,G=F2,H=G2,I=H2,J=I2,K=J2,L=K2,M=L2,N=M2,O=N2,T2=U2,A2=Y2,B1=A3,C1=B3,D1=C3,E1=D3,F1=E3,G1=F3,H1=G3,I1=H3,J1=I3,K1=J3,L1=K3,M1=L3,N1=M3,O1=N3,P1=O3,Q1=P3,R1=Q3,S1=R3,U1=T3,V1=U3,W1=V3,X1=W3,B>=2,F>=A,Z2>=A,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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[[24],26]: 0+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*A+ -1*B,it1=<1*Q+ -2,it1=<1*Z1+ -2,it1=<1*A2+ -2,it1=<1*A2+ -1*B,it1=<1*P2+ -2,it1=<1*P2+ -1*B
  with precondition: [P=0,T1=2,Y1=1,O2=0,S3=2,A=Q,R=T,A=Z1,C=B2,D=C2,E=D2,F=E2,G=F2,H=G2,I=H2,J=I2,K=J2,L=K2,M=L2,N=M2,O=N2,A=P2,Q2=S2,U=T2,V=U2,W=V2,X=W2,Y=X2,Z=Y2,A1=Z2,B1=A3,C1=B3,D1=C3,E1=D3,F1=E3,G1=F3,H1=G3,I1=H3,J1=I3,K1=J3,L1=K3,M1=L3,N1=M3,O1=N3,P1=O3,Q1=P3,R1=Q3,S1=R3,U1=T3,V1=U3,W1=V3,X1=W3,B>=2,A2>=B+1,A>=A2] 

Inferred cost of f116(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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3): 
f116(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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[29]: 1
  with precondition: [P=0,U=0,Y1=0,O2=1,T2=0,F3=0,H3=0,K3+1=0,A2=B,C2=D,D2=E,F2=G,G2=H,H2=I,I2=J,J2=K,K2=L,L2=M,M2=N,P2=Q,Q2=R,R2=S,S2=T,V2=W,W2=X,X2=Y,Y2=Z,Z2=A1,E3=F1,J3=K1,L3=M1,M3=N1,N3=O1,P3=Q1,Q3=R1,R3=S1,S3=T1,T3=U1,U3=V1,V3=W1,W3=X1,A=Z1,E1+1=B2,F=E2,F=N2,V=U2,E1=A3,V=B3,V=C3,E1=D3,V=G3,V=I3,A>=2,C>=0,F>=0,O3>=0] 

f116(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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[30]: 0
  with precondition: [Y1=1,Z1=A,A2=B,B2=C,C2=D,D2=E,E2=F,F2=G,G2=H,H2=I,I2=J,J2=K,K2=L,L2=M,M2=N,N2=O,O2=P,P2=Q,Q2=R,R2=S,S2=T,T2=U,U2=V,V2=W,W2=X,X2=Y,Y2=Z,Z2=A1,A3=B1,B3=C1,C3=D1,D3=E1,E3=F1,F3=G1,G3=H1,H3=I1,I3=J1,J3=K1,K3=L1,L3=M1,M3=N1,N3=O1,O3=P1,P3=Q1,Q3=R1,R3=S1,S3=T1,T3=U1,U3=V1,V3=W1,W3=X1] 

f116(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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[31]: 1
  with precondition: [P=1,Y1=1,O2=1,Z1=A,A2=B,B2=C,C2=D,D2=E,F2=G,G2=H,H2=I,I2=J,J2=K,K2=L,L2=M,M2=N,P2=Q,Q2=R,R2=S,S2=T,T2=U,U2=V,V2=W,W2=X,X2=Y,Y2=Z,Z2=A1,A3=B1,B3=C1,C3=D1,D3=E1,E3=F1,F3=G1,G3=H1,H3=I1,I3=J1,J3=K1,K3=L1,L3=M1,M3=N1,N3=O1,O3=P1,P3=Q1,Q3=R1,R3=S1,S3=T1,T3=U1,U3=V1,V3=W1,W3=X1,F=E2,O=N2,F>=O] 

f116(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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[28,30]: 1
  with precondition: [P=0,Y1=1,O2=1,B2=C+1,U=M1,A=Z1,B=A2,D=C2,E=D2,F=E2+1,G=F2,H=G2,I=H2,J=I2,K=J2,L=K2,M=L2,N=M2,F=N2,Q=P2,R=Q2,S=R2,T=S2,U=T2,V=U2,W=V2,X=W2,Y=X2,Z=Y2,A1=Z2,B1=A3,C1=B3,D1=C3,E1=D3,F1=E3,G1=F3,H1=G3,I1=H3,J1=I3,K1=J3,L1=K3,U=L3,B2=M3,F=N3+1,P1=O3,Q1=P3,R1=Q3,S1=R3,T1=S3,U1=T3,V1=U3,W1=V3,X1=W3,A>=2,F>=0,B2>=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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3): 
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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[34]: 1
  with precondition: [Y1=1,A2=B,B2=C,C2=D,D2=E,E2=F,F2=G,G2=H,H2=I,I2=J,J2=K,K2=L,L2=M,M2=N,N2=O,O2=P,P2=Q,Q2=R,R2=S,S2=T,T2=U,U2=V,V2=W,W2=X,Y2=Z,Z2=A1,A3=B1,G1=D1,E3=F1,J3=K1,K3=L1,L3=M1,M3=N1,N3=O1,O3=P1,P3=Q1,Q3=R1,R3=S1,S3=T1,T3=U1,U3=V1,V3=W1,W3=X1,E1=D3,E1>=0] 

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,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3):[[33],34]: 1+it1*(1)
  Such that:it1=<1*E1+1,it1=<1*E1+ -1*D3
  with precondition: [U=0,D1=0,G1=0,I1=0,Y1=1,T2=0,V=H1,V=J1,B=A2,C=B2,D=C2,E=D2,F=E2,G=F2,H=G2,I=H2,J=I2,K=J2,L=K2,M=L2,N=M2,O=N2,P=O2,Q=P2,R=Q2,S=R2,T=S2,V=U2,W=V2,X=W2,Z=Y2,A1=Z2,B1=A3,F1=E3,D3=J3,L1=K3,M1=L3,N1=M3,O1=N3,P1=O3,Q1=P3,R1=Q3,S1=R3,T1=S3,U1=T3,V1=U3,W1=V3,X1=W3,A>=2,D3>=0,E1>=D3+1] 

Inferred cost of loop_cont_f116(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): 
loop_cont_f116(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):[36]: 1
  with precondition: [G1=D1,E1>=0] 

loop_cont_f116(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):[37]: 1+it1*(1)
  Such that:it1=<1*E1,it1=<1*E1+1
  with precondition: [U=0,D1=0,G1=0,I1=0,V=H1,V=J1,A>=2,E1>=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,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): 
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,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):[39]: 2
  with precondition: [P=0,U=0,V=0,A>=2,C>=0,F>=0,E1>=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,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):[40]: 2+it1*(1)
  Such that:it1=<1*E1,it1=<1*E1+1
  with precondition: [P=0,U=0,V=0,A>=2,C>=0,F>=0,E1>=1] 

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,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):[41]: 0
  with precondition: [] 

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,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):[42]: 1
  with precondition: [P=1,F>=O] 

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,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):[43]: 1
  with precondition: [P=0,M1=U,A>=2,C>=0,F>=0] 

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,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): 
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,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):[45]: 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,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):[46]: 1
  with precondition: [S=0,W=0] 

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,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):[47]: 4
  with precondition: [C=0,S=0,W=0,F>=2,E1>=0] 

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,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):[48]: 4+it1*(1)
  Such that:it1=<1*E1,it1=<1*E1+1
  with precondition: [C=0,S=0,W=0,F>=2,E1>=1] 

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,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):[49]: 2
  with precondition: [C=0,W=S,F>=2] 

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,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):[50]: 3
  with precondition: [C=0,S=W,S=M1,F>=2] 

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,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):[51]: 4+it1*(1)
  Such that:it1=<1*F+ -2
  with precondition: [C=0,W=S,F>=3,E1>=0] 

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,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):[52]: 4+it1*(1)+it2*(1)
  Such that:it1=<1*F+ -2,it2=<1*E1,it2=<1*E1+1
  with precondition: [C=0,W=S,F>=3,E1>=1] 

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,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):[53]: 2+it1*(1)
  Such that:it1=<1*F+ -2
  with precondition: [C=0,W=S,F>=3] 

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,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):[54]: 3+it1*(1)
  Such that:it1=<1*F+ -2
  with precondition: [C=0,W=S,F>=3] 

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,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):[55]: 1
  with precondition: [W=S] 

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,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):[56]: inf
  with precondition: [W=S] 

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,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): 
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,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):[45]: 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,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):[46]: 1  with precondition: [S=0,W=0] 
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,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):[47]: 4  with precondition: [C=0,S=0,W=0,F>=2,E1>=0] 
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,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):[48]: 1*E1+4  with precondition: [C=0,S=0,W=0,F>=2,E1>=1] 
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,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):[49]: 2  with precondition: [C=0,W=S,F>=2] 
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,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):[50]: 3  with precondition: [C=0,S=W,S=M1,F>=2] 
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,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):[51]: 1*F+2  with precondition: [C=0,W=S,F>=3,E1>=0] 
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,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):[52]: 1*F+1*E1+2  with precondition: [C=0,W=S,F>=3,E1>=1] 
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,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):[53]: 1*F  with precondition: [C=0,W=S,F>=3] 
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,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):[54]: 1*F+1  with precondition: [C=0,W=S,F>=3] 
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,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):[55]: 1  with precondition: [W=S] 
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,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):[56]: inf  with precondition: [W=S] 
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,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): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 226 ms.
Invariants computed in 715 ms.
----Backward Invariants 328 ms.
----Transitive Invariants 135 ms.
Refinement performed in 1178 ms.
Termination proved in 583 ms.
Upper bounds computed in 452 ms.
----Phase cost structures 214 ms.
--------Equation cost structures 210 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 213 ms.
----Solving cost expressions 2 ms.

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