% 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 BA 4-basis

x v (y v z) = y v (x v z).      % AJ
x ^ y = c(c(x) v c(y)).         % DM
x v c(x) = y v c(y).            % ONE
(x v c(y)) ^ (x v y) = x.       % CUT

% 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.

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