% This is a Mace4 input file.  It won't work with Mace2.

op(400, infix, ^).
op(400, infix, v).

assign(max_models, -1).     % no limit
set(print_models_portable).

clauses(theory).

% Here is the MOL 6-basis

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
c(c(x)) = x.                            % CC
x v c(x) = y v c(y).                    % ONE
x v (y ^ (x v z)) = x v (z ^ (x v y)).  % MOD

% definition of Sheffer Stroke

f(x,y) = c(x) v c(y).

% Add some ortholattice properties to help Mace4,
% and specify the top and bottom elements.

x ^ (x v y) = x.            % B2

x v y = y v x.
x ^ y = y ^ x.

x v c(x) = 1.
x ^ c(x) = 0.

x v 0 = x.
x v 1 = 1.
x ^ 1 = x.
x ^ 0 = 0.

end_of_list.