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

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

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

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

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

lbl62(A,B,C,D,E,F,G,H,I,J,K,L,M):[[19,20],21]: 2+it1*(1)+it2*(2)
  Such that:it1=<nat(min([1*A+ -1,1*D+ -1,1*F+ -1]))*min([1*A+ -1,1*F+ -1])+min([1*B,1*A+ -1,1*F+ -1]),it2=<1*A+ -1,it2=<1*D+ -1,it2=<1*F+ -1,it2=<nat(min([1*A+ -1,1*D+ -1,1*F+ -1]))*min([1*A+ -1,1*F+ -1])+min([1*B,1*A+ -1,1*F+ -1])+min([1,-1*B+1,1*D+ -1])
  with precondition: [G=1,A=F,A>=2,B>=0,D>=1,A>=B+1,A>=D,B+D>=2] 

lbl62(A,B,C,D,E,F,G,H,I,J,K,L,M):[[19,20],22]: 1+it1*(1)+it2*(2)
  Such that:it1=<nat(min([1*A+ -1,1*D+ -1,1*F+ -1]))*min([1*A+ -1,1*F+ -1])+min([1*B,1*A+ -1,1*F+ -1]),it2=<1*A+ -1,it2=<1*D+ -1,it2=<1*F+ -1,it2=<nat(min([1*A+ -1,1*D+ -1,1*F+ -1]))*min([1*A+ -1,1*F+ -1])+min([1*B,1*A+ -1,1*F+ -1])+min([1,-1*B+1,1*D+ -1])
  with precondition: [G=1,A=F,A>=2,B>=0,D>=1,A>=B+1,A>=D,B+D>=2] 

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

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

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

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

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

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

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

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

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

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

Solved cost expressions of start0(A,B,C,D,E,F): 
start0(A,B,C,D,E,F):[30]: 2  with precondition: [0>=A] 
start0(A,B,C,D,E,F):[31]: 4  with precondition: [A=1] 
start0(A,B,C,D,E,F):[32]: 3  with precondition: [A=1] 
start0(A,B,C,D,E,F):[33]: nat(min([1*A+ -1,1*A+ -1+ (1*A+ -1)* (1*A+ -1)+ (-1*A+2)]))*2+nat(1*A+ -1+ (1*A+ -1)* (1*A+ -1))+4  with precondition: [A>=2] 
start0(A,B,C,D,E,F):[34]: nat(min([1*A+ -1,1*A+ -1+ (1*A+ -1)* (1*A+ -1)+ (-1*A+2)]))*2+nat(1*A+ -1+ (1*A+ -1)* (1*A+ -1))+3  with precondition: [A>=2] 
Maximum cost of start0(A,B,C,D,E,F): max([4,nat(min([1*A+ -1,1*A+ -1+ (1*A+ -1)* (1*A+ -1)+ (-1*A+2)]))*2+nat(1*A+ -1+ (1*A+ -1)* (1*A+ -1))+3,nat(min([1*A+ -1,1*A+ -1+ (1*A+ -1)* (1*A+ -1)+ (-1*A+2)]))*2+nat(1*A+ -1+ (1*A+ -1)* (1*A+ -1))+4]) 
Asymptotic class: n^2 
Time statistics: 
Partial evaluation computed in 13 ms.
Invariants computed in 40 ms.
----Backward Invariants 20 ms.
----Transitive Invariants 5 ms.
Refinement performed in 42 ms.
Termination proved in 11 ms.
Upper bounds computed in 111 ms.
----Phase cost structures 60 ms.
--------Equation cost structures 56 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 43 ms.
----Solving cost expressions 3 ms.

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