/* 

*/




:-option(special_relations(off)).


% theory axioms
'-eq'(X,X).
'-eq'(X,Y) -> '-eq'(Y,X).
'-eq'(X,Y), '-eq'(Y,Z) -> '-eq'(X,Z).


% restricted forward computation
'+eq'(X,Y) -> '+eq'(Y,X).
axiom([['+eq'(B,C),'+eq'(C,D)], ['+eq'(B,D)], [[[C>D,C>B],[]]]]).

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



:-option([crw_depth(3),memo_constraints(on)
	]).	
:-sama([]).             % ordered resolution w/o selection
	% 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:
Saturation terminated.

Persisting Clauses:

    1(1) : -eq(B,B)
    2(1) : -eq(B,C) -> -eq(C,B)
    3(1) : -eq(B,C),-eq(C,D) -> -eq(B,D)
    4(1) : +eq(B,C) -> +eq(C,B)
    5(1) : +eq(B,C),+eq(C,D) -> +eq(B,D) {[[[C>D,C>B],[]]]}
    6(1) : +eq(B,C) -> -eq(B,C)
    9(2) : +eq(B,C),-eq(C,D) -> -eq(B,D) {[[[B>D,B>C],[]]]}
   11(2) : +eq(B,C),-eq(D,B) -> -eq(D,C) {[[[C>D,C>B],[]]]}
   13(2) : +eq(B,C),-eq(D,B) -> -eq(D,C) {[[[B>D,B>C],[]]]}



Total time: 11270 milliseconds

Number of forward inferences: 24
Number of tableau inferences: 0
Number of kept clauses: 10


Clauses 2,3 and 13 are eliminated since 
they have a negative -eq-literal that is maximal.

Clauses 9 and 11 represent superposition left into equations.
Clause 5 is superposition right between two equations.

Clause 1 represents equality resolution.

*/