eq(eval1(A,B,C,D),1,[eval2(A-1,B,C,D,E,F,G,H,I),loop_cont_eval2(F,G,H,I)],[E=0,A>=2]).
eq(eval1(A,B,C,D),1,[eval2(A-1,B,C,D,E,F,G,H,I)],[E=1,A>=2]).
eq(eval1(A,B,C,D),1,[eval2(A,B-1,C,D,E,F,G,H,I),loop_cont_eval2(F,G,H,I)],[E=0,1>=A]).
eq(eval1(A,B,C,D),1,[eval2(A,B-1,C,D,E,F,G,H,I)],[E=1,1>=A]).
eq(eval2(A,B,C,D,E,F,G,H,I),1,[eval3(A,B,A,2*A,J,K,L,M,N),loop_cont_eval3(K,L,M,N,E,F,G,H,I)],[J=0,B>=2]).
eq(eval2(A,B,C,D,E,F,G,H,I),1,[eval3(A,B,A,2*A,J,K,L,M,N)],[E=1,J=1,B>=2]).
eq(eval3(A,B,C,D,E,F,G,H,I),1,[eval3(A,B,D,2*D,E,F,G,H,I)],[B>=D,B>=1+D,D>=1]).
eq(eval3(A,B,C,D,E,F,G,H,I),1,[eval3(A,B,D+1,2*D+2,E,F,G,H,I)],[B>=D,B>=1+D,D>=1]).
eq(eval3(A,B,C,D,E,F,G,H,I),1,[eval3(A,B,D,2*D,E,F,G,H,I)],[D>=1,B=D]).
eq(loop_cont_eval3(A,B,C,D,E,F,G,H,I),0,[eval4(A,B,C,D,E,F,G,H,I)],[]).
eq(eval4(A,B,C,D,E,F,G,H,I),1,[eval2(A-1,B,C,D,E,F,G,H,I)],[A>=2,A>=1,B>=2]).
eq(eval4(A,B,C,D,E,F,G,H,I),1,[eval2(A,B-1,C,D,E,F,G,H,I)],[B>=2,A=1]).
eq(eval2(A,B,C,D,E,A,B,C,D),0,[],[E=1]).
eq(eval3(A,B,C,D,E,A,B,C,D),1,[],[E=0,B>=D,B>=1+D]).
eq(eval3(A,B,C,D,E,A,B,C,D),0,[],[E=1]).
eq(eval3(A,B,C,D,E,A,B,C,D+1),1,[],[E=0,B>=D,B>=1+D]).
eq(eval3(A,B,C,D,E,A,B,C,D),1,[],[E=0,B=D]).