Home / Computer science / 3-satisfiability (3SAT) / Explore / Case 4: More than three literals / Proof / Case 2: \(c\) is not satisfiable
Case 2A: \(y_1 = 0\)
The first clause is not satisfied:
\begin{align*} c'_1 & = (\ell_1 \lor \ell_2 \lor y_1) \\ & = (0 \lor 0 \lor \boxed{0}) \\ & = 0 \\[1ex] \vdots & \end{align*}