Consider the house wiring example depicted in Figure 5.2 and represented in Example 5.7. A background knowledge base suitable for consistency-based diagnosis is given in Figure 5.8. Normality assumptions, specifying that switches, circuit breakers, and lights must be ok to work as expected, are added to the clauses. There are no clauses for the $o\mathit{}k$ atoms, but they are made assumable.

The user is able to observe the switch positions and whether a light is lit or dark.

A light cannot be both lit and dark. This knowledge is stated in the following integrity constraints:

Suppose the user observes that all three switches are up, and that $l_{\mathrm{1}}$ and $l_{\mathrm{2}}$ are both dark. This is represented by the atomic clauses

Given the knowledge of Figure 5.8 together with the observations, there are two minimal conflicts:

Thus, it follows that

which means that at least one of the components $c\mathit{}{b}_{\mathrm{1}}$, $s_{\mathrm{1}}$, $s_{\mathrm{2}}$, or $l_{\mathrm{1}}$ must not be ok, and least one of the components $c\mathit{}{b}_{\mathrm{1}}$, $s_{\mathrm{3}}$, or $l_{\mathrm{2}}$ must not be ok.

In Example 5.23, the disjunction of the negation of the two conflicts is a logical consequence of the clauses. Thus, the conjunction

follows from the knowledge base. This conjunction of disjunctions in conjunctive normal form (CNF) can be distributed into disjunctive normal form (DNF), a disjunction of conjunctions, here of negated atoms:

Thus, either $c\mathit{}{b}_{\mathrm{1}}$ is broken or there is at least one of six double faults.

The propositions that are disjoined together correspond to the seven minimal diagnoses: $\mathrm{\{}{\mathit{\text{ok\_cb}}}_{\mathrm{1}}\mathrm{\}}$, $\mathrm{\{}{\mathit{\text{ok\_s}}}_{\mathrm{1}}\mathrm{,}{\mathit{\text{ok\_s}}}_{\mathrm{3}}\mathrm{\}}$, $\mathrm{\{}{\mathit{\text{ok\_s}}}_{\mathrm{1}}\mathrm{,}{\mathit{\text{ok\_l}}}_{\mathrm{2}}\mathrm{\}}$, $\mathrm{\{}{\mathit{\text{ok\_s}}}_{\mathrm{2}}\mathrm{,}{\mathit{\text{ok\_s}}}_{\mathrm{3}}\mathrm{\}}$, $\mathrm{\{}{\mathit{\text{ok\_s}}}_{\mathrm{2}}\mathrm{,}{\mathit{\text{ok\_l}}}_{\mathrm{2}}\mathrm{\}}$, $\mathrm{\{}{\mathit{\text{ok\_l}}}_{\mathrm{1}}\mathrm{,}{\mathit{\text{ok\_s}}}_{\mathrm{3}}\mathrm{\}}$, $\mathrm{\{}{\mathit{\text{ok\_l}}}_{\mathrm{1}}\mathrm{,}{\mathit{\text{ok\_l}}}_{\mathrm{2}}\mathrm{\}}$. The system has proved that one of these combinations must be faulty.