/*
This exercises an encoding of transitivity
of a relation p such that

   p(a,b) in trans_closure({p(a1,b1),...,p(ak,bk)})

iff

  |- pr([p(a1,b1),...,p(ak,bk)],a,b)

with respect to the encoding.

The point is that the antecedent of the queries
in the original problem occur as auxiliary argument
in the encoding, and ordering constraints in
initial clauses are used to access that list.


*/


predicates( [pr,islist] ).


:-option([special_relations(off),crw_depth(1)]).

pr(As,X,Y), pr(As,Y,Z) -> pr(As,X,Z).
axiom( [ [islist(As)], [pr(As,X,Y)], [[[As>p(X,Y)],[]]]] ).

islist(nil).
islist(cons(p(_,_),As)) <- islist(As).

precedence( [pr,islist,p,cons,nil] ).


:-ordering(sto).
:-sama([]).             % 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.
:-saci([2]).            % inherit ordering constraints