eq(start0(A,B,C,D,E,F,G,H,I,J),1,[start(A,C,C,E,E,A,H,H,J,J)],[]). eq(start(A,B,C,D,E,F,G,H,I,J),1,[stop(A,B,C,D,E,F,G,H,1,J)],[1>=A,B=C,D=E,F=A,G=H,I=J]). eq(start(A,B,C,D,E,F,G,H,I,J),1,[lbl31(A,K,C,D,E,F,G,H,1,J,L,M,N,O,P,Q,R,S,T,U,V),loop_cont_lbl31(M,N,O,P,Q,R,S,T,U,V)],[L=0,A>=2,B=C,D=E,F=A,G=H,I=J]). eq(start(A,B,C,D,E,F,G,H,I,J),1,[lbl31(A,K,C,D,E,F,G,H,1,J,L,M,N,O,P,Q,R,S,T,U,V)],[L=1,A>=2,B=C,D=E,F=A,G=H,I=J]). eq(lbl31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[lbl13(A,B,C,I,E,F,I-1,H,1+I,J,K,L,M,N,O,P,Q,R,S,T,U)],[I>=1,A>=I+1,F=A]). eq(lbl31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[lbl43(A,B,C,D,E,F,I-2,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1),loop_cont_lbl43(W,X,Y,Z,A1,B1,C1,D1,E1,F1,K,L,M,N,O,P,Q,R,S,T,U)],[V=0,I>=1,A>=I+1,F=A]). eq(lbl31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[lbl43(A,B,C,D,E,F,I-2,H,I,J,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1)],[K=1,V=1,I>=1,A>=I+1,F=A]). eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[lbl43(A,B,C,D,E,F,G-1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[G>=0,I>=G+2,G+1>=0,A>=I+1,F=A]). eq(lbl13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),1,[lbl31(A,V,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[A>=D+2,G+D>=1,G+1>=0,A>=D+1,D>=G+1,F=A,I=D+1]). eq(loop_cont_lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U),0,[lbl13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U)],[]). eq(lbl13(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),1,[],[K=1,G+A>=2,G+1>=0,A>=2+G,F=A,I=A,D+1=A]). eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,A,B,C,I,E,F,G,H,1+I,J),1,[],[K=0,I>=G+2,G+1>=0,A>=I+1,F=A]). eq(lbl43(A,B,C,D,E,F,G,H,I,J,K,A,B,C,D,E,F,G,H,I,J),0,[],[K=1]).