eq(evalrealshellsortstart(A,B,C,D,E),1,[evalrealshellsortentryin(A,B,C,D,E)],[]).
eq(evalrealshellsortreturnin(A,B,C,D,E),1,[evalrealshellsortstop(A,B,C,D,E)],[]).
eq(evalrealshellsortentryin(A,B,C,D,E),1,[evalrealshellsortbb8in(A,0,C,D,E,F,G,H,I,J,K),loop_cont_evalrealshellsortbb8in(G,H,I,J,K)],[F=0,A=0]).
eq(evalrealshellsortentryin(A,B,C,D,E),1,[evalrealshellsortbb8in(A,0,C,D,E,F,G,H,I,J,K)],[F=1,A=0]).
eq(evalrealshellsortentryin(A,B,C,D,E),1,[evalrealshellsortbb8in(A,F,C,D,E,G,H,I,J,K,L),loop_cont_evalrealshellsortbb8in(H,I,J,K,L)],[G=0,A>=1,F>=0,A>=2*F,1+2*F>=A]).
eq(evalrealshellsortentryin(A,B,C,D,E),1,[evalrealshellsortbb8in(A,F,C,D,E,G,H,I,J,K,L)],[G=1,A>=1,F>=0,A>=2*F,1+2*F>=A]).
eq(evalrealshellsortentryin(A,B,C,D,E),1,[evalrealshellsortbb8in(A,F,C,D,E,G,H,I,J,K,L),loop_cont_evalrealshellsortbb8in(H,I,J,K,L)],[G=0,0>=A+1,0>=F,2*F>=A,1+A>=2*F]).
eq(evalrealshellsortentryin(A,B,C,D,E),1,[evalrealshellsortbb8in(A,F,C,D,E,G,H,I,J,K,L)],[G=1,0>=A+1,0>=F,2*F>=A,1+A>=2*F]).
eq(loop_cont_evalrealshellsortbb8in(A,B,C,D,E),0,[evalrealshellsortreturnin(A,B,C,D,E)],[]).
eq(evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb6in(A,B,0,D,E,L,M,N,O,P,Q),loop_cont_evalrealshellsortbb6in(M,N,O,P,Q,F,G,H,I,J,K)],[L=0,B>=1]).
eq(evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb6in(A,B,0,D,E,L,M,N,O,P,Q)],[F=1,L=1,B>=1]).
eq(evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb1in(A,B,C,D,E,F,G,H,I,J,K)],[A>=C+1]).
eq(evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb4in(A,B,C,D,E,F,G,H,I,J,K)],[E>=B]).
eq(loop_cont_evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K),0,[evalrealshellsortbb7in(A,B,C,D,E,F,G,H,I,J,K)],[]).
eq(evalrealshellsortbb1in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb3in(A,B,C,L,C,M,N,O,P,Q,R),loop_cont_evalrealshellsortbb3in(N,O,P,Q,R,F,G,H,I,J,K)],[M=0]).
eq(evalrealshellsortbb1in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb3in(A,B,C,L,C,M,N,O,P,Q,R)],[F=1,M=1]).
eq(evalrealshellsortbb4in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb2in(A,B,C,D,E,F,G,H,I,J,K)],[L>=D+1]).
eq(evalrealshellsortbb7in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb8in(A,0,C,D,E,F,G,H,I,J,K)],[B=0]).
eq(evalrealshellsortbb7in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb8in(A,L,C,D,E,F,G,H,I,J,K)],[B>=1,L>=0,B>=2*L,1+2*L>=B]).
eq(evalrealshellsortbb7in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb8in(A,L,C,D,E,F,G,H,I,J,K)],[0>=B+1,0>=L,2*L>=B,1+B>=2*L]).
eq(loop_cont_evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K),0,[evalrealshellsortbb5in(A,B,C,D,E,F,G,H,I,J,K)],[]).
eq(evalrealshellsortbb2in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb3in(A,B,C,D,E-B,F,G,H,I,J,K)],[]).
eq(evalrealshellsortbb5in(A,B,C,D,E,F,G,H,I,J,K),1,[evalrealshellsortbb6in(A,B,C+1,D,E,F,G,H,I,J,K)],[]).
eq(evalrealshellsortbb8in(A,B,C,D,E,F,A,B,C,D,E),1,[],[F=0,0>=B]).
eq(evalrealshellsortbb6in(A,B,C,D,E,F,A,B,C,D,E),1,[],[F=0,C>=A]).
eq(evalrealshellsortbb4in(A,B,C,D,E,F,A,B,C,D,E),1,[],[F=0,D>=G]).
eq(evalrealshellsortbb4in(A,B,C,D,E,F,A,B,C,D,E),0,[],[F=1,G>=D]).
eq(evalrealshellsortbb3in(A,B,C,D,E,F,A,B,C,D,E),1,[],[F=0,B>=E+1]).