:-option(special_relations(off)).	% otherwise trivially saturated
					% wrt. superposition.		
% reflexivity	
eq(X,X).
% symmetry
eq(X,Y) -> eq(Y,X).
% transitivity
eq(X,Y), eq(Y,Z) -> eq(X,Z).


(eq(X,X1), eq(Y,f(X1)) -> pf(X,Y)).
(eq(X,X1), pf(X,Y) -> eq(Y,f(X1)))  if [X>=X1].


%pf('$min',Y) -> p.
%pf(a,Y) -> p.



top_predicates_precedence([pf]).


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

:-option([crw_depth(2),memo_constraints(on)]).
:- saci([2]).