predicates( [r,-] ).


P-W -> '$or'(P,Q)-W.
Q-W -> '$or'(P,Q)-W.
'$or'(P,Q)-W -> P-W, Q-W.
P-W, '$not'(P)-W.
P-W, '$not'(P)-W -> [].

'$diam'('$var'(P))-X -> '$var'(P)-g(P,X).
'$diam'('$var'(P))-X -> r(X,g(P,X)).
r(X,W), '$var'(P)-W -> '$diam'('$var'(P))-X.

%'$box'(P)= '$not'('$diam'('$not'(P))).


%'$and'(P,Q)='$not'('$or'('$not'(P),'$not'(Q))).
%'$impl'(P,Q)='$or'('$not'(P),Q).
%'$equiv'(P,Q)='$and'('$impl'(P,Q),'$impl'(Q,P)).
%'$not'('$not'(P))=P.

first_predicate_precedence([-]).
%precedence( [g,h,f,'$box','$diam','$equiv','$impl','$and','$or','$var','$not',r,p,q,w] ).
precedence( [g,h,f,'$diam','$or','$var','$not',r,p,q,w] ).

%:-option(term_var_size).





:-option([crw_depth(1),memo_constraints(on)]).
:-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.
:-saci([2]).
%:-ordering(sto).  % subterm ordering