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]: 0 with precondition: [S=1,T=A,U=B,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] 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):[53]: 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]: 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,C=V,E=X,F=Y,G=Z,K=D1,L=E1,M=F1,N=G1,O=H1,P=I1,Q=J1,R=K1,W>=D+1,A+1>=W] 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],53]: 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):[56]: 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):[[55],56]: 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]: 3 with precondition: [S=1,A>=2,D>=A+1,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]: 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):[82]: 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):[83]: 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):[84]: 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):[85]: 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]: 3+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],83]: 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],85]: 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]: 5+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],83]: 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],85]: 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]: 5+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,83]: 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,85]: 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]: 5+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],83]: 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],85]: 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]: 5+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):[67,83]: 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]: 8+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],83]: 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],85]: 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]: 8+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,83]: 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,85]: 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]: 8+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],83]: 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],85]: 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]: 8+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,83]: 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,85]: 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]: 8+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],83]: 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],85]: 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]: 8+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,83]: 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,85]: 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]: 8+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],83]: 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],85]: 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]: 8+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,83]: 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,85]: 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]: 8+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],83]: 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],85]: 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]: 8+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,83]: 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,85]: 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]: 8+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],83]: 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],85]: 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]: 8+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,83]: 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,85]: 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]: 8+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],83]: 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],85]: 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]: 8+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,83]: 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,85]: 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]: 8+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],83]: 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],85]: 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]: 8+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,83]: 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,85]: 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):[87]: 4 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):[88]: 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):[89]: 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):[90]: 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):[91]: 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):[92]: 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):[93]: 4+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):[94]: 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):[95]: 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):[96]: 6+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):[97]: 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):[98]: 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):[99]: 6+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):[100]: 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):[101]: 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):[102]: 6+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):[103]: 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):[104]: 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):[105]: 6+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):[106]: 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):[107]: 9+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):[108]: 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):[109]: 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):[110]: 9+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):[111]: 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):[112]: 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):[113]: 9+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):[114]: 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):[115]: 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):[116]: 9+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):[117]: 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):[118]: 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):[119]: 9+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):[120]: 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):[121]: 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):[122]: 9+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):[123]: 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):[124]: 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):[125]: 9+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):[126]: 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):[127]: 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):[128]: 9+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):[129]: 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):[130]: 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):[131]: 9+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):[132]: 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):[133]: 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):[134]: 9+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):[135]: 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):[136]: 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):[137]: 9+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):[138]: 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):[139]: 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):[140]: 9+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):[141]: 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):[142]: 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):[143]: 9+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):[144]: 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):[145]: 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):[146]: 9+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):[147]: 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):[148]: 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):[149]: 9+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):[150]: 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):[151]: 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):[152]: 9+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):[153]: 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):[154]: 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):[87]: 4 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):[88]: 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):[89]: 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):[90]: 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):[91]: 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):[92]: 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):[93]: 5*A+ -5*B+ -5+nat(1*A+ -1*K+1)*3+4 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):[94]: 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):[95]: 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):[96]: 5*A+ -5*B+ -10+nat(1*A+ -1*K+1)*3+ (1*A+ -1*D+1)+6 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):[97]: 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):[98]: 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):[99]: 1*A+ -1*D+7 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):[100]: 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):[101]: 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):[102]: 5*A+ -5*B+ -5+nat(1*A+ -1*K+1)*3+ (1*A+ -1*D+1)+6 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):[103]: 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):[104]: 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):[105]: 1*A+ -1*D+7 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):[106]: 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):[107]: 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):[108]: 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):[109]: 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):[110]: 1*A+ -1*D+10 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):[111]: 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):[112]: 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):[113]: 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):[114]: 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):[115]: 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):[116]: 4*A+ -1*D+ -3*K+13 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]: 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):[118]: 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):[119]: 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):[120]: 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):[121]: 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):[122]: 1*A+ -1*D+10 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):[123]: 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):[124]: 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):[125]: 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):[126]: 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):[127]: 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):[128]: 4*A+ -1*D+ -3*K+13 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):[129]: 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):[130]: 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):[131]: 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):[132]: 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):[133]: 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):[134]: 1*A+ -1*D+10 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):[135]: 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):[136]: 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):[137]: 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):[138]: 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):[139]: 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):[140]: 4*A+ -1*D+ -3*K+13 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):[141]: 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):[142]: 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):[143]: 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):[144]: 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):[145]: 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):[146]: 1*A+ -1*D+10 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):[147]: 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):[148]: 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):[149]: 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):[150]: 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):[151]: 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):[152]: 4*A+ -1*D+ -3*K+13 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):[153]: 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):[154]: 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 250 ms. Invariants computed in 2354 ms. ----Backward Invariants 1268 ms. ----Transitive Invariants 105 ms. Refinement performed in 2334 ms. Termination proved in 340 ms. Upper bounds computed in 4000 ms. ----Phase cost structures 1722 ms. --------Equation cost structures 1538 ms. --------Inductive compression(1) 160 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 2141 ms. ----Solving cost expressions 64 ms. Compressed phase information: 97 Compressed Chains: 0 Compressed invariants: 12 Total analysis performed in 9724 ms.