Improvements to equality inference module: add missing cases for solvable variables...

Improvements to equality inference module: add missing cases for solvable variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations.  Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort.