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_lbl72/8 in equation start/8 
Inferred cost of lbl72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): 
lbl72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[13]: 1
  with precondition: [I=1,B+1=C,A+1=D,E=F,A=G,Q=H,A=J,B=K,B+1=L,A+1=M,E=N,E=O,A=P,100>=A,E>=101,B+1>=E] 

lbl72(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[14]: 1
  with precondition: [I=1,B+1=C,A+1=D,E=F,A=G,Q=H,A=J,B=K,B+1=L,A+1=M,E=N,E=O,A=P,100>=A,A>=B,B+1>=E] 

lbl72(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*B+ -1*K,it1=<1*L+ -101,it1=<-1*K+1*C+ -1,it1=<-1*K+1*L+ -1,it1=<-1/2*M+1*L+ -51,it1=<-1*E+ -1*J+1*P+101,it1=<-1*J+ -1*N+1*P+101,it1=<1*P+ -1*D+ -1*F+102,it1=<1*P+ -1*F+ -1*G+101,it1=<-1/2*E+ -1/2*J+1/2*C+99/2,it1=<-1/2*E+ -1/2*J+1/2*L+99/2,it1=<-1/2*J+ -1/2*N+1/2*L+99/2,it1=<-1/2*K+ -1/2*M+1*L+ -1,it1=<1/2*B+ -1/2*D+ -1/2*F+101/2,it1=<1/2*K+1/2*P+ -1*D+ -1*F+203/2,it1=<1/2*K+1/2*P+ -1*F+ -1*G+201/2,it1=<1*B+1*P+ -1*A+ -1*C+ -1*N+102,it1=<1/2*A+1/2*C+1/2*N+ -1*D+ -1*F+101/2
  with precondition: [I=1,O=101,N=E,A=J,C=L,P+1=M,H=Q,A+C+N=K+P+102,A+C+N=B+D+F,A+C+N=B+F+G+1,100>=A,100>=F,C>=B+1,C>=N,A+C+N>=P+202,B+F+101>=A+C+N,B+P+101>=A+C+N] 

lbl72(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*O+1*L,it1=<1*B+ -1*K,it1=<-1*K+1*C+ -1,it1=<-1*K+1*L+ -1,it1=<-1*A+ -1*N+1*O+1*P,it1=<-1*E+ -1*J+1*O+1*P,it1=<-1*J+ -1*N+1*O+1*P,it1=<-1*O+ -1/2*P+1*L+99/2,it1=<1*O+1*P+ -1*F+ -1*G,it1=<-1/2*J+ -1/2*N+1/2*L+99/2,it1=<1/2*B+ -1/2*D+ -1/2*F+101/2,it1=<1*O+1*P+ -1*D+ -1*F+1,it1=<-1/2*K+ -1/2*M+ -1/2*O+1*L+99/2,it1=<1/2*A+1/2*C+1/2*N+ -1*D+ -1*F+101/2,it1=<1/2*C+1/2*E+1/2*J+ -1*D+ -1*F+101/2,it1=<1/2*E+1/2*J+1/2*L+ -1*D+ -1*F+101/2,it1=<1/2*E+1/2*J+1/2*L+ -1*F+ -1*G+99/2,it1=<1/2*J+1/2*L+1/2*N+ -1*F+ -1*G+99/2
  with precondition: [I=1,G+1=D,A=J,C=L,E=N,M=P+1,H=Q,K+M+O=A+C+E,A+C+E=B+F+G+1,100>=A,100>=G,101>=M,C>=B+1,C>=E,B>=G+1,B>=K+1,M>=K+1,K+3>=M,B+G+101>=A+C+E,M+2*K+1>=A+C+E,G+M+2*B>=A+C+E+K+1] 

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: [F=A,C=B,E=D,H=G,F>=101] 

start(A,B,C,D,E,F,G,H):[17]: 1
  with precondition: [F=A,C=B,E=D,H=G,E>=C+1] 

start(A,B,C,D,E,F,G,H):[18]: 2
  with precondition: [F=A,C=B,E=D,H=G,100>=F,E>=101,C>=E] 

start(A,B,C,D,E,F,G,H):[19]: 2
  with precondition: [F=A,C=B,E=D,H=G,100>=F,F+1>=C,C>=E] 

start(A,B,C,D,E,F,G,H):[20]: 2+it1*(1)
  Such that:it1=<1*B+ -101,it1=<1*C+ -101,it1=<-1/2*E+ -1/2*F+1*B+ -3/2,it1=<-1/2*E+ -1/2*F+1*C+ -3/2,it1=<1/2*B+ -1/2*E+ -1/2*F+99/2,it1=<1/2*C+ -1/2*E+ -1/2*F+99/2
  with precondition: [F=A,C=B,E=D,H=G,100>=E,100>=F,C>=102] 

start(A,B,C,D,E,F,G,H):[21]: 2+it1*(1)
  Such that:it1=<-1*A+ -1*E+201,it1=<-1*D+ -1*F+201,it1=<-1*D+ -1*F+401/2,it1=<-1*E+ -1*F+201,it1=<-1*E+ -1*F+401/2,it1=<-1*A+ -1*E+1*B+99,it1=<-1*A+ -1*E+2*B+ -1,it1=<-1*D+ -1*F+1*B+197/2,it1=<-1*D+ -1*F+1*C+197/2,it1=<-1*D+ -1*F+3/2*B+97/2,it1=<-1*D+ -1*F+3/2*C+97/2,it1=<-1*E+ -1*F+1*B+99,it1=<-1*E+ -1*F+1*C+99,it1=<-1*E+ -1*F+2*B+ -1,it1=<-1*E+ -1*F+2*C+ -1,it1=<-1/2*A+ -1/2*E+1/2*B+50,it1=<-1/2*D+ -1/2*F+1/2*B+50,it1=<-1/2*D+ -1/2*F+1/2*C+50,it1=<-1/3*A+ -1/3*E+2/3*B+1/3,it1=<-1/3*D+ -1/3*F+2/3*B+1/3,it1=<-1/3*D+ -1/3*F+2/3*C+1/3,it1=<1/2*B+ -1/2*E+ -1/2*F+99/2,it1=<1/2*C+ -1/2*D+ -1/2*F+99/2
  with precondition: [F=A,C=B,E=D,H=G,100>=E,100>=F,C>=E,C>=F+2,302>=C+E+F] 

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: [E>=C+1] 

start0(A,B,C,D,E,F,G,H):[25]: 3
  with precondition: [100>=A,E>=101,C>=E] 

start0(A,B,C,D,E,F,G,H):[26]: 3
  with precondition: [100>=A,A+1>=C,C>=E] 

start0(A,B,C,D,E,F,G,H):[27]: 3+it1*(1)
  Such that:it1=<1*C+ -101,it1=<1*C+ -1/2*A+ -1/2*E+ -3/2,it1=<1/2*C+ -1/2*A+ -1/2*E+99/2
  with precondition: [100>=A,100>=E,C>=102] 

start0(A,B,C,D,E,F,G,H):[28]: 3+it1*(1)
  Such that:it1=<-1*A+ -1*E+201,it1=<-1*A+ -1*E+401/2,it1=<1*C+ -1*A+ -1*E+99,it1=<1*C+ -1*A+ -1*E+197/2,it1=<2*C+ -1*A+ -1*E+ -1,it1=<1/2*C+ -1/2*A+ -1/2*E+50,it1=<1/2*C+ -1/2*A+ -1/2*E+99/2,it1=<2/3*C+ -1/3*A+ -1/3*E+1/3,it1=<3/2*C+ -1*A+ -1*E+97/2
  with precondition: [100>=A,100>=E,C>=A+2,C>=E,302>=A+C+E] 

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: [E>=C+1] 
start0(A,B,C,D,E,F,G,H):[25]: 3  with precondition: [100>=A,E>=101,C>=E] 
start0(A,B,C,D,E,F,G,H):[26]: 3  with precondition: [100>=A,A+1>=C,C>=E] 
start0(A,B,C,D,E,F,G,H):[27]: nat(min([-1/2*A+1/2*C+ -1/2*E+99/2,1*C+ -101]))+3  with precondition: [100>=A,100>=E,C>=102] 
start0(A,B,C,D,E,F,G,H):[28]: nat(min([-1/3*A+2/3*C+ -1/3*E+1/3,-1/2*A+1/2*C+ -1/2*E+99/2]))+3  with precondition: [100>=A,100>=E,C>=A+2,C>=E,302>=A+C+E] 
Maximum cost of start0(A,B,C,D,E,F,G,H): max([3,nat(min([-1/2*A+1/2*C+ -1/2*E+99/2,1*C+ -101]))+3,nat(min([-1/3*A+2/3*C+ -1/3*E+1/3,-1/2*A+1/2*C+ -1/2*E+99/2]))+3]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 10 ms.
Invariants computed in 64 ms.
----Backward Invariants 38 ms.
----Transitive Invariants 7 ms.
Refinement performed in 51 ms.
Termination proved in 114 ms.
Upper bounds computed in 289 ms.
----Phase cost structures 133 ms.
--------Equation cost structures 132 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 138 ms.
----Solving cost expressions 9 ms.

Compressed phase information: 1 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 560 ms.