/* 

These are the axioms for congruences.
With the given setting we can saturate
the system, which proves that the congruence closure
problem has a polynomial time upper bound.

This is the case of one unary function symbol.
For the binary and higher-order cases cf. cong2 and congHO, respectively.


We are interested in saturation up to redundancy by ordered resolution,
hence the special treatment of transitive relations is switched off.

*/


predicates( [eq] ).


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


eq(X,Y), eq(Y,Z) -> eq(X,Z).
eq(X,X).
eq(X,Y) -> eq(Y,X).
eq(X,Y),eq(f(X),Z) -> eq(f(Y),Z). 



precedence( [f,eq] ).

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