The clausal form of the disjunctive normal form ¬A ∨ ¬B ∨ ¬C ∨ D is:

Key identity: p → q ≡ ¬p ∨ q — an implication with antecedent p and consequent q is logically equivalent to the disjunction ¬p ∨ q. To recover the clausal (if...then) form of a disjunction of literals, group the negated literals into one conjunctive antecedent p and leave the remaining positive literal as the consequent q.

Given expression: ¬A ∨ ¬B ∨ ¬C ∨ D.

Set p = A ∧ B ∧ C and q = D. Working from the identity:

1. ¬p ∨ q = ¬(A ∧ B ∧ C) ∨ D

2. By De Morgan's law, ¬(A ∧ B ∧ C) = ¬A ∨ ¬B ∨ ¬C, so ¬p ∨ q = ¬A ∨ ¬B ∨ ¬C ∨ D

This matches the given expression exactly, so the clausal form is (A ∧ B ∧ C) → D, i.e. A ∧ B ∧ C ⇒ D.

Cross-check -- why the other candidate forms do not match:

• An implication of the form (A ∨ B ∨ C ∨ D) → true is a tautology (always true), whereas the given formula can be false (e.g., A = true, B = true, C = true, D = false).

• An implication of the form (A ∧ B ∧ C ∧ D) → true is also always true, so it fails on the same counterexample.

• An implication (A ∧ B ∧ C ∧ D) → false is equivalent to ¬(A ∧ B ∧ C ∧ D) = ¬A ∨ ¬B ∨ ¬C ∨ ¬D, which differs from the given expression because the last literal is ¬D rather than D.

Conclusion: the clausal form of ¬A ∨ ¬B ∨ ¬C ∨ D is A ∧ B ∧ C ⇒ D.