:-option(special_relations(off)).      % otherwise trivial


X<s(X).
X<Y -> X<s(Y).
X<Y -> p(X)<Y.



:-ordering(sto).
:-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.