/* 

Natural numbers with ordering

*/




precedence( [s,p,<,0,n,n1,m,m1,a,b,rs,ce] ).


s(p(X))=X.
p(s(X))=X.

s(X)=s(Y) -> X=Y.

X<s(X).
%s(X)<X -> [].

X<Y -> X<s(Y).
(s(X)<s(Y)) -> (X<Y).
(s(X)<Y) -> (X<Y).


rs(X)->s(n(X))=n1(X).
ce(X)->n(X)=n1(X).

%s(n)=n1.
%p(n1)=m.

%a<b.



%:-ordering(sto).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,15]).  




/*
Saturation terminated.

Persisting Clauses:

    1(1) : s(p(B))=B
    2(1) : p(s(B))=B
    3(1) : s(B)=s(C) -> B=C
    4(1) : B<s(B)
    5(1) : s(B)<B -> 
    6(1) : B<C -> B<s(C)
    7(1) : s(B)<s(C) -> B<C
    8(1) : s(B)<C -> B<C
   11(2) : p(B)<B
   12(2) : B<p(B) -> 
   13(2) : B<C -> p(B)<C
   15(2) : B<p(C) -> B<C
   20(2) : s(B)<C -> B<p(C)
   21(2) : B<s(C) -> p(B)<C



Total time: 380 milliseconds

Number of forward inferences: 26
Number of tableau inferences: 0
Number of kept clauses: 14

*/