assign(max_seconds, 1800). assign(new_constants, 1). formulas(sos). f(f(x, f(f(y, x), x)), f(y, f(z, x))) = y # label(Sh_1). 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.