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