/* 

This is a modification of an example by McAllester.
Without the inductive property (*) of even sums
the system in in no sense local.
With (*) it can be saturated
under the subterm ordering.
It would be nice if (*) could be found automatically
when saturating the system without (*).

*/




:-option(special_relations(off)).	% otherwise trivially saturated
					% wrt. superposition.		
even(0).
even(X) -> odd(s(X)).
odd(X) -> even(s(X)).

add(X,0,X).
add(X,Y,Z) -> add(X,s(Y),s(Z)).

add(X,Y,Z), even(Z) -> es(X,Y).


% (*)
es(X,Y) -> es(X,s(s(Y))).

precedence([s,0,es,add,even,odd]).


:-ordering(sto).

:-option([crw_depth(1),memo_constraints(on)]).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10]).    % the usual + clausal rewriting  
:-sams([3,19]).         % messages about redundancy proofs by clausal rewrtng.


/*
Saturation terminated.

Persisting Clauses:

    1(1) : even(0)
    2(1) : even(B) -> odd(s(B))
    3(1) : odd(B) -> even(s(B))
    4(1) : add(B,0,B)
    5(1) : add(B,C,D) -> add(B,s(C),s(D))
    6(1) : add(B,C,D),even(D) -> es(B,C)
    7(1) : es(B,C) -> es(B,s(s(C)))
    8(2) : add(B,C,D),even(s(D)) -> es(B,s(C))
    9(3) : add(B,C,D),odd(D) -> es(B,s(C))
   10(4) : add(B,C,D),odd(s(D)) -> es(B,s(s(C)))



Total time: 5340 milliseconds

Number of search inferences: 4
Number of kept clauses: 10

*/