eq(start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[start(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S,A)],[]).
eq(start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)],[2>=A,B=C,D=E,F=G,H=I,J=K,L=M,N=O,P=Q,R=S,T=A]).
eq(start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S,T)],[A>=3,B=C,D=E,F=G,H=I,J=K,L=M,N=O,P=Q,R=S,T=A]).
eq(lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1+P,Q,R,S,T)],[2*N+P+2>=A,P>=0,N>=1,A>=2*N+P,A>=N+P+2,B>=2*J+1,B+1>=A,R=N,T=A]).
eq(lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1+2*R,O,P,Q,T,S,T)],[A>=2*N+P+3,P>=0,N>=1,A>=2*N+P,A>=N+P+2,B>=2*J+1,B+1>=A,R=N,T=A]).
eq(lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1+2*R,O,P,Q,1+2*R,S,T)],[A>=2*N+P+3,P>=0,N>=1,A>=2*N+P,A>=N+P+2,B>=2*J+1,B+1>=A,R=N,T=A]).
eq(lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2+2*R,O,P,Q,T,S,T)],[A>=2*N+P+4,P>=0,N>=1,A>=2*N+P,A>=N+P+2,B>=2*J+1,B+1>=A,R=N,T=A]).
eq(lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2+2*R,O,P,Q,2+2*R,S,T)],[A>=2*N+P+4,P>=0,N>=1,A>=2*N+P,A>=N+P+2,B>=2*J+1,B+1>=A,R=N,T=A]).
eq(lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1+P,Q,R,S,T)],[A+P+2>=0,N>=1,P>=0,A>=P+N+2,B>=2*J+1,B+1>=A,T=A,R=A]).
eq(lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1+2*R,O,P,Q,T,S,T)],[0>=A+P+3,N>=1,P>=0,A>=P+N+2,B>=2*J+1,B+1>=A,T=A,R=A]).
eq(lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1+2*R,O,P,Q,1+2*R,S,T)],[0>=A+P+3,N>=1,P>=0,A>=P+N+2,B>=2*J+1,B+1>=A,T=A,R=A]).
eq(lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2+2*R,O,P,Q,T,S,T)],[0>=A+P+4,N>=1,P>=0,A>=P+N+2,B>=2*J+1,B+1>=A,T=A,R=A]).
eq(lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2+2*R,O,P,Q,2+2*R,S,T)],[0>=A+P+4,N>=1,P>=0,A>=P+N+2,B>=2*J+1,B+1>=A,T=A,R=A]).
eq(lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)],[L+2>=A,R+L+2+N>=A,R>=N,L+N>=1,L>=0,A>=L+2+N,B>=2*J+1,B+1>=A,P=L+1,T=A]).
eq(lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1+P,Q,0,S,T)],[R+N>=1,R>=N,A+N>=4,A>=3,1>=N,B>=2*J+1,B+1>=A,T=A,P+2=A,L+3=A]).
eq(lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S,T)],[A>=L+4,R+L+2+N>=A,R>=N,L+N>=1,L>=0,A>=L+2+N,B>=2*J+1,B+1>=A,P=L+1,T=A]).
eq(lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S,T)],[A>=L+4,R+L+2+N>=A,R>=N,L+N>=1,L>=0,A>=L+2+N,B>=2*J+1,B+1>=A,P=L+1,T=A]).
eq(lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S,T)],[A>=L+5,R+L+2+N>=A,R>=N,L+N>=1,L>=0,A>=L+2+N,B>=2*J+1,B+1>=A,P=L+1,T=A]).
eq(lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S,T)],[A>=L+5,R+L+2+N>=A,R>=N,L+N>=1,L>=0,A>=L+2+N,B>=2*J+1,B+1>=A,P=L+1,T=A]).
eq(lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl101(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)],[R>=1,R>=2*J+1,2*J+2>=R,P>=1,A>=3,P>=R,T=A,N=O,L=M]).
eq(lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl43(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1+P,Q,R,S,T)],[R>=2*J+1,2*J+2>=R,P>=1,A>=3,P>=R,T=A,N=O,L=M]).
eq(lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S,T)],[R>=2*H+1,2*H+2>=R,A>=3,R>=1,R>=2*D+1,R>=2*F+1,R>=2*J+1,P>=R,2*J+2>=R,2*F+2>=R,2*D+2>=R,L=M,N=O,T=A]).
eq(lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S,T)],[2*H+1>=0,P>=1,2*F+1>=0,2*J+1>=0,2*D+1>=0,P>=2*J+1,P>=2*F+1,P>=2*D+1,P>=2*H+1,2*D+1>=2*F,2*H+1>=2*J,2*H+1>=2*D,2*H+1>=2*F,2*J+1>=2*D,2*J+1>=2*F,2*D+1>=2*J,2*D+1>=2*H,2*F+1>=2*D,2*F+1>=2*J,2*F+1>=2*H,2*J+1>=2*H,A>=3,R=H,L=M,T=A,N=O]).
eq(lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl121(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S,T)],[R>=2*F+1,2*F+2>=R,A>=3,R>=1,R>=2*D+1,R>=2*J+1,P>=R,2*J+2>=R,2*D+2>=R,L=M,N=O,T=A]).
eq(lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl111(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)],[R>=2*D+1,2*D+2>=R,A>=3,R>=1,R>=2*J+1,P>=R,2*J+2>=R,L=M,N=O,T=A]).
eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T)],[A>=B+2,A>=3,R>=2*J+1,B>=1,2*J+2>=R,B>=R,P=B+1,L=M,N=O,T=A]).
eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T)],[B+1>=A,1>=A,A>=3,R>=2*J+1,B>=1,2*J+2>=R,B>=R,P=B+1,L=M,N=O,T=A]).
eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl133(A,B,C,D,E,F,G,H,I,J,K,0,M,0,O,1,Q,0,S,T)],[B>=1,0>=1,R>=2*J+1,2*J+2>=R,B>=R,T=2,P=B+1,L=M,N=O,A=2]).
eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S,T)],[A>=3,B+1>=A,R>=2*J+1,B>=1,2*J+2>=R,B>=R,P=B+1,L=M,N=O,T=A]).
eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S,T)],[A>=3,B+1>=A,R>=2*J+1,B>=1,2*J+2>=R,B>=R,P=B+1,L=M,N=O,T=A]).
eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S,T)],[A>=4,B+1>=A,A>=3,R>=2*J+1,B>=1,2*J+2>=R,B>=R,P=B+1,L=M,N=O,T=A]).
eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T),1,[lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S,T)],[A>=4,B+1>=A,A>=3,R>=2*J+1,B>=1,2*J+2>=R,B>=R,P=B+1,L=M,N=O,T=A]).