Previously this was done in Solver during the semantic reduction of
formulas. It appears to be much cleaner as an (optional) preprocessing
step in the normalization.

KnowledgeBase::Entails() has a Boolean `distribute' parameter to control
the setting.
In the TUI this step can be disabled with "Call: disable_distribute()",
which is, for instance, important for the QBF reduction.