warning: Ignored call to loop_cont_f1/29 in equation f999/29 
Inferred cost of f2(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): 
f2(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):[21]: 1
  with precondition: [A=0,B=0,C=0,D1=0,E1=1,F1=1,H1=0,L1=0,I1=E,J1=F,K1=G,M1=I,N1=J,O1=K,P1=L,Q1=M,R1=N,S1=O,T1=P,U1=Q,V1=R,W1=S,X1=T,Y1=U,Z1=V,A2=W,B2=X,C2=Y,D2=Z,E2=A1,F2=B1,G2=C1,D+H=G1+1,D+H>=1] 

f2(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):[22]: 0
  with precondition: [A=0,B=0,C=0,D1=1,E1=0,F1=0,G1=0,I1=E,J1=F,K1=G,M1=I,N1=J,O1=K,P1=L,Q1=M,R1=N,S1=O,T1=P,U1=Q,V1=R,W1=S,X1=T,Y1=U,Z1=V,A2=W,B2=X,C2=Y,D2=Z,E2=A1,F2=B1,G2=C1,D=H1,H=L1,0>=D+H] 

f2(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):[23]: 1
  with precondition: [A=0,B=0,C=0,D1=0,H1=0,I1=0,J1=0,K1=0,M1=0,N1=0,P1=0,L1=H,F1=J+1,E1=L+1,S1=O,T1=P,U1=Q,V1=R,W1=S,X1=T,Y1=U,Z1=V,A2=W,B2=X,C2=Y,D2=Z,E2=A1,F2=B1,G2=C1,O1=E+K,Q1=F+M,R1=G+N,D+I=G1+1,D>=1] 

f2(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):[24]: 0
  with precondition: [A=0,B=0,C=0,D1=1,E1=0,F1=0,G1=0,I1=E,J1=F,K1=G,L1=H,M1=I,N1=J,O1=K,P1=L,Q1=M,R1=N,S1=O,T1=P,U1=Q,V1=R,W1=S,X1=T,Y1=U,Z1=V,A2=W,B2=X,C2=Y,D2=Z,E2=A1,F2=B1,G2=C1,D=H1,0>=D] 

f2(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):[25]: 1
  with precondition: [A=0,B=0,C=0,D1=0,E1=1,F1=1,H1=0,I1=0,J1=0,K1=0,L1=0,M1=0,N1=J+1,P1=L+1,S1=O,T1=P,U1=Q,V1=R,W1=S,X1=T,Y1=U,Z1=V,A2=W,B2=X,C2=Y,D2=Z,E2=A1,F2=B1,G2=C1,O1=E+K,Q1=F+M,R1=G+N,D+H+I=G1+2,D>=1,D+H+I>=2] 

f2(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):[26]: 0
  with precondition: [A=0,B=0,C=0,D1=1,E1=0,F1=0,G1=0,H1=D,I1=E,J1=F,K1=G,L1=H,M1=I,N1=J,O1=K,P1=L,Q1=M,R1=N,S1=O,T1=P,U1=Q,V1=R,W1=S,X1=T,Y1=U,Z1=V,A2=W,B2=X,C2=Y,D2=Z,E2=A1,F2=B1,G2=C1] 

f2(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):[[19,20],21]: inf
  with precondition: [A=0,B=0,C=0,D1=0,E1=1,F1=1,H1=0,L1=0,O=S1,P=T1,Q=U1,R=V1,S=W1,A1+G+N+Y=C2+E2+K1+R1,B1+F+M+X+Z=B2+D2+F2+J1+Q1,G1>=0,N1>=J,P1>=L,E+K+V+W>=A2+I1+O1+Z1] 

f2(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):[[19,20],22]: inf
  with precondition: [A=0,B=0,C=0,D1=1,E1=0,F1=0,G1=0,H=L1,O=S1,P=T1,Q=U1,R=V1,S=W1,A1+G+N+Y=C2+E2+K1+R1,B1+F+M+X+Z=B2+D2+F2+J1+Q1,0>=H+H1,N1>=J,P1>=L,E+K+V+W>=A2+I1+O1+Z1] 

f2(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):[[19,20],23]: inf
  with precondition: [A=0,B=0,C=0,D1=0,H1=0,I1=0,J1=0,K1=0,M1=0,N1=0,P1=0,H=L1,O=S1,P=T1,Q=U1,R=V1,S=W1,A1+G+N+Y=C2+E2+R1,B1+F+M+X+Z=B2+D2+F2+Q1,F1>=J+1,E1>=L+1,E+K+V+W>=A2+O1+Z1] 

f2(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):[[19,20],24]: inf
  with precondition: [A=0,B=0,C=0,D1=1,E1=0,F1=0,G1=0,H=L1,O=S1,P=T1,Q=U1,R=V1,S=W1,A1+G+N+Y=C2+E2+K1+R1,B1+F+M+X+Z=B2+D2+F2+J1+Q1,0>=H1,N1>=J,P1>=L,E+K+V+W>=A2+I1+O1+Z1] 

f2(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):[[19,20],25]: inf
  with precondition: [A=0,B=0,C=0,D1=0,E1=1,F1=1,H1=0,I1=0,J1=0,K1=0,L1=0,M1=0,O=S1,P=T1,Q=U1,R=V1,S=W1,A1+G+N+Y=C2+E2+R1,B1+F+M+X+Z=B2+D2+F2+Q1,G1>=0,N1>=J+1,P1>=L+1,E+K+V+W>=A2+O1+Z1] 

f2(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):[[19,20],26]: inf
  with precondition: [A=0,B=0,C=0,D1=1,E1=0,F1=0,G1=0,H=L1,O=S1,P=T1,Q=U1,R=V1,S=W1,A1+G+N+Y=C2+E2+K1+R1,B1+F+M+X+Z=B2+D2+F2+J1+Q1,N1>=J,P1>=L,E+K+V+W>=A2+I1+O1+Z1] 

f2(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):[[19,20],27]...: inf
  with precondition: [A=0,B=0,C=0,1>=D1,D1>=0] 

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

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

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

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

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):[42]: 0
  with precondition: [A=1,B=1,D=0,E=0,F=0,G=0,H=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,D1=1,E1=1,F1=1,H1=0,I1=0,J1=0,K1=0,L1=0,M1=0,N1=0,O1=0,P1=0,Q1=0,R1=0,S1=0,T1=0,U1=0,V1=0,W1=0,X1=0,Y1=0,Z1=0,A2=0,B2=0,C2=0,D2=0,E2=0,F2=0,G2=C1,C=G1,C>=0] 

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

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

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):[[28,29,30,31,32,33,34,35],36]: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,D1=1,A>=1,B>=1,J>=0,L>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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):[[28,29,30,31,32,33,34,35],37]: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,D1=1,A>=1,B>=1,J>=0,L>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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):[[28,29,30,31,32,33,34,35],38]: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,D1=1,A>=1,B>=1,J>=0,L>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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):[[28,29,30,31,32,33,34,35],39]: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,D1=1,A>=1,B>=1,J>=0,L>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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):[[28,29,30,31,32,33,34,35],40]: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,D1=1,A>=1,B>=1,J>=0,L>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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):[[28,29,30,31,32,33,34,35],41]: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,D1=1,A>=1,B>=1,J>=0,L>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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):[[28,29,30,31,32,33,34,35],42]: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,D1=1,H1=0,L1=0,S1=0,T1=0,U1=0,V1=0,W1=0,A>=1,B>=1,J>=0,L>=0,E1>=1,F1>=1,N1>=0,P1>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0,C2+E2+K1+R1>=A1+G+N+Y,B2+D2+F2+J1+Q1>=B1+F+M+X+Z,B2+D2+E1+F2+J1+Q1>=A+B1+F+M+X+Z,B2+D2+E1+F2+J1+P1+Q1>=A+B1+F+L+M+X+Z] 

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):[[28,29,30,31,32,33,34,35],43]...: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,1>=D1,A>=1,B>=1,J>=0,L>=0,D1>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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):[[28,29,30,31,32,33,34,35],44]...: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,D1=1,A>=1,B>=1,J>=0,L>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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):[[28,29,30,31,32,33,34,35],45]...: inf
  with precondition: [D=0,H=0,O=0,P=0,Q=0,R=0,S=0,1>=D1,A>=1,B>=1,J>=0,L>=0,D1>=0,A1+G+N+Y>=0,B1+F+M+X+Z>=0] 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Solved cost expressions of f999(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): 
f999(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):[46]: 2  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,H=1,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0] 
f999(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):[47]: 2  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,H=1,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0] 
f999(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):[48]: 2  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[49]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[50]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[51]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[52]: 1  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[53]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[54]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[55]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[56]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[57]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[58]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[59]: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[60]...: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[61]...: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[62]...: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[63]...: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[64]...: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[65]...: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[66]...: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
f999(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):[67]...: inf  with precondition: [A=0,B=0,C=0,D=0,E=0,F=0,G=0,I=0,J=0,K=0,L=0,M=0,N=0,O=0,P=0,Q=0,R=0,S=0,T=0,U=0,V=0,W=0,X=0,Y=0,Z=0,A1=0,B1=0,H>=1] 
Maximum cost of f999(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): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 139 ms.
Invariants computed in 2177 ms.
----Backward Invariants 1711 ms.
----Transitive Invariants 129 ms.
Refinement performed in 1189 ms.
Termination proved in 453 ms.
Upper bounds computed in 615 ms.
----Phase cost structures 167 ms.
--------Equation cost structures 164 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 404 ms.
----Solving cost expressions 0 ms.

Compressed phase information: 21 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 4855 ms.