motivated by the notion of clause normal forms and virtual substitutions.

Virtual substitutions would be performed prior to clause normal form computation, as substitutions might result in an increase in the number of clauses.

The clause normal form has been chosen as the preferred format for computational efficiency. The fact that any given prenex formula can be converted to a clause normal form enables us to perform the experimental evaluation on test cases containing solely of clause normal forms.

We now list the proposed algorithm.

1.  Compute the negation normal form of $f$ and call it $f'$.

2.  Perform virtual substitutions after identifying substitutors and substituends and call the resulting formula, $f''$.

3.  Compute the clause normal form of $f''$ and call it $f'''$.

4.  Call an instance of CAD for each clause in $f'''$, with each instance being an independent thread of execution.

5.  Concatenate the outputs of the $k$ instances of CAD using boolean conjunction.

Structural Notions of the Prenex Formulae and the Preprocessor
==============================================================

The introduction of CNF computation introduces the notion of partitioning the space of all prenex formulae into classes, depending on how many clauses it could be separated into. To interpret the results presented 