/* 

One of MacAllester's examples of fragments of propositional calculus
with polytime satisfiability test. We use an auxiliary predicate ``pn''
to show that the saturated variant of it (with respect to the lpo)
is subterm-local. Also see file ``bool''.


*/




predicates( [p,pn] ).


p(X) -> p(or(X,Y)).
p(Y) -> p(or(X,Y)).
p(or(X,Y)), p(nt(X)) -> p(Y).
p(or(X,Y)), p(nt(Y)) -> p(X).
p(nt(X)),p(nt(Y)) -> p(nt(or(X,Y))).
p(nt(or(X,Y))) -> p(nt(X)).
p(nt(or(X,Y))) -> p(nt(Y)).
p(X),p(nt(X)) -> p('$min').
p('$min') -> p(X).



p(nt(nt(X)))==p(X).



% this auxiliary predicate helps to avoid problems with nt-terms
pn(X) == p(nt(X)).
pn(nt(X)) == p(X).


precedence( [or,nt,p,pn] ).
:-option(crw_depth(2)).
:-sama([]).                % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).       % full power	  
:-sams([3,19]).


/*

The saturated system has the dual subterm property, hence is subterm-local.

    1(1) : p(B) -> p(or(B,C))
    2(1) : p(B) -> p(or(C,B))
    9(1) : p(min) -> p(B)
   11(1) : p(nt(B))==pn(B)
   12(1) : pn(nt(B))==p(B)
   13(2) : p(or(B,C)),pn(B) -> p(C)
   14(2) : p(or(B,C)),pn(C) -> p(B)
   15(2) : pn(B),pn(C) -> pn(or(B,C))
   16(2) : pn(or(B,C)) -> pn(B)
   17(2) : pn(or(B,C)) -> pn(C)
   18(2) : p(B),pn(B) -> p(min)
   19(2) : p(min) -> pn(B)


Total time: 1570 milliseconds

*/