Added flags in AutomatedProver to permit a number of heuristics to be to...

...ggled on or off.  Added a new step to the automated prover that occasionally prunes out 'obvious' antecedents like 'true' or 'S = S'.