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

% This is a proof-checking rather than a proof-finding job.
% It uses hints from a previous proof of the same theorem.

set(knuth_bendix).
assign(pick_given_ratio, 4).

assign(max_mem, 200000).
assign(max_weight, 19).

clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).

set(back_unit_deletion).

list(usable).
x = x.
end_of_list.

list(sos).

% Each of the following, along with commutativity, is a basis (Veroff).
% Pick one.  The hints below are good for both.

% (x # y) # (x # (y # z)) = x.  % V-26a
(x # z) # (x # (y # z)) = x.  % V-27a

x # y = y # x.

% Denial of the simple Meredith 2-basis.

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

end_of_list.

assign(bsub_hint_wt, 0).

list(hints).

% These hints are from 2 proofs.

% Hints from proof of V-27a

x# ((x#y)# (z# (x# (u#y))))=x#y.
((x#y)# (z#y))#x=x#y.
(x# (y#z))# (x#z)=x.
(x#y)# ((z#y)#x)=x.
(x#y)# (y# (z#x))=y.
x# ((y#x)# (z# (x# (u#y))))=x#y.
x# ((x#y)# (z# (x# (y#u))))=x#y.
x# ((x#y)# ((x# (z#y))#u))=x#y.
x# ((x#y)#x)=x#y.
x# ((x# (y#z))#z)=x# (y#z).
((x#y)# (z#x))#y=y#x.
((x#y)# (z#y))#z=z#y.
(x# (y#z))# (x#y)=x.
((x#y)#z)# (z#y)=z.
((x# (y#z))#z)#x=x# (y#z).
(Y# (Z#Y))#X!=X# (Y# (X#Z))|$Ans(Meredith_2).
(x# (y#z))# (y#x)=x.
(x# (x#y))#x=x#y.
x# ((x# (y#z))#y)=x# (y#z).
x# (((y#z)#x)#y)=x# (y#z).
x# (((y#z)#x)#z)=x# (y#z).
x# ((x# (y#z))# ((x#y)#u))=x# (y#z).
x# (x# (x#y))=x#y.
(x#x)# (x#y)=x.
x# (y#z)=x# (z#y).
(x#x)# (y#x)=x.
x# (y# (x# (z#y)))=x# (z#y).
((x#y)# (x#z))#y=y#x.
x# (y# (x#y))=x#x.
((x# (y#z))#y)# ((u#z)#y)=y.
x# (y# (y#x))=x#x.
(x#y)#z=z# (y#x).
((x#y)# (x#z))#z=z#x.
x# ((((y#z)#x)#z)# (x# (y#z)))=x#x.
(x# (y#x))#y=y#y.
(x# (x#y))#y=y#y.
x# (y#y)=x# (x#y).
x# (x#y)=x# (y#y).
x# ((((y#z)#x)#z)# ((y#z)#x))=x#x.
((((x#y)#z)#x)# (z# (x#y)))#z=z#z.
x# (y#y)=x# (y#x).
x# (y#x)=x# (y#y).
(x#x)#y=y# (y#x).
x# (x# (y#y))=x#y.
(x#y)#x=x# (y#y).
x# (((y#z)#x)# (z#z))=x#x.
((x#y)#z)# (y#x)= (x#y)# (z#z).
(((x#y)#z)# (x#x))#z=z#z.
(x# (y#x))#z=z# ((y#y)#x).
x# (((y# (y#z))#x)#z)=x#x.
(x#x)# (y#y)= (x#x)# ((x#z)#y).
X# ((Z#Z)#Y)!=X# (Y# (X#Z))|$Ans(Meredith_2).
x# ((x# (y# (y#z)))#z)=x#x.
x# (y#y)=x# (((x#x)#z)#y).
x# (y# (y# ((x#y)#z)))=x#x.
x# (((x#x)#y)#z)=x# (x#z).
x# (y# (y# (z# (y#x))))=x#x.
x# (x# (y# ((x#x)#z)))=x#y.
x# ((y#z)# (y# ((x#x)#u)))=x#y.
x# ((y# (z#x))#z)=x# (x#z).
(x#x)# ((y#z)# (y# (x#u)))= (x#x)#y.
x# ((y# (x# (x#z)))# (z#z))=x#z.
(x#x)# ((y#z)# (y# (u#x)))= (x#x)#y.
x# ((y#y)#z)=x# (z# (x#y)).

% Hints from proof of V-26a

(x# (y#z))# (x#y)=x.
x# ((x#y)#x)=x#y.
x# ((x# (y#z))# ((x#y)#u))=x# (y#z).
x# ((x# (y#z))# (u# (x#y)))=x# (y#z).
x# (x# (x#y))=x#y.
x# ((x# (y#z))# ((x#z)#u))=x# (z#y).
(x# (y#z))# (x#z)=x.
(x# (y#z))# (y#x)=x.
(x#y)# (y# (x#z))=y.
(x# (x#y))#x=x#y.
(x#x)# (x#y)=x.
x# ((x# (y#z))#z)=x# (y#z).
x# ((x# (y#z))#y)=x# (y#z).
((x#y)#z)# (z#y)=z.
x# (y#z)=x# (z#y).
(x#x)# (y#x)=x.
((Z#Y)#Y)#X!=X# (Y# (X#Z)).
x# (((y#z)#x)#z)=x# (y#z).
x# (y# (y#x))=x#x.
x# (y# (x#y))=x#x.
x# (y# (x# (z#y)))=x# (z#y).
((x# (y#z))#z)#x=x# (y#z).
x# (((y#z)#x)#y)=x# (y#z).
(x#y)# (y# (z#x))=y.
(x#y)#z=z# (y#x).
x# (y# (z#u))=x# (y# (u#z)).
(x# (x#y))#y=y#y.
x# ((((y#z)#x)#z)# (x# (y#z)))=x#x.
(x# (y#x))#y=y#y.
x# (y#y)=x# (x#y).
x# (x#y)=x# (y#y).
((x#y)# (z#y))#x=x#y.
(x# (y#z))#u=u# ((z#y)#x).
(x#x)#y=y# (y#x).
x# ((((y#z)#x)#z)# ((y#z)#x))=x#x.
((((x#y)#z)#x)# (z# (x#y)))#z=z#z.
x# (y#y)=x# (y#x).
x# (y#x)=x# (y#y).
x# (x# (y#y))=x#y.
(x#y)#x=x# (y#y).
x# (((y#z)#x)# (z#z))=x#x.
((x#y)#z)# (y#x)= (x#y)# (z#z).
(((x#y)#z)# (x#x))#z=z#z.
((x#y)# (z#y))#z=z#y.
(x#y)#y=y# (x#x).
(Y# (Z#Z))#X!=X# (Y# (X#Z)).
x# (((y# (y#z))#x)#z)=x#x.
(x#x)# (y#y)= (x#x)# ((x#z)#y).
((x# (y#z))#y)# ((u#z)#y)=y.
x# ((x# (y# (y#z)))#z)=x#x.
x# (y#y)=x# (((x#x)#z)#y).
x# (y# (y# (z# (x#y))))=x#x.
x# (((x#x)#y)#z)=x# (x#z).
x# (x# (y# ((x#x)#z)))=x#y.
x# ((y# (z#x))#z)=x# (x#z).
x# ((y# (x# (x#z)))# (z#z))=x#z.
((x#y)# (x#z))#z=x#z.
x# ((y#z)# (y# ((x#x)#u)))=x#y.
(x#x)# ((y#z)# (y# (x#u)))= (x#x)#y.
X# ((Z#Z)#Y)!=X# (Y# (X#Z)).
x# ((y#y)#z)=x# (z# (y#x)).
X# (Y# (Z#X))!=X# (Y# (X#Z)).

end_of_list.