Added support for proof production in Equality Engine.  Cleaned up existing proof signatures and added proof signature for theory of arrays.  Added new MBQI technique based on interval abstraction.  Cleaned up option names.  Improved symmetry breaking for uf strong solver.  Other minor cleanup.
proof cleanup
more proof cleanup
some work on proof-production
integration
break stats reg