signature { automatic } theory
{
n1:<>(!((<>(n1 & p1) & <>(n1 & p2))-> <>(p1 & p2)));
<>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(n2:n1)))))));
[]!p1;
[][]!p1;
[][][]!p1;
[][][][]!p1;
[][][][][]!p1;
n2:<>true
}