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