containing more than one clause. A CNF is a conjunctive normal form with universally quantified variables. Hence, 100 prenex formulae were randomly generated, which do not conform to the normal form defined previously. They were subjected to a logic converter, which converts them to a minimal conjunctive normal form. We have observed the following from the plot in Fig. 5: only 8% of the formulae were 1-separable. Hence, in 92% of the cases, the algorithm would lead to a parallel execution of CAD.\

![image](prenexdist.jpg)\

On the Performance of CAD with the Proposed Preprocessor
--------------------------------------------------------

With the above two analyses in place, the next step is to experimentally compare the running times of an implementation of CAD algorithm with and without the preprocessor. The analysis is done for 2,3 and 4 variable cases. In each case, the prenex formula is 100-separable and is in Clause Normal Form. Each clause has at most 5 polynomials and each polynomial has at most 5 terms. The analysis is done for the 2, 3 and the 4 variable case. The implementation uses OpenMP library to divide the processing of the prenex formula into independent threads of execution, each running on a separate Intel Xeon CPU. 