/* 

Natural numbers with ordering

*/




precedence( [<,s,0] ).


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

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

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




:-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.


:-option([memo_constraints(on),crw_depth(1)]).


/*

why is eq(s(X),s(Y)) not simplified to eq(X,Y)


Saturation terminated.

Persisting Clauses:

    1(1) : eq(B,B)
    2(1) : eq(B,C) -> eq(C,B)
    3(1) : eq(B,C),eq(C,D) -> eq(B,D)
    4(1) : eq(B,C),B<D -> C<D
    5(1) : eq(B,C),D<B -> D<C
    6(1) : eq(s(B),s(C))==eq(B,C)
    9(1) : B<C -> s(B)<s(C)
   10(1) : s(B)<s(C) -> B<C
   12(2) : eq(0,B) -> B<s(C)
   13(2) : eq(B,s(C)),B<0 -> 
   14(2) : eq(B,s(C)),B<s(D) -> C<D
   16(2) : s(B)<C,eq(C,0) -> 
   17(2) : eq(B,s(C)),s(D)<B -> D<C
   20(2) : B<C,eq(s(B),D) -> D<s(C)
   21(2) : B<C,eq(s(C),D) -> s(B)<D
   23(3) : eq(B,0),C<B,eq(C,s(D)) -> 
   29(3) : eq(0,B),eq(s(C),D) -> B<D
   35(4) : eq(s(B),0) -> 
   45(3) : B<C,eq(s(B),D),eq(s(C),E) -> D<E
   56(3) : eq(B,s(C)),D<B,eq(D,s(E)) -> E<C
   61(3) : B<C,eq(s(C),s(D)),eq(s(B),s(E)) -> E<D



Total time: 219440 milliseconds

Number of forward inferences: 75
Number of tableau inferences: 0
Number of kept clauses: 21


*/