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

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

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

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

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

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

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

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

Solved cost expressions of start(A,B,C,D,E,F): 
start(A,B,C,D,E,F):[16]: 1  with precondition: [E+1=C,A=F,A>=0,D>=0,B>=A+1,A+B>=2*E,2*E+2>=A+B] 
start(A,B,C,D,E,F):[17]: -1*A+1*B+2  with precondition: [E+1=C,A=F,A>=0,D>=0,E>=A,B>=E+1,A+B>=2*E,2*E+2>=A+B] 
start(A,B,C,D,E,F):[18]: -1*A+1*B+2  with precondition: [E+1=C,A=F,A>=0,D>=0,E>=A,B>=E+1,A+B>=2*E,2*E+2>=A+B] 
start(A,B,C,D,E,F):[19]: -1*A+1*B+1  with precondition: [E+1=C,A=F,A>=0,D>=0,E>=A,B>=E+1,A+B>=2*E,2*E+2>=A+B] 
Maximum cost of start(A,B,C,D,E,F): max([-1*A+1*B+2,1]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 9 ms.
Invariants computed in 132 ms.
----Backward Invariants 63 ms.
----Transitive Invariants 14 ms.
Refinement performed in 71 ms.
Termination proved in 76 ms.
Upper bounds computed in 3465 ms.
----Phase cost structures 419 ms.
--------Equation cost structures 416 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 2989 ms.
----Solving cost expressions 46 ms.

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