Substitution Tree Variable Bank Refactor

[joe-hauns]

Before this PR variable banks when querying a substitution tree were hard coded, to be the constants

static constexpr int QUERY_BANK=0;
static constexpr int RESULT_BANK=1;
static constexpr int NORM_RESULT_BANK=3;

This has been replaced in this PR by adding fields _queryBank, _normInternalBank, _internalBank to the SubstutionTree retrieval algorithms RobUnification and UnificationWithAbstraction.

Why do we do this? The reason is that we prepare for the ALASCA merge, which involves a ternary inference. In order to implement that efficiently we need to match one clause with 2 substitution trees in sequence. The is only (soundly) possible if we use different _normInternalBank and _internalBank values for both of the queries. Thus we need to make this change.

As a further preparation for implementing the trinary inference rule we ad an overload getUwa(AbstractingUnifier* state, ...) to LiteralSubstitutionTree and TermSubstitutionTree which differs from the old overload that does not contain the state argument by starting the unification with a already initialized unifier, instead of a fresh one. Using this functoin we can use multiple substitutiontrees in sequence.

As this PR touches some bits of core routines of vampire (i.e. indexing) it would be great if @quickbeam123 could do some regression testing. The changes are not very drastic so I think there shouldn't be a difference in performance but we should be sure anyways. I already did some randomized runs and didn't run into any issues.