eq(evalrealheapsortstep2start(A,B,C,D),1,[evalrealheapsortstep2entryin(A,B,C,D)],[]).
eq(evalrealheapsortstep2entryin(A,B,C,D),1,[evalrealheapsortstep2bbin(A,B,C,D)],[A>=3]).
eq(evalrealheapsortstep2entryin(A,B,C,D),1,[evalrealheapsortstep2returnin(A,B,C,D)],[2>=A]).
eq(evalrealheapsortstep2returnin(A,B,C,D),1,[evalrealheapsortstep2stop(A,B,C,D)],[]).
eq(evalrealheapsortstep2bbin(A,B,C,D),1,[evalrealheapsortstep2bb11in(A,0,C,D,E,F,G,H,I),loop_cont_evalrealheapsortstep2bb11in(F,G,H,I)],[E=0]).
eq(evalrealheapsortstep2bbin(A,B,C,D),1,[evalrealheapsortstep2bb11in(A,0,C,D,E,F,G,H,I)],[E=1]).
eq(loop_cont_evalrealheapsortstep2bb11in(A,B,C,D),0,[evalrealheapsortstep2returnin(A,B,C,D)],[]).
eq(evalrealheapsortstep2bb11in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb1in(A,B,C,D,E,F,G,H,I)],[A>=2+B]).
eq(evalrealheapsortstep2bb9in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb2in(A,B,C,D,E,F,G,H,I)],[A>=B+3+2*C]).
eq(evalrealheapsortstep2bb1in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb9in(A,B,0,D,J,K,L,M,N),loop_cont_evalrealheapsortstep2bb9in(K,L,M,N,E,F,G,H,I)],[J=0]).
eq(evalrealheapsortstep2bb1in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb9in(A,B,0,D,J,K,L,M,N)],[E=1,J=1]).
eq(evalrealheapsortstep2bb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb4in(A,B,C,D,E,F,G,H,I)],[A=2*C+3+B]).
eq(evalrealheapsortstep2bb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb3in(A,B,C,D,E,F,G,H,I)],[A>=B+4+2*C]).
eq(evalrealheapsortstep2bb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb3in(A,B,C,D,E,F,G,H,I)],[2*C+2+B>=A]).
eq(loop_cont_evalrealheapsortstep2bb9in(A,B,C,D,E,F,G,H,I),0,[evalrealheapsortstep2bb10in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb4in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb6in(A,B,C,2*C+1,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb3in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb4in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb3in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb5in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb10in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb11in(A,B+1,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb6in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb7in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb6in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb9in(A,B,A,D,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb5in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb6in(A,B,C,2*C+2,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb7in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortstep2bb9in(A,B,D,D,E,F,G,H,I)],[]).
eq(evalrealheapsortstep2bb11in(A,B,C,D,E,A,B,C,D),1,[],[E=0,B+1>=A]).
eq(evalrealheapsortstep2bb9in(A,B,C,D,E,A,B,C,D),1,[],[E=0,2*C+2+B>=A]).