:-option(special_relations(off)).

'-r'(X,X).
'-r'(X,Y),'-r'(Y,Z) -> '-r'(X,Z).

'+r'(X,Y) -> '-r'(X,Y).


true(X,W) -> true(or(X,Y),W).
true(Y,W) -> true(or(X,Y),W).
true(or(X,Y),W) -> true(X,W),true(Y,W).
true(not(X),W),true(X,W) -> [].
true(not(X),W),true(X,W).


true(box(P),W), '-r'(X,W) -> true(P,W).
true(box(P),X),'+r'(X,f(P,X)).
true(P,f(P,X)) -> true(box(P),X).


precedence( [box,not,or,f,true] ).
:-option(crw_depth(1)).
:-sama([]).        % We want saturation by ordered resolution w/o sel.
:-sarp([1-4,6,7,10]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
:-saci([2]).