/* 

These are again the axioms for congruences.
With the given setting we obtain a saturated system
that can be used to justify superposition as a specialized
form of ordered resolution modulo this
set of axioms.

In particular 

eq(X,Y),eq(U,V),eq(f(X,U),Z) -> eq(F(Y,V),Z)

is not in the final system. This shows that peaks that
result from rewriting in independent subterms are redundant.


*/


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,U),Z) -> eq(f(Y,U),Z). 
eq(X,Y),eq(f(U,X),Z) -> eq(f(U,Y),Z). 



precedence( [f,eq] ).


:-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),E) -> eq(f(C,D),E)
    5(1) : eq(B,C),eq(f(D,B),E) -> eq(f(D,C),E)



Total time: 31030 milliseconds

Number of search inferences: 18
Number of kept clauses: 5


*/