less(N,s(N)).
less(N,s(M)) <- less(N,M).
p <- less(X,Y),less(Y,X).

:-ordering(sto).

:-option([crw_depth(1),memo_constraints(on)]).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).         % messages about redundancy proofs by clausal rewrtng.