NF distributes conjunctions over K and disjunctions over M.

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.