% Sh_1 takes less than 1 second.
% Sh_2 takes about 30 seconds.

set(auto).

list(usable).
x = x.
f(f(x, f(f(y, x), x)), f(y, f(z, x))) = y.  % Sh_1
% f(f(f(y, f(x, y)), y), f(x, f(z, y))) = x.  % Sh_2
f(a,b) != f(b,a).
end_of_list.