Fix in term abduction: sort initial candidates in increasing size. `cleanup` moved from `Abduction` to `Terms`. More aggressive simplification of invariants: allow elimination of parameters found in previous iterations.