assign(new_constants, 1).

formulas(sos).

f(f(x, f(f(y, x), x)), f(y, f(z, x))) = y # label(Sh_1).

% Denial of the Sheffer basis.

f(f(a, a), f(a, a)) != a
	| f(a, f(b, f(b, b))) != f(a, a)
	| f(f(f(b, b), a), f(f(c, c), a)) != f(f(a, f(b, c)), f(a, f(b, c)))
	# answer("Sheffer").

end_of_list.