:-option(special_relations(off)).	% otherwise trivially saturated


use(congf2g1).

eq(f(f(X,Y),Z),f(X,f(Y,Z))).
eq(f(X,Y),f(Y,X)).
eq(f(X,0),X).


precedence( [g,f,eq,0] ).


:-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.