  The Cylindrical Algebraic Decomposition (CAD) algorithm is a comprehensive
tool to perform quantifier elimination over real closed fields. CAD has doubly
exponential running time, making it infeasible for practical purposes. We
propose to use the notions of clause normal forms and virtual substitutions to
develop a preprocessor for CAD, that will enable an input-level parallelism. We
study the performance of CAD in the presence of the preprocessor by extensive
experimentation. Since parallelizability of CAD depends on the structure of
given prenex formula, we introduce some structural notions to study the
performance of CAD with the proposed preprocessor.
