eq(start0(A,B,C,D,E,F,G,H),1,[start(A,C,C,E,E,G,G,A)],[]).
eq(start(A,B,C,D,E,F,G,H),1,[stop(A,B,C,D,E,F,G,H)],[1>=A,B=C,D=E,F=G,H=A]).
eq(lbl16(A,B,C,D,E,F,G,H),1,[stop(A,B,C,D,E,F,G,H)],[A>=2,A>=B+1,F=0,H=A,D=A]).
eq(start(A,B,C,D,E,F,G,H),1,[lbl111(A,H,C,1,E,H-1,G,H,I,J,K,L,M,N,O,P,Q),loop_cont_lbl111(J,K,L,M,N,O,P,Q)],[I=0,A>=2,B=C,D=E,F=G,H=A]).
eq(start(A,B,C,D,E,F,G,H),1,[lbl111(A,H,C,1,E,H-1,G,H,I,J,K,L,M,N,O,P,Q)],[I=1,A>=2,B=C,D=E,F=G,H=A]).
eq(loop_cont_lbl111(A,B,C,D,E,F,G,H),0,[lbl16(A,B,C,D,E,F,G,H)],[]).
eq(lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl111(A,B,C,D-F,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[D>=F,A>=F+1,A>=F+D,A>=B,F>=1,D>=0,H=A]).
eq(lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl82(A,B,C,H,E,F-1,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_lbl82(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,F>=D+1,0>=D+1,A>=F+1,A>=F+D,A>=B,F>=1,D>=0,H=A]).
eq(lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl82(A,B,C,H,E,F-1,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_lbl82(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,F>=D+1,D>=1,A>=F+1,A>=F+D,A>=B,F>=1,D>=0,H=A]).
eq(lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl82(A,B-F,C,H,E,F-1,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_lbl82(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,F>=1,A>=F+1,A>=F,A>=B,D=0,H=A]).
eq(lbl82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl82(A,B,C,H,E,F-1,G,H,I,J,K,L,M,N,O,P,Q)],[F>=A+1,A>=1,F>=0,A>=F+2,A>=B,A+F>=B+1,H=A,D=A]).
eq(lbl82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl82(A,B,C,H,E,F-1,G,H,I,J,K,L,M,N,O,P,Q)],[F>=1,0>=A+1,F>=0,A>=F+2,A>=B,A+F>=B+1,H=A,D=A]).
eq(lbl82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[lbl82(A,B-F,C,H,E,F-1,G,H,I,J,K,L,M,N,O,P,Q)],[F>=1,F>=0,0>=F+2,0>=B,F>=B+1,D=0,H=0,A=0]).
eq(loop_cont_lbl82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[]).
eq(lbl82(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=0,A>=2,A>=B,A>=B+1,F=0,H=A,D=A]).
eq(lbl82(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),0,[],[I=1]).
eq(lbl82(A,B,C,D,E,F,G,H,I,A,B,C,D-F,E,F,G,H),1,[],[I=0,F>=1,A>=F,F>=0,A>=F+2,A>=B,A+F>=B+1,H=A,D=A]).