eq(start0(A,B,C,D,E,F),1,[start(A,C,C,E,E,A)],[]).
eq(start(A,B,C,D,E,F),1,[stop(A,B,C,F,E,F)],[0>=A+1,B=C,D=E,F=A]).
eq(start(A,B,C,D,E,F),1,[lbl121(A,1,C,F-1,E,F)],[A>=0,1>=A,B=C,D=E,F=A]).
eq(start(A,B,C,D,E,F),1,[lbl101(A,2,C,F,E,F)],[A>=2,B=C,D=E,F=A]).
eq(lbl121(A,B,C,D,E,F),1,[stop(A,B,C,D,E,F)],[A>=0,B>=0,B>=1,D+1=0,F=A]).
eq(lbl121(A,B,C,D,E,F),1,[lbl121(A,1,C,D-1,E,F)],[D>=0,1>=D,A>=D+1,B>=D+1,B>=1,D+1>=0,F=A]).
eq(lbl121(A,B,C,D,E,F),1,[lbl101(A,2,C,D,E,F)],[D>=2,A>=D+1,B>=D+1,B>=1,D+1>=0,F=A]).
eq(lbl101(A,B,C,D,E,F),1,[lbl101(A,2*B,C,D,E,F)],[D>=B+1,B>=2,2*D>=B+2,A>=D,F=A]).
eq(lbl101(A,B,C,D,E,F),1,[lbl121(A,B,C,D-1,E,F)],[B>=D,B>=2,2*D>=B+2,A>=D,F=A]).