introduce skolem functors of high exponents, but the doubly exponential running time of CAD enables us to cope with them in practice, due to a reduction in the number of variables (brought about by skolemization).

CNFs are used to impose a structure on the input prenex formulae, that will make computation easier. But, a well-crafted transformation on a prenex formula may result in a form which performs better than the CNF case. But, such well-crafted transformations usually require a great amount of computational power (and possibly non-determinism) to achieve in practical scenarios. Thus, the CNF has been used to give a measure of speed-up that can be achieved in an average case, as the CNF can be obtained using a deterministic algorithm, which terminates for any input.

Using Virtual Substitutions
---------------------------

The CAD algorithm benefits from substitutions, which might reduce the number of variables in some clauses, prior to the separation phase. This may decrease the dependence of one clause on another. But substitutions can be non-trivial and in many cases, impossible. Substitutions can be used with linear and quadratic equations and inequalities directly. For cubic and quartic polynomials, substitutions can be used only if it is obtained easily. Newton 