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