The Missionaries and Cannibals Puzzle

There are three missionaries and three cannibals on the west bank of a river. There is a boat on the west bank that can hold no more than two people. The missionaries wish to cross to the east bank. But they have a problem: If on either bank the cannibals ever outnumber the missionaries, the outnumbered missionaries will be eaten.

Question: Is there a way for the missionaries to get their wish--to get to the east bank without losing anyone?

Application: This puzzle is vaguely reminiscent of scheduling problems. For example, a number of meetings must be held, some of which must run in parallel. Various constraints exist on scheduling all the meetings. Some must precede others, while some must not be held in parallel. Certain speakers have prior travel arrangements, and so must give various talks consistent with their prior plans. The question is: With all of the constraints, does a schedule exist that conforms to the requirements?

A detailed discussion of this puzzle and others is given in Automated Reasoning: Introduction and Applications, by Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. The book, published by McGraw-Hill, includes a diskette of the automated reasoning program OTTER, which can be used to solve puzzles as well as extremely challenging problems in mathematics and logic.

Those who have OTTER already may simply take the input and start experimenting. The clauses are explained separately.