/* 

This is the case of a congruence in the absence of function
symbols. The saturated system indicates why superposition
is complete. The case of function symbols would require some second-order
notation for contexts which is beyond the scope of Saturate.

Equality is split into 2 halves. We assume that
equations that are produced by the context into which this theory
is embedded to arise in the form of +eq-facts only.
To put it differently, we assume that clause sets which import
this theory do not have positive [negative] occurrences
of -eq [+eq]. 


Also see cong_sat for a definition with initial constraints
that is saturated right away.

*/




:-option(special_relations(off)).


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


% monotonicity
%'-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). 

'+eq'(X,Y),p(X,Z) -> p(Y,Z).
'+eq'(X,Y),p(Z,X) -> p(Z,Y).


% assumptions
'+eq'(X,Y) -> '-eq'(X,Y).
'+eq'(X,Y) -> '+eq'(Y,X).




:-option([crw_depth(2),memo_constraints(on)
	]).	
:-sama([3]).            % user-guided selection: we select the -eq-literal
	% in 4 and 5 below. In any other clause we don't select anything.
:-sarp([1-7,10]).	% the usual + clausal rewriting  
:-sams([3,19]).         % messages about redundancy proofs by clausal rewrtng.
:-saci([2]).		% constraint inheritance

/*

Saturation terminated.

Persisting Clauses:


    2(1) : -eq(B,C) -> -eq(C,B)
    3(1) : -eq(B,C),-eq(C,D) -> -eq(B,D)
*   4(1) : -eq(B,C),p(B,D) -> p(C,D)
*   5(1) : -eq(B,C),p(D,B) -> p(D,C)
   14(2) : +eq(B,C),-eq(D,B) -> -eq(D,C) {[[[B>D,B>C],[]]]}


    6(1) : +eq(B,C) -> -eq(B,C)
    7(1) : +eq(B,C) -> +eq(C,B)

    1(1) : -eq(B,B)
   10(2) : +eq(B,C),-eq(C,D) -> -eq(B,D) {[[[B>D,B>C],[]]]}
   12(2) : +eq(B,C),-eq(D,B) -> -eq(D,C) {[[[C>D,C>B],[]]]}

   15(2) : +eq(B,C),p(B,D) -> p(C,D)
   16(2) : +eq(B,C),p(D,B) -> p(D,C)

   41(3) : +eq(B,C),+eq(C,D) -> -eq(B,D) {[[[C>D,C>B],[]]]}



Total time: 21000 milliseconds

Number of search inferences: 40
Number of kept clauses: 12


Clauses 2,3,4,5, and 14 are eliminated since 
they have a negative -eq-literal that is either maximal
or else has been selected.

In clause 41, -eq can be replaced by +eq without affecting
saturation.

Clauses 15 and 16 represent superposition of equations
into nonequational atoms. 
For instance, in 15, if B>C, we have superposition right:
then maximal literal is the negative p(B,D) and hyperresolving it
with a p-fact and an equation is the same as superposition right.
If C>B, the positive p(C,D) becomes strictly maximal, and
resolving 15 with a negative p-literal, followed by a resolution
step with a positive equation, represents superposition left.

Clauses 10 and 12 represent superposition left into equations.
Clause 41 is, after replacement of -eq by +eq, superposition
right between two equations.

*/