eq(evalrealheapsortstep1start(A,B,C),1,[evalrealheapsortstep1entryin(A,B,C)],[]).
eq(evalrealheapsortstep1entryin(A,B,C),1,[evalrealheapsortstep1returnin(A,B,C)],[2>=A]).
eq(evalrealheapsortstep1returnin(A,B,C),1,[evalrealheapsortstep1stop(A,B,C)],[]).
eq(evalrealheapsortstep1entryin(A,B,C),1,[evalrealheapsortstep1bb6in(A,1,C,D,E,F,G),loop_cont_evalrealheapsortstep1bb6in(E,F,G)],[D=0,A>=3]).
eq(evalrealheapsortstep1entryin(A,B,C),1,[evalrealheapsortstep1bb6in(A,1,C,D,E,F,G)],[D=1,A>=3]).
eq(loop_cont_evalrealheapsortstep1bb6in(A,B,C),0,[evalrealheapsortstep1returnin(A,B,C)],[]).
eq(evalrealheapsortstep1bb6in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,B,H,I,J,K),loop_cont_evalrealheapsortstep1bb3in(I,J,K,D,E,F,G)],[H=0,A>=1+B]).
eq(evalrealheapsortstep1bb6in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,B,H,I,J,K)],[D=1,H=1,A>=1+B]).
eq(evalrealheapsortstep1bb3in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb4in(A,B,C,D,E,F,G)],[C>=1]).
eq(loop_cont_evalrealheapsortstep1bb3in(A,B,C,D,E,F,G),0,[evalrealheapsortstep1bb5in(A,B,C,D,E,F,G)],[]).
eq(evalrealheapsortstep1bb4in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb2in(A,B,C,D,E,F,G)],[C+1=0]).
eq(evalrealheapsortstep1bb4in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb2in(A,B,C,D,E,F,G)],[C>=0,H>=0,C+1>=2*H,2*H>=C]).
eq(evalrealheapsortstep1bb4in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb2in(A,B,C,D,E,F,G)],[0>=C+2,0>=H,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb5in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb6in(A,B+1,C,D,E,F,G)],[]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,-1,D,E,F,G)],[C+1=0]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=1,H>=0,0>=2*H,1+2*H>=0,C+1=0]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=1,0>=H,C+1=0,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,-1,D,E,F,G)],[0>=1,H>=0,0>=2*H,1+2*H>=0,C+1=0]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=1,I>=0,0>=2*I,1+2*I>=0,H>=0,0>=2*H,1+2*H>=0,C+1=0]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=1,I>=0,0>=2*I,1+2*I>=0,0>=H,C+1=0,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,-1,D,E,F,G)],[0>=1,0>=H,C+1=0,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=1,0>=I,H>=0,0>=2*H,1+2*H>=0,C+1=0,2*I>=C+1,2+C>=2*I]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=1,0>=I,0>=H,C+1=0,2*I>=C+1,2+C>=2*I,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,-1,D,E,F,G)],[0>=1,H>=0,0>=2*H,1+2*H>=0,I>=0,0>=2*I,1+2*I>=0,C+1=0]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[C>=0,I>=0,C+1>=2*I,2*I>=C,J>=0,C+1>=2*J,2*J>=C,H>=0,C+1>=2*H,2*H>=C]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[C>=0,I>=0,C+1>=2*I,2*I>=C,J>=0,C+1>=2*J,2*J>=C,0>=C+2,0>=H,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,-1,D,E,F,G)],[0>=1,H>=0,0>=2*H,1+2*H>=0,0>=I,C+1=0,2*I>=C+1,2+C>=2*I]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[C>=0,I>=0,C+1>=2*I,2*I>=C,0>=C+2,0>=J,H>=0,C+1>=2*H,2*H>=C,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[C>=0,I>=0,C+1>=2*I,2*I>=C,0>=C+2,0>=J,0>=H,2*J>=C+1,2+C>=2*J,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,-1,D,E,F,G)],[0>=1,0>=H,I>=0,0>=2*I,1+2*I>=0,C+1=0,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=C+2,0>=I,C>=0,J>=0,C+1>=2*J,2*J>=C,H>=0,C+1>=2*H,2*H>=C,2*I>=C+1,2+C>=2*I]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=C+2,0>=I,C>=0,J>=0,C+1>=2*J,2*J>=C,0>=H,2*I>=C+1,2+C>=2*I,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,-1,D,E,F,G)],[0>=1,0>=H,0>=I,C+1=0,2*H>=C+1,2+C>=2*H,2*I>=C+1,2+C>=2*I]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=C+2,0>=I,0>=J,C>=0,H>=0,C+1>=2*H,2*H>=C,2*I>=C+1,2+C>=2*I,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortstep1bb2in(A,B,C,D,E,F,G),1,[evalrealheapsortstep1bb3in(A,B,H-1,D,E,F,G)],[0>=C+2,0>=I,0>=J,0>=H,2*I>=C+1,2+C>=2*I,2*J>=C+1,2+C>=2*J,2*H>=C+1,2+C>=2*H]).
eq(evalrealheapsortstep1bb6in(A,B,C,D,A,B,C),1,[],[D=0,B>=A]).
eq(evalrealheapsortstep1bb4in(A,B,C,D,A,B,C),1,[],[D=0,C+1=0]).
eq(evalrealheapsortstep1bb4in(A,B,C,D,A,B,C),0,[],[D=1]).
eq(evalrealheapsortstep1bb4in(A,B,C,D,A,B,C),1,[],[D=0,C>=0,E>=0,C+1>=2*E,2*E>=C]).
eq(evalrealheapsortstep1bb4in(A,B,C,D,A,B,C),1,[],[D=0,0>=C+2,0>=E,2*E>=C+1,2+C>=2*E]).
eq(evalrealheapsortstep1bb3in(A,B,C,D,A,B,C),1,[],[D=0,0>=C]).