Fixed: split_order_matters optimisation in Solver::Split was unsound.

The split order does matter in general. We use this in the QBF
reduction.

Incidentally, formulas (in particular, conjunctions) must not be
normalised for the QBF reduction to work. Toggling normalisation is a
feature planned in the near future (the normalisation must be moved out
of Solver first).