[Part 8] Raymond Smullyan's Knights, Knaves, and Normals puzzles Fourth puzzle, on the island of Bahava

For our fourth puzzle, we will use the \(46^{th}\) (and last) puzzle in Chapter 3 of Raymond Smullyan's 1978 book entitled "What Is the Name of This Book?: The Riddle of Dracula and Other Logical Puzzles". This puzzle takes place again on the island of Bahava, on which marriage is highly regulated. As stated on pages 25-26 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

[...] Thus, given any married couple, either they are both normal, or one of them is a knight and the other a knave. [...]

This problem concerns two married couples on the island of Bahava, Mr. and Mrs. A, and Mr. and Mrs. B. They are being interviewed, and three of the four people give the following testimony:

Mr. A: Mr B. is a knight.

Mrs. A: My husband is right; Mr. B is a knight.  

Mrs. B: That's right. My husband is indeed a knight.  

What are each of the four people, and which of the three statements are true?

As always in this series, the following axioms represent the possible types for all inhabitants:

Kni(x) | Kna(x) | Nor(x).

-Kni(x) | -Kna(x).

-Kni(x) | -Nor(x).

-Kna(x) | -Nor(x).

Like in the previous post, we represent the fact that two inhabitants A and B are married with the formula:

Mar(A,B).

 Since the "married" relationship is symmetrical, we add the following axiom:

Mar(x,y) -> Mar(y,x).

Then we represent the marriage restrictions based on types with the axiom:

Mar(x,y) -> ((Nor(x) & Nor(y)) | (Kni(x) & Kna(y))).

Finally, we encode the fact that polygamy is not allowed with the axiom:

(Mar(x,y) & Mar(x,z)) -> y = z.

This concludes our representation of the island of Bahava's general conditions.

Turning to our specific puzzle, we represent the fact that we have two couples made of four distinct islanders, and that there are no other islanders in this puzzle, as follows:

Mar(MrA,MrsA).

Mar(MrB,MrsB).

MrA != MrsA & MrA != MrB & ...  [formula continued on the next line]

... MrA != MrsB & MrsA != MrB & MrsA != MrsB | MrB != MrsB.

x = MrA | x = MrsA | x = MrB | x = MrsB.

Finally, we represent the three statements using our usual representation principle for the knights/knaves/normals puzzle, yielding the three formulas:

(Kni(MrA) & Kni(MrB)) | (Kna(MrA) & -Kni(MrB)) | Nor(MrA). 

(Kni(MrsA) & Kni(MrB)) | (Kna(MrsA) & -Kni(MrB)) | Nor(MrsA). 

(Kni(MrsB) & Kni(MrB)) | (Kna(MrsB) & -Kni(MrB)) | Nor(MrsB).

The entire input given to Mace4 is thus:

and its output is:

The only model in this output demonstrates that there is only one solution to this puzzle: all four islanders are normals; therefore all three statements are false.