are TRUE. The disjunction of the formulae of these cells is the required quantifier-free formula and is returned.

Towards Parallelization
=======================

Using Clause Normal Forms
-------------------------

In this section we introduce the application of miniscoping and clause normal forms to obtain a preprocessor that can parallelize CAD. Miniscoping is prevalent in the standard literature as a way of localising quantifiers. One can use an algorithm by Nonnengart and Weidenbach [@miniscoping] to compute ‘clause normal forms’.

A sentence $\phi$ is said to be in ‘Clause Normal Form’, if $\phi = \forall x_1,. . . ,\forall x_{k}[C_1 \wedge . . . \wedge C_{k}]$ where $C_{i} = L_{i,1} \vee . . . \vee L_{i,l_{i}}$ and each $L_{i,j}$ is a literal. Clause normal forms shall be represented by ‘CNF’ throughout this paper.

Their work introduces this algorithm and proves that it terminates in a finite amount of time and that the generated clause normal form is equivalent to the input. The time complexity of this algorithm is polynomial in the number of statements.

The algorithm to compute clause normal forms uses the concept of skolemization to eliminate existential quantifiers (by systematic replacement of existentially quantified variables by functions of universally quantified variables). Skolemization may 