/* 

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).
%'-p'(X,Y) -> '+p'(X,Y).  % like to have this for simplification (not possible)
axiom([['+p'(B,C),'+p'(C,D)],['+p'(B,D)],[[[C>D,C>B],[]]]]).  % (*)


:-option([crw_depth(2),memo_constraints(on)]).
%:-sama([3]).             % We want saturation by ordered resolution w/o sel.
:-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 



/*

1.  case without (*) in input

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



2. case with (*) in input (then 25 above is not generated)

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)
    4(1) : +p(B,C),+p(C,D) -> +p(B,D) {[[[C>D,C>B],[]]]}
    7(2) : +p(B,C),-p(C,D) -> -p(B,D) {[[[B>D,B>C],[]]]}
    9(2) : +p(B,C),-p(D,B) -> -p(D,C) {[[[C>D,C>B],[]]]}
   11(2) : +p(B,C),-p(D,B) -> -p(D,C) {[[[B>D,B>C],[]]]}



Total time: 8310 milliseconds

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

*/