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

lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M):[26]: 0
  with precondition: [G=1,B=C,A=D,M=F,A=H,B=I,B=J,A=K,E=L,E>=0,A>=E+2,B>=A+E+1] 

lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M):[[24],25]: 1+it1*(1)
  Such that:it1=<1*E,it1=<1*A+ -2,it1=<1*D+ -2,it1=<1*K+ -2,it1=<-1*A+1*B+ -1,it1=<-1*D+1*I+ -1,it1=<-1*K+1*B+ -1,it1=<-1*K+1*C+ -1
  with precondition: [G=0,L=0,B=C,A=D,A=H,B=I,B=J,A=K,F=M,E>=1,A>=E+2,B>=A+E+1] 

lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M):[[24],26]: 0+it1*(1)
  Such that:it1=<1*E,it1=<1*A+ -2,it1=<1*D+ -2,it1=<1*E+ -1*L,it1=<-1*A+1*B+ -1,it1=<-1*D+1*B+ -1,it1=<-1*D+1*C+ -1,it1=<-1*D+1*I+ -1,it1=<-1*L+1*A+ -2,it1=<-1*L+1*D+ -2,it1=<-1*A+ -1*L+1*B+ -1,it1=<-1*D+ -1*L+1*B+ -1,it1=<-1*D+ -1*L+1*C+ -1,it1=<-1*D+ -1*L+1*I+ -1
  with precondition: [G=1,B=C,A=D,A=H,B=I,B=J,A=K,F=M,L>=0,A>=E+2,E>=L+1,B>=A+E+1] 

Inferred cost of lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M): 
lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[31]: 1
  with precondition: [G=1,B=C,A=D,B=A+E,B>=A+1,2*A>=B+1] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[32]: 1+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*D+ -2,it1=<1*E+ -1,it1=<-1*A+1*B+ -1,it1=<-1*D+1*B+ -1,it1=<-1*D+1*C+ -1,it1=<-1*E+1*B+ -2,it1=<-1*E+1*C+ -2,it1=<1*B+ -1*A+ -1,it1=<1*B+ -1*D+ -1,it1=<1*B+ -1*E+ -2,it1=<1*C+ -1*D+ -1,it1=<1*C+ -1*E+ -2
  with precondition: [G=1,B=C,A=D,B=A+E,B>=A+2,2*A>=B+1] 

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

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],29,33]: 3+it1*(1)
  Such that:it1=<1*E,it1=<-1*A+1*B,it1=<-1*D+1*I,it1=<-1*H+1*I,it1=<-1*K+1*B,it1=<-1*K+1*C,it1=<-1*K+1*I,it1=<-1*K+1*J,it1=<1*E+ -1,it1=<-2*D+1*I+1,it1=<-2*H+1*I+1,it1=<-2*K+1*B+1,it1=<-2*K+1*C+1,it1=<-2*K+1*I+1,it1=<-2*K+1*J+1,it1=<-1*A+1*B+ -1,it1=<-1*D+1*I+ -1,it1=<-1*H+1*I+ -1,it1=<-1*K+1*B+ -1,it1=<-1*K+1*C+ -1,it1=<-1*K+1*I+ -1,it1=<-1*K+1*J+ -1,it1=<1*E+ -1*A+1,it1=<1*E+ -1*K+1
  with precondition: [G=0,L=0,B=C,A=D,A=H,B=I,B=J,A=K,F=M,A>=2,E>=A+1,B>=A+E] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],29,34]: 2+it1*(1)
  Such that:it1=<1*E,it1=<-1*A+1*B,it1=<-1*D+1*I,it1=<-1*H+1*I,it1=<-1*K+1*B,it1=<-1*K+1*C,it1=<-1*K+1*I,it1=<-1*K+1*J,it1=<1*E+ -1,it1=<-2*D+1*I+1,it1=<-2*H+1*I+1,it1=<-2*K+1*B+1,it1=<-2*K+1*C+1,it1=<-2*K+1*I+1,it1=<-2*K+1*J+1,it1=<-1*A+1*B+ -1,it1=<-1*D+1*I+ -1,it1=<-1*H+1*I+ -1,it1=<-1*K+1*B+ -1,it1=<-1*K+1*C+ -1,it1=<-1*K+1*I+ -1,it1=<-1*K+1*J+ -1,it1=<1*E+ -1*A+1,it1=<1*E+ -1*K+1
  with precondition: [G=1,L=0,B=C,A=D,A=H,B=I,B=J,A=K,F=M,A>=2,E>=A+1,B>=A+E] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],30,33]: 3+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<1*E+ -4,it1=<1*H+ -2,it1=<1*I+ -4,it1=<1*J+ -4,it1=<1*K+ -2,it1=<1/2*B+ -3,it1=<1/2*C+ -3,it1=<1/2*I+ -3,it1=<1/2*J+ -3,it1=<-1*E+1*B+ -2,it1=<-1*E+1*C+ -2,it1=<1*B+ -2*D+ -1,it1=<1*B+ -1*K+ -1,it1=<1*C+ -2*D+ -1,it1=<1*C+ -1*K+ -1,it1=<1*I+ -2*A+ -1,it1=<1*I+ -2*D+ -1,it1=<1*I+ -2*H+ -1,it1=<1*I+ -2*K+ -1,it1=<1*I+ -1*K+ -1,it1=<1*J+ -2*K+ -1,it1=<1*J+ -1*K+ -1,it1+it2=<1*E+ -1,it1+it2=<-1*A+1*B+ -1,it1+it2=<-1*D+1*I+ -1,it1+it2=<-1*H+1*I+ -1,it1+it2=<-1*K+1*B+ -1,it1+it2=<-1*K+1*C+ -1,it1+it2=<-1*K+1*I+ -1,it1+it2=<-1*K+1*J+ -1,it2=<1*E,it2=<-1*A+1*B,it2=<-1*D+1*I,it2=<-1*H+1*I,it2=<-1*K+1*B,it2=<-1*K+1*C,it2=<-1*K+1*I,it2=<-1*K+1*J,it2=<-2*D+1*I+1,it2=<-2*H+1*I+1,it2=<-2*K+1*B+1,it2=<-2*K+1*C+1,it2=<-2*K+1*I+1,it2=<-2*K+1*J+1,it2=<1*E+ -1*A+1,it2=<1*E+ -1*K+1
  with precondition: [G=0,L=0,B=C,A=D,A=H,B=I,B=J,A=K,F=M,A>=3,E>=A+2,B>=A+E] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],30,34]: 2+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<1*E+ -4,it1=<1*H+ -2,it1=<1*I+ -4,it1=<1*J+ -4,it1=<1*K+ -2,it1=<1/2*B+ -3,it1=<1/2*C+ -3,it1=<1/2*I+ -3,it1=<1/2*J+ -3,it1=<-1*E+1*B+ -2,it1=<-1*E+1*C+ -2,it1=<1*B+ -2*D+ -1,it1=<1*B+ -1*K+ -1,it1=<1*C+ -2*D+ -1,it1=<1*C+ -1*K+ -1,it1=<1*I+ -2*A+ -1,it1=<1*I+ -2*D+ -1,it1=<1*I+ -2*H+ -1,it1=<1*I+ -2*K+ -1,it1=<1*I+ -1*K+ -1,it1=<1*J+ -2*K+ -1,it1=<1*J+ -1*K+ -1,it1+it2=<1*E+ -1,it1+it2=<-1*A+1*B+ -1,it1+it2=<-1*D+1*I+ -1,it1+it2=<-1*H+1*I+ -1,it1+it2=<-1*K+1*B+ -1,it1+it2=<-1*K+1*C+ -1,it1+it2=<-1*K+1*I+ -1,it1+it2=<-1*K+1*J+ -1,it2=<1*E,it2=<-1*A+1*B,it2=<-1*D+1*I,it2=<-1*H+1*I,it2=<-1*K+1*B,it2=<-1*K+1*C,it2=<-1*K+1*I,it2=<-1*K+1*J,it2=<-2*D+1*I+1,it2=<-2*H+1*I+1,it2=<-2*K+1*B+1,it2=<-2*K+1*C+1,it2=<-2*K+1*I+1,it2=<-2*K+1*J+1,it2=<1*E+ -1*A+1,it2=<1*E+ -1*K+1
  with precondition: [G=1,L=0,B=C,A=D,A=H,B=I,B=J,A=K,F=M,A>=3,E>=A+2,B>=A+E] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],31]: 1+it1*(1)
  Such that:it1=<1*E,it1=<-1*A+1*B,it1=<-1*D+1*B,it1=<-1*D+1*C,it1=<1*B+ -3,it1=<1*C+ -3,it1=<1*E+ -1,it1=<-1*A+1*B+ -1,it1=<-1*D+1*B+ -1,it1=<-1*D+1*C+ -1,it1=<1*E+ -1*A+1,it1=<1*E+ -1*D+1
  with precondition: [G=1,B=C,A=D,A>=2,E>=A+1,B>=A+E] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],32]: 1+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<1*E+ -4,it1=<-1*E+1*B+ -2,it1=<-1*E+1*C+ -2,it1=<1*B+ -1*D+ -1,it1=<1*C+ -1*D+ -1,it1+it2=<1*E+ -1,it1+it2=<-1*A+1*B+ -1,it1+it2=<-1*D+1*B+ -1,it1+it2=<-1*D+1*C+ -1,it2=<1*E,it2=<-1*A+1*B,it2=<-1*D+1*B,it2=<-1*D+1*C,it2=<1*B+ -5,it2=<1*C+ -5,it2=<1*E+ -2,it2=<1*E+ -1*A+1,it2=<1*E+ -1*D+1
  with precondition: [G=1,B=C,A=D,A>=3,E>=A+2,B>=A+E] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],33]: 1+it1*(1)
  Such that:it1=<1*E,it1=<-1*A+1*B,it1=<-1*D+1*I,it1=<-1*H+1*I,it1=<-1*K+1*B,it1=<-1*K+1*C,it1=<-1*K+1*I,it1=<-1*K+1*J,it1=<-2*D+1*I+1,it1=<-2*H+1*I+1,it1=<-2*K+1*B+1,it1=<-2*K+1*C+1,it1=<-2*K+1*I+1,it1=<-2*K+1*J+1,it1=<1*E+ -1*A+1,it1=<1*E+ -1*K+1
  with precondition: [G=0,L=0,B=C,A=D,A=H,B=I,B=J,A=K,F=M,A>=1,E>=A,B>=A+E] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],34]: 0+it1*(1)
  Such that:it1=<1*E,it1=<-1*K+1*B,it1=<-1*K+1*C,it1=<-1*K+1*I,it1=<-1*K+1*J,it1=<1*E+ -1*L,it1=<-2*H+1*B+1,it1=<-2*H+1*C+1,it1=<-2*H+1*I+1,it1=<-2*K+1*I+1,it1=<-2*K+1*J+1,it1=<-1*A+ -1*L+1*B,it1=<-1*D+ -1*L+1*I,it1=<-1*H+ -1*L+1*I,it1=<-1*K+ -1*L+1*B,it1=<-1*K+ -1*L+1*C,it1=<-1*K+ -1*L+1*I,it1=<-1*K+ -1*L+1*J,it1=<1*E+ -1*A+1,it1=<1*E+ -1*D+1,it1=<1*E+ -1*K+1
  with precondition: [G=1,B=C,A=D,A=H,B=I,B=J,A=K,F=M,A>=1,L>=0,B>=A+E,E>=A+L] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[29,33]: 3
  with precondition: [E=1,G=0,L=0,A+1=B,A+1=C,A=D,A=H,A+1=I,A+1=J,A=K,F=M,A>=2] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[29,34]: 2
  with precondition: [E=1,G=1,L=0,A+1=B,A+1=C,A=D,A=H,A+1=I,A+1=J,A=K,F=M,A>=2] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[30,33]: 3+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<1*E+ -1,it1=<1*H+ -2,it1=<1*I+ -4,it1=<1*J+ -4,it1=<1*K+ -2,it1=<2*A+ -5,it1=<2*D+ -5,it1=<2*H+ -5,it1=<2*K+ -5,it1=<1*B+ -1*E+ -2,it1=<1*B+ -1*H+ -1,it1=<1*C+ -1*A+ -1,it1=<1*C+ -1*E+ -2,it1=<1*C+ -1*H+ -1,it1=<1*E+1*K+ -4,it1=<1*I+ -1*K+ -1,it1=<1*J+ -1*D+ -1,it1=<1*J+ -1*E+ -2,it1=<1*J+ -1*H+ -1,it1=<1*J+ -1*K+ -1
  with precondition: [G=0,L=0,B=C,A=D,A=H,B=I,B=J,A=K,F=M,A+E=B,B>=A+2,2*A>=B+1] 

lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M):[30,34]: 2+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<1*E+ -1,it1=<1*H+ -2,it1=<1*I+ -4,it1=<1*J+ -4,it1=<1*K+ -2,it1=<2*A+ -5,it1=<2*D+ -5,it1=<2*H+ -5,it1=<2*K+ -5,it1=<1*B+ -1*E+ -2,it1=<1*B+ -1*H+ -1,it1=<1*C+ -1*A+ -1,it1=<1*C+ -1*E+ -2,it1=<1*C+ -1*H+ -1,it1=<1*E+1*K+ -4,it1=<1*I+ -1*K+ -1,it1=<1*J+ -1*D+ -1,it1=<1*J+ -1*E+ -2,it1=<1*J+ -1*H+ -1,it1=<1*J+ -1*K+ -1
  with precondition: [G=1,L=0,B=C,A=D,A=H,B=I,B=J,A=K,F=M,A+E=B,B>=A+2,2*A>=B+1] 

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

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

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

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

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

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

start(A,B,C,D,E,F):[45]: 5+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<1/2*B+ -3,it1=<1/2*C+ -3,it1=<1*B+ -2*D+ -1,it1=<1*B+ -1*D+ -4,it1=<1*B+ -1*D+ -1,it1=<1*C+ -2*A+ -1,it1=<1*C+ -2*D+ -1,it1=<1*C+ -1*D+ -4,it1=<1*C+ -1*D+ -1,it1+it2=<1*B+ -1*D+ -1,it1+it2=<1*C+ -1*D+ -1,it2=<1*B+ -1*D,it2=<1*C+ -1*D,it2=<1*B+ -2*D+1,it2=<1*C+ -2*A+1,it2=<1*C+ -2*D+1
  with precondition: [D=A,C=B,F=E,D>=3,C>=2*D+2] 

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

start(A,B,C,D,E,F):[47]: 5
  with precondition: [A+1=B,A+1=C,A=D,F=E,A>=2] 

start(A,B,C,D,E,F):[48]: 5+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<2*A+ -5,it1=<2*B+ -9,it1=<2*C+ -9,it1=<2*D+ -5,it1=<1*B+ -1*D+ -1,it1=<1*C+ -1*A+ -1,it1=<1*C+ -1*D+ -1
  with precondition: [D=A,C=B,F=E,2*D>=C+1,C>=D+2] 

start(A,B,C,D,E,F):[49]: 2
  with precondition: [D=A,C=B,F=E,2*D>=C+1,C>=D+1] 

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

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

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

start(A,B,C,D,E,F):[53]: 3+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<1/2*B+ -3,it1=<1/2*C+ -3,it1=<1*B+ -2*D+ -1,it1=<1*B+ -1*D+ -4,it1=<1*B+ -1*D+ -1,it1=<1*C+ -2*A+ -1,it1=<1*C+ -2*D+ -1,it1=<1*C+ -1*D+ -4,it1=<1*C+ -1*D+ -1,it1+it2=<1*B+ -1*D+ -1,it1+it2=<1*C+ -1*D+ -1,it2=<1*B+ -1*D,it2=<1*C+ -1*D,it2=<1*B+ -2*D+1,it2=<1*C+ -2*A+1,it2=<1*C+ -2*D+1
  with precondition: [D=A,C=B,F=E,D>=3,C>=2*D+2] 

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

start(A,B,C,D,E,F):[55]: 2+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<1/2*B+ -3,it1=<1/2*C+ -3,it1=<1*B+ -1*D+ -4,it1=<1*B+ -1*D+ -1,it1=<1*C+ -1*D+ -4,it1=<1*C+ -1*D+ -1,it1+it2=<1*B+ -1*D+ -1,it1+it2=<1*C+ -1*D+ -1,it2=<1*B+ -5,it2=<1*B+ -1*D,it2=<1*C+ -5,it2=<1*C+ -1*D,it2=<1*B+ -2*D+1,it2=<1*B+ -1*D+ -2,it2=<1*C+ -2*A+1,it2=<1*C+ -2*D+1,it2=<1*C+ -1*D+ -2
  with precondition: [D=A,C=B,F=E,D>=3,C>=2*D+2] 

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

start(A,B,C,D,E,F):[57]: 3
  with precondition: [A+1=B,A+1=C,A=D,F=E,A>=2] 

start(A,B,C,D,E,F):[58]: 3+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*B+ -4,it1=<1*C+ -4,it1=<1*D+ -2,it1=<2*A+ -5,it1=<2*B+ -9,it1=<2*C+ -9,it1=<2*D+ -5,it1=<1*B+ -1*D+ -1,it1=<1*C+ -1*A+ -1,it1=<1*C+ -1*D+ -1
  with precondition: [D=A,C=B,F=E,2*D>=C+1,C>=D+2] 

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

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

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

start0(A,B,C,D,E,F):[63]: 6+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*C+ -7,it1=<1*C+ -4,it1=<1/2*C+ -3,it1=<1*C+ -2*A+ -1,it1=<1*C+ -1*A+ -4,it1=<1*C+ -1*A+ -1,it1+it2=<1*C+ -4,it1+it2=<1*C+ -1*A+ -1,it2=<1*C+ -5,it2=<1*C+ -3,it2=<1*C+ -1*A,it2=<1*C+ -2*A+1
  with precondition: [A>=3,C>=2*A+2] 

start0(A,B,C,D,E,F):[64]: 4+it1*(1)
  Such that:it1=<1*C+ -1,it1=<1*C+ -1*A,it1=<1*C+ -2*A+1
  with precondition: [A>=1,C>=2*A] 

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

start0(A,B,C,D,E,F):[66]: 6+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*C+ -4,it1=<2*A+ -5,it1=<2*C+ -9,it1=<4*A+ -11,it1=<1/2*C+ -3/2,it1=<1*C+ -1*A+ -1
  with precondition: [C>=A+2,2*A>=C+1] 

start0(A,B,C,D,E,F):[67]: 3
  with precondition: [C>=A+1,2*A>=C+1] 

start0(A,B,C,D,E,F):[68]: 3+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*C+ -4,it1=<2*A+ -5,it1=<1/2*C+ -3/2,it1=<1*C+ -1*A+ -1
  with precondition: [C>=A+2,2*A>=C+1] 

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

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

start0(A,B,C,D,E,F):[71]: 4+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*C+ -7,it1=<1*C+ -4,it1=<1/2*C+ -3,it1=<1*C+ -2*A+ -1,it1=<1*C+ -1*A+ -4,it1=<1*C+ -1*A+ -1,it1+it2=<1*C+ -4,it1+it2=<1*C+ -1*A+ -1,it2=<1*C+ -5,it2=<1*C+ -3,it2=<1*C+ -1*A,it2=<1*C+ -2*A+1
  with precondition: [A>=3,C>=2*A+2] 

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

start0(A,B,C,D,E,F):[73]: 3+it1*(1)+it2*(1)
  Such that:it1=<1*A+ -2,it1=<1*C+ -7,it1=<1*C+ -4,it1=<1/2*C+ -3,it1=<1*C+ -1*A+ -4,it1=<1*C+ -1*A+ -1,it1+it2=<1*C+ -4,it1+it2=<1*C+ -1*A+ -1,it2=<1*C+ -5,it2=<1*C+ -3,it2=<1*C+ -1*A,it2=<1*C+ -2*A+1,it2=<1*C+ -1*A+ -2
  with precondition: [A>=3,C>=2*A+2] 

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

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

start0(A,B,C,D,E,F):[76]: 4+it1*(1)
  Such that:it1=<1*A+ -2,it1=<1*C+ -4,it1=<2*A+ -5,it1=<2*C+ -9,it1=<4*A+ -11,it1=<1/2*C+ -3/2,it1=<1*C+ -1*A+ -1
  with precondition: [C>=A+2,2*A>=C+1] 

Solved cost expressions of start0(A,B,C,D,E,F): 
start0(A,B,C,D,E,F):[60]: 2  with precondition: [0>=A] 
start0(A,B,C,D,E,F):[61]: 3  with precondition: [A>=1,A>=C] 
start0(A,B,C,D,E,F):[62]: -2*A+1*C+7  with precondition: [A>=2,C>=2*A+1] 
start0(A,B,C,D,E,F):[63]: -1*A+1*C+5  with precondition: [A>=3,C>=2*A+2] 
start0(A,B,C,D,E,F):[64]: -2*A+1*C+5  with precondition: [A>=1,C>=2*A] 
start0(A,B,C,D,E,F):[65]: 6  with precondition: [A+1=C,A>=2] 
start0(A,B,C,D,E,F):[66]: -1*A+1*C+5  with precondition: [C>=A+2,2*A>=C+1] 
start0(A,B,C,D,E,F):[67]: 3  with precondition: [C>=A+1,2*A>=C+1] 
start0(A,B,C,D,E,F):[68]: -1*A+1*C+2  with precondition: [C>=A+2,2*A>=C+1] 
start0(A,B,C,D,E,F):[69]: 2  with precondition: [A>=1,C>=A+1] 
start0(A,B,C,D,E,F):[70]: -2*A+1*C+5  with precondition: [A>=2,C>=2*A+1] 
start0(A,B,C,D,E,F):[71]: -1*A+1*C+3  with precondition: [A>=3,C>=2*A+2] 
start0(A,B,C,D,E,F):[72]: -2*A+1*C+4  with precondition: [A>=2,C>=2*A+1] 
start0(A,B,C,D,E,F):[73]: -1*A+1*C+2  with precondition: [A>=3,C>=2*A+2] 
start0(A,B,C,D,E,F):[74]: -2*A+1*C+3  with precondition: [A>=1,C>=2*A] 
start0(A,B,C,D,E,F):[75]: 4  with precondition: [A+1=C,A>=2] 
start0(A,B,C,D,E,F):[76]: -1*A+1*C+3  with precondition: [C>=A+2,2*A>=C+1] 
Maximum cost of start0(A,B,C,D,E,F): max([-1*A+1*C+5,6,-2*A+1*C+7]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 16 ms.
Invariants computed in 174 ms.
----Backward Invariants 110 ms.
----Transitive Invariants 6 ms.
Refinement performed in 123 ms.
Termination proved in 17 ms.
Upper bounds computed in 2439 ms.
----Phase cost structures 584 ms.
--------Equation cost structures 576 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 1820 ms.
----Solving cost expressions 13 ms.

Compressed phase information: 12 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 2813 ms.