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,B=C,D=E,F=A]).
eq(start(A,B,C,D,E,F),1,[lbl52(A,B-1,C,F,E,F)],[A>=1,C>=1,B=C,D=E,F=A]).
eq(start(A,B,C,D,E,F),1,[lbl72(A,F,C,F-1,E,F)],[A>=1,0>=C,B=C,D=E,F=A]).
eq(lbl52(A,B,C,D,E,F),1,[stop(A,B,C,D,E,F)],[0>=D,B>=0,D>=1,A>=D,F=A]).
eq(lbl52(A,B,C,D,E,F),1,[lbl52(A,B-1,C,D,E,F)],[D>=1,B>=1,B>=0,A>=D,F=A]).
eq(lbl52(A,B,C,D,E,F),1,[lbl72(A,F,C,D-1,E,F)],[D>=1,A>=D,B=0,F=A]).
eq(lbl72(A,B,C,D,E,F),1,[stop(A,B,C,D,E,F)],[A>=1,D=0,F=A,B=A]).
eq(lbl72(A,B,C,D,E,F),1,[lbl52(A,B-1,C,D,E,F)],[D>=1,A>=1,D>=0,A>=D+1,F=A,B=A]).
eq(lbl72(A,B,C,D,E,F),1,[lbl72(A,F,C,D-1,E,F)],[D>=1,0>=A,D>=0,A>=D+1,F=A,B=A]).