would be on the cluster, using the parallel CAD algorithm. This has been demonstrated by considering prenex formulae with zero sharing factor.

But, as the sharing factor between two clauses increases, we find that these two clauses become interdependent to a greater extent. Thus, executing them in parallel would lead to greater amount of work being done, as compared to the case where the conditions imposed by one clause influences the computation of CAD on another clause.

Experimental Evaluation
=======================

The simulation results in this paper utilize the clause normal form (CNF), to ease the process of generating prenex formulae. The test cases are always in the CNF. The simulations are performed on a cluster, comprising of 36 nodes, with 8 Intel Xeon quad-core CPUs in each node. The preprocessor is implemented using C and the OpenMP library. The code used for these experiments has been uploaded at http://algoalgebra.csa.iisc.ernet.in/Preprocessor/.

The experimental setup is as follows:

(i) The dependence of running time of QEPCAD B on number of terms, highest exponent and total number of terms in a prenex formula,

(ii) The distribution of prenex formulae according to the number of clauses in their corresponding CNFs,

(iii) The comparison of running 