set(auto).

assign(max_weight, 50).
  
list(usable).

x = x.

f(f(f(y, f(x, y)), y), f(x, f(z, y))) = x.  % Sh_2

f(f(X, f(f(Y, X), X)), f(Y, f(Z, X))) != Y.  % Denial of Sh_1

end_of_list.