% binary variant of ground rewriting
% locality of this theory shows
% that reachability can be decided in PTIME
% for ground rewrite systems.

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

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

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




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

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


/*

2001-05-09
Saturation terminated.


Persisting Clauses:

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



Total time: 51160 milliseconds

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

*/