HTab-1.6.1: examples/unsat/test15.frm

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