eq(start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),1,[start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P)],[]).
eq(start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),1,[lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P)],[A=B,C=D,E=F,G=H,I=J,K=L,M=N,O=P]).
eq(lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),1,[stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P)],[L>=2*O,0>=O,2*O+1>=L,M=N,A=B,C=D,E=F,G=H,I=J,K=L]).
eq(lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),1,[lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1),loop_cont_lbl71(S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1)],[R=0,L>=2*O,O>=1,2*O+1>=L,M=N,A=B,C=D,E=F,G=H,I=J,K=L]).
eq(lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),1,[lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1)],[R=1,L>=2*O,O>=1,2*O+1>=L,M=N,A=B,C=D,E=F,G=H,I=J,K=L]).
eq(lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl53(A,B,C,D,E,F,G,H,1+I,J,K,L,I,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[2*O+1>=L,O>=G,G>=1,E>=0,L>=E+1,I=E,K=L]).
eq(lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl101(A,B,C,D,E-G,F,G,H,I,J,K,L,M,N,O,P,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1),loop_cont_lbl101(I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[H1=0,E>=G,2*O+1>=L,O>=G,G>=1,E>=0,L>=E+1,I=E,K=L]).
eq(lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl101(A,B,C,D,E-G,F,G,H,I,J,K,L,M,N,O,P,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1)],[Q=1,H1=1,E>=G,2*O+1>=L,O>=G,G>=1,E>=0,L>=E+1,I=E,K=L]).
eq(lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl101(A,B,C,D,E-G,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[E>=G,I>=G+E,O>=G,L>=I+1,G>=1,2*O+1>=L,E>=0,K=L]).
eq(lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[G>=2*A,2*A+1>=G,2*O+1>=L,O>=G,E>=0,G>=1,L>=1+E,K=L,I=L,M+1=L]).
eq(lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl71(A,B,H1,D,I,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[L>=M+2,L>=M+1,M>=E,G>=1,E>=0,O>=G,2*O+1>=L,I=M+1,K=L]).
eq(lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl121(H1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1),loop_cont_lbl121(J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[I1=0,L>=1+E,G>=1,E>=0,O>=G,2*O+1>=L,I=L,K=L,M+1=L]).
eq(lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl121(H1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1)],[Q=1,I1=1,L>=1+E,G>=1,E>=0,O>=G,2*O+1>=L,I=L,K=L,M+1=L]).
eq(loop_cont_lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),0,[lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[]).
eq(lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),1,[lbl121(H1,B,C,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[A>=1,0>=L,A>=0,E>=0,2*O+1>=L,O>=1,L>=E+1,O>=2*A,K=L,I=L,M+1=L,G=A]).
eq(loop_cont_lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1),0,[lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1)],[]).
eq(lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),0,[],[Q=1]).
eq(lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,A,B,C,D,E,F,G,H,1+I,J,K,L,I,N,O,P),1,[],[Q=0,I>=G+E,O>=G,L>=I+1,G>=1,2*O+1>=L,E>=0,K=L]).
eq(lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),0,[],[Q=1]).
eq(lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,A,B,R,D,0,F,G,H,0,J,K,L,M,N,O,P),1,[],[Q=0,L>=1,A>=1,A>=0,E>=0,2*O+1>=L,O>=1,L>=E+1,O>=2*A,K=L,I=L,M+1=L,G=A]).
eq(lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),0,[],[Q=1]).
eq(lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P),1,[],[Q=1,E>=0,2*O+1>=L,O>=1,L>=E+1,O>=0,G=0,K=L,I=L,M+1=L,A=0]).