A formula of first-order logic is in prenex normal form if it is of the form Q_1 x_1 ...Q_n x_n M, where each Q_i is a quantifier for all ("for all") or exists ("exists") and M is quantifier-free. For example, the formula exists x for all y exists z(P(x)⋁Q(x, y, z)) is in prenex normal form, whereas formula exists x for all y(P(x)⋁exists z Q(x, y, z)) is not, where ⋁ denotes OR. Every formula of first-order logic can be converted to an equivalent formula in prenex normal form.