This is an example of how certain logic Puzzles can be solved using a model checker for monadic predicate logic with identity. Specifically it has been written to solve some of the puzzles in Chapter VIII of Raymond Smullyan's book The Riddle of Scheherazade.
A series of articles explaining how the solver works can be found here: Solving Logic Puzzles Automatically (With Swift).