WARNING: Excluded non-linear constraints:[M1=L1*L1,N1=J+L1*L1]
WARNING: Excluded non-linear constraints:[M1=L1*L1,N1=J+L1*L1]
WARNING: Excluded non-linear constraints:[N1=J+L1*M1]
WARNING: Excluded non-linear constraints:[J>=U*V,U*V+U>=J+1,J>=V*W,V*W+W>=J+1]
warning: Ignored call to loop_cont_f5/18 in equation f2/18 
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): 
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):[40]: 1
  with precondition: [C=0,S=0,V=0,K1=0,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,A=T,B+1=U,D=W,D>=A+1,A>=B+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):[41]: 0
  with precondition: [C=0,S=1,V=0,W=D,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,B=U,A>=B+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):[[38,39],40]: 1+it1*(1)
  Such that:it1=<1*W+ -1*D,it1=<1*A+ -1*D+1
  with precondition: [C=0,S=0,V=0,X=0,K1=0,A=T,B+1=U,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,0>=Y,A>=B+1,A>=D] 

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):[[38,39],41]: 0+it1*(1)
  Such that:it1=<1*W+ -1*D,it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1
  with precondition: [S=1,A=T,B=U,Y=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,C>=0,A>=B+1,X>=C,W>=D+1,A+1>=W,V>=X,V>=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,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1):[[38,39],43]: 1+it1*(1)
  Such that:it1=<1*W+ -1*D,it1=<1*A+ -1*D+1
  with precondition: [S=0,A=T,B=U,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,C>=0,V>=1,A>=B+1,X>=C,A>=D,V>=X,V>=Y] 

Inferred cost of f26(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): 
f26(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):[46]: 1
  with precondition: [S=0,U=B,V=C,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,D=W,D>=A+1] 

f26(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):[[45],46]: 1+it1*(1)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1
  with precondition: [S=0,A=T,B=U,C=V,A+1=W,E=X,F=Y,G=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,A>=D] 

Inferred cost of f32(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): 
f32(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):[51]: 1
  with precondition: [S=0,U=B,V=C,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,I1=P,J1=Q,K1=R,A=T,D=W,H1=G1,D>=A+1] 

f32(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):[52]: 1
  with precondition: [S=0,U=B,V=C,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,K1=R,A=T,D=W,H1+J1=0,D>=A+1] 

f32(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):[[48,49,50],51]: 1+it1*(1)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1
  with precondition: [S=0,A=T,B=U,C=V,A+1=W,E=X,F=Y,G=Z,K=D1,L=E1,G1=H1,P=I1,Q=J1,R=K1,A>=D] 

f32(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):[[48,49,50],52]: 1+it1*(1)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1
  with precondition: [S=0,A=T,B=U,C=V,A+1=W,E=X,F=Y,G=Z,K=D1,L=E1,M=F1,N=G1,R=K1,H1+J1=0,A>=D] 

Inferred cost of f55(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): 
f55(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):[55]: 1
  with precondition: [S=0,U=B,V=C,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,D=W,K=D1,D>=A+1,A>=K] 

f55(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):[[54],55]: 1+it1*(1)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1
  with precondition: [S=0,A=T,B=U,C=V,A+1=W,E=X,F=Y,G=Z,H=A1,I=B1,K=D1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,A>=D,A>=K] 

Inferred cost of f62(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): 
f62(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):[59]: 1
  with precondition: [S=0,U=B,V=C,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,D1=K+1,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,D=W,D>=A+1] 

f62(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):[[58],59]: 1+it1*(1)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1
  with precondition: [S=0,A=T,B=U,C=V,A+1=W,E=X,F=Y,G=Z,H=A1,I=B1,J=C1,K+1=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,A>=D] 

Inferred cost of f52(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): 
f52(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):[63]: 1
  with precondition: [S=0,U=B+1,V=C,W=D,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,K=D1,K>=A+1] 

f52(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):[[61],63]: 1+it1*(3)
  Such that:it1=<1*W+ -1*K,it1=<1*D1+ -1*K,it1=<1*A+ -1*K+1
  with precondition: [S=0,A=T,B+1=U,C=V,D=W,E=X,F=Y,G=Z,H=A1,I=B1,J=C1,A+1=D1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,D>=A+1,A>=K] 

f52(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):[62,[61],63]: 4+it1*(3)+it2*(1)
  Such that:it1=<1*A+ -1*K,it1=<1*D1+ -1*K+ -1,it2=<1*A+ -1*D+1,it2=<1*T+ -1*D+1
  with precondition: [S=0,A=T,B+1=U,C=V,A+1=W,E=X,F=Y,G=Z,H=A1,I=B1,A+1=D1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,A>=D,A>=K+1] 

f52(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):[62,63]: 4+it1*(1)
  Such that:it1=<1*W+ -1*D,it1=<1*A+ -1*D+1
  with precondition: [S=0,A=K,A=T,B+1=U,C=V,A+1=W,E=X,F=Y,G=Z,H=A1,I=B1,A+1=D1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,A>=D] 

Inferred cost of f5(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): 
f5(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):[80]: 1
  with precondition: [S=1,A>=2,A>=B+1] 

f5(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):[81]: 1+it1*(1)
  Such that:it1=<-1*D+1*A+1,it1=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,A>=B+1,A>=D] 

f5(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):[82]: 1
  with precondition: [S=1,V=C,W=D,X=E,Y=F,Z=G,A1=H,B1=I,C1=J,D1=K,E1=L,F1=M,G1=N,H1=O,I1=P,J1=Q,K1=R,A=T,B=U,A>=2,B>=A] 

f5(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):[[65,68,69,70,71],80]: 1+it1*(2)+it2*(5)+it3*(3)
  Such that:it1+it2=<1*A+ -1*B,it1+it2=<-1*B+1*A+ -1,it1+it2=<-1*B+1*D+ -2,it1+it2=<-1*B+1*D+ -1,it1+it2=<1*D+ -1*B+ -1,it3=<-1*K+1*D,it3=<1*D+ -1*K,it3=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,D>=A+1,A>=B+2] 

f5(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):[[65,68,69,70,71],82]: 1+it1*(2)+it2*(5)+it3*(3)
  Such that:it1+it2=<1*A+ -1*B,it1+it2=<1*T+ -1*B,it1+it2=<1*U+ -1*B,it1+it2=<1*W+ -1*B+ -1,it3=<1*W+ -1*K,it3=<1*D1+ -1*K,it3=<1*T+ -1*K+1
  with precondition: [S=1,V=0,K1=0,A=T,D=W,E=X,F=Y,G=Z,H=A1,I=B1,J=C1,A>=2,D>=A+1,U>=A,A>=B+1,D1>=K,A+1>=U] 

f5(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):[66,[65,68,69,70,71],80]: 3+it1*(2)+it2*(5)+it3*(3)+it4*(1)
  Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*K+1,it4=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,A>=B+3,A>=D] 

f5(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):[66,[65,68,69,70,71],82]: 3+it1*(2)+it2*(5)+it3*(3)+it4*(1)
  Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*T+ -1*B+ -1,it1+it2=<1*U+ -1*B+ -1,it3=<1*D1+ -1*K,it3=<1*T+ -1*K+1,it4=<1*W+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [S=1,V=0,X=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,0>=Y,A>=2,U>=A,A>=B+2,A>=D,D1>=K,A+1>=U] 

f5(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):[66,80]: 3+it1*(1)
  Such that:it1=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,A>=B+2,A>=D] 

f5(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):[66,82]: 3+it1*(1)
  Such that:it1=<1*W+ -1*D,it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2
  with precondition: [S=1,V=0,X=0,K1=0,A=B+1,A=T,A=U,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,0>=Y,A>=2,A>=D] 

f5(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):[67,[65,68,69,70,71],80]: 3+it1*(2)+it2*(5)+it3*(3)+it4*(1)
  Such that:it1+it2=<1*A+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*K+1,it4=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,A>=B+2,A>=D] 

f5(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):[67,[65,68,69,70,71],82]: 3+it1*(2)+it2*(5)+it3*(3)+it4*(1)
  Such that:it1+it2=<1*A+ -1*B,it1+it2=<1*T+ -1*B,it1+it2=<1*U+ -1*B,it3=<1*D1+ -1*K,it3=<1*T+ -1*K+1,it4=<1*W+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [S=1,V=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,A>=2,X>=0,U>=A,A>=B+1,A>=D,D1>=K,A+1>=U] 

f5(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):[67,80]: 3+it1*(1)
  Such that:it1=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,A>=B+1,A>=D] 

f5(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):[72,[65,68,69,70,71],80]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*K+ -4,it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<1*A+ -1*B+ -3,it1+it2+it3=<1*A+ -1*B+ -2,it4=<-1*D+1*K,it4=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,K>=A+1,A>=B+4,A>=D] 

f5(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):[72,[65,68,69,70,71],82]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*T+ -1*B+ -2,it1+it2+it3=<1*U+ -1*B+ -2,it4=<1*W+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [S=1,V=0,X=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,0>=Y,A>=2,K>=A+1,U>=A,A>=B+3,A>=D,A+1>=U] 

f5(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):[72,80]: 6+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,K>=A+1,A>=B+3,A>=D] 

f5(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):[72,82]: 6+it1*(1)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1
  with precondition: [S=1,V=0,X=0,K1=0,U=B+2,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,L=E1,G1=H1,P=I1,Q=J1,0>=Y,A>=2,K>=A+1,U>=A,A>=D,A+1>=U] 

f5(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):[73,[65,68,69,70,71],80]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -3,it1+it2+it3=<1*A+ -1*B+ -2,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,A>=B+4,A>=D,A>=K] 

f5(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):[73,[65,68,69,70,71],82]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*U+ -1*B+ -2,it1+it2+it3=<1*D1+ -1*B+ -3,it4=<1*D1+ -1*D,it4=<1*A+ -1*D+1,it5=<1*D1+ -1*K,it5=<1*A+ -1*K+1
  with precondition: [S=1,V=0,X=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,A+1=D1,0>=Y,A>=2,U>=A,A>=B+3,A>=D,A>=K,A+1>=U] 

f5(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):[73,80]: 6+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it2=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,A>=B+3,A>=D,A>=K] 

f5(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):[73,82]: 6+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1,it2=<1*A+ -1*K+1,it2=<1*T+ -1*K+1
  with precondition: [S=1,V=0,X=0,K1=0,U=B+2,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,A+1=D1,G1=H1,P=I1,Q=J1,0>=Y,A>=2,U>=A,A>=D,A>=K,A+1>=U] 

f5(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):[74,[65,68,69,70,71],80]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*K+ -4,it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<1*A+ -1*B+ -3,it1+it2+it3=<1*A+ -1*B+ -2,it4=<-1*D+1*K,it4=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,K>=A+1,A>=B+4,A>=D] 

f5(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):[74,[65,68,69,70,71],82]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*T+ -1*B+ -2,it1+it2+it3=<1*U+ -1*B+ -2,it4=<1*W+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [S=1,V=0,X=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,0>=Y,A>=2,K>=A+1,U>=A,A>=B+3,A>=D,A+1>=U] 

f5(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):[74,80]: 6+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,K>=A+1,A>=B+3,A>=D] 

f5(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):[74,82]: 6+it1*(1)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1
  with precondition: [S=1,V=0,X=0,K1=0,U=B+2,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,H1+J1=0,0>=Y,A>=2,K>=A+1,U>=A,A>=D,A+1>=U] 

f5(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):[75,[65,68,69,70,71],80]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -3,it1+it2+it3=<1*A+ -1*B+ -2,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,A>=B+4,A>=D,A>=K] 

f5(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):[75,[65,68,69,70,71],82]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*U+ -1*B+ -2,it1+it2+it3=<1*D1+ -1*B+ -3,it4=<1*D1+ -1*D,it4=<1*A+ -1*D+1,it5=<1*D1+ -1*K,it5=<1*A+ -1*K+1
  with precondition: [S=1,V=0,X=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,A+1=D1,0>=Y,A>=2,U>=A,A>=B+3,A>=D,A>=K,A+1>=U] 

f5(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):[75,80]: 6+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it2=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,A>=B+3,A>=D,A>=K] 

f5(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):[75,82]: 6+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it1=<1*T+ -1*D+1,it2=<1*A+ -1*K+1,it2=<1*T+ -1*K+1
  with precondition: [S=1,V=0,X=0,K1=0,U=B+2,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,A+1=D1,M=F1,N=G1,H1+J1=0,0>=Y,A>=2,U>=A,A>=D,A>=K,A+1>=U] 

f5(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):[76,[65,68,69,70,71],80]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<-1*B+1*K+ -2,it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*A+ -1*B+ -1,it4=<-1*D+1*K,it4=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,K>=A+1,A>=B+3,A>=D] 

f5(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):[76,[65,68,69,70,71],82]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<1*A+ -1*B+ -1,it1+it2+it3=<1*T+ -1*B+ -1,it1+it2+it3=<1*U+ -1*B+ -1,it4=<1*W+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [S=1,V=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,A>=2,X>=0,K>=A+1,U>=A,A>=B+2,A>=D,A+1>=U] 

f5(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):[76,80]: 6+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,K>=A+1,A>=B+2,A>=D] 

f5(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):[76,82]: 6+it1*(1)
  Such that:it1=<1*W+ -1*D,it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2
  with precondition: [S=1,A=B+1,A=T,A=U,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,L=E1,G1=H1,P=I1,Q=J1,R=K1,A>=2,V>=1,X>=0,K>=A+1,A>=D,V>=X,V>=Y] 

f5(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):[77,[65,68,69,70,71],80]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*A+ -1*B+ -1,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,A>=B+3,A>=D,A>=K] 

f5(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):[77,[65,68,69,70,71],82]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -1,it1+it2+it3=<1*U+ -1*B+ -1,it1+it2+it3=<1*D1+ -1*B+ -2,it4=<1*D1+ -1*D,it4=<1*A+ -1*D+1,it5=<1*D1+ -1*K,it5=<1*A+ -1*K+1
  with precondition: [S=1,V=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,A+1=D1,A>=2,X>=0,U>=A,A>=B+2,A>=D,A>=K,A+1>=U] 

f5(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):[77,80]: 6+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it2=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,A>=B+2,A>=D,A>=K] 

f5(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):[77,82]: 6+it1*(1)+it2*(3)
  Such that:it1=<1*D1+ -1*D,it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2,it2=<1*D1+ -1*K,it2=<1*A+ -1*K+1,it2=<1*B+ -1*K+2
  with precondition: [S=1,A=B+1,A=T,A=U,A+1=W,Y=Z,H=A1,I=B1,J=C1,A+1=D1,G1=H1,P=I1,Q=J1,R=K1,A>=2,V>=1,X>=0,A>=D,A>=K,V>=X,V>=Y] 

f5(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):[78,[65,68,69,70,71],80]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<-1*B+1*K+ -2,it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*A+ -1*B+ -1,it4=<-1*D+1*K,it4=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,K>=A+1,A>=B+3,A>=D] 

f5(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):[78,[65,68,69,70,71],82]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<1*A+ -1*B+ -1,it1+it2+it3=<1*T+ -1*B+ -1,it1+it2+it3=<1*U+ -1*B+ -1,it4=<1*W+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [S=1,V=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,A>=2,X>=0,K>=A+1,U>=A,A>=B+2,A>=D,A+1>=U] 

f5(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):[78,80]: 6+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*A+ -1*D+1
  with precondition: [S=1,A>=2,K>=A+1,A>=B+2,A>=D] 

f5(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):[78,82]: 6+it1*(1)
  Such that:it1=<1*W+ -1*D,it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2
  with precondition: [S=1,A=B+1,A=T,A=U,A+1=W,Y=Z,H=A1,I=B1,J=C1,K=D1,L=E1,M=F1,N=G1,R=K1,H1+J1=0,A>=2,V>=1,X>=0,K>=A+1,A>=D,V>=X,V>=Y] 

f5(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):[79,[65,68,69,70,71],80]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*A+ -1*B+ -1,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,A>=B+3,A>=D,A>=K] 

f5(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):[79,[65,68,69,70,71],82]: 6+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -1,it1+it2+it3=<1*U+ -1*B+ -1,it1+it2+it3=<1*D1+ -1*B+ -2,it4=<1*D1+ -1*D,it4=<1*A+ -1*D+1,it5=<1*D1+ -1*K,it5=<1*A+ -1*K+1
  with precondition: [S=1,V=0,K1=0,A=T,A+1=W,Y=Z,H=A1,I=B1,J=C1,A+1=D1,A>=2,X>=0,U>=A,A>=B+2,A>=D,A>=K,A+1>=U] 

f5(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):[79,80]: 6+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it2=<1*A+ -1*K+1
  with precondition: [S=1,A>=2,A>=B+2,A>=D,A>=K] 

f5(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):[79,82]: 6+it1*(1)+it2*(3)
  Such that:it1=<1*D1+ -1*D,it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2,it2=<1*D1+ -1*K,it2=<1*A+ -1*K+1,it2=<1*B+ -1*K+2
  with precondition: [S=1,A=B+1,A=T,A=U,A+1=W,Y=Z,H=A1,I=B1,J=C1,A+1=D1,M=F1,N=G1,R=K1,H1+J1=0,A>=2,V>=1,X>=0,A>=D,A>=K,V>=X,V>=Y] 

Inferred cost of f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R): 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[84]: 2
  with precondition: [A>=2,A>=B+1] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[85]: 2+it1*(1)
  Such that:it1=<1*A+ -1*D+1
  with precondition: [A>=2,A>=B+1,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[86]: 2
  with precondition: [A>=2,B>=A] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[87]: 2+it1*(2)+it2*(5)+it3*(3)
  Such that:it1+it2=<1*A+ -1*B,it1+it2=<-1*B+1*D+ -2,it1+it2=<-1*B+1*D+ -1,it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*D+ -1*B+ -2,it1+it2=<1*D+ -1*B+ -1,it3=<-1*K+1*D,it3=<1*D+ -1*K,it3=<1*A+ -1*K+1
  with precondition: [A>=2,D>=A+1,A>=B+2] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[88]: 2+it1*(2)+it2*(5)+it3*(3)
  Such that:it1+it2=<-1*B+1*D,it1+it2=<1*A+ -1*B,it1+it2=<-1*B+1*A+1,it1+it2=<-1*B+1*D+ -1,it1+it2=<1*D+ -1*B+ -1,it3=<-1*K+1*D,it3=<1*D+ -1*K,it3=<1*A+ -1*K+1
  with precondition: [A>=2,D>=A+1,A>=B+1] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[89]: 4+it1*(2)+it2*(5)+it3*(3)+it4*(1)
  Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*K+1,it4=<1*A+ -1*D+1
  with precondition: [A>=2,A>=B+3,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[90]: 4+it1*(2)+it2*(5)+it3*(3)+it4*(1)
  Such that:it1+it2=<-1*B+1*A,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*K+1,it4=<1*A+ -1*D+1
  with precondition: [A>=2,A>=B+2,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[91]: 4+it1*(1)
  Such that:it1=<1*A+ -1*D+1
  with precondition: [A>=2,A>=B+2,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[92]: 4+it1*(1)
  Such that:it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2
  with precondition: [A=B+1,A>=2,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[93]: 4+it1*(2)+it2*(5)+it3*(3)+it4*(1)
  Such that:it1+it2=<1*A+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*K+1,it4=<1*A+ -1*D+1
  with precondition: [A>=2,A>=B+2,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[94]: 4+it1*(2)+it2*(5)+it3*(3)+it4*(1)
  Such that:it1+it2=<1*A+ -1*B,it1+it2=<-1*B+1*A+1,it3=<1*A+ -1*K+1,it4=<1*A+ -1*D+1
  with precondition: [A>=2,A>=B+1,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[95]: 4+it1*(1)
  Such that:it1=<1*A+ -1*D+1
  with precondition: [A>=2,A>=B+1,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[96]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*K+ -4,it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<1*A+ -1*B+ -3,it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*K+ -1*B+ -4,it1+it2+it3=<1*K+ -1*B+ -3,it4=<-1*D+1*K,it4=<1*K+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+4,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[97]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*A+ -1,it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<-1*B+1*K+ -2,it1+it2+it3=<1*A+ -1*B+ -2,it4=<-1*D+1*K,it4=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[98]: 7+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*K+ -1*D,it1=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[99]: 7+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<-1*D+1*B+3,it1=<1*A+ -1*D+1
  with precondition: [A>=2,B+2>=A,K>=A+1,A>=B+1,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[100]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -3,it1+it2+it3=<1*A+ -1*B+ -2,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+4,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[101]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<-1*B+1*A+ -1,it1+it2+it3=<1*A+ -1*B+ -2,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[102]: 7+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it2=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[103]: 7+it1*(1)+it2*(3)
  Such that:it1=<-1*D+1*B+3,it1=<1*A+ -1*D+1,it2=<-1*K+1*B+3,it2=<1*A+ -1*K+1
  with precondition: [A>=2,B+2>=A,A>=B+1,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[104]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*K+ -4,it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<1*A+ -1*B+ -3,it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*K+ -1*B+ -4,it1+it2+it3=<1*K+ -1*B+ -3,it4=<-1*D+1*K,it4=<1*K+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+4,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[105]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*A+ -1,it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<-1*B+1*K+ -2,it1+it2+it3=<1*A+ -1*B+ -2,it4=<-1*D+1*K,it4=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[106]: 7+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*K+ -1*D,it1=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[107]: 7+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<-1*D+1*B+3,it1=<1*A+ -1*D+1
  with precondition: [A>=2,B+2>=A,K>=A+1,A>=B+1,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[108]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -3,it1+it2+it3=<1*A+ -1*B+ -2,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+4,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[109]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<-1*B+1*A+ -1,it1+it2+it3=<1*A+ -1*B+ -2,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[110]: 7+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it2=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[111]: 7+it1*(1)+it2*(3)
  Such that:it1=<-1*D+1*B+3,it1=<1*A+ -1*D+1,it2=<-1*K+1*B+3,it2=<1*A+ -1*K+1
  with precondition: [A>=2,B+2>=A,A>=B+1,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[112]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<-1*B+1*K+ -2,it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*A+ -1*B+ -1,it1+it2+it3=<1*K+ -1*B+ -3,it1+it2+it3=<1*K+ -1*B+ -2,it4=<-1*D+1*K,it4=<1*K+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[113]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*A,it1+it2+it3=<-1*B+1*K+ -2,it1+it2+it3=<-1*B+1*K+ -1,it1+it2+it3=<1*A+ -1*B+ -1,it4=<-1*D+1*K,it4=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+2,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[114]: 7+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*K+ -1*D,it1=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+2,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[115]: 7+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2
  with precondition: [A=B+1,A>=2,K>=A+1,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[116]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*A+ -1*B+ -1,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[117]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<-1*B+1*A,it1+it2+it3=<1*A+ -1*B+ -1,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+2,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[118]: 7+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it2=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+2,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[119]: 7+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2,it2=<1*A+ -1*K+1,it2=<1*B+ -1*K+2
  with precondition: [A=B+1,A>=2,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[120]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*K+ -3,it1+it2+it3=<-1*B+1*K+ -2,it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*A+ -1*B+ -1,it1+it2+it3=<1*K+ -1*B+ -3,it1+it2+it3=<1*K+ -1*B+ -2,it4=<-1*D+1*K,it4=<1*K+ -1*D,it4=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[121]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)
  Such that:it1+it2+it3=<-1*B+1*A,it1+it2+it3=<-1*B+1*K+ -2,it1+it2+it3=<-1*B+1*K+ -1,it1+it2+it3=<1*A+ -1*B+ -1,it4=<-1*D+1*K,it4=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+2,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[122]: 7+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*K+ -1*D,it1=<1*A+ -1*D+1
  with precondition: [A>=2,K>=A+1,A>=B+2,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[123]: 7+it1*(1)
  Such that:it1=<-1*D+1*K,it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2
  with precondition: [A=B+1,A>=2,K>=A+1,A>=D] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[124]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<1*A+ -1*B+ -2,it1+it2+it3=<1*A+ -1*B+ -1,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[125]: 7+it1*(2)+it2*(5)+it3*(inf)+it4*(1)+it5*(3)
  Such that:it1+it2+it3=<-1*B+1*A,it1+it2+it3=<1*A+ -1*B+ -1,it4=<1*A+ -1*D+1,it5=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+2,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[126]: 7+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it2=<1*A+ -1*K+1
  with precondition: [A>=2,A>=B+2,A>=D,A>=K] 

f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[127]: 7+it1*(1)+it2*(3)
  Such that:it1=<1*A+ -1*D+1,it1=<1*B+ -1*D+2,it2=<1*A+ -1*K+1,it2=<1*B+ -1*K+2
  with precondition: [A=B+1,A>=2,A>=D,A>=K] 

Solved cost expressions of f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R): 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[84]: 2  with precondition: [A>=2,A>=B+1] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[85]: 1*A+ -1*D+3  with precondition: [A>=2,A>=B+1,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[86]: 2  with precondition: [A>=2,B>=A] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[87]: 5*A+ -5*B+ -5+nat(1*A+ -1*K+1)*3+2  with precondition: [A>=2,D>=A+1,A>=B+2] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[88]: 5*A+ -5*B+nat(1*A+ -1*K+1)*3+2  with precondition: [A>=2,D>=A+1,A>=B+1] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[89]: 5*A+ -5*B+ -10+nat(1*A+ -1*K+1)*3+ (1*A+ -1*D+1)+4  with precondition: [A>=2,A>=B+3,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[90]: 5*A+ -5*B+ -5+nat(1*A+ -1*K+1)*3+ (1*A+ -1*D+1)+4  with precondition: [A>=2,A>=B+2,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[91]: 1*A+ -1*D+5  with precondition: [A>=2,A>=B+2,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[92]: 1*A+ -1*D+5  with precondition: [A=B+1,A>=2,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[93]: 5*A+ -5*B+ -5+nat(1*A+ -1*K+1)*3+ (1*A+ -1*D+1)+4  with precondition: [A>=2,A>=B+2,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[94]: 5*A+ -5*B+nat(1*A+ -1*K+1)*3+ (1*A+ -1*D+1)+4  with precondition: [A>=2,A>=B+1,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[95]: 1*A+ -1*D+5  with precondition: [A>=2,A>=B+1,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[96]: inf  with precondition: [A>=2,K>=A+1,A>=B+4,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[97]: inf  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[98]: 1*A+ -1*D+8  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[99]: 1*A+ -1*D+8  with precondition: [A>=2,B+2>=A,K>=A+1,A>=B+1,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[100]: inf  with precondition: [A>=2,A>=B+4,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[101]: inf  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[102]: 4*A+ -1*D+ -3*K+11  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[103]: 4*A+ -1*D+ -3*K+11  with precondition: [A>=2,B+2>=A,A>=B+1,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[104]: inf  with precondition: [A>=2,K>=A+1,A>=B+4,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[105]: inf  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[106]: 1*A+ -1*D+8  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[107]: 1*A+ -1*D+8  with precondition: [A>=2,B+2>=A,K>=A+1,A>=B+1,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[108]: inf  with precondition: [A>=2,A>=B+4,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[109]: inf  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[110]: 4*A+ -1*D+ -3*K+11  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[111]: 4*A+ -1*D+ -3*K+11  with precondition: [A>=2,B+2>=A,A>=B+1,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[112]: inf  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[113]: inf  with precondition: [A>=2,K>=A+1,A>=B+2,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[114]: 1*A+ -1*D+8  with precondition: [A>=2,K>=A+1,A>=B+2,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[115]: 1*A+ -1*D+8  with precondition: [A=B+1,A>=2,K>=A+1,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[116]: inf  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[117]: inf  with precondition: [A>=2,A>=B+2,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[118]: 4*A+ -1*D+ -3*K+11  with precondition: [A>=2,A>=B+2,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[119]: 4*A+ -1*D+ -3*K+11  with precondition: [A=B+1,A>=2,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[120]: inf  with precondition: [A>=2,K>=A+1,A>=B+3,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[121]: inf  with precondition: [A>=2,K>=A+1,A>=B+2,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[122]: 1*A+ -1*D+8  with precondition: [A>=2,K>=A+1,A>=B+2,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[123]: 1*A+ -1*D+8  with precondition: [A=B+1,A>=2,K>=A+1,A>=D] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[124]: inf  with precondition: [A>=2,A>=B+3,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[125]: inf  with precondition: [A>=2,A>=B+2,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[126]: 4*A+ -1*D+ -3*K+11  with precondition: [A>=2,A>=B+2,A>=D,A>=K] 
f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R):[127]: 4*A+ -1*D+ -3*K+11  with precondition: [A=B+1,A>=2,A>=D,A>=K] 
Maximum cost of f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 261 ms.
Invariants computed in 2000 ms.
----Backward Invariants 963 ms.
----Transitive Invariants 108 ms.
Refinement performed in 2196 ms.
Termination proved in 361 ms.
Upper bounds computed in 3379 ms.
----Phase cost structures 1622 ms.
--------Equation cost structures 1435 ms.
--------Inductive compression(1) 168 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 1653 ms.
----Solving cost expressions 44 ms.

Compressed phase information: 59 
Compressed Chains: 0 
Compressed invariants: 8 
Total analysis performed in 8660 ms.