Eliminate a level of nesting of traversals in theory preprocessing (#7345)

Eliminate a level of nesting of traversals in theory preprocessing (#7345)

This simplifies the theory preprocessor so that it does not rely on the term formula removal to do a nested traversal. Instead, it only relies on its "runCurrent" method.

Notice that this PR essentially replaces TheoryPreprocessor's theoryPreprocess method with TermFormulaRemoval's runInternal method, while adding the required call to rewriteWithProof and preprocessWithProof as post-rewrites. This is far simpler than the previous method, which invoked nested traversals using TermFormulaRemoval::run.

There are two things that will be improved in follow up PRs:

The initial full rewrite step in the theory preprocessor can be merged into the main traversal of theory preprocess (I believe this is why we are slower on nec benchmark than we were previously),
We should eliminate the traversal methods from TermFormulaRemoval altogether, as they are now subsumed by the theory preprocessors main traversal. This will require refactoring how "early ITE removal" works, as this is the only user now of TermFormulaRemoval::run.
Note we should probably performance test this change.

This incidentally fixes #6973, as the previous theory preprocessing code was to blame for that issue.