eq(start0(A,B,C,D,E,F,G,H),1,[start(A,C,C,A,F,F,H,H)],[]). eq(start(A,B,C,D,E,F,G,H),1,[stop(A,B,C,D,E,F,G,H)],[0>=A,B=C,D=A,E=F,G=H]). eq(start(A,B,C,D,E,F,G,H),1,[lbl6(A,B,C,D,E,F,G,H)],[A>=1,A>=C,B=C,D=A,E=F,G=H]). eq(lbl6(A,B,C,D,E,F,G,H),1,[stop(A,B,C,D,E,F,G,H)],[A>=1,A>=C,G=H,E=F,D=A,B=C]). eq(cut(A,B,C,D,E,F,G,H),1,[stop(A,B,C,D,E,F,G,H)],[C>=A+1,A>=2,E=0,G=C,D=A,B=C]). eq(start(A,B,C,D,E,F,G,H),1,[lbl121(A,B,C,D,1,F,0,H,I,J,K,L,M,N,O,P,Q),loop_cont_lbl121(J,K,L,M,N,O,P,Q)],[I=0,A>=1,C>=A+1,B=C,D=A,E=F,G=H]). eq(start(A,B,C,D,E,F,G,H),1,[lbl121(A,B,C,D,1,F,0,H,I,J,K,L,M,N,O,P,Q)],[I=1,A>=1,C>=A+1,B=C,D=A,E=F,G=H]). eq(loop_cont_lbl121(A,B,C,D,E,F,G,H),0,[cut(A,B,C,D,E,F,G,H)],[]). eq(lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl121(A,B,C,D,1+E,F,G,H,I,J,K,L,M,N,O,P,Q)],[A>=E+1,C>=G+1,A+C>=G+3,A>=E,E>=1,G>=0,C>=A+1,D=A,B=C]). eq(lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl141(A,B,C,D,0,F,1+G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_lbl141(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,C>=G+1,A+C>=G+3,A>=1,G>=0,C>=A+1,E=A,D=A,B=C]). eq(lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl141(A,B,C,D,0,F,1+G,H,R,S,T,U,V,W,X,Y,Z)],[I=1,R=1,C>=G+1,A+C>=G+3,A>=1,G>=0,C>=A+1,E=A,D=A,B=C]). eq(lbl141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl141(A,B,C,D,0,F,1+G,H,I,J,K,L,M,N,O,P,Q)],[0>=A,C>=G+1,A>=2,C>=A+1,G>=1,C>=G,E=0,D=A,B=C]). eq(loop_cont_lbl141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[]). eq(lbl141(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=0,A>=2,C>=A+1,C>=1,G=C,E=0,D=A,B=C]). eq(lbl141(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),0,[],[I=1]). eq(lbl121(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=0,G>=C,C>=G+1,A+C>=G+3,A>=E,E>=1,G>=0,C>=A+1,D=A,B=C]). eq(lbl121(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),0,[],[I=1]). eq(lbl141(A,B,C,D,E,F,G,H,I,A,B,C,D,1+E,F,G,H),1,[],[I=0,A>=1,C>=G+1,A>=2,C>=A+1,G>=1,C>=G,E=0,D=A,B=C]).