TAOCP 7.2.2.2 Exercise 242
You've hit your limit.
Section 7.2.2.2: Satisfiability
Exercise 242. [M20] The pigeonhole axioms (106) and (107) are equivalent to the clauses (15) and (16) that arise if we try to color the complete graph $K_{m+1}$ with $m$ colors.
Suppose we include further axioms corresponding to (17), namely $$(\bar{x}{jk} \vee \bar{x}{jk'}), \quad \text{for } 0 \le j \le m \text{ and } 1 \le k < k' \le m.$$
Does Theorem B still hold, or do these additional axioms decrease the refutation width?
Verified: no
Solve time: 1m07s
You've hit your limit. Please try again later.