eq(evalrealheapsortstart(A,B,C,D),1,[evalrealheapsortentryin(A,B,C,D)],[]).
eq(evalrealheapsortentryin(A,B,C,D),1,[evalrealheapsortreturnin(A,B,C,D)],[2>=A]).
eq(evalrealheapsortreturnin(A,B,C,D),1,[evalrealheapsortstop(A,B,C,D)],[]).
eq(evalrealheapsortentryin(A,B,C,D),1,[evalrealheapsortbb6in(A,1,C,D,E,F,G,H,I),loop_cont_evalrealheapsortbb6in(F,G,H,I)],[E=0,A>=3]).
eq(evalrealheapsortentryin(A,B,C,D),1,[evalrealheapsortbb6in(A,1,C,D,E,F,G,H,I)],[E=1,A>=3]).
eq(loop_cont_evalrealheapsortbb6in(A,B,C,D),0,[evalrealheapsortbb7in(A,B,C,D)],[]).
eq(evalrealheapsortbb7in(A,B,C,D),1,[evalrealheapsortbb18in(A,0,C,D,E,F,G,H,I),loop_cont_evalrealheapsortbb18in(F,G,H,I)],[E=0]).
eq(evalrealheapsortbb7in(A,B,C,D),1,[evalrealheapsortbb18in(A,0,C,D,E,F,G,H,I)],[E=1]).
eq(loop_cont_evalrealheapsortbb18in(A,B,C,D),0,[evalrealheapsortreturnin(A,B,C,D)],[]).
eq(evalrealheapsortbb6in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,B,D,J,K,L,M,N),loop_cont_evalrealheapsortbb3in(K,L,M,N,E,F,G,H,I)],[J=0,A>=1+B]).
eq(evalrealheapsortbb6in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,B,D,J,K,L,M,N)],[E=1,J=1,A>=1+B]).
eq(evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb4in(A,B,C,D,E,F,G,H,I)],[C>=1]).
eq(evalrealheapsortbb18in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb8in(A,B,C,D,E,F,G,H,I)],[A>=2+B]).
eq(evalrealheapsortbb16in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb9in(A,B,C,D,E,F,G,H,I)],[A>=B+3+2*C]).
eq(loop_cont_evalrealheapsortbb3in(A,B,C,D,E,F,G,H,I),0,[evalrealheapsortbb5in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb4in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I)],[C+1=0]).
eq(evalrealheapsortbb4in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I)],[C>=0,J>=0,C+1>=2*J,2*J>=C]).
eq(evalrealheapsortbb4in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I)],[0>=C+2,0>=J,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb8in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb16in(A,B,0,D,J,K,L,M,N),loop_cont_evalrealheapsortbb16in(K,L,M,N,E,F,G,H,I)],[J=0]).
eq(evalrealheapsortbb8in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb16in(A,B,0,D,J,K,L,M,N)],[E=1,J=1]).
eq(evalrealheapsortbb9in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb11in(A,B,C,D,E,F,G,H,I)],[A=2*C+3+B]).
eq(evalrealheapsortbb9in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb10in(A,B,C,D,E,F,G,H,I)],[A>=B+4+2*C]).
eq(evalrealheapsortbb9in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb10in(A,B,C,D,E,F,G,H,I)],[2*C+2+B>=A]).
eq(evalrealheapsortbb5in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb6in(A,B+1,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,-1,D,E,F,G,H,I)],[C+1=0]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=1,J>=0,0>=2*J,1+2*J>=0,C+1=0]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=1,0>=J,C+1=0,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,-1,D,E,F,G,H,I)],[0>=1,J>=0,0>=2*J,1+2*J>=0,C+1=0]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=1,K>=0,0>=2*K,1+2*K>=0,J>=0,0>=2*J,1+2*J>=0,C+1=0]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=1,K>=0,0>=2*K,1+2*K>=0,0>=J,C+1=0,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,-1,D,E,F,G,H,I)],[0>=1,0>=J,C+1=0,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=1,0>=K,J>=0,0>=2*J,1+2*J>=0,C+1=0,2*K>=C+1,2+C>=2*K]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=1,0>=K,0>=J,C+1=0,2*K>=C+1,2+C>=2*K,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,-1,D,E,F,G,H,I)],[0>=1,J>=0,0>=2*J,1+2*J>=0,K>=0,0>=2*K,1+2*K>=0,C+1=0]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[C>=0,K>=0,C+1>=2*K,2*K>=C,L>=0,C+1>=2*L,2*L>=C,J>=0,C+1>=2*J,2*J>=C]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[C>=0,K>=0,C+1>=2*K,2*K>=C,L>=0,C+1>=2*L,2*L>=C,0>=C+2,0>=J,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,-1,D,E,F,G,H,I)],[0>=1,J>=0,0>=2*J,1+2*J>=0,0>=K,C+1=0,2*K>=C+1,2+C>=2*K]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[C>=0,K>=0,C+1>=2*K,2*K>=C,0>=C+2,0>=L,J>=0,C+1>=2*J,2*J>=C,2*L>=C+1,2+C>=2*L]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[C>=0,K>=0,C+1>=2*K,2*K>=C,0>=C+2,0>=L,0>=J,2*L>=C+1,2+C>=2*L,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,-1,D,E,F,G,H,I)],[0>=1,0>=J,K>=0,0>=2*K,1+2*K>=0,C+1=0,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=C+2,0>=K,C>=0,L>=0,C+1>=2*L,2*L>=C,J>=0,C+1>=2*J,2*J>=C,2*K>=C+1,2+C>=2*K]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=C+2,0>=K,C>=0,L>=0,C+1>=2*L,2*L>=C,0>=J,2*K>=C+1,2+C>=2*K,2*J>=C+1,2+C>=2*J]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,-1,D,E,F,G,H,I)],[0>=1,0>=J,0>=K,C+1=0,2*J>=C+1,2+C>=2*J,2*K>=C+1,2+C>=2*K]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=C+2,0>=K,0>=L,C>=0,J>=0,C+1>=2*J,2*J>=C,2*K>=C+1,2+C>=2*K,2*L>=C+1,2+C>=2*L]).
eq(evalrealheapsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb3in(A,B,J-1,D,E,F,G,H,I)],[0>=C+2,0>=K,0>=L,0>=J,2*K>=C+1,2+C>=2*K,2*L>=C+1,2+C>=2*L,2*J>=C+1,2+C>=2*J]).
eq(loop_cont_evalrealheapsortbb16in(A,B,C,D,E,F,G,H,I),0,[evalrealheapsortbb17in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb11in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb13in(A,B,C,2*C+1,E,F,G,H,I)],[]).
eq(evalrealheapsortbb10in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb11in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb10in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb12in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb17in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb18in(A,B+1,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb13in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb14in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb13in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb16in(A,B,A,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb12in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb13in(A,B,C,2*C+2,E,F,G,H,I)],[]).
eq(evalrealheapsortbb14in(A,B,C,D,E,F,G,H,I),1,[evalrealheapsortbb16in(A,B,D,D,E,F,G,H,I)],[]).
eq(evalrealheapsortbb6in(A,B,C,D,E,A,B,C,D),1,[],[E=0,B>=A]).
eq(evalrealheapsortbb4in(A,B,C,D,E,A,B,C,D),1,[],[E=0,C+1=0]).
eq(evalrealheapsortbb4in(A,B,C,D,E,A,B,C,D),0,[],[E=1]).
eq(evalrealheapsortbb4in(A,B,C,D,E,A,B,C,D),1,[],[E=0,C>=0,F>=0,C+1>=2*F,2*F>=C]).
eq(evalrealheapsortbb4in(A,B,C,D,E,A,B,C,D),1,[],[E=0,0>=C+2,0>=F,2*F>=C+1,2+C>=2*F]).
eq(evalrealheapsortbb3in(A,B,C,D,E,A,B,C,D),1,[],[E=0,0>=C]).
eq(evalrealheapsortbb18in(A,B,C,D,E,A,B,C,D),1,[],[E=0,B+1>=A]).
eq(evalrealheapsortbb16in(A,B,C,D,E,A,B,C,D),1,[],[E=0,2*C+2+B>=A]).