above, we use the following definitions.

A prenex formula is said to be separable if it can be split into two or more clauses. Separability is a property of the prenex formula. Separability may result in the loss of structure in a given prenex formula. By this we mean that the interdependencies among the formula’s constituent polynomials might be lost, resulting in wasteful and redundant computations, which would not have been required if the formula was not separated. We need a formal, quantitative definition of ‘structure’ with respect to a given formula to study it’s effects on the running time of the proposed algorithm.

The ‘sharing factor’ existing among two given prenex formulae, $f$ and $g$, is the number of variables that are shared between $f$ and $g$. It’s denoted by $T_{f,g}$.

The sharing factor essentially captures the distribution of variables among the constituent polynomials of a prenex formula. If formulae $f$ and $g$ have $k$ variables in common, it implies that $f$ imposes conditions on $g$ in $k$ dimensions. The sharing factor gives a measure of structure present in a formula, as the sharing of variables between polynomials causes interdependencies among them. Having defined the sharing factor, we now 