In normalization, remove from premises the atoms known to be true even without unification.
Quantifier checking bug fix: only for assignment to a [bvs] variable assume that it will land in solution for predicate variable.
Move short premise branches to the front; but do not sort branches since the original order is otherwise good.