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