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