/* 

With this definition of transitivity we obtain a saturated system
from which the ordered chaining calculus can be justified.

*/



:-option(special_relations(off)).      % otherwise trivial


'-p'(X,Y), '-p'(Y,Z) -> '-p'(X,Z).
'+p'(X,Y) -> '-p'(X,Y).
%axiom([['+p'(X,Y), '+p'(Y,Z)],['-p'(X,Z)],[[[Y>X,Y>Z],[]]]]).



:-option([crw_depth(1),memo_constraints(on)]).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-4,6,7,10]).   % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
:-saci([2]).	     % constraint inheritance provides us with 



/*

Saturation terminated.

Persisting Clauses:

    1(1) : -p(B,C),-p(C,D) -> -p(B,D)
    2(1) : +p(B,C) -> -p(B,C)
    3(2) : +p(B,C),-p(C,D) -> -p(B,D) {[[[D>C],[B=D]],[[D>C,B>D,B>C],[]]]}
    5(2) : +p(B,C),-p(C,D) -> -p(B,D) {[[[B>D,B>C],[]]]}
    7(2) : +p(B,C),-p(D,B) -> -p(D,C) {[[[C>D,C>B],[]]]}
    9(2) : +p(B,C),-p(D,B) -> -p(D,C) {[[[B>D,B>C],[]]]}
   10(3) : +p(B,C),+p(D,B) -> -p(D,C) {[[[C>B],[D=C]]]}
   31(3) : +p(B,C),+p(C,D) -> -p(B,D) {[[[C>D,C>B],[]]]}
   33(3) : +p(B,C),-p(D,B),+p(E,D) -> -p(E,C) {[[[C>D,C>B],[E=C]]]}



Total time: 17520 milliseconds

Number of search inferences: 38
Number of kept clauses: 9



*/