WARNING: Excluded non-linear constraints:[B1>=C*C1,C*C1+C1>=B1+1,B1>=C*D1,C*D1+D1>=B1+1] WARNING: Excluded non-linear constraints:[B1>=C*C1,C*C1+C1>=B1+1,B1>=C*D1,C*D1+D1>=B1+1] warning: Ignored call to loop_cont_f2/8 in equation start/8 Inferred cost of f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[42]: 1 with precondition: [C=0,I=0,L=0,B=D,O=F,P=G,Q=H,A=J,B=K,B=M,E=N,E>=A+1,A>=B+1] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[43]: 0 with precondition: [C=0,I=1,L=0,B=D,N=E,O=F,P=G,Q=H,A=J,B=K,B=M,A>=B+1] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[40,41],42]: 1+it1*(1) Such that:it1=<1*N+ -1*E,it1=<1*A+ -1*E+1 with precondition: [I=0,M=B,A=J,M=K,A+1=N,H=Q,A>=D,A>=E,A>=M+1] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[40,41],43]: 0+it1*(1) Such that:it1=<1*N+ -1*E,it1=<1*A+ -1*E+1,it1=<1*J+ -1*E+1 with precondition: [I=1,A=J,B=K,H=Q,A>=B+1,A>=D,N>=E+1,A>=M,A+1>=N] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[40,41],44]: 1+it1*(1) Such that:it1=<1*N+ -1*E,it1=<1*A+ -1*E+1 with precondition: [I=0,A=J,B=K,A+1=N,H=Q,A>=B+1,A>=D,A>=E,B>=M+1] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[40,41],45]: 1+it1*(1) Such that:it1=<1*N+ -1*E,it1=<1*A+ -1*E+1 with precondition: [I=0,A=J,B=K,A+1=N,H=Q,M>=B+1,A>=D,A>=E,A>=M] Inferred cost of f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[48]: 1 with precondition: [I=0,K=B,L=C,M=D,O=F,P=G,Q=H,A=J,E=N,E>=A+1] f19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[47],48]: 1+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*J+ -1*E+1 with precondition: [I=0,A=J,B=K,C=L,D=M,A+1=N,F=O,G=P,A>=E] Inferred cost of f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[51]: 1 with precondition: [I=0,K=B,L=C,O=F,P=G,Q=H,A=J,D=M,E=N,E>=A+1,A>=D] f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[50],51]: 1+it1*(1) Such that:it1=<1*N+ -1*E,it1=<1*A+ -1*E+1 with precondition: [I=0,A=J,B=K,C=L,D=M,A+1=N,F=O,G=P,H=Q,A>=D,A>=E] Inferred cost of f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[54]: 1 with precondition: [I=0,K=B,L=C,M=D+1,O=F,P=G,Q=H,A=J,E=N,E>=A+1] f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[53],54]: 1+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*J+ -1*E+1 with precondition: [I=0,A=J,B=K,C=L,D+1=M,A+1=N,F=O,G=P,H=Q,A>=E] Inferred cost of f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[61]: 1 with precondition: [I=0,K=B+1,L=C,N=E,O=F,P=G,Q=H,A=J,D=M,D>=A+1] f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[56,57,58,59,60],61]: 1+it1*(1)+it2*(3)+it3*(3)+it4*(1) Such that:it1+it2+it3=<1*A+ -1*D+1,it1+it2+it3=<1*J+ -1*D+1,it2=<-1*D+1*E+nat(min([1*M+ -1*E,1*A+ -1*E+1]))*max([min([1*A+ -1*D,1*J+ -1*D]),min([1*A+ -1*D,1*J+ -1*D])]),it3=<1*M+ -1*E,it3=<1*N+ -1*E,it3=<1*A+ -1*E+1,it4=<1*M+ -1*E,it4=<1*N+ -1*E,it4=<1*A+ -1*E+1 with precondition: [I=0,A=J,B+1=K,C=L,A+1=M,F=O,G=P,A>=D,N>=E] Inferred cost of f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[64]: 1 with precondition: [I=0,K=B,L=C,M=D,O=F,P=G,Q=H,A=J,E=N,E>=A+1] f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[63],64]: 1+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*J+ -1*E+1 with precondition: [I=0,A=J,B=K,C=L,D=M,A+1=N,F=O,G=P,A>=E] Inferred cost of f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[86]: 1 with precondition: [I=1,A>=B+1] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[87]: 1+it1*(1) Such that:it1=<-1*E+1*A+1,it1=<1*A+ -1*E+1 with precondition: [I=1,A>=B+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[88]: 1 with precondition: [I=1,L=C,M=D,N=E,O=F,P=G,Q=H,A=J,B=K,B>=A] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[66,76],86]: 1+it1*(3)+it2*(5) Such that:it1+it2=<1*A+ -1*B,it1+it2=<-1*B+1*A+ -1,it1+it2=<-1*B+1*E+ -2,it1+it2=<-1*B+1*E+ -1,it1+it2=<1*E+ -1*B+ -1 with precondition: [I=1,E>=A+1,A>=B+2] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[66,76],88]: 1+it1*(3)+it2*(5) Such that:it1+it2=<1*A+ -1*B,it1+it2=<1*M+ -1*B+1,it1+it2=<1*N+ -1*B+ -1 with precondition: [I=1,L=0,A=J,A=K,A=M+1,E=N,F=O,G=P,H=Q,E>=A+1,A>=B+1] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[67,[66,76],86]: 4+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[67,[66,76],88]: 4+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*M+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*N+ -1*E,it3=<1*A+ -1*E+1 with precondition: [I=1,L=0,A=J,A=K,A=M+1,A+1=N,H=Q,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[67,86]: 4+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[67,88]: 4+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*M+ -1*E+2 with precondition: [I=1,L=0,A=B+1,A=J,A=K,A=M+1,A+1=N,H=Q,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[68,[66,76],86]: 4+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[68,[66,76],88]: 4+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*M+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*N+ -1*E,it3=<1*A+ -1*E+1 with precondition: [I=1,L=0,A=J,A=K,A=M+1,A+1=N,H=Q,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[68,86]: 4+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[68,88]: 4+it1*(1) Such that:it1=<1*N+ -1*E,it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2 with precondition: [I=1,L=0,A=B+1,A=J,A=K,A+1=N,H=Q,A>=E,A>=M+2] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[69,[66,76],86]: 4+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[69,[66,76],88]: 4+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*M+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*N+ -1*E,it3=<1*A+ -1*E+1 with precondition: [I=1,L=0,A=J,A=K,A=M+1,A+1=N,H=Q,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[69,86]: 4+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[69,88]: 4+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*M+ -1*E+1 with precondition: [I=1,L=0,A=B+1,A=J,A=K,A=M,A+1=N,H=Q,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[70,[66,76],86]: 5+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[70,[66,76],88]: 5+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*K+ -1*B+ -1,it1+it2=<1*N+ -1*B+ -2,it3=<1*A+ -1*E+1,it3=<1*M+ -1*E+2,it4+it5=<1*A+ -1*B+1,it4+it5=<1*K+ -1*B+1,it5==A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[70,86]: 5+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B+1,it3==B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[70,88]: 5+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*K+ -1*E+1,it2+it3=<2,it3==L+1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[71,[66,76],86]: inf with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[71,[66,76],88]: inf with precondition: [I=1,L=0,A=J,A=K,A=M+1,N>=A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[71,86]: inf with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[71,88]: inf with precondition: [I=1,A=B+1,A=J,A=K,A+1=M,0>=L+1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[72,[66,76],86]: 5+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[72,[66,76],88]: 5+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*K+ -1*B+ -1,it1+it2=<1*N+ -1*B+ -2,it3=<1*A+ -1*E+1,it3=<1*M+ -1*E+2,it4+it5=<1*A+ -1*B,it4+it5=<1*M+ -1*B+1,it5==A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[72,86]: 5+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B,it3==B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[72,88]: 5+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*K+ -1*E+1,it2+it3=<1,it3==L+1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[73,[66,76],86]: 5+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[73,[66,76],88]: 5+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*K+ -1*B+ -1,it1+it2=<1*N+ -1*B+ -2,it3=<1*A+ -1*E+1,it3=<1*M+ -1*E+2,it4+it5=<1*A+ -1*B+1,it4+it5=<1*K+ -1*B+1,it5==A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[73,86]: 5+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B+1,it3==B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[73,88]: 5+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*K+ -1*E+1,it2+it3=<2,it3==1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[74,[66,76],86]: inf with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[74,[66,76],88]: inf with precondition: [I=1,L=0,A=J,A=K,A=M+1,N>=A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[74,86]: inf with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[74,88]: inf with precondition: [I=1,A=B+1,A=J,A=K,A+1=M,L>=1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[75,[66,76],86]: 5+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[75,[66,76],88]: 5+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*K+ -1*B+ -1,it1+it2=<1*N+ -1*B+ -2,it3=<1*A+ -1*E+1,it3=<1*M+ -1*E+2,it4+it5=<1*A+ -1*B,it4+it5=<1*M+ -1*B+1,it5==A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[75,86]: 5+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B,it3==B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[75,88]: 5+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*K+ -1*E+1,it2+it3=<1,it3==1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[77,[66,76],86]: 6+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[77,[66,76],88]: 6+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*M+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*N+ -1*E,it3=<1*A+ -1*E+1 with precondition: [I=1,L=0,A=J,A=K,A=M+1,A+1=N,H=Q,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[77,86]: 6+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[77,88]: 6+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*M+ -1*E+2 with precondition: [I=1,L=0,A=B+1,A=J,A=K,A=M+1,A+1=N,H=Q,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[78,[66,76],86]: 6+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[78,[66,76],88]: 6+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*M+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*N+ -1*E,it3=<1*A+ -1*E+1 with precondition: [I=1,L=0,A=J,A=K,A=M+1,A+1=N,H=Q,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[78,86]: 6+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[78,88]: 6+it1*(1) Such that:it1=<1*N+ -1*E,it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2 with precondition: [I=1,L=0,A=B+1,A=J,A=K,A+1=N,H=Q,A>=E,A>=M+2] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[79,[66,76],86]: 6+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[79,[66,76],88]: 6+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*M+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*N+ -1*E,it3=<1*A+ -1*E+1 with precondition: [I=1,L=0,A=J,A=K,A=M+1,A+1=N,H=Q,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[79,86]: 6+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[79,88]: 6+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*M+ -1*E+1 with precondition: [I=1,L=0,A=B+1,A=J,A=K,A=M,A+1=N,H=Q,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[80,[66,76],86]: 7+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[80,[66,76],88]: 7+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*K+ -1*B+ -1,it1+it2=<1*N+ -1*B+ -2,it3=<1*A+ -1*E+1,it3=<1*M+ -1*E+2,it4+it5=<1*A+ -1*B+1,it4+it5=<1*K+ -1*B+1,it5==A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[80,86]: 7+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B+1,it3==B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[80,88]: 7+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*K+ -1*E+1,it2+it3=<2,it3==L+1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[81,[66,76],86]: inf with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[81,[66,76],88]: inf with precondition: [I=1,L=0,A=J,A=K,A=M+1,N>=A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[81,86]: inf with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[81,88]: inf with precondition: [I=1,A=B+1,A=J,A=K,A+1=M,0>=L+1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[82,[66,76],86]: 7+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[82,[66,76],88]: 7+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*K+ -1*B+ -1,it1+it2=<1*N+ -1*B+ -2,it3=<1*A+ -1*E+1,it3=<1*M+ -1*E+2,it4+it5=<1*A+ -1*B,it4+it5=<1*M+ -1*B+1,it5==A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[82,86]: 7+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B,it3==B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[82,88]: 7+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*K+ -1*E+1,it2+it3=<1,it3==L+1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[83,[66,76],86]: 7+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[83,[66,76],88]: 7+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*K+ -1*B+ -1,it1+it2=<1*N+ -1*B+ -2,it3=<1*A+ -1*E+1,it3=<1*M+ -1*E+2,it4+it5=<1*A+ -1*B+1,it4+it5=<1*K+ -1*B+1,it5==A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[83,86]: 7+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B+1,it3==B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[83,88]: 7+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*K+ -1*E+1,it2+it3=<2,it3==1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[84,[66,76],86]: inf with precondition: [I=1,A>=B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[84,[66,76],88]: inf with precondition: [I=1,L=0,A=J,A=K,A=M+1,N>=A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[84,86]: inf with precondition: [I=1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[84,88]: inf with precondition: [I=1,A=B+1,A=J,A=K,A+1=M,L>=1,N>=A+1,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[85,[66,76],86]: 7+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+3,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[85,[66,76],88]: 7+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*K+ -1*B+ -1,it1+it2=<1*N+ -1*B+ -2,it3=<1*A+ -1*E+1,it3=<1*M+ -1*E+2,it4+it5=<1*A+ -1*B,it4+it5=<1*M+ -1*B+1,it5==A+1,A>=B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[85,86]: 7+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B,it3==B+2,A>=E] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[85,88]: 7+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it1=<1*K+ -1*E+1,it2+it3=<1,it3==1,N>=A+1,A>=E] Inferred cost of start(A,B,C,D,E,F,G,H): start(A,B,C,D,E,F,G,H):[90]: 2 with precondition: [A>=B+1] start(A,B,C,D,E,F,G,H):[91]: 2+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [A>=B+1,A>=E] start(A,B,C,D,E,F,G,H):[92]: 2 with precondition: [B>=A] start(A,B,C,D,E,F,G,H):[93]: 2+it1*(3)+it2*(5) Such that:it1+it2=<1*A+ -1*B,it1+it2=<-1*B+1*E+ -2,it1+it2=<-1*B+1*E+ -1,it1+it2=<1*A+ -1*B+ -1,it1+it2=<1*E+ -1*B+ -2,it1+it2=<1*E+ -1*B+ -1 with precondition: [E>=A+1,A>=B+2] start(A,B,C,D,E,F,G,H):[94]: 2+it1*(3)+it2*(5) Such that:it1+it2=<1*A+ -1*B,it1+it2=<-1*B+1*E+ -1,it1+it2=<1*E+ -1*B+ -1 with precondition: [E>=A+1,A>=B+1] start(A,B,C,D,E,F,G,H):[95]: 5+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[96]: 5+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[97]: 5+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[98]: 5+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[99]: 5+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[100]: 5+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[101]: 5+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[102]: 5+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[103]: 5+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[104]: 5+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[105]: 5+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[106]: 5+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[107]: 6+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+3,A>=E] start(A,B,C,D,E,F,G,H):[108]: 6+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+2,A>=E] start(A,B,C,D,E,F,G,H):[109]: 6+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B+1,it3==B+2,A>=E] start(A,B,C,D,E,F,G,H):[110]: 6+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it2+it3=<2,it3==E] start(A,B,C,D,E,F,G,H):[111]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[112]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[113]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[114]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[115]: 6+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+3,A>=E] start(A,B,C,D,E,F,G,H):[116]: 6+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+2,A>=E] start(A,B,C,D,E,F,G,H):[117]: 6+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B,it3==B+2,A>=E] start(A,B,C,D,E,F,G,H):[118]: 6+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it2+it3=<1,it3==E] start(A,B,C,D,E,F,G,H):[119]: 6+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+3,A>=E] start(A,B,C,D,E,F,G,H):[120]: 6+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+2,A>=E] start(A,B,C,D,E,F,G,H):[121]: 6+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B+1,it3==B+2,A>=E] start(A,B,C,D,E,F,G,H):[122]: 6+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it2+it3=<2,it3==E] start(A,B,C,D,E,F,G,H):[123]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[124]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[125]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[126]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[127]: 6+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+3,A>=E] start(A,B,C,D,E,F,G,H):[128]: 6+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+2,A>=E] start(A,B,C,D,E,F,G,H):[129]: 6+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B,it3==B+2,A>=E] start(A,B,C,D,E,F,G,H):[130]: 6+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it2+it3=<1,it3==E] start(A,B,C,D,E,F,G,H):[131]: 7+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[132]: 7+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[133]: 7+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[134]: 7+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[135]: 7+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[136]: 7+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[137]: 7+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[138]: 7+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[139]: 7+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[140]: 7+it1*(3)+it2*(5)+it3*(1) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[141]: 7+it1*(1) Such that:it1=<1*A+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[142]: 7+it1*(1) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[143]: 8+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+3,A>=E] start(A,B,C,D,E,F,G,H):[144]: 8+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+2,A>=E] start(A,B,C,D,E,F,G,H):[145]: 8+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B+1,it3==B+2,A>=E] start(A,B,C,D,E,F,G,H):[146]: 8+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it2+it3=<2,it3==E] start(A,B,C,D,E,F,G,H):[147]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[148]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[149]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[150]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[151]: 8+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+3,A>=E] start(A,B,C,D,E,F,G,H):[152]: 8+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+2,A>=E] start(A,B,C,D,E,F,G,H):[153]: 8+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B,it3==B+2,A>=E] start(A,B,C,D,E,F,G,H):[154]: 8+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it2+it3=<1,it3==E] start(A,B,C,D,E,F,G,H):[155]: 8+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+3,A>=E] start(A,B,C,D,E,F,G,H):[156]: 8+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B+1,it5==B+2,A>=E] start(A,B,C,D,E,F,G,H):[157]: 8+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B+1,it3==B+2,A>=E] start(A,B,C,D,E,F,G,H):[158]: 8+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it2+it3=<2,it3==E] start(A,B,C,D,E,F,G,H):[159]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[160]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[161]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[162]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[163]: 8+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -2,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+3,A>=E] start(A,B,C,D,E,F,G,H):[164]: 8+it1*(3)+it2*(5)+it3*(1)+it4*(1)+it5*(3) Such that:it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*E+1,it4+it5=<1*A+ -1*B,it5==B+2,A>=E] start(A,B,C,D,E,F,G,H):[165]: 8+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it2+it3=<1*A+ -1*B,it3==B+2,A>=E] start(A,B,C,D,E,F,G,H):[166]: 8+it1*(1)+it2*(1)+it3*(3) Such that:it1=<1*A+ -1*E+1,it1=<1*B+ -1*E+2,it2+it3=<1,it3==E] Solved cost expressions of start(A,B,C,D,E,F,G,H): start(A,B,C,D,E,F,G,H):[90]: 2 with precondition: [A>=B+1] start(A,B,C,D,E,F,G,H):[91]: 1*A+ -1*E+3 with precondition: [A>=B+1,A>=E] start(A,B,C,D,E,F,G,H):[92]: 2 with precondition: [B>=A] start(A,B,C,D,E,F,G,H):[93]: 5*A+ -5*B+ -3 with precondition: [E>=A+1,A>=B+2] start(A,B,C,D,E,F,G,H):[94]: 5*A+ -5*B+2 with precondition: [E>=A+1,A>=B+1] start(A,B,C,D,E,F,G,H):[95]: 6*A+ -5*B+ -1*E+ -4 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[96]: 6*A+ -5*B+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[97]: 1*A+ -1*E+6 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[98]: 1*A+ -1*E+6 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[99]: 6*A+ -5*B+ -1*E+ -4 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[100]: 6*A+ -5*B+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[101]: 1*A+ -1*E+6 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[102]: 1*A+ -1*E+6 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[103]: 6*A+ -5*B+ -1*E+ -4 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[104]: 6*A+ -5*B+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[105]: 1*A+ -1*E+6 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[106]: 1*A+ -1*E+6 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[107]: 9*A+ -8*B+ -1*E with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[108]: 9*A+ -8*B+ -1*E+5 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[109]: 4*A+ -3*B+ -1*E+10 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[110]: 1*A+ -1*E+13 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[111]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[112]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[113]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[114]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[115]: 9*A+ -8*B+ -1*E+ -3 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[116]: 9*A+ -8*B+ -1*E+2 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[117]: 4*A+ -3*B+ -1*E+7 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[118]: 1*A+ -1*E+10 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[119]: 9*A+ -8*B+ -1*E with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[120]: 9*A+ -8*B+ -1*E+5 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[121]: 4*A+ -3*B+ -1*E+10 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[122]: 1*A+ -1*E+13 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[123]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[124]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[125]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[126]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[127]: 9*A+ -8*B+ -1*E+ -3 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[128]: 9*A+ -8*B+ -1*E+2 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[129]: 4*A+ -3*B+ -1*E+7 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[130]: 1*A+ -1*E+10 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[131]: 6*A+ -5*B+ -1*E+ -2 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[132]: 6*A+ -5*B+ -1*E+3 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[133]: 1*A+ -1*E+8 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[134]: 1*A+ -1*E+8 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[135]: 6*A+ -5*B+ -1*E+ -2 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[136]: 6*A+ -5*B+ -1*E+3 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[137]: 1*A+ -1*E+8 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[138]: 1*A+ -1*E+8 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[139]: 6*A+ -5*B+ -1*E+ -2 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[140]: 6*A+ -5*B+ -1*E+3 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[141]: 1*A+ -1*E+8 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[142]: 1*A+ -1*E+8 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[143]: 9*A+ -8*B+ -1*E+2 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[144]: 9*A+ -8*B+ -1*E+7 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[145]: 4*A+ -3*B+ -1*E+12 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[146]: 1*A+ -1*E+15 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[147]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[148]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[149]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[150]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[151]: 9*A+ -8*B+ -1*E+ -1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[152]: 9*A+ -8*B+ -1*E+4 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[153]: 4*A+ -3*B+ -1*E+9 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[154]: 1*A+ -1*E+12 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[155]: 9*A+ -8*B+ -1*E+2 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[156]: 9*A+ -8*B+ -1*E+7 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[157]: 4*A+ -3*B+ -1*E+12 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[158]: 1*A+ -1*E+15 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[159]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[160]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[161]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[162]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[163]: 9*A+ -8*B+ -1*E+ -1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[164]: 9*A+ -8*B+ -1*E+4 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[165]: 4*A+ -3*B+ -1*E+9 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[166]: 1*A+ -1*E+12 with precondition: [A=B+1,A>=E] Maximum cost of start(A,B,C,D,E,F,G,H): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 159 ms. Invariants computed in 873 ms. ----Backward Invariants 372 ms. ----Transitive Invariants 32 ms. Refinement performed in 962 ms. Termination proved in 86 ms. Upper bounds computed in 4006 ms. ----Phase cost structures 1498 ms. --------Equation cost structures 1456 ms. --------Inductive compression(1) 13 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 2377 ms. ----Solving cost expressions 65 ms. Compressed phase information: 146 Compressed Chains: 0 Compressed invariants: 26 Total analysis performed in 6278 ms.