Logical System
◊ S5 world, k, must be new [here the computer will choose for you]
□ S5 any world, stage 1, your choice
□ S5 any world, stage 2, w chosen
