eq(start0(A,B,C,D,E,F,G,H),1,[start(A,A,D,D,F,F,H,H)],[]).
eq(start(A,B,C,D,E,F,G,H),1,[a(A,B,C,D,E,F,G,H)],[A>=1,B=A,C=D,E=F,G=H]).
eq(a(A,B,C,D,E,F,G,H),1,[d(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),loop_cont_d(J,K,L,M,N,O,P,Q)],[I=0,A>=1,G=H,E=F,C=D,B=A]).
eq(a(A,B,C,D,E,F,G,H),1,[d(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[I=1,A>=1,G=H,E=F,C=D,B=A]).
eq(d(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[b(A,B,C,D,E,F,1+C,H,R,S,T,U,V,W,X,Y,Z),loop_cont_b(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,A>=C+1,A>=C,A>=1,C>=1,B=A]).
eq(d(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[b(A,B,C,D,E,F,1+C,H,R,S,T,U,V,W,X,Y,Z)],[I=1,R=1,A>=C+1,A>=C,A>=1,C>=1,B=A]).
eq(b(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[c(A,B,C,D,B,F,G,H,R,S,T,U,V,W,X,Y,Z),loop_cont_c(S,T,U,V,W,X,Y,Z,I,J,K,L,M,N,O,P,Q)],[R=0,A>=G,A+1>=G,A>=C+1,C>=1,G>=C+1,B=A]).
eq(b(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[c(A,B,C,D,B,F,G,H,R,S,T,U,V,W,X,Y,Z)],[I=1,R=1,A>=G,A+1>=G,A>=C+1,C>=1,G>=C+1,B=A]).
eq(c(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),1,[c(A,B,C,D,E-1,F,G,H,I,J,K,L,M,N,O,P,Q)],[E>=C+1,A>=E,A>=G,C>=1,E>=C,G>=C+1,B=A]).
eq(loop_cont_b(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[d(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[]).
eq(loop_cont_c(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q),0,[b(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q)],[]).
eq(d(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),1,[],[I=1,A>=1,C=A,B=A]).
eq(b(A,B,C,D,E,F,G,H,I,A,B,1+C,D,E,F,G,H),1,[],[I=0,A>=C+1,C>=1,A>=C,G=A+1,B=A]).
eq(b(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),0,[],[I=1]).
eq(c(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,1+G,H),1,[],[I=0,A>=E,A>=G,E>=1,G>=E+1,C=E,B=A]).
eq(c(A,B,C,D,E,F,G,H,I,A,B,C,D,E,F,G,H),0,[],[I=1]).