% The op commands declare infix/prefix/postfix operations

op(400, infix, ^).  % meet
op(400, infix, v).  % join
op(400, infix, |).  % Sheffer stroke (this is also the OR symbol for clauses).

% The lex command orders operations for orienting equations

lex([A, B, C, D, 0, 1, x v x, c(x), x ^ x, (x | x)]).

% A standard equational strategy (can be modified below)

set(anl_eq).
assign(pick_given_ratio, 3).
assign(max_weight, 25).

% Limit time and space

assign(max_seconds, 60).
assign(max_mem, 100000).   % 100 MB

% Limit what goes to the output file.

clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
clear(print_kept).
assign(stats_level, 1).

% Always include reflexivity for equational problems.

list(usable).
x = x.
end_of_list.

% OML basis: { AJ, B1, DM, OM }

assign(max_proofs, 2).

list(sos).

x v (y v z) = y v (x v z).     % AJ
x v (x ^ y) = x.               % B1
x ^ y = c(c(x) v c(y)).        % DM
x v (c(x) ^ (x v y)) = x v y.  % OM

end_of_list.

list(passive).

c(c(A)) != A.            % denial of CC
A v c(A) != B v c(B).    % denial of ONE

end_of_list.