op(400, xfx, [*,+,#]).  % infix operators
op(300, yf, @).         % postfix operator

lex([p(_,_,_), f1(_,_,_), f2(_,_), _#_]).  % see demodulators below

set(knuth_bendix).
set(back_unit_deletion).
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
assign(max_mem, 100000).
assign(pick_given_ratio, 4).

list(usable).
x = x.
end_of_list.

list(sos).

%  Single axiom for BA in terms of Sheffer stroke (weight 185, 8 variables)

(((((x#y)# (x# (z#y)))# (x# (x# ((u#v)# (v#v)))))# ((x# (x# ((x#y)#
(x# (z#y)))))# ((u#v)# (v#v))))# (v# (v# ((w# (v6# (v6# ((w# (v7#
(v7#v7)))# ((v7# (v7#w))#v7)))))# ((v6# (v6#w))# ((w# (v7# (v7#v7)))#
((v7# (v7#w))#v7)))))))# ((v# (v# ((((x#y)# (x# (z#y)))# (x# (x#
((u#v)# (v#v)))))# ((x# (x# ((x#y)# (x# (z#y)))))# ((u#v)# (v#v))))))#
((w# (v6# (v6# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))# ((v6#
(v6#w))# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))=w.

end_of_list.

list(demodulators).

% These 3 demodulators are definitions that are designed to contract
% the single axiom on input.  The important part of the proof, deriving
% G and W17, happens in terms of f1, f2, and p.
% Since they are equational definitions, they don't change the theory.

(x # (y # (y # z))) # ((y # (y # x)) # z) = p(x,y,z). % Pixley-4
(x # z) # (x # (y # z)) = f1(x,y,z).                  % related to Veroff-27a
(y # x) # (x # x) = f2(x,y).                          % related to Meredith-1c

end_of_list.

list(usable).

% This is the denial of the McCune 2-basis.

(X # Z) # (X # (Y # Z)) != X | (Y # X) # (X # X) != X.

end_of_list.
