/*

This example shows that splitting of equations
eliminates commutation (= symmetry+transitivity)

*/


id(X,X).
eq(X,Y) <- id(X,Y).
eq(Y,Z) <- eq(X,Y), eq(X,Z) if [Y>=Z].
eq(Y,X) <- eq(X,Y) if [X>Y].
eq(b,X) <- eq(a,X) if [b>=X].
eq(a,X) <- id(b,X) if [b>=X].
e(X,Y)==eq(Y,X).


precedence([a,b]).
top_predicates_precedence([eq,e,id]).


:-option([crw_depth(2),memo_constraints(on)]).
:-sama([3]).             % 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]).

/*

Saturation terminated.

Persisting Clauses:

    1(1) : id(B,B)
    2(1) : id(B,C) -> eq(B,C)
*   3(1) : eq(B,C),eq(B,D) -> eq(C,D) {[conj([C>=D],[],[])]}
    4(1) : eq(a,B) -> eq(b,B) {[conj([b>=B],[],[])]}
    5(1) : id(b,B) -> eq(a,B) {[conj([b>=B],[],[])]}
    6(2) : id(a,B) -> eq(b,B) {[conj([b>B],[],[])]}
*   8(2) : id(B,C),eq(B,D) -> eq(C,D) {[conj([C>D],[],[])]}
*  10(3) : id(a,B),eq(b,C) -> eq(B,C) {[conj([B>C,b>B],[],[])]}



Total time: 1410 milliseconds

Number of forward inferences: 5
Number of tableau inferences: 0
Number of kept clauses: 5


(8) and (10) are effectively eliminated since (1) is the only 
clause for id. Equation (6) is also redundant.

ST form should have, for any equation a=b with a>b:

a=x  -> b=x  if b>=x
b=x  -> a=x  if b>=x
a==x -> b=x  

This form is maintained under resolution inferences.

In particular, from ordered resolution inferences
of the form

a==x -> b=x         b=x -> c=x
------------------------------
       a==x -> c=x

one again generates a clause of the form (*)
as b>c for the inference to be ordered.

*/