Representing the Puzzle to an Automated Reasoning Program 
<P>
To have an automated reasoning program attack this puzzle,
we must represent various facts about the state of the checkerboard--about which complete coverings and which partial coverings are achievable.
<P>
The following clauses are needed:
<P>
(1)  ACHIEVABLE(row(1),squares(r,n,n,n,n,n,n,n)).
<br>
(2)  -ACHIEVABLE(row(x),squares(n,n,y3,y4,y5,y6,y7,y8))
 | ACHIEVABLE(row(x),squares(c,c,y3,y4,y5,y6,y7,y8)).
<br>
(3)  -ACHIEVABLE(row(x),squares(y1,n,n,y4,y5,y6,y7,y8))
| ACHIEVABLE(row(x),squares(y1,c,c,y4,y5,y6,y7,y8)).
<br>
(4)  -ACHIEVABLE(row(x),squares(y1,y2,n,n,y5,y6,y7,y8))
 | ACHIEVABLE(row(x),squares(y1,y2,c,c,y5,y6,y7,y8)).
<br>
(5)  -ACHIEVABLE(row(x),squares(y1,y2,y3,n,n,y6,y7,y8))
 | ACHIEVABLE(row(x),squares(y1,y2,y3,c,c,y6,y7,y8)).
<br>
(6)  -ACHIEVABLE(row(x),squares(y1,y2,y3,y4,n,n,y7,y8))
 | ACHIEVABLE(row(x),squares(y1,y2,y3,y4,c,c,y7,y8)).
<br>
(7)  -ACHIEVABLE(row(x),squares(y1,y2,y3,y4,y5,n,n,y8))
 | ACHIEVABLE(row(x),squares(y1,y2,y3,y4,y5,c,c,y8)).
<br>
(8)  -ACHIEVABLE(row(x),squares(y1,y2,y3,y4,y5,y6,n,n))
 | ACHIEVABLE(row(x),squares(y1,y2,y3,y4,y5,y6,c,c)).
<br>
(9)  -ACHIEVABLE(row(x),squares(y1,y2,y3,y4,y5,y6,y7,y8))
 |  ACHIEVABLE(row($SUM(x,1)),squares(compl(y1),compl(y2),
    compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))).
<br>
(10)  EQUAL(compl(c),n).
<br>
(11)  EQUAL(compl(n),c).
<br>
(12)  EQUAL(compl(r),n)
<br>
(13)  ACHIEVABLE(row(9),squares(y1,y2,y3,y4,y5,y6,y7,y8)).
<br>
(14)  -ACHIEVABLE(row(8),squares(c,c,c,c,c,c,c,n)).
<P>
<br>
Clause 1 says that
row 1 has its first square removed, and its remaining squares not covered.
<br>
Clause 2 says
a domino can be played horizontally in the first two squares when those two squares are not covered.
<br>
Clauses 3 through 8 permit a reasoning program to play dominoes horizontally beginning, respectively, in square 2 of the row under consideration.
Seven clauses are used to make horizontal plays because there are eight squares in a row, each domino covers two squares, and no domino is allowed to protrude past the edge of the board.
<br>
Clauses 9-12 are needed
to enable a reasoning program to make vertical plays.
<br>
Clause 13 prevents the play from extending into the nonexistent row 9. 
<br>
Clause 14 is used for a proof by contradiction: it denies 
that the board can be covered.