eq(evalfstart(A,B,C,D),1,[evalfentryin(A,B,C,D)],[]).
eq(evalfreturnin(A,B,C,D),1,[evalfstop(A,B,C,D)],[]).
eq(evalfentryin(A,B,C,D),1,[evalfbb7in(0,B,C,D,E,F,G,H,I),loop_cont_evalfbb7in(F,G,H,I)],[E=0]).
eq(evalfentryin(A,B,C,D),1,[evalfbb7in(0,B,C,D,E,F,G,H,I)],[E=1]).
eq(loop_cont_evalfbb7in(A,B,C,D),0,[evalfreturnin(A,B,C,D)],[]).
eq(evalfbb7in(A,B,C,D,E,F,G,H,I),1,[evalfbb5in(A,B,0,D,J,K,L,M,N),loop_cont_evalfbb5in(K,L,M,N,E,F,G,H,I)],[J=0,B*B*B>=0,0>=B*B*B,0>=1+A]).
eq(evalfbb7in(A,B,C,D,E,F,G,H,I),1,[evalfbb5in(A,B,0,D,J,K,L,M,N),loop_cont_evalfbb5in(K,L,M,N,E,F,G,H,I)],[J=0,B*B*B>=1,O>=0,B*B*B>=2*O,1+2*O>=B*B*B,O>=1+A]).
eq(evalfbb7in(A,B,C,D,E,F,G,H,I),1,[evalfbb5in(A,B,0,D,J,K,L,M,N),loop_cont_evalfbb5in(K,L,M,N,E,F,G,H,I)],[J=0,0>=B*B*B+1,0>=O,O>=1+A,2*O>=B*B*B,1+B*B*B>=2*O]).
eq(evalfbb5in(A,B,C,D,E,F,G,H,I),1,[evalfbb3in(A,B,C,0,J,K,L,M,N),loop_cont_evalfbb3in(K,L,M,N,E,F,G,H,I)],[J=0,B>=1+C]).
eq(evalfbb5in(A,B,C,D,E,F,G,H,I),1,[evalfbb3in(A,B,C,0,J,K,L,M,N)],[E=1,J=1,B>=1+C]).
eq(evalfbb3in(A,B,C,D,E,F,G,H,I),1,[evalfbb2in(A,B,C,D,E,F,G,H,I)],[C>=1+D]).
eq(loop_cont_evalfbb5in(A,B,C,D,E,F,G,H,I),0,[evalfbb6in(A,B,C,D,E,F,G,H,I)],[]).
eq(loop_cont_evalfbb3in(A,B,C,D,E,F,G,H,I),0,[evalfbb4in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalfbb2in(A,B,C,D,E,F,G,H,I),1,[evalfbb3in(A,B,C,D+1,E,F,G,H,I)],[]).
eq(evalfbb6in(A,B,C,D,E,F,G,H,I),1,[evalfbb7in(A+1,B,C,D,E,F,G,H,I)],[]).
eq(evalfbb4in(A,B,C,D,E,F,G,H,I),1,[evalfbb5in(A,B,C+1,D,E,F,G,H,I)],[]).
eq(evalfbb7in(A,B,C,D,E,A,B,C,D),1,[],[E=0,B*B*B>=0,0>=B*B*B,A>=0]).
eq(evalfbb7in(A,B,C,D,E,A,B,C,D),0,[],[E=1]).
eq(evalfbb7in(A,B,C,D,E,A,B,C,D),1,[],[E=0,B*B*B>=1,F>=0,B*B*B>=2*F,1+2*F>=B*B*B,A>=F]).
eq(evalfbb7in(A,B,C,D,E,A,B,C,D),1,[],[E=0,0>=B*B*B+1,0>=F,A>=F,2*F>=B*B*B,1+B*B*B>=2*F]).
eq(evalfbb5in(A,B,C,D,E,A,B,C,D),1,[],[E=0,C>=B]).
eq(evalfbb3in(A,B,C,D,E,A,B,C,D),1,[],[E=0,D>=C]).