/*

This example shows that splitting of equations
eliminates commutation (= symmetry+transitivity).
We need to syntactically distinguish between trivial
equational proofs (by reflexivity id) and nontrivial proofs
(by eq).

*/


id(X,X).
eq(X,Y) <- id(X,Y).
eq(Y,Z) <- eq(X,Y), eq(X,Z).

eq(a,b).
eq(b,X) <- eq(a,X).
%
eq(a,X) <- eq(b,X).


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



:-sama([3]).            % We want saturation by ordered resolution w/ 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) : id(B,B)
    2(1) : id(B,C) -> eq(B,C)
*   3(1) : eq(B,C),eq(B,D) -> eq(C,D)
    4(1) : eq(a,B) -> eq(b,B)
    5(1) : eq(b,B) -> eq(a,B)


    6(2) : id(a,B) -> eq(b,B)
*   7(2) : id(B,C),eq(B,D) -> eq(C,D)
*   9(3) : id(a,B),eq(b,C) -> eq(B,C)



Total time: 890 milliseconds

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

(7) and (9) 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 
b=x  -> a=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.

*/