assign(new_constants, 1).

% pick given ratio:

assign(age_part, 1).            % by age
assign(false_part, 4).          % by "false in some interp"
assign(true_part, 1).           % by "true in all interps"

assign(max_minutes, 10).

clauses(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).

% Denial of previously known BA Sheffer 3-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.