Writing in CNF that only one statement can be true 
Consider 5 Boolean variables $x_1, x_2, x_3, x_4, x_5$.

*

*Write a propositional formula that expresses the fact that one and at most one among the Boolean variables $x_1, x_2, x_3, x_4, x_5$ is true.


*Compute a conjunctive normal form of this formula.
Your answer must be justified.

I thought this was straightforward as I could just define $\phi_i$ as the conjunction of $x_i$ and not the others, but I'm not seeing a nice way to put that into CNF.

The proposition for "none are true" is: $(\neg x_1\wedge\neg x_2\wedge\neg x_3\wedge\neg x_4\wedge\neg x_5)$
The proposition for "only $x_1$ is true" is: $(x_1\wedge\neg x_2\wedge\neg x_3\wedge\neg x_4\wedge\neg x_5)$
And so forth.  Use that to build a DNF for "at most one from the five is true," and simplify it (hint: use idempotence, distribution, and complementation).
Convert this to CNF.
