Expanded the flexibility of the SubstituteInPlaceInAntecedent transformation to handle an 'and' on either side of the substitution more gracefully.  Added a timeout to the prover.  Added a preliminary ExistentialInstantiation transformation.