warning: Ignored call to stop/12 in equation start/12 
warning: Ignored call to stop/12 in equation lbl53/12 
warning: Ignored call to stop/12 in equation lbl13/12 
Inferred cost of lbl53(A,B,C,D,E,F,G,H,I,J,K,L): 
lbl53(A,B,C,D,E,F,G,H,I,J,K,L):[18]: 1
  with precondition: [A=2,B=0,D=0,H=2,I=1,K=1] 

lbl53(A,B,C,D,E,F,G,H,I,J,K,L):[19]: 2
  with precondition: [A=2,B=0,D=1,H=2,I=1,K=1] 

lbl53(A,B,C,D,E,F,G,H,I,J,K,L):[[14,15,16,17],18]: 1+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<1*H+ -2,it1+it2=<1*K+ -1,it1+it2=<nat(min([1*A+ -2,1*H+ -2,1*K+ -1]))*max([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1*A+ -1*I+ -1,1*H+ -1*B+ -2,1*H+ -1*I+ -1])+min([1*B,1*A+ -2,1*H+ -2,1*I+ -1,1*K+ -1,1*D+1*K+ -2]),it2=<nat(min([1*A+ -2,1*H+ -2,1*K+ -1]))*max([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1*A+ -1*I+ -1,1*H+ -1*B+ -2,1*H+ -1*I+ -1])+min([1,1*D]),it3+it4=<nat(min([1*A+ -2,1*H+ -2,1*K+ -1]))*max([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])])+min([1*A+ -2,1*H+ -2,1*K+ -1,1*K+ -1*I,1*K+ -1*B+ -1]),it3+it4=<nat(min([1*A+ -2,1*H+ -2,1*K+ -1]))*max([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1*A+ -1*I+ -1,1*H+ -1*B+ -2,1*H+ -1*I+ -1])
  with precondition: [I=B+1,A=H,1>=D,D>=0,I>=1,K>=2,A>=K+1,D+K>=I+1] 

lbl53(A,B,C,D,E,F,G,H,I,J,K,L):[[14,15,16,17],19]: 2+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<1*H+ -2,it1+it2=<1*K+ -1,it1+it2=<nat(min([1*A+ -2,1*H+ -2,1*K+ -1]))*max([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1*A+ -1*I+ -1,1*H+ -1*B+ -2,1*H+ -1*I+ -1])+min([1*B,1*A+ -2,1*H+ -2,1*I+ -1,1*K+ -1,1*D+1*K+ -2]),it2=<nat(min([1*A+ -2,1*H+ -2,1*K+ -1]))*max([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1*A+ -1*I+ -1,1*H+ -1*B+ -2,1*H+ -1*I+ -1])+min([1,1*D]),it3+it4=<nat(min([1*A+ -2,1*H+ -2,1*K+ -1]))*max([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])])+min([1*A+ -2,1*H+ -2,1*K+ -1,1*K+ -1*I,1*K+ -1*B+ -1]),it3+it4=<nat(min([1*A+ -2,1*H+ -2,1*K+ -1]))*max([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1*A+ -1*I+ -1,1*H+ -1*B+ -2,1*H+ -1*I+ -1])
  with precondition: [I=B+1,A=H,1>=D,D>=0,I>=1,K>=2,A>=K+1,D+K>=I+1] 

Inferred cost of start(A,B,C,D,E,F,G,H,I,J,K,L): 
start(A,B,C,D,E,F,G,H,I,J,K,L):[21]: 1
  with precondition: [H=A,C=B,E=D,G=F,J=I,L=K,1>=H] 

start(A,B,C,D,E,F,G,H,I,J,K,L):[22]: 4
  with precondition: [A=2,H=2,C=B,E=D,G=F,J=I,L=K] 

start(A,B,C,D,E,F,G,H,I,J,K,L):[23]: 3+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<1*H+ -2,it1+it2=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([0,min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),0,min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),it2=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1,1]),it3+it4=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])]),min([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),it3+it4=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])
  with precondition: [H=A,C=B,E=D,G=F,J=I,L=K,H>=3] 

start(A,B,C,D,E,F,G,H,I,J,K,L):[24]: 4+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<1*H+ -2,it1+it2=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([0,min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),0,min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),it2=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1,1]),it3+it4=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])]),min([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),it3+it4=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])
  with precondition: [H=A,C=B,E=D,G=F,J=I,L=K,H>=3] 

start(A,B,C,D,E,F,G,H,I,J,K,L):[25]: 2
  with precondition: [A=2,H=2,C=B,E=D,G=F,J=I,L=K] 

start(A,B,C,D,E,F,G,H,I,J,K,L):[26]: 2+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<1*H+ -2,it1+it2=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([0,min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),0,min([1*A+ -2,1*H+ -2]),min([1*A+ -3,1*H+ -3])]),it2=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1,0]),it3+it4=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])]),min([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),it3+it4=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])
  with precondition: [H=A,C=B,E=D,G=F,J=I,L=K,H>=3] 

start(A,B,C,D,E,F,G,H,I,J,K,L):[27]: 3+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<1*H+ -2,it1+it2=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([0,min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),0,min([1*A+ -2,1*H+ -2]),min([1*A+ -3,1*H+ -3])]),it2=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])+min([1,0]),it3+it4=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])]),min([min([1*A+ -3,1*H+ -3]),min([1*A+ -3,1*H+ -3])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),it3+it4=<nat(min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]))*max([min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])]),min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])])+min([min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2]),min([1*A+ -2,1*H+ -2])])
  with precondition: [H=A,C=B,E=D,G=F,J=I,L=K,H>=3] 

Inferred cost of start0(A,B,C,D,E,F,G,H,I,J,K,L): 
start0(A,B,C,D,E,F,G,H,I,J,K,L):[29]: 2
  with precondition: [1>=A] 

start0(A,B,C,D,E,F,G,H,I,J,K,L):[30]: 5
  with precondition: [A=2] 

start0(A,B,C,D,E,F,G,H,I,J,K,L):[31]: 4+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])+min([0,min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),0,min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),it2=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])+min([1,1]),it3+it4=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -3,1*A+ -3]),min([1*A+ -3,1*A+ -3])]),min([min([1*A+ -3,1*A+ -3]),min([1*A+ -3,1*A+ -3])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),it3+it4=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])
  with precondition: [A>=3] 

start0(A,B,C,D,E,F,G,H,I,J,K,L):[32]: 5+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])+min([0,min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),0,min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),it2=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])+min([1,1]),it3+it4=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -3,1*A+ -3]),min([1*A+ -3,1*A+ -3])]),min([min([1*A+ -3,1*A+ -3]),min([1*A+ -3,1*A+ -3])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),it3+it4=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])
  with precondition: [A>=3] 

start0(A,B,C,D,E,F,G,H,I,J,K,L):[33]: 3
  with precondition: [A=2] 

start0(A,B,C,D,E,F,G,H,I,J,K,L):[34]: 3+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])+min([0,min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),0,min([1*A+ -2,1*A+ -2]),min([1*A+ -3,1*A+ -3])]),it2=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])+min([1,0]),it3+it4=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -3,1*A+ -3]),min([1*A+ -3,1*A+ -3])]),min([min([1*A+ -3,1*A+ -3]),min([1*A+ -3,1*A+ -3])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),it3+it4=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])
  with precondition: [A>=3] 

start0(A,B,C,D,E,F,G,H,I,J,K,L):[35]: 4+it1*(3)+it2*(2)+it3*(2)+it4*(1)
  Such that:it1+it2=<1*A+ -2,it1+it2=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])+min([0,min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),0,min([1*A+ -2,1*A+ -2]),min([1*A+ -3,1*A+ -3])]),it2=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])+min([1,0]),it3+it4=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -3,1*A+ -3]),min([1*A+ -3,1*A+ -3])]),min([min([1*A+ -3,1*A+ -3]),min([1*A+ -3,1*A+ -3])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),it3+it4=<nat(min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]))*max([min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])]),min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])])+min([min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2]),min([1*A+ -2,1*A+ -2])])
  with precondition: [A>=3] 

Solved cost expressions of start0(A,B,C,D,E,F,G,H,I,J,K,L): 
start0(A,B,C,D,E,F,G,H,I,J,K,L):[29]: 2  with precondition: [1>=A] 
start0(A,B,C,D,E,F,G,H,I,J,K,L):[30]: 5  with precondition: [A=2] 
start0(A,B,C,D,E,F,G,H,I,J,K,L):[31]: max([nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2,nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*3])+max([nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)])),nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2])+4  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H,I,J,K,L):[32]: max([nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2,nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*3])+max([nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)])),nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2])+5  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H,I,J,K,L):[33]: 3  with precondition: [A=2] 
start0(A,B,C,D,E,F,G,H,I,J,K,L):[34]: max([nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2,nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*3])+max([nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)])),nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2])+3  with precondition: [A>=3] 
start0(A,B,C,D,E,F,G,H,I,J,K,L):[35]: max([nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2,nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*3])+max([nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)])),nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2])+4  with precondition: [A>=3] 
Maximum cost of start0(A,B,C,D,E,F,G,H,I,J,K,L): max([5,max([nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2,nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*3])+max([nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)])),nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2])+3,max([nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2,nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*3])+max([nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)])),nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2])+4,max([nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2,nat(min([1*A+ -2,1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*3])+max([nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)])),nat(min([1*A+ -2+ (1*A+ -2)* (1*A+ -3),1*A+ -2+ (1*A+ -2)* (1*A+ -2)]))*2])+5]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 25 ms.
Invariants computed in 60 ms.
----Backward Invariants 29 ms.
----Transitive Invariants 10 ms.
Refinement performed in 64 ms.
Termination proved in 30 ms.
Upper bounds computed in 454 ms.
----Phase cost structures 269 ms.
--------Equation cost structures 237 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 166 ms.
----Solving cost expressions 8 ms.

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