/* 

doesn't terminate

*/


predicates( [eq] ).


:-option(special_relations(off)).	% otherwise trivially saturated
					% wrt. superposition.		
% reflexivity	
eq(X,X).
% symmetry
eq(X,Y) -> eq(Y,X).
% transitivity
axiom([[e(h(X,Y)), eq(Y,Z)],[eq(X,Z)],[[[X>=Y,X>=Z],[]]]]).
axiom([[e(h(X,Y)), eq(Y,Z)],[eq(X,Z)],[[[Y>=X,Y>=Z],[]]]]).
axiom([[e(h(X,Y)), eq(Y,Z)],[eq(X,Z)],[[[Z>=Y,Z>=X],[]]]]).
% replacement
% f(X) max
axiom([[e(h(X,Y)), eq(f(Y),Z)],[eq(f(X),Z)],[[[f(X)>=f(Y),f(X)>=Z],[]]]]).
% f(Y) max
axiom([[e(h(X,Y)), eq(f(Y),Z)],[eq(f(X),Z)],[[[f(Y)>=f(X),f(Y)>=Z],[]]]]).
% Z max
axiom([[e(h(X,Y)), eq(f(Y),Z)],[eq(f(X),Z)],[[[Z>=f(Y),Z>=f(X)],[]]]]).




precedence( [f,eq,e,h] ).

:-ordering(sto).

:-option([crw_depth(1),memo_constraints(on)]).
:-sama([3]).             % 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]).

/*
*/