% binary case of increasing ground rewriting
% after Plaisted
% ==> is top rewriting
% ===> is rewriting increasing prefixes

% For GRS which are closed under reachable pairs
% of terms, only increasing rewriting sequences
% need to be considered

:-op(200,xfx,==>).
:-op(200,xfx,===>).

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

:-option([special_relations(off)]).




X==>Y, Y==>Z -> X==>Z.

X===>Y.

X==>Y, Y===>Z -> X==>Z.
X===>Y, U===>V -> f(X,U)===>f(Y,V).




:-option([crw_depth(1),memo_constraints(on)]).
:-sarp([1-7,10-15]). % the usual + clausal rewriting  
:-sama([]).
%:-saci([2]).        % not needed and wouldn't terminate anymore
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
:-ordering(sto).     % subterm ordering


/*


Saturation terminated.

Persisting Clauses:

    1(1) : B==>C,C==>D -> B==>D
    2(1) : B===>B
    3(1) : B==>C,C===>D -> B===>D
    4(1) : B===>C,D===>E -> f(B,D)===>f(C,E)
    9(2) : B===>C,D===>E,F==>f(B,D) -> F===>f(C,E)



Total time: 910 milliseconds

Number of forward inferences: 7
Number of tableau inferences: 0
Number of kept clauses: 5

*/