/* 

This is one of MacAllester's examples of fragments of propositional calculus
where satisfiability is in PTIME.

This Horn theory is not subterm-local and cannot even be saturated finitely
under the subterm ordering. Hence it shows that an ordering-based
approach can be more flexible.

Using the precedence subterm ordering sto, which is the union
of the subterm ordering with inequations of the form

	s=f(...) > t=g(...ti...)

if the ti are proper subterms of s and if f>g wrt. the given precedence
on function symbols, we show that the theory is saturated as is.
This proves the polynomial-time complexity of that example.

The file boolst contains a formulation of the same Horn theory
using an auxiliary predicate pn (for ``not provable'') that can
be saturated finitely into a presentation that is subterm-local.

*/




predicates( [p,pn] ).


p(X) -> p(lor(X,Y)).
p(Y) -> p(lor(X,Y)).
p(lor(X,Y)), p(nt(X)) -> p(Y).
p(lor(X,Y)), p(nt(Y)) -> p(X).
p(nt(X)),p(nt(Y)) -> p(nt(lor(X,Y))).
p(nt(lor(X,Y))) -> p(nt(X)).
p(nt(lor(X,Y))) -> p(nt(Y)).
p(X),p(nt(X)) -> p(ff).
p(ff) -> p(X).



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




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


:-ordering(sto).