/*
  This is also called the monadic ground reachability problem.
  At present no algorithm better than O(n^3) is known.
  The problem is 2NPDA-complete (wrt. nlog n reduction
*/


predicates([>]).
precedence([f,>]).

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


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


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

:-ordering(sto).  % subterm ordering


/* 


*/