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):[40]: 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):[41]: 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):[[38,39],40]: 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):[[38,39],41]: 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):[[38,39],42]: 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):[[38,39],43]: 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):[46]: 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):[[45],46]: 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):[49]: 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):[[48],49]: 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):[52]: 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):[[51],52]: 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):[57]: 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):[[54,55,56],57]: 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]))*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):[60]: 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):[[59],60]: 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):[82]: 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):[83]: 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):[84]: 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):[[62,72],82]: 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):[[62,72],84]: 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):[63,[62,72],82]: 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):[63,[62,72],84]: 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):[63,82]: 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):[63,84]: 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):[64,[62,72],82]: 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):[64,[62,72],84]: 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):[64,82]: 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):[64,84]: 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):[65,[62,72],82]: 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):[65,[62,72],84]: 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):[65,82]: 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):[65,84]: 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):[66,[62,72],82]: 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):[66,[62,72],84]: 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):[66,82]: 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):[66,84]: 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):[67,[62,72],82]: 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):[67,[62,72],84]: 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):[67,82]: 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):[67,84]: 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):[68,[62,72],82]: 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):[68,[62,72],84]: 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):[68,82]: 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):[68,84]: 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):[69,[62,72],82]: 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):[69,[62,72],84]: 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):[69,82]: 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):[69,84]: 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):[70,[62,72],82]: 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):[70,[62,72],84]: 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):[70,82]: 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):[70,84]: 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):[71,[62,72],82]: 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):[71,[62,72],84]: 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):[71,82]: 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):[71,84]: 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):[73,[62,72],82]: 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):[73,[62,72],84]: 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):[73,82]: 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):[73,84]: 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):[74,[62,72],82]: 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):[74,[62,72],84]: 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):[74,82]: 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):[74,84]: 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):[75,[62,72],82]: 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):[75,[62,72],84]: 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):[75,82]: 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):[75,84]: 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):[76,[62,72],82]: 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):[76,[62,72],84]: 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):[76,82]: 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):[76,84]: 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):[77,[62,72],82]: 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):[77,[62,72],84]: 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):[77,82]: 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):[77,84]: 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):[78,[62,72],82]: 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):[78,[62,72],84]: 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):[78,82]: 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):[78,84]: 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):[79,[62,72],82]: 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):[79,[62,72],84]: 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):[79,82]: 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):[79,84]: 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):[80,[62,72],82]: 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):[80,[62,72],84]: 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):[80,82]: 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):[80,84]: 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):[81,[62,72],82]: 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):[81,[62,72],84]: 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):[81,82]: 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):[81,84]: 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):[86]: 2 with precondition: [A>=B+1] start(A,B,C,D,E,F,G,H):[87]: 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):[88]: 2 with precondition: [B>=A] start(A,B,C,D,E,F,G,H):[89]: 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):[90]: 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):[91]: 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):[92]: 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):[93]: 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):[94]: 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):[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]: 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):[104]: 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):[105]: 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):[106]: 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):[107]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[108]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[109]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[110]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[111]: 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):[112]: 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):[113]: 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):[114]: 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):[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+1,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+1,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+1,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=<2,it3==E] start(A,B,C,D,E,F,G,H):[119]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[120]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[121]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[122]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[123]: 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):[124]: 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):[125]: 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):[126]: 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):[127]: 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):[128]: 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):[129]: 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):[130]: 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):[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]: 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):[140]: 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):[141]: 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):[142]: 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):[143]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[144]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[145]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[146]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[147]: 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):[148]: 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):[149]: 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):[150]: 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):[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+1,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+1,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+1,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=<2,it3==E] start(A,B,C,D,E,F,G,H):[155]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[156]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[157]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[158]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[159]: 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):[160]: 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):[161]: 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):[162]: 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):[86]: 2 with precondition: [A>=B+1] start(A,B,C,D,E,F,G,H):[87]: 1*A+ -1*E+3 with precondition: [A>=B+1,A>=E] start(A,B,C,D,E,F,G,H):[88]: 2 with precondition: [B>=A] start(A,B,C,D,E,F,G,H):[89]: 5*A+ -5*B+ -3 with precondition: [E>=A+1,A>=B+2] start(A,B,C,D,E,F,G,H):[90]: 5*A+ -5*B+2 with precondition: [E>=A+1,A>=B+1] start(A,B,C,D,E,F,G,H):[91]: 6*A+ -5*B+ -1*E+ -4 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[92]: 6*A+ -5*B+ -1*E+1 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[93]: 1*A+ -1*E+6 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[94]: 1*A+ -1*E+6 with precondition: [A=B+1,A>=E] 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]: 9*A+ -8*B+ -1*E with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[104]: 9*A+ -8*B+ -1*E+5 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[105]: 4*A+ -3*B+ -1*E+10 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[106]: 1*A+ -1*E+13 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[107]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[108]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[109]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[110]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[111]: 9*A+ -8*B+ -1*E+ -3 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[112]: 9*A+ -8*B+ -1*E+2 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[113]: 4*A+ -3*B+ -1*E+7 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[114]: 1*A+ -1*E+10 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[115]: 9*A+ -8*B+ -1*E with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[116]: 9*A+ -8*B+ -1*E+5 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[117]: 4*A+ -3*B+ -1*E+10 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[118]: 1*A+ -1*E+13 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[119]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[120]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[121]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[122]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[123]: 9*A+ -8*B+ -1*E+ -3 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[124]: 9*A+ -8*B+ -1*E+2 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[125]: 4*A+ -3*B+ -1*E+7 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[126]: 1*A+ -1*E+10 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[127]: 6*A+ -5*B+ -1*E+ -2 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[128]: 6*A+ -5*B+ -1*E+3 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[129]: 1*A+ -1*E+8 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[130]: 1*A+ -1*E+8 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]: 9*A+ -8*B+ -1*E+2 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[140]: 9*A+ -8*B+ -1*E+7 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[141]: 4*A+ -3*B+ -1*E+12 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[142]: 1*A+ -1*E+15 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[143]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[144]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[145]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[146]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[147]: 9*A+ -8*B+ -1*E+ -1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[148]: 9*A+ -8*B+ -1*E+4 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[149]: 4*A+ -3*B+ -1*E+9 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[150]: 1*A+ -1*E+12 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[151]: 9*A+ -8*B+ -1*E+2 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[152]: 9*A+ -8*B+ -1*E+7 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[153]: 4*A+ -3*B+ -1*E+12 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[154]: 1*A+ -1*E+15 with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[155]: inf with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[156]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[157]: inf with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[158]: inf with precondition: [A=B+1,A>=E] start(A,B,C,D,E,F,G,H):[159]: 9*A+ -8*B+ -1*E+ -1 with precondition: [A>=B+3,A>=E] start(A,B,C,D,E,F,G,H):[160]: 9*A+ -8*B+ -1*E+4 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[161]: 4*A+ -3*B+ -1*E+9 with precondition: [A>=B+2,A>=E] start(A,B,C,D,E,F,G,H):[162]: 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 139 ms. Invariants computed in 867 ms. ----Backward Invariants 371 ms. ----Transitive Invariants 30 ms. Refinement performed in 922 ms. Termination proved in 74 ms. Upper bounds computed in 3716 ms. ----Phase cost structures 1358 ms. --------Equation cost structures 1326 ms. --------Inductive compression(1) 11 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 2245 ms. ----Solving cost expressions 60 ms. Compressed phase information: 146 Compressed Chains: 0 Compressed invariants: 26 Total analysis performed in 5898 ms.