   More generally, suppose \(A\) is any prenex formula, of the form \[ \mathbf{Q}_1 x_1 \ldots \mathbf{Q}_n x_n B(x_1, \ldots, x_n), \] where   \(B\) is quantifier-free. Then \(B\) is said to be the matrix of \(A\), and an instance of \(B\) is obtained by substituting terms in the language of \(B\) for some of its variables. The Herbrand normal form \(A^H\) of \(A\) is obtained by