/* 
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.


*/


predicates( [p] ).


:-option(special_relations(off)).      % otherwise trivial


p(X,Y), p(Y,Z) -> p(X,Z).
p(X,X).
p(X,Y) -> p(Y,X).
p(X,Y) -> p(f(X,U),f(Y,U)).   
p(U,V) -> p(f(X,U),f(X,V)).   




precedence( [f,p] ).

:-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.
:-saci([2]).
:-ordering(sto).  % subterm ordering

/*

990809

Saturation terminated.

Persisting Clauses:

    1(1) : p(B,C),p(C,D) -> p(B,D)
    2(1) : p(B,B)
    3(1) : p(B,C) -> p(C,B)
    6(2) : p(B,C),p(f(C,D),E) -> p(f(B,D),E)
   11(2) : p(B,C),p(f(D,C),E) -> p(f(D,B),E)
   24(3) : p(B,C),p(D,E) -> p(f(D,B),f(E,C))
   26(4) : p(B,C),p(D,E),p(f(E,C),F) -> p(f(D,B),F)



Total time: 1368720 milliseconds

Number of forward inferences: 55
Number of tableau inferences: 0
Number of kept clauses: 9

*/