op(400,xfx,+).
op(300,yf,@).

set(hyper_res).
set(para_into).
set(para_from).
set(order_eq).

assign(bsub_hint_add_wt,-1000).
set(keep_hint_subsumers).
assign(max_weight,0).

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

list(usable).
x = x.

% Denial of the Robbins basis.

B + A != A + B
	| (A + B) + C != A + (B + C)
	| ((A + B) @ + (A @ + B) @) @ != B
	| $Ans(Robbins_basis).
end_of_list.

list(sos).
(((x + y) @ + z) @ + (x + (z @ + (z + u) @) @) @) @ = z.
end_of_list.

% This list of hints guides Otter directly to a particular (short) proof.

list(hints).
((x+y)@ + (((z+u)@ +x)@ + (y@ + (y+v)@ )@ )@ )@ =y.
((x+y)@ + ((z+x)@ + (y@ + (y+u)@ )@ )@ )@ =y.
((x+x@ )@ +x)@ =x@ .
((x+y)@ + ((z+x)@ + (((y+y@ )@ +y)@ + (y+u)@ )@ )@ )@ =y.
((x+y)@ + ((z+x)@ +y)@ )@ =y.
((x+y)@ + (x@ +y)@ )@ =y.
(((x+y)@ +x)@ + (x+y)@ )@ =x.
(x+ ((x+y)@ +x)@ )@ = (x+y)@ .
(((x+y)@ +z)@ + (x+z)@ )@ =z.
(x+ ((y+z)@ + (y+x)@ )@ )@ = (y+x)@ .
((((x+y)@ +z)@ + (x@ +y)@ )@ +y)@ = (x@ +y)@ .
(x+ ((y+z)@ + (z+x)@ )@ )@ = (z+x)@ .
((x+y)@ + ((z+x)@ + (y@ + (u+y)@ )@ )@ )@ =y.
(x+y)@ = (y+x)@ .
(((x+y)@ + (y+z)@ )@ +z)@ = (y+z)@ .
((x+ ((x+y)@ +z)@ )@ +z)@ = ((x+y)@ +z)@ .
(((x+y)@ +x)@ +y)@ = (y+y)@ .
(x@ + (y+x)@ )@ =x.
((x+y)@ +y@ )@ =y.
(x+ (y+x@ )@ )@ =x@ .
(x+x)@ =x@ .
(((x+y)@ +x)@ +y)@ =y@ .
x@ @ =x.
((x+y)@ +x)@ +y=y@ @ .
(x+y)@ @ =y+x.
x+ ((y+z)@ + (y+x)@ )@ = (y+x)@ @ .
x+y=y+x.
((x+y)@ +x)@ +y=y.
((x+y)@ +y)@ +x=x.
x+ ((y+x)@ +y)@ =x.
(x+y@ )@ + (y@ +y)@ = (x+y@ )@ .
(x+y)@ + (y+y@ )@ = (x+y)@ .
(x+y)@ + (y@ +y)@ = (x+y)@ .
((x+y@ )@ @ +y)@ = (y@ +y)@ .
((x+y@ )+y)@ = (y@ +y)@ .
((((x+y@ )+z)@ +y)@ + (y@ +y)@ )@ =y.
x+ ((y+z)@ + (y+x)@ )@ =y+x.
x+ (y+ ((z+y)@ +x)@ )@ = (z+y)@ +x.
x+ ((y+x)@ + (y+z)@ )@ =y+x.
((x+y)@ + ((x+y)@ + (x+z)@ )@ )@ +y=y.
(((x+y@ )+z)@ +y)@ @ =y.
x+ ((y+x@ )+z)@ =x.
x@ + ((y+x)+z)@ =x@ .
(x+y)@ +x=x+y@ .
(x+ (x+y@ )@ )@ = (x+y)@ .
((x+y)@ + (x+z))@ +y=y.
(((x+y)@ +z)@ + (x@ +y)@ )@ +y= (x@ +y)@ @ .
(((x+y)@ +z)@ + (x@ +y)@ )@ +y=x@ +y.
(x@ + ((y+x)@ @ + (y+z))@ )@ + (y+z)= (y+x)@ @ + (y+z).
(x@ + ((y+x)+ (y+z))@ )@ + (y+z)= (y+x)@ @ + (y+z).
(x@ + ((y+x)+ (y+z))@ )@ + (y+z)= (y+x)+ (y+z).
x@ @ + (y+z)= (y+x)+ (y+z).
(x+y)+ (x+z)=y+ (x+z).
(x+y)+ (x+z)=z+ (x+y).
x+ (y+z)=z+ (y+x).
x+ (y+z)=y+ (z+x).
(x+y)+z=x+ (y+z).
end_of_list.