207. The five clauses of 
resolve to the single clause xyz. Thus C(x, y, y; 1, 2, 3)∪C
∪C(
, z, z; 7, 8, 9)∪
is a solution. [K. Iwama and K. Takaki, DIMACS 35 (1997), 315–333, noted that the 16 clauses 
∪ C(x, x, x; 1, 2, 3) ∪ C(y, y, y; 4, 5, 6) ∪ C(
Get The Art of Computer Programming: Satisfiability, Volume 4, Fascicle 6 now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
