/* 
The theory of lists.

*/




cons(X,Y)=Z -> car(Z)=X.
cons(X,Y)=Z -> cdr(Z)=Y.
cons(X,Y)=cons(U,V) -> X=U.
cons(X,Y)=cons(U,V) -> Y=V.


precedence( [car,cdr,cons] ).
:-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)]).


/* 

*/