Bug fix: disjunction elimination of equal terms.
Disjuncts of an existential type can come from the same branch but distinct connected components -- fix: find connected components before sending to disjunction elimination.
Abduction: more logging. Invariants: more tests. NumS: drop repeating atoms at the end of simplification.