warning: Ignored call to f10/38 in equation f9/38 
warning: Ignored call to f10/38 in equation f9/38 
warning: Ignored call to f10/38 in equation f7/38 
warning: Ignored call to loop_cont_f8/38 in equation f7/38 
warning: Ignored call to loop_cont_f8/38 in equation f13/38 
warning: Ignored call to loop_cont_f8/38 in equation loop_cont_f16/38 
Warning: the following predicates are never called:[f12/38,f13/38,f7/38]
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): 
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):[24]: 1
  with precondition: [A=2,B=0,C=2,Q=2,L1=2,M1=0,O1=0,Y2=2,R1=E,S1=F,U1=H,V1=I,W1=J,X1=K,Y1=L,A2=N,B2=O,C2=P,R=T,H2=U,I2=V,R=W,N2=A1,O2=B1,P2=C1,Q2=D1,R2=E1,S2=F1,T2=G1,U2=H1,V2=I1,W2=J1,X2=K1,G=N1,R=Q1,G=T1,R=Z1,P1>=2,G>=P1,M2>=P1] 

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):[25]: 0
  with precondition: [A=2,L1=2,M1=1,N1=2,Y2=2,O1=B,Q1=D,R1=E,S1=F,T1=G,U1=H,V1=I,W1=J,X1=K,Y1=L,Z1=M,A2=N,B2=O,C2=P,C=Q,F2=S,R=T,H2=U,I2=V,R=W,K2=X,L2=Y,M2=Z,N2=A1,O2=B1,P2=C1,Q2=D1,R2=E1,S2=F1,T2=G1,U2=H1,V2=I1,W2=J1,X2=K1,C=P1,C=D2,R=E2,R=G2,R=J2,C>=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):[[23],24]: 1+it1*(1)
  Such that:it1=<1*C+ -2,it1=<1*Q+ -2,it1=<1*I2+ -1,it1=<1*I2+ -1*A+1
  with precondition: [B=0,L1=2,M1=0,O1=0,Y2=2,C=Q,R=T,G=N1,E=R1,F=S1,G=T1,H=U1,I=V1,J=W1,K=X1,L=Y1,Q1=Z1,N=A2,O=B2,P=C2,C=I2+1,A1=N2,B1=O2,C1=P2,D1=Q2,E1=R2,F1=S2,G1=T2,H1=U2,I1=V2,J1=W2,K1=X2,A>=2,P1>=2,C>=A+1,G>=P1,M2>=P1] 

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):[[23],25]: 0+it1*(1)
  Such that:it1=<1*C+ -2,it1=<1*Q+ -2,it1=<1*Q+ -1*A,it1=<1*N1+ -2,it1=<1*P1+ -2,it1=<1*D2+ -2,it1=<1*I2+ -1,it1=<1*I2+ -1*A+1
  with precondition: [L1=2,M1=1,Y2=2,C=Q,R=T,I2+1=N1,B=O1,C=P1,D=Q1,E=R1,F=S1,G=T1,H=U1,I=V1,J=W1,K=X1,L=Y1,M=Z1,N=A2,O=B2,P=C2,C=D2,E2=G2,W=J2,X=K2,Y=L2,Z=M2,A1=N2,B1=O2,C1=P2,D1=Q2,E1=R2,F1=S2,G1=T2,H1=U2,I1=V2,J1=W2,K1=X2,A>=2,I2>=A,C>=I2+1] 

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,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): 
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,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):[28]: 1
  with precondition: [M=0,M1=0,Z1=0,O2=0,Q2=0,N1=A,R1=E,S1=F,U1=H,V1=I,W1=J,X1=K,Y1=L,A2=N,B2=O,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,V2=I1,W2=J1,X2=K1,Y2=L1,H1+1=O1,D=Q1,G=T1,H1=N2,D=P2,D=R2,D=S2,D=T2,H1=U2,B>=0,G>=0,P1>=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,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):[29]: 0
  with precondition: [M1=1,N1=A,O1=B,P1=C,Q1=D,R1=E,S1=F,T1=G,U1=H,V1=I,W1=J,X1=K,Y1=L,Z1=M,A2=N,B2=O,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,L2=Y,M2=Z,N2=A1,O2=B1,P2=C1,Q2=D1,R2=E1,S2=F1,T2=G1,U2=H1,V2=I1,W2=J1,X2=K1,Y2=L1] 

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,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):[[27],28]: 1+it1*(1)
  Such that:it1=<1*G+1,it1=<1*G+ -1*T1
  with precondition: [M=0,M1=0,Y1=0,Z1=0,O2=0,Q2=0,A=N1,H1+1=O1,F=S1,H=U1,I=V1,J=W1,K=X1,T1=C2,Q=D2,R=E2,S=F2,T=G2,U=H2,V=I2,W=J2,X=K2,Y=L2,Z=M2,H1=N2,Q1=P2,Q1=R2,Q1=S2,Q1=T2,H1=U2,I1=V2,J1=W2,K1=X2,L1=Y2,B+G=B2+T1,B>=0,P1>=2,T1>=0,G>=T1+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,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):[[27],29]: 0+it1*(1)
  Such that:it1=<1*G+1,it1=<1*G+ -1*T1
  with precondition: [M1=1,A=N1,F=S1,H=U1,I=V1,J=W1,K=X1,M=Y1,M=Z1,O1=B2,T1=C2,Q=D2,R=E2,S=F2,T=G2,U=H2,V=I2,W=J2,X=K2,Y=L2,Z=M2,A1=N2,B1=O2,C1=P2,D1=Q2,E1=R2,F1=S2,G1=T2,H1=U2,I1=V2,J1=W2,K1=X2,L1=Y2,B>=0,P1>=2,T1+1>=0,O1>=B+1,G>=T1+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): 
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):[32]: 1
  with precondition: [M1=1,N1=A,O1=B,Q1=D,R1=E,S1=F,T1=G,U1=H,V1=I,W1=J,X1=K,Y1=L,Z1=M,A2=N,B2=O,C2=P,D2=Q,E2=R,F2=S,G2=T,H2=U,I2=V,J2=W,K2=X,M2=Z,N2=A1,G1=B1,V2=I1,W2=J1,X2=K1,Y2=L1,H1=U2,H1>=0,P1>=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,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):[[31],32]: 1+it1*(1)
  Such that:it1=<1*H1+1,it1=<1*H1+ -1*U2
  with precondition: [B1=0,G1=0,M1=1,Z1=0,A=N1,B=O1,F=S1,G=T1,H=U1,I=V1,J=W1,K=X1,L=Y1,N=A2,O=B2,P=C2,Q=D2,R=E2,S=F2,T=G2,U=H2,V=I2,W=J2,X=K2,Z=M2,A1=N2,V2=U2,J1=W2,K1=X2,L1=Y2,P1>=2,V2>=0,H1>=V2+1] 

Inferred cost of loop_cont_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,D1,E1,F1,G1,H1,I1,J1,K1,L1): 
loop_cont_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,D1,E1,F1,G1,H1,I1,J1,K1,L1):[34]: 1
  with precondition: [G1=B1,H1>=0] 

loop_cont_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,D1,E1,F1,G1,H1,I1,J1,K1,L1):[35]: 1+it1*(1)
  Such that:it1=<1*H1,it1=<1*H1+1
  with precondition: [B1=0,G1=0,H1>=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): 
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):[37]: 2
  with precondition: [D=0,M=0,B>=0,G>=0,H1>=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):[38]: 2+it1*(1)
  Such that:it1=<1*H1,it1=<1*H1+1
  with precondition: [D=0,M=0,B>=0,G>=0,H1>=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):[39]: 2+it1*(1)
  Such that:it1=<1*G,it1=<1*G+1
  with precondition: [M=0,B>=0,G>=1,H1>=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):[40]: 2+it1*(1)+it2*(1)
  Such that:it1=<1*G,it1=<1*G+1,it2=<1*H1,it2=<1*H1+1
  with precondition: [M=0,B>=0,G>=1,H1>=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):[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):[42]: 0+it1*(1)
  Such that:it1=<1*G+1
  with precondition: [B>=0,G>=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): 
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):[44]: 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):[45]: 1
  with precondition: [S=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):[46]: 4
  with precondition: [B=0,G>=2,H1>=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):[47]: 4+it1*(1)
  Such that:it1=<1*H1,it1=<1*H1+1
  with precondition: [B=0,G>=2,H1>=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):[48]: 4+it1*(1)
  Such that:it1=<1*G,it1=<1*G+1
  with precondition: [B=0,G>=2,H1>=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):[49]: 4+it1*(1)+it2*(1)
  Such that:it1=<1*G,it1=<1*G+1,it2=<1*H1,it2=<1*H1+1
  with precondition: [B=0,G>=2,H1>=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):[50]: 2
  with precondition: [B=0,G>=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):[51]: 2+it1*(1)
  Such that:it1=<1*G+1
  with precondition: [B=0,G>=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):[52]: inf
  with precondition: [B=0,G>=2,H1>=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):[53]: inf
  with precondition: [B=0,G>=2,H1>=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):[54]: inf
  with precondition: [B=0,G>=2,H1>=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):[55]: inf
  with precondition: [B=0,G>=2,H1>=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):[56]: inf
  with precondition: [B=0,G>=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):[57]: inf
  with precondition: [B=0,G>=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):[58]: 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):[59]: 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,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1): 
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):[44]: 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):[45]: 1  with precondition: [S=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):[46]: 4  with precondition: [B=0,G>=2,H1>=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):[47]: 1*H1+4  with precondition: [B=0,G>=2,H1>=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):[48]: 1*G+4  with precondition: [B=0,G>=2,H1>=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):[49]: 1*G+1*H1+4  with precondition: [B=0,G>=2,H1>=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):[50]: 2  with precondition: [B=0,G>=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):[51]: 1*G+3  with precondition: [B=0,G>=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):[52]: inf  with precondition: [B=0,G>=2,H1>=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):[53]: inf  with precondition: [B=0,G>=2,H1>=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):[54]: inf  with precondition: [B=0,G>=2,H1>=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):[55]: inf  with precondition: [B=0,G>=2,H1>=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):[56]: inf  with precondition: [B=0,G>=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):[57]: inf  with precondition: [B=0,G>=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):[58]: 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):[59]: 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,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 137 ms.
Invariants computed in 585 ms.
----Backward Invariants 263 ms.
----Transitive Invariants 116 ms.
Refinement performed in 724 ms.
Termination proved in 419 ms.
Upper bounds computed in 372 ms.
----Phase cost structures 163 ms.
--------Equation cost structures 157 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 191 ms.
----Solving cost expressions 2 ms.

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