warning: Ignored call to stop/8 in equation start/8 
warning: Ignored call to stop/8 in equation lbl6/8 
warning: Ignored call to stop/8 in equation cut/8 
Inferred cost of lbl141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): 
lbl141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[23]: 1
  with precondition: [E=0,I=0,N=0,B=C,A=D,O=F,B=G,Q=H,A=J,B=K,B=L,A=M,B=P,A>=2,B>=A+1] 

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

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

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

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

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],28,31]: 2+it1*(1)+it2*(2)
  Such that:it1=<nat(min([1*K+ -1,1*L+ -1,1*P+ -1,1*B+ -1*G+ -1,1*C+ -1*G+ -1,1*K+ -1*G+ -1]))*min([1*A+ -1,1*B+ -2,1*C+ -2,1*D+ -1,1*J+ -1,1*K+ -2,1*L+ -2,1*M+ -1,1*P+ -2])+min([1*A+ -1*E,1*B+ -2,1*C+ -2,1*D+ -1*E,1*J+ -1,1*K+ -2,1*L+ -2,1*M+ -1,1*M+ -1*E]),it1=<nat(min([1*K+ -1,1*L+ -1,1*P+ -1,1*B+ -1*G+ -1,1*C+ -1*G+ -1,1*K+ -1*G+ -1]))*min([1*B+ -2,1*C+ -2,1*K+ -2,1*L+ -2,1*P+ -2])+min([1*B+ -2,1*C+ -2,1*K+ -2,1*L+ -2,1*P+ -2,1*L+ -1*E+ -1]),it2=<1*K+ -1,it2=<1*L+ -1,it2=<1*P+ -1,it2=<1*B+ -1*G+ -1,it2=<1*C+ -1*G+ -1,it2=<1*K+ -1*G+ -1
  with precondition: [I=1,N=0,B=C,A=D,A=J,B=K,B=L,A=M,F=O,B=P,H=Q,A>=2,E>=1,G>=0,B>=A+1,A>=E,B>=G+1,A+B>=E+G+2] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],30]: 1+it1*(1)+it2*(2)
  Such that:it1=<nat(min([1*B+ -1*G+ -1,1*C+ -1*G+ -1]))*min([1*A+ -1,1*B+ -2,1*C+ -2,1*D+ -1])+min([1*A+ -1*E,1*D+ -1*E,-1*E+1*B+ -1,-1*E+1*C+ -1]),it1=<nat(min([1*B+ -1*G+ -1,1*C+ -1*G+ -1]))*min([1*B+ -2,1*C+ -2])+min([1*B+ -1*E+ -1,1*C+ -1*E+ -1]),it2=<-1*G+1*B+ -1,it2=<-1*G+1*C+ -1,it2=<1*B+ -1*G+ -1,it2=<1*C+ -1*G+ -1
  with precondition: [I=1,B=C,A=D,A>=2,E>=1,G>=0,B>=A+1,A>=E,B>=G+1,A+B>=E+G+2] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],31]: 0+it1*(1)+it2*(2)
  Such that:it1=<nat(min([1*K+ -1,1*L+ -1,1*B+ -1*G+ -1,1*C+ -1*G+ -1,1*K+ -1*G+ -1]))*min([1*A+ -1,1*B+ -2,1*C+ -2,1*D+ -1,1*J+ -1,1*K+ -2,1*L+ -2,1*M+ -1])+min([1*A+ -1*E,1*B+ -2,1*C+ -2,1*D+ -1*E,1*J+ -1,1*J+ -1*E,1*K+ -2,1*L+ -2,1*M+ -1]),it1=<nat(min([1*K+ -1,1*L+ -1,1*B+ -1*G+ -1,1*C+ -1*G+ -1,1*K+ -1*G+ -1]))*min([1*B+ -2,1*C+ -2,1*K+ -2,1*L+ -2])+min([1*B+ -2,1*C+ -2,1*K+ -2,1*L+ -2,1*K+ -1*E+ -1]),it2=<1*P,it2=<1*B+ -1,it2=<1*C+ -1,it2=<1*K+ -1,it2=<1*L+ -1,it2=<1*P+ -1*G,it2=<1*B+ -1*G+ -1,it2=<1*C+ -1*G+ -1,it2=<1*K+ -1*G+ -1
  with precondition: [I=1,B=C,A=D,A=J,B=K,B=L,A=M,F=O,H=Q,A>=2,E>=1,G>=0,B>=A+1,A>=E,P>=G,A>=N,B>=P+1,N+P>=G+2,A+P>=E+G+1] 

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

Inferred cost of cut(A,B,C,D,E,F,G,H): 
cut(A,B,C,D,E,F,G,H):[35]: 1
  with precondition: [E=0,B=C,A=D,B=G,A>=2,B>=A+1] 

Inferred cost of loop_cont_lbl121(A,B,C,D,E,F,G,H): 
loop_cont_lbl121(A,B,C,D,E,F,G,H):[37]: 1
  with precondition: [E=0,B=C,A=D,B=G,A>=2,B>=A+1] 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Solved cost expressions of start0(A,B,C,D,E,F,G,H): 
start0(A,B,C,D,E,F,G,H):[47]: 2  with precondition: [0>=A] 
start0(A,B,C,D,E,F,G,H):[48]: 3  with precondition: [A>=1,A>=C] 
start0(A,B,C,D,E,F,G,H):[49]: 3  with precondition: [A=1,C>=2] 
start0(A,B,C,D,E,F,G,H):[50]: 2  with precondition: [A>=1,C>=A+1] 
start0(A,B,C,D,E,F,G,H):[51]: 2*C+ -2+nat(min([1*A+ -1+ (1*C+ -1)* (1*A+ -1),1*C+ -2+ (1*C+ -1)* (1*C+ -2)]))+4  with precondition: [A>=2,C>=A+1] 
start0(A,B,C,D,E,F,G,H):[52]: 2*C+ -2+nat(min([1*A+ -1+ (1*C+ -1)* (1*A+ -1),1*C+ -2+ (1*C+ -1)* (1*C+ -2)]))+3  with precondition: [A>=2,C>=A+1] 
start0(A,B,C,D,E,F,G,H):[53]: 2*C+ -2+nat(min([1*A+ -1+ (1*C+ -1)* (1*A+ -1),1*C+ -2+ (1*C+ -1)* (1*C+ -2)]))+2  with precondition: [A>=2,C>=A+1] 
Maximum cost of start0(A,B,C,D,E,F,G,H): max([3,2*C+ -2+nat(min([1*A+ -1+ (1*C+ -1)* (1*A+ -1),1*C+ -2+ (1*C+ -1)* (1*C+ -2)]))+2,2*C+ -2+nat(min([1*A+ -1+ (1*C+ -1)* (1*A+ -1),1*C+ -2+ (1*C+ -1)* (1*C+ -2)]))+3,2*C+ -2+nat(min([1*A+ -1+ (1*C+ -1)* (1*A+ -1),1*C+ -2+ (1*C+ -1)* (1*C+ -2)]))+4]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 21 ms.
Invariants computed in 95 ms.
----Backward Invariants 56 ms.
----Transitive Invariants 7 ms.
Refinement performed in 85 ms.
Termination proved in 29 ms.
Upper bounds computed in 492 ms.
----Phase cost structures 268 ms.
--------Equation cost structures 247 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 204 ms.
----Solving cost expressions 11 ms.

Compressed phase information: 2 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 771 ms.