Статья описывает применение системы проверки моделей SPIN к решению японской головоломки о переправе через реку (продвинутый вариант задачи о волке, козе и капусте) и головоломки "Irregular IQ Cube" (также называемой "Куб-1").