assign(max_seconds, 30).

assign(new_constants, 1).

formulas(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 = (x' v y')'         # label(DM).
x v x' = y v y'            # label(ONE).
(x v y') ^ (x v y) = x     # label(CUT).

end_of_list.

formulas(goals).

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.
