/* 

This is one formulation of the axioms for congruences
which is saturated.
This proves that the congruence closure
problem has a cubic time upper bound.

This is the case of one unary function symbol.
A formulation with monotonicity instead of replacement is found
in congM.

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.		
% reflexivity	
eq(X,X).
% symmetry
eq(X,Y) -> eq(Y,X).
% transitivity
eq(X,Y), eq(Y,Z) -> eq(X,Z).
% replacement
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.


/*
Saturation terminated.

Persisting Clauses:

    1(1) : eq(B,C),eq(C,D) -> eq(B,D)
    2(1) : eq(B,B)
    3(1) : eq(B,C) -> eq(C,B)
    4(1) : eq(B,C),eq(f(B),D) -> eq(f(C),D)



Total time: 16030 milliseconds

Number of search inferences: 7
Number of kept clauses: 4
*/