use(eqsup).


ordering(sto).
option(special_relations(off)).





eq(sup(X, X), X).

eq(sup(X,Y),XY),eq(sup(Y,Z),YZ) -> eq(sup(X, YZ),sup(XY, Z)).

eq(sup(X, Y),sup(Y, X)).
%sup(X, Y)=sup(Y, X).

%eq(f(sup(X, Y)),sup(f(X), f(Y))).

precedence([sup, inf, f,eq]). 
:-sama([]).             % 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]).

:-option([memo_constraints(on),crw_depth(2)]).