warning: Ignored call to stop/10 in equation start/10 
warning: Ignored call to loop_cont_lbl81/10 in equation start/10 
Inferred cost of lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U): 
lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[26]: 2
  with precondition: [A=1,B=0,D=0,H=1,J=1,K=1,L=1,M=0,O=0,S=1,U=1,N=C,P=E,R=G,T=I,F=Q,0>=F+1] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[27]: 2
  with precondition: [A=1,B=0,D=0,H=1,J=1,K=1,L=1,M=0,O=0,S=1,U=1,N=C,P=E,R=G,T=I,F=Q,F>=4] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[28]: 2
  with precondition: [A=1,B=0,D=0,F=0,H=1,J=1,K=1,L=1,M=0,O=1,Q=0,S=1,U=1,N=C,P=E,R=G,T=I] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[29]: 2
  with precondition: [A=1,B=0,D=0,F=1,H=1,J=1,K=1,L=1,M=0,O+1=0,Q=1,S=1,U=1,N=C,P=E,R=G,T=I] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[30]: 2
  with precondition: [A=1,B=0,D=0,F=2,H=1,J=1,K=1,L=1,M=1,O=0,Q=2,S=1,U=1,N=C,P=E,R=G,T=I] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[31]: 2
  with precondition: [A=1,B=0,D=0,F=3,H=1,J=1,K=1,L=1,M+1=0,O=0,Q=3,S=1,U=1,N=C,P=E,R=G,T=I] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[20,21,22,23,24,25],26]: 2+it1*(2)
  Such that:it1=<1*A+ -1*H,it1=<1*J+ -1,it1=<1*U+ -1*H,it1=<-1*D+1*U+ -1,it1=<1*D+1*U+ -1,it1=<-1*B+ -1*D+1*U+ -1,it1=<-1*B+1*D+1*U+ -1,it1=<-1*D+1*B+1*U+ -1,it1=<1*B+1*D+1*U+ -1
  with precondition: [K=1,A=J,A=L,C=N,E=P,G=R,A=S,I=T,A=U,0>=Q+1,A>=H+1,H>=B+D+1,D+H>=B+1,B+H>=D+1,B+D+H>=1,A+M+O>=B+D+H,A+D+M>=B+H+O,A+B+O>=D+H+M,A+B+D>=H+M+O] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[20,21,22,23,24,25],27]: 2+it1*(2)
  Such that:it1=<1*A+ -1*H,it1=<1*J+ -1,it1=<1*U+ -1*H,it1=<-1*D+1*U+ -1,it1=<1*D+1*U+ -1,it1=<-1*B+ -1*D+1*U+ -1,it1=<-1*B+1*D+1*U+ -1,it1=<-1*D+1*B+1*U+ -1,it1=<1*B+1*D+1*U+ -1
  with precondition: [K=1,A=J,A=L,C=N,E=P,G=R,A=S,I=T,A=U,Q>=4,A>=H+1,H>=B+D+1,D+H>=B+1,B+H>=D+1,B+D+H>=1,A+M+O>=B+D+H,A+D+M>=B+H+O,A+B+O>=D+H+M,A+B+D>=H+M+O] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[20,21,22,23,24,25],28]: 2+it1*(2)
  Such that:it1=<1*A+ -1*H,it1=<1*J+ -1,it1=<1*U+ -1*H,it1=<-1*D+1*U+ -1,it1=<1*D+1*U+ -1,it1=<-1*B+ -1*D+1*U+ -1,it1=<-1*B+1*D+1*U+ -1,it1=<-1*D+1*B+1*U+ -1,it1=<1*B+1*D+1*U+ -1
  with precondition: [K=1,Q=0,A=J,A=L,C=N,E=P,G=R,A=S,I=T,A=U,A>=H+1,H>=B+D+1,D+H>=B+1,B+H>=D+1,B+D+H>=1,A+M+O>=B+D+H+1,A+D+M+1>=B+H+O,A+B+O>=D+H+M+1,A+B+D+1>=H+M+O] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[20,21,22,23,24,25],29]: 2+it1*(2)
  Such that:it1=<1*A+ -1*H,it1=<1*J+ -1,it1=<1*U+ -1*H,it1=<-1*D+1*U+ -1,it1=<1*D+1*U+ -1,it1=<-1*B+ -1*D+1*U+ -1,it1=<-1*B+1*D+1*U+ -1,it1=<-1*D+1*B+1*U+ -1,it1=<1*B+1*D+1*U+ -1
  with precondition: [K=1,Q=1,A=J,A=L,C=N,E=P,G=R,A=S,I=T,A=U,A>=H+1,H>=B+D+1,D+H>=B+1,B+H>=D+1,B+D+H>=1,A+M+O+1>=B+D+H,A+D+M>=B+H+O+1,A+B+O+1>=D+H+M,A+B+D>=H+M+O+1] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[20,21,22,23,24,25],30]: 2+it1*(2)
  Such that:it1=<1*A+ -1*H,it1=<1*J+ -1,it1=<1*U+ -1*H,it1=<-1*D+1*U+ -1,it1=<1*D+1*U+ -1,it1=<-1*B+ -1*D+1*U+ -1,it1=<-1*B+1*D+1*U+ -1,it1=<-1*D+1*B+1*U+ -1,it1=<1*B+1*D+1*U+ -1
  with precondition: [K=1,Q=2,A=J,A=L,C=N,E=P,G=R,A=S,I=T,A=U,A>=H+1,H>=B+D+1,D+H>=B+1,B+H>=D+1,B+D+H>=1,A+M+O>=B+D+H+1,A+D+M>=B+H+O+1,A+B+O+1>=D+H+M,A+B+D+1>=H+M+O] 

lbl81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U):[[20,21,22,23,24,25],31]: 2+it1*(2)
  Such that:it1=<1*A+ -1*H,it1=<1*J+ -1,it1=<1*U+ -1*H,it1=<-1*D+1*U+ -1,it1=<1*D+1*U+ -1,it1=<-1*B+ -1*D+1*U+ -1,it1=<-1*B+1*D+1*U+ -1,it1=<-1*D+1*B+1*U+ -1,it1=<1*B+1*D+1*U+ -1
  with precondition: [K=1,Q=3,A=J,A=L,C=N,E=P,G=R,A=S,I=T,A=U,A>=H+1,H>=B+D+1,D+H>=B+1,B+H>=D+1,B+D+H>=1,A+M+O+1>=B+D+H,A+D+M+1>=B+H+O,A+B+O>=D+H+M+1,A+B+D>=H+M+O+1] 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Solved cost expressions of start0(A,B,C,D,E,F,G,H,I,J): 
start0(A,B,C,D,E,F,G,H,I,J):[47]: 2  with precondition: [0>=A] 
start0(A,B,C,D,E,F,G,H,I,J):[48]: 4  with precondition: [A=1] 
start0(A,B,C,D,E,F,G,H,I,J):[49]: 4  with precondition: [A=1] 
start0(A,B,C,D,E,F,G,H,I,J):[50]: 4  with precondition: [A=1] 
start0(A,B,C,D,E,F,G,H,I,J):[51]: 4  with precondition: [A=1] 
start0(A,B,C,D,E,F,G,H,I,J):[52]: 4  with precondition: [A=1] 
start0(A,B,C,D,E,F,G,H,I,J):[53]: 4  with precondition: [A=1] 
start0(A,B,C,D,E,F,G,H,I,J):[54]: 2*A+2  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H,I,J):[55]: 2*A+2  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H,I,J):[56]: 2*A+2  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H,I,J):[57]: 2*A+2  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H,I,J):[58]: 2*A+2  with precondition: [A>=2] 
start0(A,B,C,D,E,F,G,H,I,J):[59]: 2*A+2  with precondition: [A>=2] 
Maximum cost of start0(A,B,C,D,E,F,G,H,I,J): max([2*A+2,4]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 69 ms.
Invariants computed in 272 ms.
----Backward Invariants 194 ms.
----Transitive Invariants 19 ms.
Refinement performed in 211 ms.
Termination proved in 148 ms.
Upper bounds computed in 360 ms.
----Phase cost structures 97 ms.
--------Equation cost structures 93 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 244 ms.
----Solving cost expressions 1 ms.

Compressed phase information: 5 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 1154 ms.