13x13
KNIGHT COVERING
OPTIMALITY PROOF


28 knights are required to cover a 13x13 board.
The proof is divided into cases.

Case 1: there does not exist an unoccupied (3,3) square.
Case 2: there exists an unoccupied (3,3) square.

Case 2 is subdivided based on the status of the
other three (3,3) squares.

Case 2A: there exists exactly one unoccupied (3,3) square.
Case 2B: there exists at least two unoccupied (3,3) squares.

Case 2B is further subdivided for the two choices
of unnoccupied (3,3) square pairs.

Case 2B1: the upper left and upper right (3,3) squares
are unoccupied.
Case 2B2: the upper left and lower right (3,3) squares
are unoccupied.

Cases 1, 2A, 2B1, and 2B2 are proved below.

=========================
See the Divide and Round Proof Technique
for an explanation of the following notation and reasoning.

=========================
13x13 proof case 1

There does not exist an unoccupied (3,3) square.
This means that all four (3,3) squares are occupied.
So to prove that a total of 28 knights are required,
we need to prove that it takes 24 more knights to cover
the remaining squares.

five single-square constraints
multiplied by 2

- - - 2 - - - - - 2 - - -   - - - - - - - - - - - - -
- 2 - - - - - - - - - 2 -   - a - - - - - - - - - b -
- - - 2 - - - - - 2 - - -   - - - - - - - - - - - - -
2 - 2 - - - - - - - 2 - 2   - - - - - - - - - - - - -
- - - - - 2 - 2 - - - - -   - - - - - - - - - - - - -
- - - - 2 - - - 2 - - - -   - - - - - - - - - - - - -
- - - - - - 2 - - - - - -   - - - - - - c - - - - - -
- - - - 2 - - - 2 - - - -   - - - - - - - - - - - - -
- - - - - 2 - 2 - - - - -   - - - - - - - - - - - - -
2 - 2 - - - - - - - 2 - 2   - - - - - - - - - - - - -
- - - 2 - - - - - 2 - - -   - - - - - - - - - - - - -
- 2 - - - - - - - - - 2 -   - d - - - - - - - - - e -
- - - 2 - - - - - 2 - - -   - - - - - - - - - - - - -
>= 10

sixteen single-square constraints

1 - - - - - 1 - - - - - 1   a - - - - - o - - - - - b
- - 1 - 1 - - - 1 - 1 - -   - - - - - - - - - - - - -
- 1 - - - 1 - 1 - - - 1 -   - - - - - - - - - - - - -
- - - - 1 1 2 1 1 - - - -   - - - - - - - - - - - - -
- 1 - 1 2 1 2 1 2 1 - 1 -   - - - - - - - - - - - - -
- - 1 1 1 3 3 3 1 1 1 - -   - - - - - c d e - - - - -
1 - - 2 2 3 - 3 2 2 - - 1   o - - - - f - g - - - - o
- - 1 1 1 3 3 3 1 1 1 - -   - - - - - h i j - - - - -
- 1 - 1 2 1 2 1 2 1 - 1 -   - - - - - - - - - - - - -
- - - - 1 1 2 1 1 - - - -   - - - - - - - - - - - - -
- 1 - - - 1 - 1 - - - 1 -   - - - - - - - - - - - - -
- - 1 - 1 - - - 1 - 1 - -   - - - - - - - - - - - - -
1 - - - - - 1 - - - - - 1   k - - - - - o - - - - - l
>= 16

four small triangle constraints

- - - - 1 1 - 1 1 - - - -   - - - - - a - a - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - a - - - - - -
- - - - 1 - 1 - 1 - - - -   - - - - - - - - - - - - -
- 1 - - - 1 - 1 - - - 1 -   - - - - - - - - - - - - -
1 - 1 - - - - - - - 1 - 1   - - - - - - - - - - - - -
1 1 - 1 - - - - - 1 - 1 1   b - - - - - - - - - - - c
- 1 1 - - - - - - - 1 1 -   - b - - - - - - - - - c -
1 1 - 1 - - - - - 1 - 1 1   b - - - - - - - - - - - c
1 - 1 - - - - - - - 1 - 1   - - - - - - - - - - - - -
- 1 - - - 1 - 1 - - - 1 -   - - - - - - - - - - - - -
- - - - 1 - 1 - 1 - - - -   - - - - - - - - - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - d - - - - - -
- - - - 1 1 - 1 1 - - - -   - - - - - d - d - - - - -
>= 8

add above three constraint sets

1 - - 2 1 1 1 1 1 2 - - 1   o - - - - o o o - - - - o
- 2 1 1 1 1 1 1 1 1 1 2 -   - o - - - - o - - - - o -
- 1 - 2 1 1 1 1 1 2 - 1 -   - - - - - - - - - - - - -
2 1 2 - 1 2 2 2 1 - 2 1 2   - - - - - - - - - - - - -
1 1 1 1 2 3 2 3 2 1 1 1 1   - - - - - - - - - - - - -
1 1 1 2 3 3 3 3 3 2 1 1 1   o - - - - o o o - - - - o
1 1 1 2 2 3 2 3 2 2 1 1 1   o o - - - o o o - - - o o
1 1 1 2 3 3 3 3 3 2 1 1 1   o - - - - o o o - - - - o
1 1 1 1 2 3 2 3 2 1 1 1 1   - - - - - - - - - - - - -
2 1 2 - 1 2 2 2 1 - 2 1 2   - - - - - - - - - - - - -
- 1 - 2 1 1 1 1 1 2 - 1 -   - - - - - - - - - - - - -
- 2 1 1 1 1 1 1 1 1 1 2 -   - o - - - - o - - - - o -
1 - - 2 1 1 1 1 1 2 - - 1   o - - - - o o o - - - - o
>= 34

multiply by 2

2 - - 4 2 2 2 2 2 4 - - 2   o - - - - o o o - - - - o
- 4 2 2 2 2 2 2 2 2 2 4 -   - o - - - - o - - - - o -
- 2 - 4 2 2 2 2 2 4 - 2 -   - - - - - - - - - - - - -
4 2 4 - 2 4 4 4 2 - 4 2 4   - - - - - - - - - - - - -
2 2 2 2 4 6 4 6 4 2 2 2 2   - - - - - - - - - - - - -
2 2 2 4 6 6 6 6 6 4 2 2 2   o - - - - o o o - - - - o
2 2 2 4 4 6 4 6 4 4 2 2 2   o o - - - o o o - - - o o
2 2 2 4 6 6 6 6 6 4 2 2 2   o - - - - o o o - - - - o
2 2 2 2 4 6 4 6 4 2 2 2 2   - - - - - - - - - - - - -
4 2 4 - 2 4 4 4 2 - 4 2 4   - - - - - - - - - - - - -
- 2 - 4 2 2 2 2 2 4 - 2 -   - - - - - - - - - - - - -
- 4 2 2 2 2 2 2 2 2 2 4 -   - o - - - - o - - - - o -
2 - - 4 2 2 2 2 2 4 - - 2   o - - - - o o o - - - - o
>= 68

twenty-eight single-square constraints

2 1 2 - 1 1 1 1 1 - 2 1 2   - - a - - b o c - - d - -
1 - 2 2 2 1 - 1 2 2 2 - 1   - - e - - - - - - - f - -
2 2 - 1 2 1 2 1 2 1 - 2 2   g h - - - - - - - - - i j
- 2 1 2 - - - - - 2 1 2 -   - - - - - - - - - - - - -
1 2 2 - - - - - - - 2 2 1   - - - - - - - - - - - - -
1 1 1 - - - - - - - 1 1 1   k - - - - - - - - - - - l
1 - 2 - - - - - - - 2 - 1   o - - - - - - - - - - - o
1 1 1 - - - - - - - 1 1 1   m - - - - - - - - - - - n
1 2 2 - - - - - - - 2 2 1   - - - - - - - - - - - - -
- 2 1 2 - - - - - 2 1 2 -   - - - - - - - - - - - - -
2 2 - 1 2 1 2 1 2 1 - 2 2   o p - - - - - - - - - q r
1 - 2 2 2 1 - 1 2 2 2 - 1   - - s - - - - - - - t - -
2 1 2 - 1 1 1 1 1 - 2 1 2   - - u - - v o w - - x - -
>= 28

four small triangle constraints

- - - - 1 1 - 1 1 - - - -   - - - - - a - a - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - a - - - - - -
- - - - 1 - 1 - 1 - - - -   - - - - - - - - - - - - -
- 1 - - - 1 - 1 - - - 1 -   - - - - - - - - - - - - -
1 - 1 - - - - - - - 1 - 1   - - - - - - - - - - - - -
1 1 - 1 - - - - - 1 - 1 1   b - - - - - - - - - - - c
- 1 1 - - - - - - - 1 1 -   - b - - - - - - - - - c -
1 1 - 1 - - - - - 1 - 1 1   b - - - - - - - - - - - c
1 - 1 - - - - - - - 1 - 1   - - - - - - - - - - - - -
- 1 - - - 1 - 1 - - - 1 -   - - - - - - - - - - - - -
- - - - 1 - 1 - 1 - - - -   - - - - - - - - - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - d - - - - - -
- - - - 1 1 - 1 1 - - - -   - - - - - d - d - - - - -
>= 8

four a3 constraints

- - - - 1 1 1 1 1 - - - -   - - - - - a - a - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - a - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - a - a - - - - -
- 1 - 2 - 1 - 1 - 2 - 1 -   - - - - - - - - - - - - -
1 - 1 - 2 - 1 - 2 - 1 - 1   - - - - - - - - - - - - -
1 1 1 1 - - - - - 1 1 1 1   b - b - - - - - - - c - c
1 1 1 - 1 - - - 1 - 1 1 1   - b - - - - - - - - - c -
1 1 1 1 - - - - - 1 1 1 1   b - b - - - - - - - c - c
1 - 1 - 2 - 1 - 2 - 1 - 1   - - - - - - - - - - - - -
- 1 - 2 - 1 - 1 - 2 - 1 -   - - - - - - - - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - d - d - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - d - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - d - d - - - - -
>= 12

four b3 constraints

1 - 1 1 1 - 1 1 - - - 1 1   a - a - a - a - - - - - b
1 - 1 - 1 1 1 - 1 - 1 - -   - - - - - a - - - - - - -
- 1 - 1 - 1 - 1 - - - 1 1   - - - - - - - - - - - - b
- - - - 1 - 1 - - - 1 - 1   - - - - - - - - - - - - -
- 1 - - - - - - - 1 - 1 1   - - - - - - - - - - - - b
1 - 1 - - - - - - - 1 1 -   - - - - - - - - - - - b -
1 1 - 1 - - - - - 1 - 1 1   c - - - - - - - - - - - b
- 1 1 - - - - - - - 1 - 1   - c - - - - - - - - - - -
1 1 - 1 - - - - - - - 1 -   c - - - - - - - - - - - -
1 - 1 - - - 1 - 1 - - - -   - - - - - - - - - - - - -
1 1 - - - 1 - 1 - 1 - 1 -   c - - - - - - - - - - - -
- - 1 - 1 - 1 1 1 - 1 - 1   - - - - - - - d - - - - -
1 1 - - - 1 1 - 1 1 1 - 1   c - - - - - d - d - d - d
>= 12

another four b3 constraints

1 1 - - - 1 1 - 1 1 1 - 1   a - - - - - b - b - b - b
- - 1 - 1 - 1 1 1 - 1 - 1   - - - - - - - b - - - - -
1 1 - - - 1 - 1 - 1 - 1 -   a - - - - - - - - - - - -
1 - 1 - - - 1 - 1 - - - -   - - - - - - - - - - - - -
1 1 - 1 - - - - - - - 1 -   a - - - - - - - - - - - -
- 1 1 - - - - - - - 1 - 1   - a - - - - - - - - - - -
1 1 - 1 - - - - - 1 - 1 1   a - - - - - - - - - - - c
1 - 1 - - - - - - - 1 1 -   - - - - - - - - - - - c -
- 1 - - - - - - - 1 - 1 1   - - - - - - - - - - - - c
- - - - 1 - 1 - - - 1 - 1   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - - - 1 1   - - - - - - - - - - - - c
1 - 1 - 1 1 1 - 1 - 1 - -   - - - - - d - - - - - - -
1 - 1 1 1 - 1 1 - - - 1 1   d - d - d - d - - - - - c
>= 12

add above six constraint sets

6 2 3 5 6 6 6 6 6 5 3 2 6   o - o - o o o o o - o - o
2 4 6 6 6 6 6 6 6 6 6 4 2   - o o - - o o o - - o o -
3 6 - 6 6 6 6 6 6 6 - 6 3   o o - - - o - o - - - o o
5 6 6 4 3 6 6 6 3 4 6 6 5   - - - - - - - - - - - - -
6 6 6 3 6 6 5 6 6 3 6 6 6   o - - - - - - - - - - - o
6 6 6 6 6 6 6 6 6 6 6 6 6   o o o - - o o o - - o o o
6 6 6 6 5 6 4 6 5 6 6 6 6   o o - - - o o o - - - o o
6 6 6 6 6 6 6 6 6 6 6 6 6   o o o - - o o o - - o o o
6 6 6 3 6 6 5 6 6 3 6 6 6   o - - - - - - - - - - - o
5 6 6 4 3 6 6 6 3 4 6 6 5   - - - - - - - - - - - - -
3 6 - 6 6 6 6 6 6 6 - 6 3   o o - - - o - o - - - o o
2 4 6 6 6 6 6 6 6 6 6 4 2   - o o - - o o o - - o o -
6 2 3 5 6 6 6 6 6 5 3 2 6   o - o - o o o o o - o - o
>= 140

divide by 6 and round

1 1 1 1 1 1 1 1 1 1 1 1 1   o - o - o o o o o - o - o
1 1 1 1 1 1 1 1 1 1 1 1 1   - o o - - o o o - - o o -
1 1 - 1 1 1 1 1 1 1 - 1 1   o o - - - o - o - - - o o
1 1 1 1 1 1 1 1 1 1 1 1 1   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o - - - o o o - - - o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   - - - - - - - - - - - - -
1 1 - 1 1 1 1 1 1 1 - 1 1   o o - - - o - o - - - o o
1 1 1 1 1 1 1 1 1 1 1 1 1   - o o - - o o o - - o o -
1 1 1 1 1 1 1 1 1 1 1 1 1   o - o - o o o o o - o - o
>= 24

=========================
13x13 proof case 2A

There exists exactly one unoccupied (3,3) square.
Whichever (3,3) is unoccupied, we can rotate and reflect
the board to make that square in the upper left corner.

The upper left (3,3) square forbidden to be occupied
and the other three (3,3) squares are occupied.
So to prove that a total of 28 knights are required,
we need to prove that it takes 25 more knights to cover
the remaining squares.


four single square constraints
multiply by 2

2 2 2 - - - - - - - - - -   a b - - - - - - - - - - -
2 - 2 2 - - - - - - - - -   c - - - - - - - - - - - -
2 2 0 - - - - - - - - - -   - - - - - - - - - - - - -
- 2 - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - 2 - 2 - - - - -   - - - - - - - - - - - - -
- - - - 2 - - - 2 - - - -   - - - - - - - - - - - - -
- - - - - - 2 - - - - - -   - - - - - - d - - - - - -
- - - - 2 - - - 2 - - - -   - - - - - - - - - - - - -
- - - - - 2 - 2 - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
>= 8

two c3 constraints

- - - - - - - 1 1 1 1 1 1   - - - - - - - - a - a - a
- - - - - - 1 - 1 1 1 1 1   - - - - - - - - - a - a -
- - - - - - - 1 - 1 - 1 1   - - - - - - - - - - - - a
- - - - - - - - 1 - 1 - 1   - - - - - - - - - - - - -
- - - - - - - - - - - 1 -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - - - - - - - - - - -   - - - - - - - - - - - - -
1 - 1 - - - - - - - - - -   - - - - - - - - - - - - -
1 1 - 1 - - - - - - - - -   b - - - - - - - - - - - -
1 1 1 - - - - - - - - - -   - b - - - - - - - - - - -
1 1 - 1 - - - - - - - - -   b - - - - - - - - - - - -
1 1 1 - 1 - - - - - - - -   - b - - - - - - - - - - -
1 1 1 1 - - - - - - - - -   b - b - - - - - - - - - -
>= 6

twenty-five single-square constraints

- - - 2 1 - 1 1 1 - - - 1   - - - a - - b c - - - - d
- 3 - - 1 2 1 - 1 1 1 - -   - e - - - - f - - - - - -
- - 0 1 2 1 1 1 2 - - 1 -   - - - - - - - - - - - - -
2 - 1 - 1 1 2 1 1 - - 1 -   g - - - - - - - - - - - -
1 1 2 1 - 1 1 1 1 - 2 1 1   - - - - - - - - - - - - -
- 2 1 1 1 3 2 2 1 2 1 1 1   - - - - - h - i - - - - j
1 1 1 2 1 2 - 3 1 2 2 1 1   k l - - - - - m - - - n o
1 - 1 1 1 2 3 1 1 2 1 1 1   p - - - - q r s - - - - t
1 1 2 1 1 1 1 1 2 1 2 1 1   - - - - - - - - - - - - -
- 1 - - 1 2 2 2 1 - - 1 -   - - - - - - - - - - - - -
- 1 - - 2 1 2 1 2 - - - -   - - - - - - - - - - - - -
- - 1 1 1 1 1 1 1 1 - - -   - - - - - - u - - - - - -
1 - - - 1 1 1 1 1 - - - -   v - - - - w x y - - - - -
>= 25

add above three constraint sets

2 2 2 2 1 - 1 2 2 1 1 1 2   o o - o - - o o o - o - o
2 3 2 2 1 2 2 - 2 2 2 1 1   o o - - - - o - - o - o -
2 2 0 1 2 1 1 2 2 1 - 2 1   - - - - - - - - - - - - o
2 2 1 - 1 1 2 1 2 - 1 1 1   o - - - - - - - - - - - -
1 1 2 1 - 3 1 3 1 - 2 2 1   - - - - - - - - - - - - -
- 2 1 1 3 3 2 2 3 2 1 1 1   - - - - - o - o - - - - o
1 2 1 2 1 2 2 3 1 2 2 1 1   o o - - - - o o - - - o o
2 - 2 1 3 2 3 1 3 2 1 1 1   o - - - - o o o - - - - o
2 2 2 2 1 3 1 3 2 1 2 1 1   o - - - - - - - - - - - -
1 2 1 - 1 2 2 2 1 - - 1 -   - o - - - - - - - - - - -
1 2 - 1 2 1 2 1 2 - - - -   o - - - - - - - - - - - -
1 1 2 1 2 1 1 1 1 1 - - -   - o - - - - o - - - - - -
2 1 1 1 1 1 1 1 1 - - - -   o - o - - o o o - - - - -
>= 39

multiply by 2

4 4 4 4 2 - 2 4 4 2 2 2 4   o o - o - - o o o - o - o
4 6 4 4 2 4 4 - 4 4 4 2 2   o o - - - - o - - o - o -
4 4 0 2 4 2 2 4 4 2 - 4 2   - - - - - - - - - - - - o
4 4 2 - 2 2 4 2 4 - 2 2 2   o - - - - - - - - - - - -
2 2 4 2 - 6 2 6 2 - 4 4 2   - - - - - - - - - - - - -
- 4 2 2 6 6 4 4 6 4 2 2 2   - - - - - o - o - - - - o
2 4 2 4 2 4 4 6 2 4 4 2 2   o o - - - - o o - - - o o
4 - 4 2 6 4 6 2 6 4 2 2 2   o - - - - o o o - - - - o
4 4 4 4 2 6 2 6 4 2 4 2 2   o - - - - - - - - - - - -
2 4 2 - 2 4 4 4 2 - - 2 -   - o - - - - - - - - - - -
2 4 - 2 4 2 4 2 4 - - - -   o - - - - - - - - - - - -
2 2 4 2 4 2 2 2 2 2 - - -   - o - - - - o - - - - - -
4 2 2 2 2 2 2 2 2 - - - -   o - o - - o o o - - - - -
>= 78

two a4 constraints

- - - - - - - - - - - 1 1   - - - - - - - - - - - - b
- - - - - - - - - - 1 - -   - - - - - - - - - - - - -
- - - - - - - - - - - 1 1   - - - - - - - - - - - - b
- - - - - - - - - - 1 - 1   - - - - - - - - - - - - -
- - - - - - - - - 1 - 1 1   - - - - - - - - - - - - b
- - - - - - - - - - 1 1 1   - - - - - - - - - - - b -
- - - - - - - - - 1 - 1 1   - - - - - - - - - - - - b
- - - - - - - - - - 1 1 1   - - - - - - - - - - - b -
- - - - - - - - - 1 - 1 -   - - - - - - - - - - - - -
- - - - 1 - 1 - 1 - 1 - 1   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 1   - - - - - - - - - - - - b
1 - 1 - 1 1 1 1 1 - 1 - 1   - - - - - a - a - - - - -
1 - 1 1 1 1 1 1 - 1 1 1 -   a - a - a - a - - - a - -
>= 8

two c3 constraints

- - - - - - - - - 1 1 1 1   - - - - - - - - - - a - a
- - - - - - - - 1 - 1 1 1   - - - - - - - - - - - a -
- - - - - - - - - 1 - 1 1   - - - - - - - - - - - - a
- - - - - - - - - - 1 1 1   - - - - - - - - - - - a -
- - - - - - - - - 1 - 1 1   - - - - - - - - - - - - a
- - - - - - - - - - 1 - 1   - - - - - - - - - - - - -
- - - - - - - - - - - 1 -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - 1 -   - - - - - - - - - - - - -
- - - - - - - - 1 - 1 - 1   - - - - - - - - - - - - -
- - - - - - - 1 - 1 - 1 1   - - - - - - - - - - - - b
- - - - - - 1 - 1 1 1 1 1   - - - - - - - - - b - b -
- - - - - - - 1 1 1 1 1 1   - - - - - - - - b - b - b
>= 6

two c3 constraints

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - 1 -   - - - - - - - - - - - - -
- - - - - - - - - - 1 - 1   - - - - - - - - - - - - -
- 1 - - - - - - - 1 - 1 1   - - - - - - - - - - - - b
1 - 1 - 1 - - - - - 1 1 1   - - - - - - - - - - - b -
1 1 - 1 - 1 - - - 1 - 1 1   a - - - - - - - - - - - b
- 1 1 1 1 - 1 - 1 - 1 1 1   - a - a - - - - - - - b -
1 1 1 1 1 1 - - - 1 1 1 1   a - a - a - - - - - b - b
>= 6

twenty-eight single-square constraints

1 1 1 1 1 2 2 1 - 2 - - -   a - - - b c d e - - - - -
1 - 2 1 3 1 1 2 1 1 - 1 -   - - - - f - - g - - - h -
1 2 0 1 1 3 3 1 1 2 - - -   - - i - - - - - - - - - -
1 1 1 2 1 2 1 1 1 1 1 2 1   - - - - - - - - - - - - -
1 3 1 1 2 - 1 - 2 - 1 - 1   j k - - - - - - - - - - -
2 1 3 2 - - 1 1 - 1 1 2 1   l - - - - - m - - - n - o
2 1 3 1 1 1 - - 3 - 2 - 2   p - - - - q - - - - - - -
1 2 1 1 - 1 - 2 - 1 1 2 1   r s - - - - - - - - t - u
- 1 1 1 2 - 3 - 2 - 1 - 1   - - - - - - - - - - - - -
2 1 2 1 - 1 - 1 - 2 1 2 1   - - - - - - - - - - - - -
- - - 1 1 1 2 1 1 1 - 1 -   - - - - - v - w - - - - -
- 1 - 2 - 2 - 2 - 2 1 1 -   - x - - - - - - - - - y -
- - - 1 1 1 2 1 1 1 - - 1   - - - - - z - A - - - - B
>= 28

add above five constraint sets

5 5 5 5 3 2 4 5 4 5 3 4 6   o o - o o o o o o - o - o
5 6 6 5 5 5 5 2 6 5 6 4 3   o o - - o - o o - o - o -
5 6 0 3 5 5 5 5 5 5 - 6 4   - - o - - - - - - - - - o
5 5 3 2 3 4 5 3 5 1 5 5 5   o - - - - - - - - - - o -
3 5 5 3 2 6 3 6 4 2 5 6 5   o o - - - - - - - - - - o
2 5 5 4 6 6 5 5 6 5 5 5 5   o - - - - o o o - - o o o
4 5 5 5 3 5 4 6 5 5 6 5 5   o o - - - o o o - - - o o
5 4 5 3 6 5 6 4 6 5 5 5 5   o o - - - o o o - - o o o
4 6 5 5 4 6 5 6 6 4 5 5 4   o - - - - - - - - - - - o
5 5 5 1 4 5 5 5 4 2 4 5 4   - o - - - - - - - - - o -
3 6 - 5 5 5 6 5 5 4 - 4 3   o - - - - o - o - - - - o
3 4 6 5 6 5 5 5 5 5 4 3 3   - o - o - o o o - o - o -
6 3 4 5 5 5 5 5 4 4 3 3 3   o - o - o o o o o - o - o
>= 126

multiply by 2

10 10 10 10  6  4  8 10  8 10  6  8 12   o o - o o o o o o - o - o
10 12 12 10 10 10 10  4 12 10 12  8  6   o o - - o - o o - o - o -
10 12  0  6 10 10 10 10 10 10  - 12  8   - - o - - - - - - - - - o
10 10  6  4  6  8 10  6 10  2 10 10 10   o - - - - - - - - - - o -
 6 10 10  6  4 12  6 12  8  4 10 12 10   o o - - - - - - - - - - o
 4 10 10  8 12 12 10 10 12 10 10 10 10   o - - - - o o o - - o o o
 8 10 10 10  6 10  8 12 10 10 12 10 10   o o - - - o o o - - - o o
10  8 10  6 12 10 12  8 12 10 10 10 10   o o - - - o o o - - o o o
 8 12 10 10  8 12 10 12 12  8 10 10  8   o - - - - - - - - - - - o
10 10 10  2  8 10 10 10  8  4  8 10  8   - o - - - - - - - - - o -
 6 12  - 10 10 10 12 10 10  8  -  8  6   o - - - - o - o - - - - o
 6  8 12 10 12 10 10 10 10 10  8  6  6   - o - o - o o o - o - o -
12  6  8 10 10 10 10 10  8  8  6  6  6   o - o - o o o o o - o - o
>= 252

a3 constraint with c3 constraint

- - - - 1 1 1 1 1 - - - -   - - - - - a - a - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - a - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - a - a - - - - -
- - - 1 - 1 - 1 - 1 - - -   - - - - - - - - - - - - -
- - - - 1 - 1 - 1 - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - 1 -   - - - - - - - - - - - - -
- - - - - - - - 1 - 1 - 1   - - - - - - - - - - - - -
- - - - - - - 1 - 1 - 1 1   - - - - - - - - - - - - b
- - - - - - 1 - 1 1 1 1 1   - - - - - - - - - b - b -
- - - - - - - 1 1 1 1 1 1   - - - - - - - - b - b - b
>= 6

a3 constraint with c3 constraint

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - 1 - - - - - - - - -   - - - - - - - - - - - - -
1 - 1 - 1 - - - - - - - -   - - - - - - - - - - - - -
1 1 1 1 - - - - - - - - -   a - a - - - - - - - - - -
- 1 1 - 1 - - - - - - 1 -   - a - - - - - - - - - - -
1 1 1 1 - - - - - - 1 - 1   a - a - - - - - - - - - -
1 - 1 - 1 - - - - 1 - 1 1   - - - - - - - - - - - - b
- 1 - 1 - - - - - - 1 1 1   - - - - - - - - - - - b -
- - - - - - - - - 1 - 1 1   - - - - - - - - - - - - b
- - - - - - - - 1 - 1 1 1   - - - - - - - - - - - b -
- - - - - - - - - 1 1 1 1   - - - - - - - - - - b - b
>= 6

twenty-eight single-square constraints

- 2 2 2 1 - 1 1 2 1 1 - -   - a - - - - - - - - - - -
2 - - 1 2 1 1 1 - - - 2 -   b - - - c d e - - - - f -
2 - 0 2 1 1 1 1 1 2 - - -   - - g - - - - - - h - - -
2 1 2 2 2 3 2 3 - 1 2 2 2   - - - - - - - - - - - - -
1 2 1 2 3 - 1 - 3 1 2 - 2   - i - - j - - - - - - - -
- 1 1 3 - - 2 1 - 1 2 1 1   - k - - - - l - - - m n -
1 1 1 2 1 2 - - 2 2 - 1 1   - o - - - p - - - - - q -
1 1 1 3 - 1 - 2 - 2 1 2 1   - - - - - - - - - - - r -
2 - 1 - 3 - 2 - - 1 2 - 2   - - - - - - - - - - - - -
1 - 2 1 1 1 2 2 1 2 2 1 2   - - s - - - - - - - - - -
1 - - 2 2 2 - 1 2 2 - 2 1   - - - - - t - - - - - u -
- 2 - 2 - 1 1 2 - 1 2 1 -   - v - - - w x y - - z A -
- - - 2 2 1 1 1 2 2 1 - 1   - - - - - - - - - - - - B
>= 28

add above four constraint sets

10 12 12 12  8  5 10 12 11 11  7  8 12   o o - o o o o o o - o - o
12 12 12 12 12 12 12  6 12 11 12 10  6   o o - - o o o o - o - o -
12 12  0  8 12 12 12 12 12 12  - 12  8   - - o - - o - o - o - - o
12 12  8  8  8 12 12 10 10  4 12 12 12   o - - - - - - - - - - o -
 8 12 12  8  9 12  8 12 12  5 12 12 12   o o - - o - - - - - - - o
 5 12 12 12 12 12 12 11 12 11 12 11 11   o o o - - o o o - - o o o
 9 12 12 12  8 12  8 12 12 12 12 12 11   o o - - - o o o - - - o o
12 10 12 10 12 11 12 10 12 12 12 12 12   o o o - - o o o - - o o o
11 12 12 10 12 12 12 12 12 10 12 12 11   o - - - - - - - - - - - o
11 11 12  4  9 11 12 12 10  6 12 12 12   - o o - - - - - - - - o -
 7 12  - 12 12 12 12 12 12 12  - 12  9   o - - - - o - o - - - o o
 6 10 12 12 12 11 12 12 12 12 12  9  8   - o - o - o o o - o o o -
12  6  8 12 12 11 11 12 11 12  9  8  9   o - o - o o o o o - o - o
>= 292

divide by 12 and round

1 1 1 1 1 1 1 1 1 1 1 1 1   o o - o o o o o o - o - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o - - o o o o - o - o -
1 1 0 1 1 1 1 1 1 1 - 1 1   - - o - - o - o - o - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - o -
1 1 1 1 1 1 1 1 1 1 1 1 1   o o - - o - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o - - - o o o - - - o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   - o o - - - - - - - - o -
1 1 - 1 1 1 1 1 1 1 - 1 1   o - - - - o - o - - - o o
1 1 1 1 1 1 1 1 1 1 1 1 1   - o - o - o o o - o o o -
1 1 1 1 1 1 1 1 1 1 1 1 1   o - o - o o o o o - o - o
>= 25

=========================
13x13 proof Case 2B1

upper left and upper right (3,3) squares are unoccupied.
We must prove that 28 knights are required.


a8 constraint

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - 1 1 - 1 - 1 1 - 1 -   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 1 1 1 1   - - - - - - - - - - - - -
1 - 1 1 1 1 - 1 1 1 1 - 1   o - o - - o - o - - o - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
>= 8

seventeen single-square constraints

1 1 1 1 1 - 1 - 1 1 1 1 1   a b - - - - c - - - - d e
1 1 1 1 1 - 1 - 1 1 1 1 1   f g - - - - h - - - - i j
1 1 0 1 1 1 - 1 1 1 0 1 1   - - - - - - - - - - - - -
1 1 1 - - 2 - 2 - - 1 1 1   - - - - - - - - - - - - -
1 - 1 - 1 1 - 1 1 - 1 - 1   - - - - - - - - - - - - -
- - - 1 1 1 1 1 1 1 - - -   - - - - - - k - - - - - -
- 1 - - 2 - 1 - 2 - - 1 -   - l - - - - m - - - - n -
- - - 1 1 1 1 1 1 1 - - -   - - - - - - o - - - - - -
1 - 1 - 1 1 - 1 1 - 1 - 1   - - - - - - - - - - - - -
1 - 1 - - 1 - 1 - - 1 - 1   - - - - - - - - - - - - -
- - - 1 - - - - - 1 - - -   - - - - - - - - - - - - -
- 1 - - - - - - - - - 1 -   - p - - - - - - - - - q -
- - - 1 - - - - - 1 - - -   - - - - - - - - - - - - -
>= 17

add above two constraint sets

1 1 1 1 1 - 1 - 1 1 1 1 1   o o - - - - o - - - - o o
1 1 1 1 1 - 1 - 1 1 1 1 1   o o - - - - o - - - - o o
1 1 0 1 1 1 - 1 1 1 0 1 1   - - - - - - - - - - - - -
1 1 1 - - 2 - 2 - - 1 1 1   - - - - - - - - - - - - -
1 - 1 - 1 1 - 1 1 - 1 - 1   - - - - - - - - - - - - -
- - - 1 1 1 1 1 1 1 - - -   - - - - - - o - - - - - -
- 1 - - 2 - 1 - 2 - - 1 -   - o - - - - o - - - - o -
- - - 1 1 1 1 1 1 1 - - -   - - - - - - o - - - - - -
1 - 1 - 1 1 - 1 1 - 1 - 1   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 1 1 1 1   - - - - - - - - - - - - -
1 1 1 2 1 1 1 1 1 2 1 1 1   - - - - - - - - - - - - -
1 1 1 1 1 1 - 1 1 1 1 1 1   o o o - - o - o - - o o o
1 1 1 2 1 1 1 1 1 2 1 1 1   o o o - - o o o - - o o o
>= 25

multiply by 2

2 2 2 2 2 - 2 - 2 2 2 2 2   o o - - - - o - - - - o o
2 2 2 2 2 - 2 - 2 2 2 2 2   o o - - - - o - - - - o o
2 2 0 2 2 2 - 2 2 2 0 2 2   - - - - - - - - - - - - -
2 2 2 - - 4 - 4 - - 2 2 2   - - - - - - - - - - - - -
2 - 2 - 2 2 - 2 2 - 2 - 2   - - - - - - - - - - - - -
- - - 2 2 2 2 2 2 2 - - -   - - - - - - o - - - - - -
- 2 - - 4 - 2 - 4 - - 2 -   - o - - - - o - - - - o -
- - - 2 2 2 2 2 2 2 - - -   - - - - - - o - - - - - -
2 - 2 - 2 2 - 2 2 - 2 - 2   - - - - - - - - - - - - -
2 2 2 2 2 2 2 2 2 2 2 2 2   - - - - - - - - - - - - -
2 2 2 4 2 2 2 2 2 4 2 2 2   - - - - - - - - - - - - -
2 2 2 2 2 2 - 2 2 2 2 2 2   o o o - - o - o - - o o o
2 2 2 4 2 2 2 2 2 4 2 2 2   o o o - - o o o - - o o o
>= 50

two b4 constraints and two 3-in-a-row constraints

1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- 1 1 - - - - - - - 1 1 -   - - - - - - - - - - - - -
1 1 1 - - - - - - - 1 1 1   a - - - - - - - - - - - b
1 1 1 - - - - - - - 1 1 1   c - - - - - - - - - - - d
1 1 1 - - - - - - - 1 1 1   a - - - - - - - - - - - b
1 1 1 - - - - - - - 1 1 1   c - - - - - - - - - - - d
1 1 1 - - - - - - - 1 1 1   a - - - - - - - - - - - b
1 1 1 - - - - - - - 1 1 1   c - - - - - - - - - - - d
1 1 1 - - - - - - - 1 1 1   a - - - - - - - - - - - b
>= 12

twenty-seven single-square constraints

- 1 1 2 - 3 - 3 - 2 1 1 -   - a - b - c - d - e - f -
1 2 - 2 1 3 - 3 1 2 - 2 1   g - - - - h - i - - - - j
1 - 0 1 2 1 3 1 2 1 0 - 1   - - - - - - k - - - - - -
2 1 1 - 3 - 4 - 3 - 1 1 2   l - - - - - - - - - - - m
- 2 1 3 1 2 2 2 1 3 1 2 -   - - - - - - - - - - - - -
2 2 2 1 2 2 2 2 2 1 2 2 2   - n - - - o - p - - - q -
1 - 1 4 - 3 - 3 - 4 1 - 1   r - s - - t - u - - v - w
2 1 2 1 2 2 2 2 2 1 2 1 2   - x - - - y - z - - - A -
- 2 - 3 1 1 2 1 1 3 - 2 -   - - - - - - - - - - - - -
1 - 1 - 1 - 2 - 1 - 1 - 1   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
>= 27

add above three constraint sets

3 4 3 4 2 3 2 3 2 4 3 4 3   o o - o - o o o - o - o o
3 4 3 4 3 3 2 3 3 4 3 4 3   o o - - - o o o - - - o o
4 3 0 3 4 3 3 3 4 3 0 3 4   o - - - - - o - - - - - o
4 3 4 - 3 4 4 4 3 - 4 3 4   o - - - - - - - - - - - o
3 3 3 3 3 4 2 4 3 3 3 3 3   o - - - - - - - - - - - o
2 3 3 3 4 4 4 4 4 3 3 3 2   - o - - - o o o - - - o -
2 3 2 4 4 3 2 3 4 4 2 3 2   o o o - - o o o - - o o o
3 2 3 3 4 4 4 4 4 3 3 2 3   o o - - - o o o - - - o o
3 3 3 3 3 3 2 3 3 3 3 3 3   o - - - - - - - - - - - o
4 3 4 2 3 2 4 2 3 2 4 3 4   o - - - - - - - - - - - o
3 3 3 4 2 2 2 2 2 4 3 3 3   o - - - - - - - - - - - o
3 3 3 2 2 2 - 2 2 2 3 3 3   o o o - - o - o - - o o o
3 3 3 4 2 2 2 2 2 4 3 3 3   o o o - - o o o - - o o o
>= 89

multiply by 2

6 8 6 8 4 6 4 6 4 8 6 8 6   o o - o - o o o - o - o o
6 8 6 8 6 6 4 6 6 8 6 8 6   o o - - - o o o - - - o o
8 6 0 6 8 6 6 6 8 6 0 6 8   o - - - - - o - - - - - o
8 6 8 - 6 8 8 8 6 - 8 6 8   o - - - - - - - - - - - o
6 6 6 6 6 8 4 8 6 6 6 6 6   o - - - - - - - - - - - o
4 6 6 6 8 8 8 8 8 6 6 6 4   - o - - - o o o - - - o -
4 6 4 8 8 6 4 6 8 8 4 6 4   o o o - - o o o - - o o o
6 4 6 6 8 8 8 8 8 6 6 4 6   o o - - - o o o - - - o o
6 6 6 6 6 6 4 6 6 6 6 6 6   o - - - - - - - - - - - o
8 6 8 4 6 4 8 4 6 4 8 6 8   o - - - - - - - - - - - o
6 6 6 8 4 4 4 4 4 8 6 6 6   o - - - - - - - - - - - o
6 6 6 4 4 4 - 4 4 4 6 6 6   o o o - - o - o - - o o o
6 6 6 8 4 4 4 4 4 8 6 6 6   o o o - - o o o - - o o o
>= 178

d3 constraint

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - 1 1 1 1 - - - -   - - - - - - - - - - - - -
- - - - 1 1 - 1 1 1 - - -   - - - - - - - - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - - o o - - - - -
- - - - 1 1 1 - 1 1 - - -   - - - - - - o - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - - o o - - - - -
>= 3

d3 constraint

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - 1 1 1 1 - - - - -   - - - - - - - - - - - - -
- - - 1 1 1 - 1 1 - - - -   - - - - - - - - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - o o - - - - - -
- - - 1 1 - 1 1 1 - - - -   - - - - - - o - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - o o - - - - - -
>= 3

two a5 constraints and two 3-in-a-row constraints

1 - 1 - 1 - - - 1 - 1 - 1   c - c - c - - - d - d - d
1 - 1 - 1 - 2 - 1 - 1 - 1   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - - - - - - - - - 1 -   - - - - - - - - - - - - -
1 1 1 - - - - - - - 1 1 1   - - - - - - - - - - - - -
1 1 1 1 - - - - - 1 1 1 1   a - - - - - - - - - - - b
1 1 1 - - - - - - - 1 1 1   a a - - - - - - - - - b b
1 1 1 1 - - - - - 1 1 1 1   a - - - - - - - - - - - b
1 1 1 - - - - - - - 1 1 1   a - - - - - - - - - - - b
1 1 1 - - - - - - - 1 1 1   a - - - - - - - - - - - b
1 1 1 1 - - - - - 1 1 1 1   a - - - - - - - - - - - b
1 1 1 - - - - - - - 1 1 1   a a - - - - - - - - - b b
>= 14

twenty-five single-square constraints

1 1 1 - 1 1 - 1 1 - 1 1 1   a b - - - - - - - - - c d
1 - 1 1 1 - 1 - 1 1 1 - 1   e - - - - - f - - - - - g
1 1 0 - 1 - 1 - 1 - 0 1 1   - - - - - - h - - - - - -
- 2 - - 1 1 - 1 1 - - 2 -   - - - - - - - - - - - - -
1 2 2 1 1 1 2 1 1 1 2 2 1   - - - - - - - - - - - - -
2 - 1 2 1 1 - 1 1 2 1 - 2   i - - - - - - - - - - - j
1 1 2 - - 1 - 1 - - 2 1 1   k l m - - n - o - - p q r
1 1 1 2 1 1 - 1 1 2 1 1 1   - - - - - - - - - - - - -
1 2 1 1 1 - 2 - 1 1 1 2 1   - - - - - - - - - - - - -
- - - - - 1 - 1 - - - - -   - - - - - - - - - - - - -
1 1 1 - 2 1 1 1 1 - 1 1 1   - - - - - - - - - - - - -
- - 1 2 1 - 1 1 1 1 1 - -   - - - - - - s - - - - - -
1 1 - - 1 1 1 - 1 - - 1 1   t u - - - v w - - - - x y
>= 25

add above five constraint sets

8 9 8 8 6 7 4 7 6 8 8 9 8   o o o o o o o o o o o o o
8 8 8 9 8 6 7 6 8 9 8 8 8   o o - - - o o o - - - o o
9 8 0 7 9 7 7 7 9 7 0 8 9   o - - - - - o - - - - - o
8 8 8 - 7 9 8 9 7 - 8 8 8   o - - - - - - - - - - - o
7 9 8 7 7 9 6 9 7 7 8 9 7   o - - - - - - - - - - - o
7 7 8 8 9 9 8 9 9 8 8 7 7   o o - - - o o o - - - o o
6 8 7 9 8 7 4 7 8 9 7 8 6   o o o - - o o o - - o o o
8 6 8 8 9 9 8 9 9 8 8 6 8   o o - - - o o o - - - o o
8 9 8 8 8 8 8 8 8 8 8 9 8   o - - - - - - - - - - - o
9 7 9 5 8 7 8 7 8 5 9 7 9   o - - - - - - - - - - - o
8 8 8 8 8 7 7 7 7 8 8 8 8   o - - - - o o o - - - - o
7 7 8 8 7 5 3 6 7 7 8 7 7   o o o - - o o o - - o o o
8 8 7 8 7 7 7 6 7 8 7 8 8   o o o - - o o o - - o o o
>= 223

multiply by 2

16 18 16 16 12 14  8 14 12 16 16 18 16   o o o o o o o o o o o o o
16 16 16 18 16 12 14 12 16 18 16 16 16   o o - - - o o o - - - o o
18 16  0 14 18 14 14 14 18 14  0 16 18   o - - - - - o - - - - - o
16 16 16  - 14 18 16 18 14  - 16 16 16   o - - - - - - - - - - - o
14 18 16 14 14 18 12 18 14 14 16 18 14   o - - - - - - - - - - - o
14 14 16 16 18 18 16 18 18 16 16 14 14   o o - - - o o o - - - o o
12 16 14 18 16 14  8 14 16 18 14 16 12   o o o - - o o o - - o o o
16 12 16 16 18 18 16 18 18 16 16 12 16   o o - - - o o o - - - o o
16 18 16 16 16 16 16 16 16 16 16 18 16   o - - - - - - - - - - - o
18 14 18 10 16 14 16 14 16 10 18 14 18   o - - - - - - - - - - - o
16 16 16 16 16 14 14 14 14 16 16 16 16   o - - - - o o o - - - - o
14 14 16 16 14 10  6 12 14 14 16 14 14   o o o - - o o o - - o o o
16 16 14 16 14 14 14 12 14 16 14 16 16   o o o - - o o o - - o o o
>= 446

small triangle constraint

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - 1 - 1 - - - - -   - - - - - - - - - - - - -
- - - - 1 - 1 - 1 - - - -   - - - - - - - - - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - o - - - - - -
- - - - 1 1 - 1 1 - - - -   - - - - - o - o - - - - -
>= 2

two a3 constraints and three 3-in-a-row constraints

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - 1 - - - - - 1 - 1 -   - - - - - - - - - - - - -
1 - 1 - 1 - - - 1 - 1 - 1   - - - - - - - - - - - - -
1 1 1 1 - - - - - 1 1 1 1   a - a - - - - - - - b - b
1 1 1 - 1 - - - 1 - 1 1 1   - a - - - - - - - - - b -
1 1 1 1 - - - - - 1 1 1 1   a - a - - - - - - - b - b
1 - 1 - 1 - - - 1 - 1 - 1   - - - - - - - - - - - - -
- 1 - 1 - - - - - 1 - 1 -   - - - - - - - - - - - - -
- 1 - 1 - 1 1 1 1 1 1 1 1   - - - - - - - - - - - - -
1 - 1 - 1 1 2 1 1 1 1 1 1   - - - - - - - - - - - - -
1 - 1 - 1 - - 1 1 1 1 1 1   c - c - c - - d e d e d e
>= 12

two 3-in-a-row constraints and a b3 constraint

1 - 1 - 1 - - - 1 - 1 - 1   a - a - a - - - b - b - b
1 - 1 - 1 - 2 - 1 - 1 - 1   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - 1 - 1 - - - -   - - - - - - - - - - - - -
- - - - - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
- - - - 1 - 1 1 1 - 1 - 1   - - - - - - - c - - - - -
- - - - - 1 1 - 1 1 1 - 1   - - - - - - c - c - c - c
>= 7

two b3 constraints

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - 1 1 1 1 - - - - -   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 - - - -   - - - - - - - - - - - - -
1 1 1 1 1 2 2 1 1 1 - - -   - - - - - a b - - - - - -
1 1 1 2 2 1 1 2 - - - - -   a b a b a b a b - - - - -
>= 6

twenty-one single-square constraints

- - 1 2 1 1 1 1 1 2 1 - -   - - - - a - b - c - - - -
1 2 1 - 1 1 2 1 1 - 1 2 1   d e - - - f - g - - - h i
- 1 0 3 - 3 - 3 - 3 0 1 -   - - - - - - - - - - - - -
2 1 2 - 1 - 2 - 1 - 2 1 2   j - - - - - - - - - - - k
1 - 1 - - - - - - - 1 - 1   l - - - - - - - - - - - m
- 3 1 1 - - - - - 1 1 3 -   - - - - - - - - - - - - -
1 1 1 - 1 - - - 1 - 1 1 1   - - - - - - - - - - - - -
1 - 1 - - - - - - - 1 - 1   n - o - - - - - - - p - q
1 - 1 - 1 - - - 1 - 1 - 1   - - - - - - - - - - - - -
- 3 - 1 - - - - - 1 - 3 -   - - - - - - - - - - - - -
- - 1 - - 1 1 1 1 - 1 - -   - - - - - - - - - - - - -
1 - - - 1 1 - - 1 1 - - 1   r - - - - - - - - - - - s
- - 1 - - - 1 1 - - 1 - -   - - - - - - t u - - - - -
>= 21

add above six constraint sets

17 18 18 18 14 15  9 15 14 18 18 18 17   o o o o o o o o o o o o o
18 18 18 18 18 13 18 13 18 18 18 18 18   o o - - - o o o - - - o o
18 18  0 18 18 18 14 18 18 18  0 18 18   o - - - - - o - - - - - o
18 18 18  1 15 18 18 18 15  1 18 18 18   o - - - - - - - - - - - o
16 18 18 14 15 18 12 18 15 14 18 18 16   o - - - - - - - - - - - o
15 18 18 18 18 18 16 18 18 18 18 18 15   o o o - - o o o - - o o o
14 18 16 18 18 14  8 14 18 18 16 18 14   o o o - - o o o - - o o o
18 13 18 17 18 18 16 18 18 17 18 13 18   o o o - - o o o - - o o o
18 18 18 16 18 16 16 16 18 16 18 18 18   o - - - - - - - - - - - o
18 18 18 12 17 16 18 16 17 12 18 18 18   o - - - - - - - - - - - o
17 18 18 18 18 18 18 18 18 18 18 18 17   o - - - - o o o - - - - o
17 15 18 18 18 15 12 16 18 18 18 15 17   o o o - - o o o - - o o o
18 17 17 18 18 17 17 17 17 18 17 17 18   o o o o o o o o o o o o o
>= 494

divide by 18 and round

1 1 1 1 1 1 1 1 1 1 1 1 1   o o o o o o o o o o o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o - - - o o o - - - o o
1 1 0 1 1 1 1 1 1 1 0 1 1   o - - - - - o - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - o o o - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o o o o o o o o o o o
>= 28

=========================
13x13 proof case 2B2

upper left and lower right (3,3) squares are unoccupied.
We must prove that 28 knights are required.


four single-square constraints
multiplied by 2

- 2 2 - - - - - - - - - -   - a - - - - - - - - - - -
2 - - 2 - - - - - - - - -   b - - - - - - - - - - - -
2 - 0 - - - - - - - - - -   - - - - - - - - - - - - -
- 2 - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - 2 -   - - - - - - - - - - - - -
- - - - - - - - - - 0 - 2   - - - - - - - - - - - - -
- - - - - - - - - 2 - - 2   - - - - - - - - - - - - c
- - - - - - - - - - 2 2 -   - - - - - - - - - - - d -
>= 8

twenty-four single-square constraints

1 - - 1 1 - 1 1 1 1 1 1 1   a - - - - - b c - - - d e
- 1 1 - 1 1 1 - 1 2 1 1 1   - f - - - - g - - - - h i
- 1 - 1 1 1 1 1 2 1 2 1 1   - - - - - - - - - - - - -
1 - 1 - - 1 - 1 - - 1 2 1   - - - - - - - - - - - - -
1 1 1 - - - - - - - 2 1 1   - - - - - - - - - - - - -
- 1 1 1 - - - - - 1 1 - 1   - - - - - - - - - - - - j
1 1 1 - - - - - - - 1 1 1   k l - - - - - - - - - m n
1 - 1 1 - - - - - 1 1 1 -   o - - - - - - - - - - - -
1 1 2 - - - - - - - 1 1 1   - - - - - - - - - - - - -
1 2 1 - - 1 - 1 - - 1 - 1   - - - - - - - - - - - - -
1 1 2 1 2 1 1 1 1 1 - 1 -   - - - - - - - - - - - - -
1 1 1 2 1 - 1 1 1 - 1 1 -   p q - - - - r - - - - s -
1 1 1 1 1 1 1 - 1 1 - - 1   t u - - - v w - - - - - x
>= 24

add above two constraint sets

1 2 2 1 1 - 1 1 1 1 1 1 1   o o - - - - o o - - - o o
2 1 1 2 1 1 1 - 1 2 1 1 1   o o - - - - o - - - - o o
2 1 0 1 1 1 1 1 2 1 2 1 1   - - - - - - - - - - - - -
1 2 1 - - 1 - 1 - - 1 2 1   - - - - - - - - - - - - -
1 1 1 - - - - - - - 2 1 1   - - - - - - - - - - - - -
- 1 1 1 - - - - - 1 1 - 1   - - - - - - - - - - - - o
1 1 1 - - - - - - - 1 1 1   o o - - - - - - - - - o o
1 - 1 1 - - - - - 1 1 1 -   o - - - - - - - - - - - -
1 1 2 - - - - - - - 1 1 1   - - - - - - - - - - - - -
1 2 1 - - 1 - 1 - - 1 2 1   - - - - - - - - - - - - -
1 1 2 1 2 1 1 1 1 1 0 1 2   - - - - - - - - - - - - -
1 1 1 2 1 - 1 1 1 2 1 1 2   o o - - - - o - - - - o o
1 1 1 1 1 1 1 - 1 1 2 2 1   o o - - - o o - - - - o o
>= 32

multiply by 2

2 4 4 2 2 - 2 2 2 2 2 2 2   o o - - - - o o - - - o o
4 2 2 4 2 2 2 - 2 4 2 2 2   o o - - - - o - - - - o o
4 2 0 2 2 2 2 2 4 2 4 2 2   - - - - - - - - - - - - -
2 4 2 - - 2 - 2 - - 2 4 2   - - - - - - - - - - - - -
2 2 2 - - - - - - - 4 2 2   - - - - - - - - - - - - -
- 2 2 2 - - - - - 2 2 - 2   - - - - - - - - - - - - o
2 2 2 - - - - - - - 2 2 2   o o - - - - - - - - - o o
2 - 2 2 - - - - - 2 2 2 -   o - - - - - - - - - - - -
2 2 4 - - - - - - - 2 2 2   - - - - - - - - - - - - -
2 4 2 - - 2 - 2 - - 2 4 2   - - - - - - - - - - - - -
2 2 4 2 4 2 2 2 2 2 0 2 4   - - - - - - - - - - - - -
2 2 2 4 2 - 2 2 2 4 2 2 4   o o - - - - o - - - - o o
2 2 2 2 2 2 2 - 2 2 4 4 2   o o - - - o o - - - - o o
>= 64

two b4 constraints

1 - 1 - 1 - 1 - 1 - 1 - 1   a - a - a - a - a - a - a
1 - 1 - 1 - 1 - 1 - 1 - 1   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
1 - 1 - 1 - 1 - 1 - 1 - 1   - - - - - - - - - - - - -
1 - 1 - 1 - 1 - 1 - 1 - 1   b - b - b - b - b - b - b
>= 8

two b4 constraints

1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
>= 8

seven a3 constraints

- - - - 1 1 1 1 1 1 1 1 1   - - - - - a - a - - b - b
- - - 1 - 1 1 1 1 1 1 1 1   - - - - - - a - - - - b -
- - - - 1 1 1 1 1 1 1 1 1   - - - - - a - a - - b - b
- 1 - 2 1 1 1 1 2 2 1 1 1   - - - - - - - - - - - - -
1 - 1 1 2 1 1 1 2 2 1 1 1   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 1 1 1 1   c - c - - d - d - - e - e
1 1 1 1 1 1 1 1 1 1 1 1 1   - c - - - - d - - - - e -
1 1 1 1 1 1 1 1 1 1 1 1 1   c - c - - d - d - - e - e
1 1 1 2 2 1 1 1 2 1 1 - 1   - - - - - - - - - - - - -
1 1 1 2 2 1 1 1 1 2 - 1 -   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 - - - -   f - f - - g - g - - - - -
1 1 1 1 1 1 1 1 - 1 - - -   - f - - - - g - - - - - -
1 1 1 1 1 1 1 1 1 - - - -   f - f - - g - g - - - - -
>= 21

twenty-five single-square constraints

- - - 3 - 1 - 2 - 1 - - -   - - - a - - - - - - - - -
- 3 - - 1 2 - - 1 - - 1 -   - b - - - c - - - - - d -
- - 0 2 1 - 1 1 - 1 - - -   - - - - - - e - - - - - -
3 - 2 - 3 1 3 1 2 - 1 - 1   f - - - - - - - - - - - -
- 1 1 3 2 3 2 3 2 2 - 1 -   - - - - - - - - - - - - -
1 2 - 1 3 3 3 3 3 1 1 - 2   - g - - - h i j - - - - -
- - 1 3 2 3 1 3 2 3 1 - -   - - k - - l m n - - o - -
2 - 1 1 3 3 3 3 3 1 - 2 1   - - - - - p q r - - - s -
- 1 - 2 2 3 2 3 2 3 1 1 -   - - - - - - - - - - - - -
1 - 1 - 2 1 3 1 3 - 2 - 2   - - - - - - - - - - - - t
- - - 1 - 1 1 - 1 2 0 - -   - - - - - - u - - - - - -
- 1 - - 1 - - 2 1 - - 3 -   - v - - - - - w - - - x -
- - - 1 - 2 - 1 - 2 - - -   - - - - - - - - - y - - -
>= 25

add above five constraint sets

4 5 5 5 4 2 4 5 4 4 4 4 5   o o o o o o o o o - o o o
5 5 4 5 4 5 4 1 5 5 5 4 4   o o - - - o o - - - - o o
5 4 0 5 4 4 4 5 5 5 5 5 4   o - - - - o o o - - o - o
5 5 5 2 4 4 4 4 4 2 5 5 4   o - - - - - - - - - - - -
4 4 4 4 4 4 3 4 4 4 5 5 4   o - - - - - - - - - - - o
2 5 4 4 4 4 4 4 4 4 5 1 5   o o o - - o o o - - o - o
4 4 4 4 3 4 2 4 3 4 4 4 4   o o o - - o o o - - o o o
5 1 5 4 4 4 4 4 4 4 4 5 2   o - o - - o o o - - o o o
4 5 5 4 4 4 3 4 4 4 4 4 4   o - - - - - - - - - - - o
4 5 5 2 4 4 4 4 4 2 5 5 4   - - - - - - - - - - - - o
4 5 5 5 5 5 4 4 4 5 0 4 5   o - o - - o o o - - - - o
4 4 5 5 5 1 4 5 4 5 4 5 5   o o - - - - o o - - - o o
5 4 4 4 4 5 4 2 4 4 5 5 4   o o o - o o o o o o o o o
>= 126

multiply by 2

 8 10 10 10  8  4  8 10  8  8  8  8 10   o o o o o o o o o - o o o
10 10  8 10  8 10  8  2 10 10 10  8  8   o o - - - o o - - - - o o
10  8  0 10  8  8  8 10 10 10 10 10  8   o - - - - o o o - - o - o
10 10 10  4  8  8  8  8  8  4 10 10  8   o - - - - - - - - - - - -
 8  8  8  8  8  8  6  8  8  8 10 10  8   o - - - - - - - - - - - o
 4 10  8  8  8  8  8  8  8  8 10  2 10   o o o - - o o o - - o - o
 8  8  8  8  6  8  4  8  6  8  8  8  8   o o o - - o o o - - o o o
10  2 10  8  8  8  8  8  8  8  8 10  4   o - o - - o o o - - o o o
 8 10 10  8  8  8  6  8  8  8  8  8  8   o - - - - - - - - - - - o
 8 10 10  4  8  8  8  8  8  4 10 10  8   - - - - - - - - - - - - o
 8 10 10 10 10 10  8  8  8 10  0  8 10   o - o - - o o o - - - - o
 8  8 10 10 10  2  8 10  8 10  8 10 10   o o - - - - o o - - - o o
10  8  8  8  8 10  8  4  8  8 10 10  8   o o o - o o o o o o o o o
>= 252

two b4 constraints

1 - 1 - 1 - 1 - 1 - 1 - 1   a - a - a - a - a - a - a
1 - 1 - 1 - 1 - 1 - 1 - 1   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
1 - 1 - 1 - 1 - 1 - 1 - 1   - - - - - - - - - - - - -
1 - 1 - 1 - 1 - 1 - 1 - 1   b - b - b - b - b - b - b
>= 8

two b4 constraints

1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
- - 1 - - - - - - - 1 - -   - - - - - - - - - - - - -
1 1 - - - - - - - - - 1 1   a - - - - - - - - - - - b
>= 8

five a3 constraints

- - - - 1 1 1 1 1 - - - -   - - - - - a - a - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - a - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - a - a - - - - -
- 1 - 2 1 1 1 1 1 2 - 1 -   - - - - - - - - - - - - -
1 - 1 1 2 1 1 1 2 1 1 - 1   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 1 1 1 1   b - b - - c - c - - d - d
1 1 1 1 1 1 1 1 1 1 1 1 1   - b - - - - c - - - - d -
1 1 1 1 1 1 1 1 1 1 1 1 1   b - b - - c - c - - d - d
1 - 1 1 2 1 1 1 2 1 1 - 1   - - - - - - - - - - - - -
- 1 - 2 1 1 1 1 1 2 - 1 -   - - - - - - - - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - e - e - - - - -
- - - 1 - 1 1 1 - 1 - - -   - - - - - - e - - - - - -
- - - - 1 1 1 1 1 - - - -   - - - - - e - e - - - - -
>= 15

forty-five single-square constraints

1 1 1 2 2 3 1 1 1 1 1 1 -   a - - b c d - - - - - e -
1 2 2 1 3 1 2 2 1 1 - - 1   - - - - f - g h - - - - i
1 2 0 1 3 2 3 - 1 1 2 - 1   - - j - - - k - - - - - -
2 1 1 1 3 3 3 2 3 - 1 1 1   l - - - - - - - - - - - -
2 3 3 3 2 3 2 3 2 3 1 1 1   m n - - - - - - - - - - -
3 1 2 3 3 3 3 3 3 2 - 2 -   o - - - - p q r - - - s -
1 2 3 3 2 3 1 3 2 3 3 2 1   - t u - - v w x - - y z -
1 2 - 2 3 3 3 3 3 3 2 1 3   - A - - - B C D - - - - E
1 1 1 3 2 3 2 3 2 3 3 2 2   - - - - - - - - - - - F G
1 1 1 - 3 2 3 3 3 2 1 1 2   - - - - - - - - - - - - H
1 - 2 1 1 - 3 2 3 1 0 2 1   - - - - - - I - - - J - -
1 - - 1 1 1 2 1 3 1 2 2 1   K - - - - L M - N - - - -
- 1 1 1 1 1 1 2 2 2 1 1 1   - O - - - - - P Q R - - S
>= 45

add above five constraint sets

11 12 12 12 12  8 11 12 11  9 10 10 12   o o o o o o o o o - o o o
12 12 12 12 12 12 12  5 12 12 12  8 10   o o - - o o o o - - - o o
12 12  0 12 12 12 12 12 12 12 12 12 10   o - o - - o o o - - o - o
12 12 12  7 12 12 12 11 12  6 12 12  9   o - - - - - - - - - - - -
12 12 12 12 12 12  9 12 12 12 12 12 11   o o - - - - - - - - - - o
 8 12 12 12 12 12 12 12 12 11 12  5 11   o o o - - o o o - - o o o
11 12 12 12  9 12  6 12  9 12 12 12 11   o o o - - o o o - - o o o
12  5 12 11 12 12 12 12 12 12 12 12  8   o o o - - o o o - - o o o
11 12 12 12 12 12  9 12 12 12 12 11 12   o - - - - - - - - - - o o
 9 12 12  6 12 11 12 12 12  8 12 12 10   - - - - - - - - - - - - o
10 12 12 12 12 12 12 12 12 12  0 12 12   o - o - - o o o - - o - o
10  8 12 12 12  4 12 12 12 12 12 12 12   o o - - - o o o o - - o o
12 10 10  9 11 12 11  7 12 10 12 12 11   o o o - o o o o o o o o o
>= 328

divide by 12 and round

1 1 1 1 1 1 1 1 1 1 1 1 1   o o o o o o o o o - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o - - o o o o - - - o o
1 1 0 1 1 1 1 1 1 1 1 1 1   o - o - - o o o - - o - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 1 1 1 1   o o - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o - - - - - - - - - - o o
1 1 1 1 1 1 1 1 1 1 1 1 1   - - - - - - - - - - - - o
1 1 1 1 1 1 1 1 1 1 0 1 1   o - o - - o o o - - o - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o - - - o o o o - - o o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - o o o o o o o o o
>= 28

=========================
Constraint derivations for configurations used in the proofs.

The first group are all constraints consisting of
three-square configurations.
It is easy to see that one knight can't cover all three squares
of a configuration, so it takes at least two knights.
These constraints are valid anywhere on the board.

=========================
3-in-a-row constraint

- 1 - 1 -   - - - - -
1 - - - 1   - - - - -
- 1 1 1 -   - - o - -
1 - - - 1   - - - - -
- 1 1 1 -   - - o - -
1 - - - 1   - - - - -
- 1 1 1 -   - - o - -
1 - - - 1   - - - - -
- 1 - 1 -   - - - - -
>= 2

=========================
curve constraint

- 1 - 1 - - -   - - - - - - -
1 - 1 - 1 - -   - - - - - - -
- 1 1 - - 1 -   - - o - - - -
1 - - 1 1 - -   - - - o - - -
- 1 - 1 - 1 -   - - - - - - -
- - 1 - 1 - 1   - - - - - - -
- - - - 1 - -   - - - - o - -
- - 1 - - - 1   - - - - - - -
- - - 1 - 1 -   - - - - - - -
>= 2

=========================
large triangle constraint

- 1 - 1 - 1 -   - - - - - - -
1 - 1 - 1 - 1   - - - - - - -
- - 1 - 1 - -   - - o - o - -
1 - 1 - 1 - 1   - - - - - - -
- 1 - 1 - 1 -   - - - - - - -
- - - 1 - - -   - - - o - - -
- 1 - - - 1 -   - - - - - - -
- - 1 - 1 - -   - - - - - - -
>= 2

=========================
small triangle constraint
 
- 1 - 1 - -   - - - - - -
1 - 1 - 1 -   - - - - - -
- 1 1 1 - 1   - - o - - -
1 - - 1 1 -   - - - o - -
- 1 1 1 - 1   - - o - - -
1 - 1 - 1 -   - - - - - -
- 1 - 1 - -   - - - - - -
>= 2

=========================

Derivations of constraints that take 3 or more knights.

=========================
a3 constraint derivation

five single-square constraints

- 1 - 2 - 1 -   - - - - - - -
1 - 2 - 2 - 1   - - - - - - -
- 2 1 2 1 2 -   - - a - b - -
2 - 2 1 2 - 2   - - - c - - -
- 2 1 2 1 2 -   - - d - e - -
1 - 2 - 2 - 1   - - - - - - -
- 1 - 2 - 1 -   - - - - - - -
>= 5

divide by 2 and round

- 1 - 1 - 1 -   - - - - - - -
1 - 1 - 1 - 1   - - - - - - -
- 1 1 1 1 1 -   - - o - o - -
1 - 1 1 1 - 1   - - - o - - -
- 1 1 1 1 1 -   - - o - o - -
1 - 1 - 1 - 1   - - - - - - -
- 1 - 1 - 1 -   - - - - - - -
>= 3

=========================
b3 constraint derivation

3-in-a-row constraint

- - - - - - - - - - -   - - - - - - - - - - -
- 1 - 1 - 1 - 1 - - -   - - - - - - - - - - -
1 - 1 - 1 - 1 - 1 - -   - - - - - - - - - - -
- - 1 - 1 - 1 - - - -   - - o - o - o - - - -
>= 2

three single-square constraints

- - - - - - 1 - 1 - -   - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 2 -   - - - - - - - - - - -
1 - - - 1 - 1 1 - - 1   - - - - - - - b - - -
- - 1 - - 1 - - 1 1 -   - - a - - - - - c - -
>= 3

add above two constraints

- - - - - - 1 - 1 - -   - - - - - - - - - - -
- 2 - 2 - 2 - 2 - 2 -   - - - - - - - - - - -
2 - 1 - 2 - 2 1 1 - 1   - - - - - - - o - - -
- - 2 - 1 1 1 - 1 1 -   - - o - o - o - o - -
>= 5

divide by 2 and round

- - - - - - 1 - 1 - -   - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - -
1 - 1 - 1 - 1 1 1 - 1   - - - - - - - o - - -
- - 1 - 1 1 1 - 1 1 -   - - o - o - o - o - -
>= 3

=========================
c3 constraint derivation

3-in-a-row constraint

1 - 1 - 1 - - -   o - o - o - - -
1 - 1 - 1 - 1 -   - - - - - - - -
- 1 - 1 - 1 - -   - - - - - - - -
- - - - - - - -   - - - - - - - -
- - - - - - - -   - - - - - - - -
- - - - - - - -   - - - - - - - -
>= 2

small triangle constraint

- 1 1 1 - 1 - -   - - o - - - - -
1 1 - 1 1 - - -   - o - o - - - -
- 1 - 1 - 1 - -   - - - - - - - -
1 - 1 - 1 - - -   - - - - - - - -
- - - - - - - -   - - - - - - - -
- - - - - - - -   - - - - - - - -
>= 2

single-square constraint

- 1 - - - - - -   - - - - - - - -
- - 1 - - - - -   - - - - - - - -
1 - - - - - - -   o - - - - - - -
- - 1 - - - - -   - - - - - - - -
- 1 - - - - - -   - - - - - - - -
- - - - - - - -   - - - - - - - -
>= 1

add above three constraints

1 2 2 1 1 1 - -   o - o - o - - -
2 1 2 1 2 - 1 -   - o - o - - - -
1 2 - 2 - 2 - -   o - - - - - - -
1 - 2 - 1 - - -   - - - - - - - -
- 1 - - - - - -   - - - - - - - -
- - - - - - - -   - - - - - - - -
>= 5

divide by 2 and round

1 1 1 1 1 1 - -   o - o - o - - -
1 1 1 1 1 - 1 -   - o - o - - - -
1 1 - 1 - 1 - -   o - - - - - - -
1 - 1 - 1 - - -   - - - - - - - -
- 1 - - - - - -   - - - - - - - -
- - - - - - - -   - - - - - - - -
>= 3

=========================
d3 constraint derivation

five single-square constraints

- 1 1 2 1 1 -   - - - - - - -
1 2 1 2 1 2 1   - - - - - - -
1 - 2 1 2 - 1   - - a b c - -
1 1 2 - 2 1 1   - - d - e - -
1 1 2 2 2 1 1   - - - - - - -
- 1 - 2 - 1 -   - - - - - - -
>= 5

divide by 2 and round

- 1 1 1 1 1 -   - - - - - - -
1 1 1 1 1 1 1   - - - - - - -
1 - 1 1 1 - 1   - - o o o - -
1 1 1 - 1 1 1   - - o - o - -
1 1 1 1 1 1 1   - - - - - - -
- 1 - 1 - 1 -   - - - - - - -
>= 3

=========================
a4 constraint derivation

three single-square constraints

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - 1 - 1 - - - -   - - - - - - - - - - - - -
- - - - - 2 - 1 - 2 - 1 -   - - - - - - - - - - - - -
- - - - 1 - - 1 2 - - - 1   - - - - - - - b - - - - -
- - - - - 1 1 - - 1 1 - -   - - - - - - a - - - c - -
>= 3

divide by 2 and round

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - 1 - 1 - - - -   - - - - - - - - - - - - -
- - - - - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
- - - - 1 - - 1 1 - - - 1   - - - - - - - o - - - - -
- - - - - 1 1 - - 1 1 - -   - - - - - - o - - - o - -
>= 2

3-in-a-row constraint

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - 1 - 1 - - - - - - -   - - - - - - - - - - - - -
1 - 1 - 1 - 1 - - - - - -   - - - - - - - - - - - - -
1 - 1 - 1 - - - - - - - -   o - o - o - - - - - - - -
>= 2

three single-square constraints

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - 1 - 1 - - - - - -   - - - - - - - - - - - - -
- 1 - 1 - - - 1 - 1 - 1 -   - - - - - - - - - - - - -
- - 1 - - 1 - - 1 - - - 1   - - - - - b - - - - - - -
1 - - 1 - - - 1 - - 1 - -   a - - - - - - - - - c - -
>= 3

add above three constraints

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - 1 - 2 - 1 - - - -   - - - - - - - - - - - - -
- 2 - 2 - 2 - 2 - 2 - 2 -   - - - - - - - - - - - - -
1 - 2 - 2 1 1 1 2 - - - 2   - - - - - o - o - - - - -
2 - 1 1 1 1 1 1 - 1 2 - -   o - o - o - o - - - o - -
>= 7

divide by 2 and round

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - 1 - 1 - 1 - - - -   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
1 - 1 - 1 1 1 1 1 - - - 1   - - - - - o - o - - - - -
1 - 1 1 1 1 1 1 - 1 1 - -   o - o - o - o - - - o - -
>= 4

=========================
b4 constraint derivation

seven single-square constraints

1 - 1 - 1 - 1 - 1 - 1 - 1   a - b - c - d - e - f - g
1 - 2 - 2 - 2 - 2 - 2 - 1   - - - - - - - - - - - - -
- 2 - 2 - 2 - 2 - 2 - 2 -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
>= 7

divide by 2 and round

1 - 1 - 1 - 1 - 1 - 1 - 1   o - o - o - o - o - o - o
1 - 1 - 1 - 1 - 1 - 1 - 1   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - 1 - 1 -   - - - - - - - - - - - - -
- - - - - - - - - - - - -   - - - - - - - - - - - - -
>= 4

=========================
a5 constraint derivation

b3 constraint

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- - - - 1 - 1 - - - - - -   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - - - - -   - - - - - - - - - - - - -
1 - 1 - 1 1 1 - 1 - - - -   - - - - - o - - - - - - -
1 - 1 1 1 - 1 1 - - - - -   o - o - o - o - - - - - -
>= 3

3-in-a-row constraint

- - - - - - - - - - - - -   - - - - - - - - - - - - -
1 - 1 - 1 - 1 - - - - - -   - - - - - - - - - - - - -
- 1 - 1 - 1 - 1 - - - - -   - - - - - - - - - - - - -
- 1 - 1 - 1 - - - - - - -   - o - o - o - - - - - - -
>= 2

four single-square constraints

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 1 - 1 1 1 1 - - - - -   - - - - - - - - - - - - -
1 - 1 1 1 - - 1 1 - - - -   a - - - - - - - - - - - -
1 1 - - - 1 1 - - - - - -   b - - - - c d - - - - - -
>= 4

add above three constraint sets

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - - 1 - 1 - - - - - -   - - - - - - - - - - - - -
1 2 2 1 2 2 2 2 - - - - -   - - - - - - - - - - - - -
2 1 2 2 2 2 1 2 2 - - - -   o - - - - o - - - - - - -
2 2 1 2 1 2 2 1 - - - - -   o o o o o o o - - - - - -
>= 9

divide by 2 and round

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - - 1 - 1 - - - - - -   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 - - - - -   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 - - - -   o - - - - o - - - - - - -
1 1 1 1 1 1 1 1 - - - - -   o o o o o o o - - - - - -
>= 5

=========================
a8 constraint derivation

fifteen single-square constraints

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 2 - 1 1 - 2 - 1 1 - 2 -   - - - - - - - - - - - - -
2 2 2 2 2 2 2 2 2 2 2 2 2   - - - - - - - - - - - - -
2 - 2 2 2 2 - 2 2 2 2 - 2   a - b - - c - d - - e - f
2 1 2 1 1 2 1 2 1 1 2 1 2   g h i - - j k l - - m n o
>= 15

divide by 2 and round

- - - - - - - - - - - - -   - - - - - - - - - - - - -
- 1 - 1 1 - 1 - 1 1 - 1 -   - - - - - - - - - - - - -
1 1 1 1 1 1 1 1 1 1 1 1 1   - - - - - - - - - - - - -
1 - 1 1 1 1 - 1 1 1 1 - 1   o - o - - o - o - - o - o
1 1 1 1 1 1 1 1 1 1 1 1 1   o o o - - o o o - - o o o
>= 8