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.

If you cannot use a computer to solve the problem, you can still use it to verify your solution:
>>> from sympy import *
>>> x1, x2, x3, x4, x5 = symbols('x1 x2 x3 x4 x5')
>>> Phi1 =     x1  & Not(x2) & Not(x3) & Not(x4) & Not(x5)
>>> Phi2 = Not(x1) &     x2  & Not(x3) & Not(x4) & Not(x5)
>>> Phi3 = Not(x1) & Not(x2) &     x3  & Not(x4) & Not(x5)
>>> Phi4 = Not(x1) & Not(x2) & Not(x3) &     x4  & Not(x5)
>>> Phi5 = Not(x1) & Not(x2) & Not(x3) & Not(x4) &     x5
>>> Psi = Phi1 | Phi2 | Phi3 | Phi4 | Phi5
>>> to_cnf(Psi, simplify=True)
And(Or(Not(x1), Not(x2)), Or(Not(x1), Not(x3)), Or(Not(x1), Not(x4)), Or(Not(x1), Not(x5)), Or(Not(x2), Not(x3)), Or(Not(x2), Not(x4)), Or(Not(x2), Not(x5)), Or(Not(x3), Not(x4)), Or(Not(x3), Not(x5)), Or(Not(x4), Not(x5)), Or(x1, x2, x3, x4, x5))

Hence, the formula in CNF is
$$\left(\neg x_{1} \vee \neg x_{2}\right) \wedge \left(\neg x_{1} \vee \neg x_{3}\right) \wedge \left(\neg x_{1} \vee \neg x_{4}\right) \wedge \left(\neg x_{1} \vee \neg x_{5}\right) \wedge \left(\neg x_{2} \vee \neg x_{3}\right) \wedge \left(\neg x_{2} \vee \neg x_{4}\right) \wedge \left(\neg x_{2} \vee \neg x_{5}\right) \wedge \left(\neg x_{3} \vee \neg x_{4}\right) \wedge \left(\neg x_{3} \vee \neg x_{5}\right) \wedge \left(\neg x_{4} \vee \neg x_{5}\right) \wedge \left(x_{1} \vee x_{2} \vee x_{3} \vee x_{4} \vee x_{5}\right)$$
Note that we have $11$ clauses, as Bram predicted.
