warning: Ignored call to stop/8 in equation start/8 
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_lM1/8 in equation start/8 
Inferred cost of lZZ1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): 
lZZ1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[17]: 1
  with precondition: [B=0,I=0,K=1,L=C,N=E,F=G,A=H,A=J,D=M+1,F=O,F=P,A=Q,A>=2,D>=1,F>=A+D] 

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

Inferred cost of lM1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): 
lM1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[22]: 1
  with precondition: [A=1,B=1,H=1,I=1,D+1=F,D+1=G,D>=1] 

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

lM1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[20,21],22]: 1+it1*(1)+it2*(2)
  Such that:it1+it2=<1*D,it1+it2=<-1*B+1*F,it1+it2=<1*D+ -1,it1+it2=<1*F+ -2,it1+it2=<1*F+ -1,it1+it2=<1*G+ -2,it1+it2=<1*G+ -1,it1+it2=<-1*B+1*F+ -1
  with precondition: [I=1,F=G,A=H,A>=2,B>=1,A>=B,B+D>=A+1,F>=B+D,A+D>=B+3] 

lM1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[20,21],23]: 1+it1*(1)+it2*(2)
  Such that:it1+it2=<1*D,it1+it2=<-1*B+1*F,it1+it2=<1*F+ -1,it1+it2=<1*G+ -1,it1+it2=<1*O+ -1,it1+it2=<1*P+ -1
  with precondition: [I=1,M=0,F=G,A=H,A=J,C=L,E=N,F=O,F=P,A=Q,A>=2,B>=1,D>=1,K>=1,A>=B,A>=K,F>=B+D,B+D>=K,B+D+K>=4,D+2*A>=B+K+2] 

Inferred cost of start(A,B,C,D,E,F,G,H): 
start(A,B,C,D,E,F,G,H):[25]: 1
  with precondition: [H=A,C=B,E=D,G=F,0>=H] 

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

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

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

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

start(A,B,C,D,E,F,G,H):[30]: 2+it1*(1)+it2*(2)
  Such that:it1+it2=<1*F+ -2,it1+it2=<1*F+ -1,it1+it2=<1*G+ -2,it1+it2=<1*G+ -1
  with precondition: [H=A,C=B,E=D,G=F,H>=2,G>=H+1] 

start(A,B,C,D,E,F,G,H):[31]: 2+it1*(1)+it2*(2)
  Such that:it1+it2=<1*F+ -1,it1+it2=<1*G+ -1
  with precondition: [H=A,C=B,E=D,G=F,G>=2,H>=2] 

Inferred cost of start0(A,B,C,D,E,F,G,H): 
start0(A,B,C,D,E,F,G,H):[33]: 2
  with precondition: [0>=A] 

start0(A,B,C,D,E,F,G,H):[34]: 2
  with precondition: [0>=G+1] 

start0(A,B,C,D,E,F,G,H):[35]: 2
  with precondition: [G=0,A>=1] 

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

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

start0(A,B,C,D,E,F,G,H):[38]: 3+it1*(1)+it2*(2)
  Such that:it1+it2=<1*G+ -2,it1+it2=<1*G+ -1
  with precondition: [A>=2,G>=A+1] 

start0(A,B,C,D,E,F,G,H):[39]: 3+it1*(1)+it2*(2)
  Such that:it1+it2=<1*G+ -1
  with precondition: [A>=2,G>=2] 

Solved cost expressions of start0(A,B,C,D,E,F,G,H): 
start0(A,B,C,D,E,F,G,H):[33]: 2  with precondition: [0>=A] 
start0(A,B,C,D,E,F,G,H):[34]: 2  with precondition: [0>=G+1] 
start0(A,B,C,D,E,F,G,H):[35]: 2  with precondition: [G=0,A>=1] 
start0(A,B,C,D,E,F,G,H):[36]: 3  with precondition: [A=1,G>=2] 
start0(A,B,C,D,E,F,G,H):[37]: 3  with precondition: [G=1,A>=1] 
start0(A,B,C,D,E,F,G,H):[38]: 2*G+ -1  with precondition: [A>=2,G>=A+1] 
start0(A,B,C,D,E,F,G,H):[39]: 2*G+1  with precondition: [A>=2,G>=2] 
Maximum cost of start0(A,B,C,D,E,F,G,H): max([2*G+1,3]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 18 ms.
Invariants computed in 60 ms.
----Backward Invariants 33 ms.
----Transitive Invariants 7 ms.
Refinement performed in 61 ms.
Termination proved in 28 ms.
Upper bounds computed in 78 ms.
----Phase cost structures 36 ms.
--------Equation cost structures 34 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 36 ms.
----Solving cost expressions 1 ms.

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