Merge branches with the same premise in `simplify`.
Pass alien subterms to numerical abduction. Use them as `paramvs` in variable comparison and quantifier violation test.