/* 

Transitive-reflexive closure pp of p

where p(A,B) is assumed to be given in the form of p(h(A,B)).

We show this is subterm local,
hence of quadratic complexity,
as each clause has at most two terms
such that any variable is contained in one of them.
(Hence the encoding of p(A,B) by p(h(A,B)).)

*/


predicates( [p] ).


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

pp(X,X).
axiom([[p(X,Y), pp(Y,Z)],[pp(X,Z)],[[[X>=Y,X>=Z],[]]]]).
axiom([[p(X,Y), pp(Y,Z)],[pp(X,Z)],[[[Y>=X,Y>=Z],[]]]]).
axiom([[p(X,Y), pp(Y,Z)],[pp(X,Z)],[[[Z>=Y,Z>=X],[]]]]).


precedence( [p,pp] ).

:-ordering(sto).

:-sama([3]).     
:-saci([2]).        % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.




/*
We (manually) select negative literals containing
the maximal term.

Clauses having a selected literal are marked with a (*)
in which case their first literal is selected.
*/

/*

Saturation terminated.

Persisting Clauses:

    1(1) : pp(B,B)
*   2(1) : p(B,C),pp(C,D) -> pp(B,D) {[conj([B>=C,B>=D],[],[])]}
*   3(1) : p(B,C),pp(C,D) -> pp(B,D) {[conj([C>=B,C>=D],[],[])]}
*   4(1) : pp(B,C),p(D,B) -> pp(D,C) {[conj([C>=B,C>=D],[],[])]}
*   5(2) : p(B,C) -> pp(B,C) {[conj([C>B],[],[])]}



Total time: 80 milliseconds

Number of forward inferences: 1
Number of tableau inferences: 0
Number of kept clauses: 1

*/