“Once upon a time, three cannibals were guiding three missionaries through a jungle. They were on their way to the nearest mission station. After some time, they arrived at a wide river, filled with deadly snakes and fish. There was no way to cross the river without a boat. Fortunately, they found a rowing boat with two oars after a short search. Unfortunately, the boat was too small to carry all of them. It could barely carry two people at a time. Worse, because of the river’s width someone had to row the boat back.
“Since the missionaries could not trust the cannibals, they had to figure out a plan to get all six of them safely across the river. The problem was that these cannibals would kill and eat missionaries as soon as there were more cannibals than missionaries at some place. Thus our missionaries had to devise a plan that guaranteed that there were never any missionaries in the minority at either side of the river. The cannibals, however, could be trusted to cooperate otherwise. Specifically, they wouldn’t abandon any potential food, just as the missionaries wouldn’t abandon any potential converts.”
Formulate a reduction system that solves this puzzle. Use traces to visualize the solution space. You want to impose a side condition on the rules so that no boat is sent back to the other side of the river when a configuration represents a solutions. The other side conditions just ensure that no missionary will be eaten.
Consider running traces with a subject-reduction test. The predicate you want to check is that the parties on both sides of the river are safe.