warning: Ignored call to stop/8 in equation start/8 warning: Ignored call to stop/8 in equation start/8 warning: Ignored call to loop_cont_lbl71/8 in equation start/8 Inferred cost of lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[13]: 1 with precondition: [I=1,A=B,L=C,D+1=E,A+1=F,G=H,A=J,A=K,D=M,D+1=N,A+1=O,G=P,G=Q,100>=A,G>=101,D+1>=G] lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[14]: 1 with precondition: [I=1,A=B,L=C,D+1=E,A+1=F,G=H,A=J,A=K,D=M,D+1=N,A+1=O,G=P,G=Q,100>=A,A>=D,D+1>=G] lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[12],13]: 1+it1*(1) Such that:it1=<1*D+ -1*M,it1=<1*N+ -101,it1=<-1*M+1*E+ -1,it1=<-1*M+1*N+ -1,it1=<1*D+ -1/2*M+ -1/2*O,it1=<-1/2*O+1*N+ -51,it1=<-1*G+ -1*J+1*O+100,it1=<-1*J+ -1*P+1*O+100,it1=<-1*J+ -1/2*P+1/2*N+199/2,it1=<-1*O+1/2*P+3/2*N+ -203/2,it1=<1*O+ -1*B+ -1*H+100,it1=<1*O+ -1*F+ -1*H+101,it1=<-1/2*J+ -1/2*P+1/2*N+99/2,it1=<-1/2*M+ -1/2*O+1*E+ -1,it1=<-1/2*M+ -1/2*O+1*N+ -1,it1=<-1*A+ -1*G+1/2*M+1/2*O+100,it1=<-1*G+ -1*J+1/2*M+1/2*O+100,it1=<-1*M+ -1*O+1/2*G+3/2*N+ -3/2,it1=<-1*M+ -1*O+1/2*P+3/2*N+ -3/2,it1=<1/2*E+1/2*P+ -1*B+ -1*H+199/2,it1=<1/2*E+1/2*P+ -1*F+ -1*H+201/2,it1=<1/2*G+1/2*N+ -1*F+ -1*H+201/2,it1=<1/2*M+1/2*O+ -1*B+ -1*H+100,it1=<1/2*M+1/2*O+ -1*F+ -1*H+101,it1=<1*D+1*O+ -1*A+ -1*E+ -1*P+101,it1=<1*D+1/2*G+1/2*N+ -1*M+ -1*O+ -1/2,it1=<1/2*M+1/2*O+ -1/2*A+ -1*F+ -1*H+151 with precondition: [I=1,Q=101,F=B+1,A=J,O=K+1,C=L,E=N,M+O+101=D+F+H,A+E+G=M+O+101,A+E+P=M+O+101,100>=A,101>=F,100>=H,M>=100,O+100>=F+H,A+2*E>=M+O+101,E+F+H>=M+O+102] lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[12],14]: 1+it1*(1) Such that:it1=<-1*Q+1*N,it1=<1*D+ -1*M,it1=<-1*M+1*E+ -1,it1=<-1*M+1*N+ -1,it1=<-1*J+ -1/2*G+1/2*N+199/2,it1=<-1*J+ -1/2*P+1/2*N+199/2,it1=<-1*O+ -1/2*Q+1*N+51,it1=<1*O+1*Q+ -1*F+ -1*H,it1=<-1/2*G+ -1/2*J+1/2*N+99/2,it1=<-1/2*J+ -1/2*P+1/2*N+99/2,it1=<-2*O+ -1*Q+1/2*P+3/2*N+205/2,it1=<-1*A+ -1*P+1*O+1*Q+ -1,it1=<-1*G+ -1*J+1*O+1*Q+ -1,it1=<-1*J+ -1*P+1*O+1*Q+ -1,it1=<1*D+ -1/2*E+ -1/2*P+ -1*A+201/2,it1=<1*D+ -1/2*M+ -1/2*O+ -1/2*Q+101/2,it1=<1*O+1*Q+ -1*B+ -1*H+ -1,it1=<-1/2*M+ -1/2*O+ -1/2*Q+1*N+99/2,it1=<1/2*E+1/2*P+ -1*B+ -1*H+199/2,it1=<1/2*E+1/2*P+ -1*F+ -1*H+201/2,it1=<-1*M+ -1*O+ -1*Q+1/2*P+3/2*N+199/2,it1=<1/2*A+1/2*E+1/2*P+ -1*F+ -1*H+101/2,it1=<1/2*E+1/2*G+1/2*J+ -1*F+ -1*H+101/2,it1=<1/2*G+1/2*J+1/2*N+ -1*F+ -1*H+101/2,it1=<1/2*M+1/2*O+1/2*Q+ -1*B+ -1*H+99/2,it1=<1*D+1/2*E+1/2*P+ -1*M+ -1*O+ -1*Q+201/2,it1=<1/2*K+1/2*M+1/2*Q+ -1/2*J+ -1*F+ -1*H+101 with precondition: [I=1,A=J,C=L,E=N,K+1=O,G=P,A+E+G=B+D+H+1,A+E+G=D+F+H,A+E+G=K+M+Q+1,100>=A,100>=H,100>=K,E>=D+1,E>=G,M+2>=K,D>=M+1,K>=M,D+K>=H+M+1,D+H+101>=A+E+G,H+2*D>=A+E+G,K+2*M+2>=A+E+G] Inferred cost of start(A,B,C,D,E,F,G,H): start(A,B,C,D,E,F,G,H):[16]: 1 with precondition: [H=A,C=B,E=D,G=F,H>=101] start(A,B,C,D,E,F,G,H):[17]: 1 with precondition: [H=A,C=B,E=D,G=F,G>=E+1] start(A,B,C,D,E,F,G,H):[18]: 2 with precondition: [H=A,C=B,E=D,G=F,100>=H,G>=101,E>=G] start(A,B,C,D,E,F,G,H):[19]: 2 with precondition: [H=A,C=B,E=D,G=F,100>=H,H+1>=E,E>=G] start(A,B,C,D,E,F,G,H):[20]: 2+it1*(1) Such that:it1=<1*D+ -101,it1=<1*E+ -101,it1=<-1*H+ -1/2*G+3/2*D+ -5/2,it1=<-1*H+ -1/2*G+3/2*E+ -5/2,it1=<-1/2*G+ -1/2*H+1*D+ -3/2,it1=<-1/2*G+ -1/2*H+1*E+ -3/2,it1=<1/2*D+ -1/2*G+ -1*H+199/2,it1=<1/2*D+ -1/2*G+ -1/2*H+99/2,it1=<1/2*E+ -1/2*G+ -1*H+199/2,it1=<1/2*E+ -1/2*G+ -1/2*H+99/2 with precondition: [H=A,C=B,E=D,G=F,100>=G,100>=H,E>=102] start(A,B,C,D,E,F,G,H):[21]: 2+it1*(1) Such that:it1=<-1*A+ -1*G+201,it1=<-1*F+ -1*H+201,it1=<-1*F+ -1*H+401/2,it1=<-1*F+ -1*H+403/2,it1=<-1*G+ -1*H+201,it1=<-1*G+ -1*H+401/2,it1=<-1*G+ -1*H+403/2,it1=<-3/2*H+ -1*F+501/2,it1=<-3/2*H+ -1*F+505/2,it1=<-3/2*H+ -1*G+501/2,it1=<-3/2*H+ -1*G+505/2,it1=<-1*A+ -1*G+1*D+99,it1=<-1*A+ -1*G+2*D+ -1,it1=<-1*F+ -1/2*H+1*D+99/2,it1=<-1*G+ -1*H+1*D+99,it1=<-1*G+ -1*H+1*E+99,it1=<-1*G+ -1*H+2*D+ -1,it1=<-1*G+ -1*H+2*E+ -1,it1=<-1*G+ -1/2*H+1*E+99/2,it1=<-1*H+ -1/2*F+1/2*D+203/2,it1=<-1*H+ -1/2*G+1/2*E+203/2,it1=<-3/2*F+ -1*H+3/2*D+199/2,it1=<-3/2*G+ -1*H+3/2*E+199/2,it1=<-1/2*A+ -1/2*G+1/2*D+50,it1=<-1/2*F+ -1/2*H+1/2*D+50,it1=<-1/2*F+ -1/2*H+1/2*D+101/2,it1=<-1/2*F+ -1/2*H+1/2*E+50,it1=<-1/2*G+ -1/2*H+1/2*E+101/2,it1=<-1/3*A+ -1/3*G+2/3*D+1/3,it1=<-1/3*F+ -1/3*H+2/3*D+1/3,it1=<-1/3*F+ -1/3*H+2/3*E+1/3,it1=<1/2*D+ -1/2*G+ -1*H+199/2,it1=<1/2*D+ -1/2*G+ -1/2*H+99/2,it1=<1/2*E+ -1/2*F+ -1*H+199/2,it1=<1/2*E+ -1/2*F+ -1/2*H+99/2 with precondition: [H=A,C=B,E=D,G=F,100>=G,100>=H,E>=G,E>=H+2,302>=E+G+H] Inferred cost of start0(A,B,C,D,E,F,G,H): start0(A,B,C,D,E,F,G,H):[23]: 2 with precondition: [A>=101] start0(A,B,C,D,E,F,G,H):[24]: 2 with precondition: [G>=E+1] start0(A,B,C,D,E,F,G,H):[25]: 3 with precondition: [100>=A,G>=101,E>=G] start0(A,B,C,D,E,F,G,H):[26]: 3 with precondition: [100>=A,A+1>=E,E>=G] start0(A,B,C,D,E,F,G,H):[27]: 3+it1*(1) Such that:it1=<1*E+ -101,it1=<1*E+ -1/2*A+ -1/2*G+ -3/2,it1=<1/2*E+ -1/2*A+ -1/2*G+99/2,it1=<1/2*E+ -1/2*G+ -1*A+199/2,it1=<3/2*E+ -1/2*G+ -1*A+ -5/2 with precondition: [100>=A,100>=G,E>=102] start0(A,B,C,D,E,F,G,H):[28]: 3+it1*(1) Such that:it1=<-1*A+ -1*G+201,it1=<-1*A+ -1*G+401/2,it1=<-1*A+ -1*G+403/2,it1=<-1*G+ -3/2*A+501/2,it1=<-1*G+ -3/2*A+505/2,it1=<1*E+ -1*A+ -1*G+99,it1=<1*E+ -1/2*A+ -1*G+99/2,it1=<2*E+ -1*A+ -1*G+ -1,it1=<1/2*E+ -1/2*A+ -1/2*G+50,it1=<1/2*E+ -1/2*A+ -1/2*G+99/2,it1=<1/2*E+ -1/2*A+ -1/2*G+101/2,it1=<1/2*E+ -1/2*G+ -1*A+199/2,it1=<1/2*E+ -1/2*G+ -1*A+203/2,it1=<2/3*E+ -1/3*A+ -1/3*G+1/3,it1=<3/2*E+ -1*A+ -3/2*G+199/2 with precondition: [100>=A,100>=G,E>=A+2,E>=G,302>=A+E+G] Solved cost expressions of start0(A,B,C,D,E,F,G,H): start0(A,B,C,D,E,F,G,H):[23]: 2 with precondition: [A>=101] start0(A,B,C,D,E,F,G,H):[24]: 2 with precondition: [G>=E+1] start0(A,B,C,D,E,F,G,H):[25]: 3 with precondition: [100>=A,G>=101,E>=G] start0(A,B,C,D,E,F,G,H):[26]: 3 with precondition: [100>=A,A+1>=E,E>=G] start0(A,B,C,D,E,F,G,H):[27]: nat(min([-1/2*A+1/2*E+ -1/2*G+99/2,1*E+ -101]))+3 with precondition: [100>=A,100>=G,E>=102] start0(A,B,C,D,E,F,G,H):[28]: nat(min([-1/3*A+2/3*E+ -1/3*G+1/3,-1/2*A+1/2*E+ -1/2*G+99/2]))+3 with precondition: [100>=A,100>=G,E>=A+2,E>=G,302>=A+E+G] Maximum cost of start0(A,B,C,D,E,F,G,H): max([3,nat(min([-1/2*A+1/2*E+ -1/2*G+99/2,1*E+ -101]))+3,nat(min([-1/3*A+2/3*E+ -1/3*G+1/3,-1/2*A+1/2*E+ -1/2*G+99/2]))+3]) Asymptotic class: n Time statistics: Partial evaluation computed in 11 ms. Invariants computed in 66 ms. ----Backward Invariants 39 ms. ----Transitive Invariants 7 ms. Refinement performed in 53 ms. Termination proved in 114 ms. Upper bounds computed in 359 ms. ----Phase cost structures 197 ms. --------Equation cost structures 195 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 140 ms. ----Solving cost expressions 14 ms. Compressed phase information: 1 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 634 ms.