assign(max_seconds, 120).

set(lex_order_vars).
set(restrict_denials).
assign(new_constants, 1).

formulas(sos).

% Veroff's 2-basis for BA in terms of the Sheffer stroke.

f(x,y) = f(y,x)           # label(commutativity).
f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2).

end_of_list.

formulas(goals).

% Previously known BA Sheffer 3-basis.

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.

