New module for generating candidate equality conjectures used in inductive proofs...

New module for generating candidate equality conjectures used in inductive proofs.  Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness.  Refactoring of term database.  QcfEngine now uses central data structure for term indexing.  Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).