/* 
This example shows that Saturate has some of the capabilities
of McAllester's Ontic System for proving the locality of 
inference systems.

Saturate shows that equivalence can be finitely
saturated under ordered resolution
with respect to any signature containing p and any lpo.
In particular this applies to lpos in which for any ground atom p(s,t)
there are at most O(n^2) smaller ground atoms, where n is the
maximum of the sizes of s and t. This is the case for lpos
where the precedence of p is smaller than the precedence of any
function symbol.

*/




predicates( [eq] ).

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

% system 2
/*
eq(X,X).
eq(Z,Y) <- eq(Z,X), eq(Y,X) if [Y>=Z].
eq(Z,Y) <- eq(Y,Z)          if [Z>Y].
*/

% system 1
eq(X,Y), eq(Y,Z) -> eq(X,Z).
eq(X,X).
eq(X,Y) -> eq(Y,X).

%ordering(sto).

option([memo_constraints(on),crw_depth(1)]).

:-sama([]).    
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
%:-saci([2]).



/*
System 1:
we've selected in a way such that extra variables are bounded

Saturation terminated.

Persisting Clauses:

    1(1) : eq(B,B)
*   2(1) : eq(B,C),eq(D,C) -> eq(D,B) {[conj([B>=D],[],[])]}
    3(1) : eq(B,C) -> eq(C,B) {[conj([C>B],[],[])]}
*   4(2) : eq(B,C),eq(D,B) -> eq(D,C) {[conj([C>D,C>B],[],[])]}



Total time: 60 milliseconds

Number of forward inferences: 1
Number of tableau inferences: 0
Number of generated clauses: 4
Number of kept clauses: 2
*/