assign(new_constants, 1).

clauses(sos).

% These four equations are a basis for Boolean algebra (BA)

x v (y v z) = y v (x v z)  # label(AJ).
x ^ y = c(c(x) v c(y))     # label(DM).
x v c(x) = y v c(y)        # label(ONE).
(x v c(y)) ^ (x v y) = x   # label(CUT).

end_of_list.

clauses(goals).

c(c(x)) = x                            # answer(CC).
x v (x ^ y) = x                        # answer(B1).
x ^ (y v z) = (x ^ y) v (x ^ z)        # answer(DIST1).
x v (y ^ (x v z)) = x v (z ^ (x v y))  # answer(MOD).

end_of_list.