/* 
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 binary function symbol.
Takes 10 times longer to saturate.


*/




:-option(special_relations(off)).  


'-p'(X,Y), '-p'(Y,Z) -> '-p'(X,Z).
'-p'(X,X).
'-p'(X,Y) -> '-p'(Y,X).
%'-p'(X,Y), '-p'(U,V) -> '-p'(f(X,U),f(Y,V)).          % a
'-p'(X,Y), '-p'(U,V), '-p'(f(X,U),Z) -> '-p'(f(Y,V),Z).   % b

%'+p'(X,Y) -> '-p'(X,Y).
%'+p'(X,Y) -> '+p'(Y,X).



:-option([crw_depth(1),memo_constraints(on)]).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-4,6,7,10]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
%:-saci([2]).


/* 


*/