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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[31],33]: 2+it1*(1)+it2*(2+it3*(2+it4*(1)))
  Such that:it1=<1*A+ -1,it1=<1*B+ -1,it1+it2=<1*A+ -1*C,it1+it2=<1*B+ -1*C,it2=<1*A+ -1*C,it2=<1*B+ -1*C
            it3=<1*B+ -1,it3=<1*A+ -1,it3=<-1*C+1*B,it3=<-1*C+1*A
            it4=<1*B+ -1,it4=<1*A+ -1,it4=<-1*C+1*B,it4=<-1*C+1*A
  with precondition: [I=1,A=B,C>=1,A>=C+2] 

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

d(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[31],35]: 2+it1*(2+it2*(1))+it3*(2+it4*(2+it5*(1)))
  Such that:it1+it3=<1*A+ -1*C,it1+it3=<1*B+ -1*C,it1+it3=<1*A+ -1*C+ -1,it1+it3=<1*B+ -1*C+ -1,it3=<1*A+ -1*C,it3=<1*B+ -1*C
            it2=<-1*C+1*B+ -1,it2=<-1*C+1*A+ -1,it2=<1*B+ -1,it2=<1*A+ -1
            it4=<1*B+ -1,it4=<1*A+ -1,it4=<-1*C+1*B,it4=<-1*C+1*A
            it5=<1*B+ -1,it5=<1*A+ -1,it5=<-1*C+1*B,it5=<-1*C+1*A
  with precondition: [I=1,A=B,C>=1,A>=C+3] 

d(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[31],36]: 2+it1*(1)+it2*(2+it3*(1))+it4*(2+it5*(2+it6*(1)))
  Such that:it1=<1*A+ -1,it1=<1*B+ -1,it1+it4=<1*A+ -1*C,it1+it4=<1*B+ -1*C,it2+it4=<1*A+ -1*C,it2+it4=<1*B+ -1*C,it2+it4=<1*A+ -1*C+ -1,it2+it4=<1*B+ -1*C+ -1,it4=<1*A+ -1*C,it4=<1*B+ -1*C
            it3=<-1*C+1*B+ -1,it3=<-1*C+1*A+ -1,it3=<1*B+ -1,it3=<1*A+ -1
            it5=<1*B+ -1,it5=<1*A+ -1,it5=<-1*C+1*B,it5=<-1*C+1*A
            it6=<1*B+ -1,it6=<1*A+ -1,it6=<-1*C+1*B,it6=<-1*C+1*A
  with precondition: [I=1,A=B,C>=1,A>=C+3] 

d(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[31],37]: 1+it1*(2+it2*(1))+it3*(2+it4*(2+it5*(1)))
  Such that:it1=<1*A+ -1,it1=<1*B+ -1,it1+it3=<1*A+ -1*C,it1+it3=<1*B+ -1*C,it3=<1*A+ -1*C,it3=<1*B+ -1*C
            it2=<-1*C+1*B+ -1,it2=<-1*C+1*A+ -1,it2=<1*B+ -1,it2=<1*A+ -1
            it4=<1*B+ -1,it4=<1*A+ -1,it4=<-1*C+1*B,it4=<-1*C+1*A
            it5=<1*B+ -1,it5=<1*A+ -1,it5=<-1*C+1*B,it5=<-1*C+1*A
  with precondition: [I=1,A=B,C>=1,A>=C+2] 

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

Inferred cost of a(A,B,C,D,E,F,G,H): 
a(A,B,C,D,E,F,G,H):[40]: 3
  with precondition: [A=B,D=C,F=E,H=G,A>=2] 

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

a(A,B,C,D,E,F,G,H):[42]: 2
  with precondition: [A=B,D=C,F=E,H=G,A>=2] 

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

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

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

a(A,B,C,D,E,F,G,H):[46]: 2
  with precondition: [A=1,B=1,D=C,F=E,H=G] 

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

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

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

a(A,B,C,D,E,F,G,H):[50]: 3+it1*(2+it2*(1))+it3*(2+it4*(2+it5*(1)))
  Such that:it1+it3=<1*A+ -2,it1+it3=<1*A+ -1,it1+it3=<1*B+ -2,it1+it3=<1*B+ -1,it3=<1*A+ -1,it3=<1*B+ -1
            it2=<1*B+ -1,it2=<1*B+ -2,it2=<1*A+ -1,it2=<1*A+ -2
            it4=<1*B+ -1,it4=<1*A+ -1
            it5=<1*B+ -1,it5=<1*A+ -1
  with precondition: [A=B,D=C,F=E,H=G,A>=4] 

a(A,B,C,D,E,F,G,H):[51]: 3+it1*(1)+it2*(2+it3*(1))+it4*(2+it5*(2+it6*(1)))
  Such that:it1=<1*A+ -1,it1=<1*B+ -1,it1+it4=<1*A+ -1,it1+it4=<1*B+ -1,it2+it4=<1*A+ -2,it2+it4=<1*A+ -1,it2+it4=<1*B+ -2,it2+it4=<1*B+ -1,it4=<1*A+ -1,it4=<1*B+ -1
            it3=<1*B+ -1,it3=<1*B+ -2,it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*B+ -1,it5=<1*A+ -1
            it6=<1*B+ -1,it6=<1*A+ -1
  with precondition: [A=B,D=C,F=E,H=G,A>=4] 

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

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

Inferred cost of start(A,B,C,D,E,F,G,H): 
start(A,B,C,D,E,F,G,H):[55]: 4
  with precondition: [B=A,D=C,F=E,H=G,B>=2] 

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

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

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

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

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

start(A,B,C,D,E,F,G,H):[61]: 3
  with precondition: [A=1,B=1,D=C,F=E,H=G] 

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

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

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

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

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

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

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

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

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

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

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

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

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

start0(A,B,C,D,E,F,G,H):[76]: 4
  with precondition: [A=1] 

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

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

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

start0(A,B,C,D,E,F,G,H):[80]: 5+it1*(2+it2*(1))+it3*(2+it4*(2+it5*(1)))
  Such that:it1+it3=<1*A+ -2,it1+it3=<1*A+ -1,it3=<1*A+ -1
            it2=<1*A+ -1,it2=<1*A+ -2
            it4=<1*A+ -1
            it5=<1*A+ -1
  with precondition: [A>=4] 

start0(A,B,C,D,E,F,G,H):[81]: 5+it1*(1)+it2*(2+it3*(1))+it4*(2+it5*(2+it6*(1)))
  Such that:it1=<1*A+ -1,it1+it4=<1*A+ -1,it2+it4=<1*A+ -2,it2+it4=<1*A+ -1,it4=<1*A+ -1
            it3=<1*A+ -1,it3=<1*A+ -2
            it5=<1*A+ -1
            it6=<1*A+ -1
  with precondition: [A>=4] 

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

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

Solved cost expressions of start0(A,B,C,D,E,F,G,H): 
start0(A,B,C,D,E,F,G,H):[70]: 5  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H):[71]: 1*A+4  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H):[72]: 4  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H):[73]: (1*A+1)* (1*A+ -2)+5  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H):[74]: 1*A+ -1+ (1*A+1)* (1*A+ -2)+5  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H):[75]: (1*A+1)* (1*A+ -1)+4  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H):[76]: 4  with precondition: [A=1] 
start0(A,B,C,D,E,F,G,H):[77]: (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2)+5  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H):[78]: max([1*A+ -1, (1*A+ -1)*nat((1*A+1)* (1*A+ -1)+2)])+5  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H):[79]: (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2)+4  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H):[80]: max([ (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2), (1*A+ -2)* (1*A)])+5  with precondition: [A>=4] 
start0(A,B,C,D,E,F,G,H):[81]: max([1*A+ -1+max([ (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2), (1*A+ -2)* (1*A)]),1*A+ -1+ (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2),1*A+ -1+ (1*A+ -2)* (1*A)])+5  with precondition: [A>=4] 
start0(A,B,C,D,E,F,G,H):[82]: max([ (1*A+ -1)*nat((1*A+1)* (1*A+ -1)+2), (1*A+ -1)* (1*A)])+4  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H):[83]: (1*A+ -1)*nat((1*A+1)* (1*A+ -1)+2)+4  with precondition: [A>=2] 
Maximum cost of start0(A,B,C,D,E,F,G,H): max([1*A+4,5,max([ (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2), (1*A+ -2)* (1*A)])+5,max([ (1*A+ -1)*nat((1*A+1)* (1*A+ -1)+2), (1*A+ -1)* (1*A)])+4,max([1*A+ -1, (1*A+ -1)*nat((1*A+1)* (1*A+ -1)+2)])+5,max([1*A+ -1+max([ (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2), (1*A+ -2)* (1*A)]),1*A+ -1+ (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2),1*A+ -1+ (1*A+ -2)* (1*A)])+5, (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2)+4, (1*A+ -2)*nat((1*A+1)* (1*A+ -1)+2)+5, (1*A+ -1)*nat((1*A+1)* (1*A+ -1)+2)+4, (1*A+1)* (1*A+ -2)+5, (1*A+1)* (1*A+ -1)+4,1*A+ -1+ (1*A+1)* (1*A+ -2)+5]) 
Asymptotic class: n^3 
Time statistics: 
Partial evaluation computed in 24 ms.
Invariants computed in 174 ms.
----Backward Invariants 108 ms.
----Transitive Invariants 12 ms.
Refinement performed in 141 ms.
Termination proved in 35 ms.
Upper bounds computed in 835 ms.
----Phase cost structures 424 ms.
--------Equation cost structures 345 ms.
--------Inductive compression(1) 2 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 383 ms.
----Solving cost expressions 8 ms.

Compressed phase information: 10 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 1266 ms.