Formula (¬p1 ∨ p2 ∨ ¬p4) ∧ (¬p1 ∨ ¬p2 ∨ p3) ∧ (¬p3 ∨ ¬p4) ∧ (p4 ∨ p5 ∨ p6) ∧ (¬p5 ∨ p7) ∧ (¬p6 ∨ p7 ∨ ¬p8) ∧ (¬p2 ∨ ¬p7 ∨ ¬p6 ∨ ¬p5 ∨ ¬p3 ∨ p4) ∧ (¬p1 ∨ ¬p8 ∨ ¬p6 ∨ ¬p5 ∨ ¬p3 ∨ p4) ∧ (¬p1 ∨ ¬p8 ∨ p2 ∨ ¬p7 ∨ p3 ∨ p4) ∧ (¬p1 ∨ ¬p8 ∨ ¬p2 ∨ ¬p7 ∨ ¬p6 ∨ p5) ∧ (¬p2 ∨ ¬p7 ∨ ¬p6 ∨ ¬p5 ∨ ¬p3 ∨ ¬p4) is unsatisfiable.