/* 

Derivation of ordered chaining for quasi-orderings.

*/



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

'-p'(X,X).
'-p'(X,Y), '-p'(Y,Z) -> '-p'(X,Z).
'+p'(X,Y) -> '-p'(X,Y).



:-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,B)
    2(1) : -p(B,C),-p(C,D) -> -p(B,D)
    3(1) : +p(B,C) -> -p(B,C)
    6(2) : +p(B,C),-p(C,D) -> -p(B,D) {[[[B>D,B>C],[]]]}
    8(2) : +p(B,C),-p(D,B) -> -p(D,C) {[[[C>D,C>B],[]]]}
   10(2) : +p(B,C),-p(D,B) -> -p(D,C) {[[[B>D,B>C],[]]]}
   25(3) : +p(B,C),+p(C,D) -> -p(B,D) {[[[C>D,C>B],[]]]}



Total time: 8460 milliseconds

Number of search inferences: 24
Number of kept clauses: 8



*/