decision engine: cache start index for and/or nodes

This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.

This was triggerred by a benchmark sent by andy/viktor.

performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex
Merge remote-tracking branch 'upstream/master' into sets
Minor optimizations to datatypes, revert to checkClash not mod eq.  Minor clean up.
More minor optimizations for datatypes.
Add option --dt-stc-ind for strengthening skolemization.  Refactor skolemization.
Fix assertion from previous commit.
Simplification of EqualityEngine::areDisequal.  Comparison for production : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5.  Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.
Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.
Valuation::entailmentCheck() proxy for TheoryEngine version.  Signature and contract is the same as for TheoryEngine version.