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

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

assign(max_weight, 110).
assign(change_limit_after, 10).
assign(new_max_weight, 17).

assign(neg_weight, -100).

list(usable).
x = x.
end_of_list.

list(sos).

% Single axiom for BA (weight 111, 6 variables)

(((x * x@) + ((x * y) + (x@ * y))) * ((((z + (u + v)@)@ + (z + v)@ )@
* w@) + ((((z + (u + v)@)@ + (z + v)@)@ * z) + (w@ * z)))@) + ((((x *
x@) + ((x * y) + (x@ * y))) * z) + (((((z + (u + v)@)@ + (z + v)@)@ *
w@) + ((((z + (u + v)@)@ + (z + v)@)@ * z) + (w@ * z)))@ * z)) = y.

(A + B) + C != A + (B + C) | A + B != B + A | ((A + B)@ + (A + B@)@)@ != A | (A@ + B@)@ != A * B | $Ans(Robbins_plus_and).

end_of_list.

% Note that the following is pick-given weight, not pick-and-purge;
% therefore, even though all given clauses will match a hint and
% get pick-given weight 0, we cannot set max_weight to 0, because
% this does not affect the purge-gen weight.

assign(bsub_hint_wt, 0).

% These hints come from previous proofs.  They were derived by iteration,
% until all given clauses have weight 0.

list(hints).

(((x*x@ )+ ((x*y)+ (x@ *y)))* ((((z+ (u+v)@ )@ + (z+v)@ )@ *w@ )+ ((((z+ (u+v)@ )@ + (z+v)@ )@ *z)+ (w@ *z)))@ )+ ((((x*x@ )+ ((x*y)+ (x@ *y)))*z)+ (((((z+ (u+v)@ )@ + (z+v)@ )@ *w@ )+ ((((z+ (u+v)@ )@ + (z+v)@ )@ *z)+ (w@ *z)))@ *z))=y.
(x* ((((y+ (z+u)@ )@ + (y+u)@ )@ *v@ )+ ((((y+ (z+u)@ )@ + (y+u)@ )@ *y)+ (v@ *y)))@ )+ ((x*y)+ (((((y+ (z+u)@ )@ + (y+u)@ )@ *v@ )+ ((((y+ (z+u)@ )@ + (y+u)@ )@ *y)+ (v@ *y)))@ *y))=x.
(x*x@ )+ ((x*y)+ (x@ *y))=y.
(x* ((y+ (z+u)@ )@ + (y+u)@ )@ @ )+ ((x*y)+ (((y+ (z+u)@ )@ + (y+u)@ )@ @ *y))=x.
(((x+ (y+z)@ )@ + (x+z)@ )@ *u@ )+ ((((x+ (y+z)@ )@ + (x+z)@ )@ *x)+ (u@ *x))=x.
(x*y@ )+ ((x*y)+ (y@ *y))=x.
((x+ (y+z)@ )@ + (x+z)@ )@ =x.
(x*y@ )+ ((x*x)+ (y@ *x))=x.
((x+y@ )@ + (x+ ((y*z)+ (z@ *z)))@ )@ =x.
((x+y@ )@ + (x+ ((z*y)+ (z@ *y)))@ )@ =x.
((x+y)@ + (x+ (y+z)@ )@ )@ =x.
(x+ ((x+ (y+z)@ )@ +z)@ )@ = (x+ (y+z)@ )@ .
(((x*x@ )+ (y+ ((x*z)+ (x@ *z)))@ )@ +z@ )@ =x*x@ .
(((x+ (y+z)@ )@ + (u+ (x+z)@ )@ )@ +x)@ = (x+ (y+z)@ )@ .
(x*y)+ ((x* ((y+ (z+u)@ )@ + (y+u)@ ))+ (y* ((y+ (z+u)@ )@ + (y+u)@ )))=x.
(((x+ (y+z)@ )@ + (x+z)@ )*x)+ ((((x+ (y+z)@ )@ + (x+z)@ )*u)+ (x*u))=u.
(x*y)+ ((x*x)+ (y*x))=x.
(((x*x@ )+y@ )@ +y@ )@ =x*x@ .
((x+ (y*y@ ))@ + (x+z@ )@ )@ =x.
((x+ (y+z)@ )@ + (x+y)@ )@ =x.
(((x+y)@ +x)@ +x)@ = (x+y)@ .
(x@ + (y+z)@ )@ + (x@ +z)@ =x.
((x+ (y*z))@ + (x+y@ )@ )@ =x.
(((x*x@ )+y)@ +y)@ =x*x@ .
((x+ (y*y@ ))@ + (x+z)@ )@ =x.
((x+y@ )@ + (x+ (y*z))@ )@ =x.
(x+ ((x+y)@ +x)@ )@ = (x+y)@ .
(x+ ((x+y)@ +y)@ )@ = (x+x)@ .
((x+y)@ +x)@ +x=x+y.
x+ ((x+y)@ + (y+z)@ )@ =x+y.
(x@ + ((y*x)+ (y@ *x)))@ =y*y@ .
((x*y)+ (x@ + (x*y))@ )@ =x@ .
((x*x@ )+ (y@ + (x*x@ ))@ )@ =y@ .
(x@ +y)@ + (x@ +x@ )@ =x.
((x+y)@ + (x+x)@ )@ =x.
x+ ((x+y)@ +x)@ =x+y.
(x@ +x@ )@ + (x@ +y)@ =x.
((x+x)@ + (x+y)@ )@ =x.
x+ ((x+y)@ +y)@ =x+x.
(x@ + ((x*y)+x@ )@ )@ =x*y.
(x@ + ((x*y)+ (x*y))@ )@ =x*y.
((x*x@ )+ (y+ (x*x@ ))@ )@ =y.
(x*x@ )+ (y@ +y@ )@ =y.
x+x=x+ (y*y@ ).
x+ (y*y@ )=x+x.
(x+x)@ = (x+ (y*y@ ))@ .
((x+x)@ +y)@ +x=x+x.
(x+ (y+ (x+x)@ )@ )@ = (x+x)@ .
x+ ((x+x)@ +y)@ =x+x.
(x@ +x@ )@ + (x*y)=x.
(x*y)+ (x@ +x@ )@ =x.
(x+ (x+ (y*y@ ))@ )@ =y*y@ .
((x+y)@ + (x+ (z*z@ ))@ )@ =x.
(x*x@ )+y=y+y.
(x*x@ )+y=y+ (z*z@ ).
x+x= (y*y@ )+x.
x+ (y*y@ )=x+ (z*z@ ).
x*x@ =y*y@ .
(x@ + ((x*y)+ (z*z@ ))@ )@ =x*y.
((x+x)@ + (y*y@ ))@ =x.
((x*x@ )+ (y+y)@ )@ =y.
((x+ (y*y@ ))@ +z)@ +x=x+x.
((x+x)*y)+x=x+x.
(((x*y)+ (x@ *y))+y@ )@ =x*x@ .
((x+x)@ + (y+x)@ )@ =x.
((x+ (y*y@ ))@ + (z+x)@ )@ =x.
x+ (y+ (x+x)@ )@ =x+x.
x+ ((x+x)*y)=x+x.
(x+ (x+x)@ )@ =y*y@ .
x*x@ = (y+ (y+y)@ )@ .
((x+x)@ +x)@ =y*y@ .
((x*y)+ (x@ *y))+ (z*z@ )=y.
(x*x@ )+y= (z*z@ )+y.
(x@ + ((y*y@ )+ (x*z))@ )@ =x*z.
(x*y)+ ((z*z@ )+x@ )@ =x.
((x*x@ )+y@ )@ + (y@ +z)@ =y.
(((x*x@ )+y)@ + (y+z)@ )@ =y.
((x+y)@ + ((z*z@ )+x)@ )@ =x.
((x+x)@ + (y*y@ ))*x=z*z@ .
x+ (((y*y@ )+ (z+z)@ )*z)=x+x.
(((x*x@ )+ (y+y)@ )*y)+z=z+z.
x+x=x+ (((y*y@ )+ (z+z)@ )*z).
x+x= (((y*y@ )+ (z+z)@ )*z)+x.
(((x*x@ )+y)*z)+y=y+y.
((x*x@ )+y@ )@ = (x*y)+ (x@ *y).
(x@ + (y*y@ ))@ = (y*x)+ (y@ *x).
((x*y)+ (x@ *y))+ (y@ +z)@ =y.
(x*y)+ ((z*x)+ (z@ *x))=x.
(x* (y+y))+ (x@ * (y+y))=y.
(((x*x@ )+y)@ + (z+y)@ )@ =y.
((x+y)@ + (x+ (z+y)@ )@ )@ =x.
((x*x@ )+ (y*y@ ))*z=x*x@ .
x+ ((y*y@ )+x)@ =x+ (x+x)@ .
x+ (x+x)@ =x+ ((y*y@ )+x)@ .
x+ (y+ (y+y)@ )@ =x+x.
(x+ (x+x)@ )@ +y=y+y.
(x@ +x@ )@ + (y+ (y+y)@ )@ =x.
(x+ (x+x)@ )@ +y=y+ (z*z@ ).
x+x=x+ (y+ (y+y)@ )@ .
x+x= (y+ (y+y)@ )@ +x.
x+ (y*y@ )= (z+ (z+z)@ )@ +x.
(x*y)+ (x@ *y)= (y@ +y@ )@ .
(x+ (x+x)@ )@ +y= (z*z@ )+y.
(((x*x@ )+ (y*z))@ +y@ )@ =y*z.
(((x+ (x+x)@ )@ +y)*z)+y=y+y.
((x*x)+ (x*x))+ (x@ +y)@ =x.
(x*y)+ ((z*z@ )+ (x*x))=x.
(x*x@ )+ ((y+y)* (y+y))=y.
x+ ((x+y)@ + (z+y)@ )@ =x+y.
(x@ +x@ )@ = (x*x)+ (x*x).
(x*y)+ (x@ *y)= (y*y)+ (y*y).
((x*x)+ (x*x))+ (y+ (y+y)@ )@ =x.
(x*x@ )+ (x*x@ )=x*x@ .
(x*x@ )*y=x*x@ .
(x*x@ )+ (y*y@ )=y*y@ .
(x+ (x+x)@ )@ + ((y+y)* (y+y))=y.
(x*x@ )+ ((y+y)* ((z*z@ )+y))=y.
(x*x)+ (x*x)= (x+x)* (x+x).
((x+x)+ (x+x))* ((x+x)+ (x+x))=x.
(x+x@ )@ =y*y@ .
(x@ +x)@ =y*y@ .
((x+x)* (x+x))+ (y+ (y+y)@ )@ =x.
(x*y)+ (x@ *y)= (y+y)* (y+y).
(x@ +x@ )@ = (x+x)* (x+x).
((x+x)* (x+x))+ (x@ +y)@ =x.
x*x@ = (y+y@ )@ .
(x@ + (y*y@ ))@ = (x+x)* (x+x).
((x*x@ )+y@ )@ = (y+y)* (y+y).
(x+ (x+x)@ )@ *y=z*z@ .
x*x@ = (y+ (y+y)@ )@ *z.
(x+ (x+x)@ )@ + (y*y@ )=y*y@ .
(x+x)+ (x+x)= (x+x)+x.
(x+x)+x=x+ (x+x).
(x+ (x+x))* (x+ (x+x))=x.
(x+x)+ (x+x)=x+ (x+x).
x+ ((y*y@ )+x)@ =x+x@ .
((x*x@ )+y)@ +y=y+y@ .
x+ (x+x)@ =x+x@ .
(x+x@ )@ + (y*y@ )=y*y@ .
x*x@ = (y+y@ )@ *z.
((x+x)* (x+x))+ (y+y@ )@ =x.
(x+x@ )@ + ((y+y)* (y+y))=y.
(((x+x@ )@ +y)*z)+y=y+y.
(x+x@ )@ +y= (z*z@ )+y.
x+ (y*y@ )= (z+z@ )@ +x.
x+x= (y+y@ )@ +x.
x+x=x+ (y+y@ )@ .
(x+x@ )@ +y=y+ (z*z@ ).
(x+x@ )@ +y=y+y.
x@ +x= ((x+x)* (x+x))+x@ .
((x+y)@ + ((z+z@ )@ +x)@ )@ =x.
((x+y)@ + (x+ (z+z@ )@ )@ )@ =x.
(x+x@ )@ + ((y*y@ )+ (z*z))=z.
(((x+x@ )@ +y)@ + (y+z)@ )@ =y.
(x@ + (y+y@ )@ )@ = (x+x)* (x+x).
((x+x@ )@ +y@ )@ = (y+y)* (y+y).
x@ +x@ @ =x@ + ((x+x)* (x+x)).
(x*x@ )@ + (y+y@ )@ =y+y@ .
(x+x@ )@ *y= (z+z@ )@ *u.
(x+x@ )@ + (x+x@ )@ = (x+x@ )@ .
(x@ + (y+y@ )@ @ )@ = (y+y@ )@ .
(x+x@ )@ + (y+y@ )@ = (x+x@ )@ .
x+ (y+y@ )@ = (z+z@ )@ +x.
(x+x@ )@ +y=y+ (z+z@ )@ .
(((x+x@ )@ +y)@ +z)@ +y=y+y.
(x+ ((y+y@ )@ +x))* (x+ (x+x))=x.
((x+x@ )@ +y)+y=y+ (y+y).
(x*x)+ (y+y@ )@ = (x+x)* (x+x).
(x*x@ )+ (y+y@ )=y+y@ .
(x+x@ )+ (x+x@ )=x+x@ .
(x+x@ )* (x+x@ )=x+x@ .
(x+ (y+y@ )@ @ )@ = (y+y@ )@ .
(x+ (y+x@ )@ )@ = (x+x)@ .
(x+x@ )@ + ((y+y@ )@ + (z*z))=z.
(x*x@ )@ =y+y@ .
(x+x@ )@ @ + (y+y@ )@ =y+y@ .
x+ (y+y@ )=y+y@ .
(x+x@ )* (y+y@ )=y+y@ .
x+ (y+y@ )@ @ =y+y@ .
((x+y)+ (x+y))@ = ((x+y)+x)@ .
((x+y)+y)@ = ((x+y)+x)@ .
x+ (y+x@ )@ =x+x.
(((x+x)* (x+x))+ (y*x))@ =x@ .
(x+y)+ (x+y)= (x+y)+x.
(x+y)+x= (x+y)+y.
(x+y)+y= (x+y)+x.
x+ (((x+y)+x)* ((x+y)+x))=x+y.
((x+x)* (x+x))+ (y*x)=x.
(x+x@ )@ + (y+z)= (y+z)+y.
(x+y)+x= (z+z@ )@ + (x+y).
(x*y)+ (y*y)= (y+y)* (y+y).
x+ (((x+y)+x)* ((x+y)+y))=x+y.
(x*x@ )+ (y* (z*z@ ))=z*z@ .
x+ (y*x)=x+x.
(x+y)+y= (z+z@ )@ + (x+y).
(x+x@ )@ + (y+z)= (y+z)+z.
x+ (((x+y)+y)* ((x+y)+y))=x+y.
x* (y+y@ )@ = (y+y@ )@ .
x* (y*y@ )=y*y@ .
(x* (y*y@ )@ )+ (y*y@ )=x.
(x* (y+y@ ))+ (z*z@ )=x.
(x* (y+y@ ))+ ((z+z@ )@ *u)=x.
((x+y@ )@ + (x+y)@ )@ =x.
(x+x@ )@ +y=y.
(x+x@ )@ +y=y.
(x+y)+y=x+y.
x*x=x.
x+ (x+x)=x+x.
x+x=x.
(x@ +y)@ +x=x.
x+ (y+y@ )@ =x.
x@ @ =x.
(x@ + (x+y)@ )@ =x.
(x*x@ )+y=y.
x+ (y*y@ )=x.
(x*y)+x=x.
x+ (x+y)=x+y.
(x*y)+y=y.
(x*y)+ (x@ *y)=y.
x+ (y+x@ )@ =x.
(x@ *x)+y=y.
x+ (y@ *y)=x.
(x@ + (x*y)@ )@ =x*y.
(x*y@ )+ (x*y)=x.
(((x+y@ )@ +y)@ +x)@ = (x+y@ )@ .
((x+y)@ + (x+y@ )@ )@ =x.
(x+y)+ (z+y@ )@ =x+y.
(x@ *y)+ (x*y)=y.
(x*y)+ (x*y@ )=x.
(x+y@ )@ + (x+y)@ =x@ .
(x+y)@ + (x+ (z+y)@ )@ =x@ .
(x+y@ )@ + (x+ (y*z))@ =x@ .
(x+y)@ +x@ =x@ .
x@ + (x+y)@ =x@ .
x@ + (y+x)@ =x@ .
(x+ (x@ *y)@ )@ =x@ *y.
(((x+y)@ +y@ )@ +x)@ = (x+y)@ .
((x+y@ )@ +y)@ +x=x+y@ .
(x@ + ((y*x)+x@ )@ )@ =y*x.
(((x*y@ )+y)@ +y)@ =x*y@ .
(x+ (y+z))+z=x+ (y+z).
(x+ (y+z))+y=x+ (y+z).
(x*y)+ (x@ + ((x*y@ )+z)@ )@ =x.
x+ ((x+y@ )@ + (x+y))@ =x+y@ .
((x+y@ )@ + (x+y))@ +x=x+y@ .
((x+y)@ + (z+y)@ )@ +x=x+y.
(x*y)@ =x@ +y@ .
(x+y@ )@ =x@ *y.
((x+y)* (z+y))+x=x+y.
((x@ *y)+ (x+y))@ +x=x+y@ .
x+ ((x@ *y)+ (x+y))@ =x+y@ .
(x*y)+ (x* ((x*y@ )+z))=x.
(x@ + ((y@ +x@ )*x))@ =y*x.
x@ +y=y+x@ .
(((x+y)*y)+x)@ = (x+y)@ .
((x*y@ )+y)@ +y=x@ +y.
(x@ +y)@ =x*y@ .
x* ((y*x)+x@ )=y*x.
(x+y)+ (z*y)=x+y.
(x+y)+ (y*z)=x+y.
(x+y)@ =x@ *y@ .
x* (y+x)=x.
x* (x+y)=x.
(x+y)*x=x.
x@ *y@ =y@ *x@ .
x+ ((x+y@ )* (x@ *y@ ))=x+y@ .
((x+y@ )* (x@ *y@ ))+x=x+y@ .
x+y=y+x.
x@ * ((y*x@ )+x)=y*x@ .
(x+y)+ (x*z)=x+y.
(x*y)* (z+y)=x*y.
(x*y)*x=x*y.
(x* (y+x@ ))+x@ =y+x@ .
(x+y)* (x+ (x@ *y@ ))=x.
x+ (x@ * (x+y))=x+y.
x* (y*x)=y*x.
x*y@ =y@ *x.
x+ ((x+y)* (x@ *y))=x+y.
(x*y@ )+ ((x@ +y)*y@ )=y@ .
((x+y)* (x@ *y))+x=x+y.
(x*y)+ (z+y)=z+y.
x+ (y+z)=x+ (z+y).
((x*y@ )+y)*y@ =x*y@ .
(x*y)+ (x+z)=x+z.
x* ((x*y)+x@ )=x*y.
(x+y)* ((x@ *y@ )+x)=x.
(x+ (x@ *y@ ))* (x+y)=x.
(x+y)* (z*y)=z*y.
(x@ *y)+x=x+y.
x+ (x@ *y)=x+y.
(x+y)* (x+y@ )=x.
(x+y@ )* (x+y)=x.
x*y=y*x.
(x*y)+ (x* (z+y@ ))=x.
(x+y)+z=z+ (y+x).
x+ (y+z)= (z+y)+x.
((x*y)+y@ )*y=x*y.
x* (x@ + (x*y))=x*y.
x@ + (x*y)=x@ +y.
x* (x@ +y)=x*y.
x* (y+x@ )=y*x.
(x*y)+y@ =x+y@ .
(x+y@ )*y=x*y.
(x@ +y)* (y+x)=y.
(x+y)*x@ =y*x@ .
x+ (y*x@ )=x+y.
(x*y@ )+ (x* (z+y))=x.
(x@ +y)* (x+y)=y.
(x* (y+z))* (x@ +z)=x*z.
(x* (y+z))*z=x*z.
(x+ (y@ *z@ ))*z=x*z.
(x+ (y*z@ ))*z=x*z.
x+ (y+ (z*x))=x+y.
(x+y)+ (z+y)= (x+y)+z.
(x+y)+ (z+x)= (x+y)+z.
(x+y)+z= (z+x)+y.
(x+y)+z=x+ (y+z).

end_of_list.