% The number of rules for level I is the same
aux_equal(I) :- 
  aux_degree(I), aux_rule(N), 
  #count{R: r(R,I)}=N, #count{S: aux_o(S,I)}=N.

aux_somenonequalbefore(I) :-
  aux_degree(I),aux_degree(J),J<I,not aux_equal(J).

aux_better :- 
  aux_degree(I), aux_rule(N), 
  #count{R: r(R,I)}=N, #count{S: aux_o(S,I)}<N, 
  not aux_somenonequalbefore(I).

:- not aux_better.