In `Invariants.simplify`, eliminate the later introduced variables rather than earlier ones, to faciliate convergence.
Upgraded abduction tests.
Fixed answer splitting.