assign(max_seconds, 60).

assign(new_constants, 1).

assign(eq_defs, fold).

formulas(sos).

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

% Define a new operation (which turns out to be complement).
% The "assign(eq_defs, fold)" above causes this definition to be
% oriented as a rewrite rule so that the operation is introduced
% whenever possible.

  x' = f(x,x).

end_of_list.

formulas(goals).

% Sheffer basis for Boolean Algebra

  f(f(x, x), f(x, x)) = x
  & f(x, f(y, f(y, y))) = f(x, x)
  & f(f(f(y, y), x), f(f(z, z), x)) = f(f(x, f(y, z)), f(x, f(y, z)))
  # answer("Sheffer").

end_of_list.