The Possible Asylum

The Impossible Asylum" showing, using automated reasoning tools, that the last puzzle of Raymond Smullyan's article "The Asylum of Doctor Tarr and Professor Fether" is inconsistent.We here argue to the contrary: the puzzle is consistent after all.Our solution was also found using automated reasoning and is small enough to be presented here.In fact, the smallest asylum satisfying the original puzzle is only inhabited by four persons.So how can we explain this discrepancy, where on the one hand we have a formal proof of inconsistency and other hand a satisfying assignment?Well, this is due to an ambiguity in the natural language statement of the original puzzle.We will argue that with a more natural reading of the original puzzle, its logical representation changes ever-so-slightly and becomes consistent.