signature { automatic } theory
{ 
!((!<>(n1:n3 v <>(p1 <--> []p3)) & <>(n3:<>p1 --> [](p3 v <>(p4 <-->
<>p2)))) --> <>(!(n1:n3 v <>(p1 <--> []p3) & (n3:<>p1 --> [](p3 v <>(p4 <-->
<>p2)))))) 
}