/* 

Natural numbers with ordering

*/

:-option(special_relations(off)).

use(eq).

precedence( [s,p,<,0] ).

eq(s(X),s(Y)) -> eq(X,Y).
eq(p(X),p(Y)) -> eq(X,Y).
eq(s(X),s(Y)) <- eq(X,Y).
eq(p(X),p(Y)) <- eq(X,Y).
eq(X,Y),eq(U,V),X<U -> Y<V.

eq(p(X),Y) -> eq(s(Y),X).
eq(s(X),Y) -> eq(p(Y),X).

p(X)<X.
X<s(X).
X<Y,Y<X -> [].

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

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

(s(X)<Y) -> (X<Y).
(X<p(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


*/