HTab-1.5.4: examples/sat/test15.frm

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