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

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


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


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

:-ordering(sto).  % subterm ordering


/* 
sto case:  bottom-up proof search in clausal rewriting very useful.
950511 (Quintus 3.2)

Saturation terminated.

Persisting Clauses:

    1 : B>C,C>D -> B>D
    2 : B>B -> 
    3 : f(B)>B
    4 : B>C -> f(B)>f(C)
    5 : B>C -> f(B)>C
    6 : B>f(C) -> B>C
    7 : B>C,f(C)>D -> f(B)>D
    8 : B>C,D>f(B) -> D>f(C)



Total time: 433690 milliseconds




---------------------------------------------------------



lpo case in SCIStus
950328

Saturation terminated.

    1 : C>D,D>E -> C>E
    2 : C>C -> 
    3 : f(C)>C
    4 : C>D -> f(C)>f(D)
    5 : C>D,D>C -> 
    6 : C>D -> f(C)>D
    7 : C>f(D) -> C>D
    8 : f(C)>f(D),D>C -> 
   10 : C>D,f(D)>E -> f(C)>E
   11 : C>D,E>f(C) -> E>f(D)



Total time: 131050 milliseconds



-------------------------------------------------------------



This can also be saturated with special_relations(on):

Saturation terminated.

    1 : C>D,D>E -> C>E
    2 : C>C -> 
    3 : f(C)>C
    4 : C>D -> f(C)>f(D)



Total time: 640 milliseconds


*/