/* 
*/


predicates( [eq] ).


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


eq(X,Y), eq(Y,Z) -> eq(X,Z).
eq(X,X).
eq(X,Y) -> eq(Y,X).
eq(X,Y) -> eq(f(X),f(Y)).
eq(X,Y) -> eq(h(X),h(Y)).

eq(h(X),H),eq(f(X),F) -> eq(f(H),h(F)).



precedence( [eq,h,f] ).
:-ordering(sto).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-saci([2]).
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.


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

/*



*/