A molecular statement written as

a conjunction of disjunctions of possibly negated variables

\(\{ x_1, x_2, \ldots \}\) in the form

\begin{gather*} f = \underbrace{(\ell_{11} \lor \ell_{12} \lor \cdots)}_{\textstyle c_1} \land \underbrace{(\ell_{21} \lor \ell_{22} \lor \cdots)}_{\textstyle c_2} \land \cdots, \\[1ex] \text{with} \quad \forall (i, j), \> \quad \exists k \quad \text{such that} \quad \boxed{\ell_{ij} = x_k} \quad \text{or} \quad \boxed{\ell_{ij} = \lnot x_k}, \end{gather*}

where	\(f\)	is the formula in CNF,
	\(c_i\)	is the \(i\)-th clause of \(f\), and
	\(\ell_{ij}\)	is the \(j\)-th literal of \(c_i\).