eq(evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I),1,[evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I)],[]).
eq(evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I),1,[evalbinsearchStepSize2stop(A,B,C,D,E,F,G,H,I)],[]).
eq(evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I),1,[evalbinsearchStepSize2bbin(0,0,4,A,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),loop_cont_evalbinsearchStepSize2bbin(K,L,M,N,O,P,Q,R,S)],[J=0]).
eq(evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I),1,[evalbinsearchStepSize2bbin(0,0,4,A,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[J=1]).
eq(loop_cont_evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I),0,[evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I)],[]).
eq(evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb1in(A,B,C,D,T,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[0>=C]).
eq(evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb1in(A,B,C,D,T,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[C>=2]).
eq(evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[0>=B+1]).
eq(evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[B>=1]).
eq(evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb3in(A,B,C,D,E,C,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[B=0]).
eq(evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb3in(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[C=0]).
eq(evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb3in(A,B,C,D,E,T,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[C>=1,T>=0,C>=2*T,1+2*T>=C]).
eq(evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb3in(A,B,C,D,E,T,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[0>=C+1,0>=T,2*T>=C,1+C>=2*T]).
eq(evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[E>=G+1]).
eq(evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[G>=E]).
eq(evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[A=1,B=0]).
eq(evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F,J,K,L,M,N,O,P,Q,R,S)],[0>=A]).
eq(evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F,J,K,L,M,N,O,P,Q,R,S)],[A>=2]).
eq(evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F,J,K,L,M,N,O,P,Q,R,S)],[0>=B+1]).
eq(evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F,J,K,L,M,N,O,P,Q,R,S)],[B>=1]).
eq(evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[G>=E+1]).
eq(evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,0,J,K,L,M,N,O,P,Q,R,S)],[F=0]).
eq(evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,T,J,K,L,M,N,O,P,Q,R,S)],[F>=1,T>=0,F>=2*T,1+2*T>=F]).
eq(evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,T,J,K,L,M,N,O,P,Q,R,S)],[0>=F+1,0>=T,2*T>=F,1+F>=2*T]).
eq(evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bbin(2,H,I,D+I,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[255>=D+I]).
eq(evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[A=2,B=0]).
eq(evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F,J,K,L,M,N,O,P,Q,R,S)],[1>=A]).
eq(evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F,J,K,L,M,N,O,P,Q,R,S)],[A>=3]).
eq(evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F,J,K,L,M,N,O,P,Q,R,S)],[0>=B+1]).
eq(evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F,J,K,L,M,N,O,P,Q,R,S)],[B>=1]).
eq(evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,0,J,K,L,M,N,O,P,Q,R,S)],[F=0]).
eq(evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,T,J,K,L,M,N,O,P,Q,R,S)],[F>=1,T>=0,F>=2*T,1+2*T>=F]).
eq(evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,T,J,K,L,M,N,O,P,Q,R,S)],[0>=F+1,0>=T,2*T>=F,1+F>=2*T]).
eq(evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),1,[evalbinsearchStepSize2bbin(1,H,I,D-I,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)],[D>=I]).
eq(evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I,J,A,B,C,D,E,F,G,H,I),1,[],[J=0,D+I>=256]).
eq(evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I,J,A,B,C,D,E,F,G,H,I),1,[],[J=0,I>=D+1]).
eq(evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I,J,A,B,C,D,E,F,G,H,I),1,[],[J=0,E>=G]).
eq(evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,A,B,C,D,E,F,G,H,I),1,[],[J=0,C=1]).
eq(evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,A,B,C,D,E,F,G,H,I),0,[],[J=1]).