HTab-1.6.1: examples/unsat/test14.frm

begin
!((!<>(n1:n3 v <>(p1 <--> []p3)) & <>(n3:<>p1 --> [](p3 v <>(p4 <-->
<>p2)))) --> <>(!(n1:n3 v <>(p1 <--> []p3) & (n3:<>p1 --> [](p3 v <>(p4 <-->
<>p2)))))) 
end