hylotab-1.2.0: examples/unsat/form20.frm

begin
-(
   (
      (<><><><>(@ n1 n2))
      &
         @ n1 (
                 ([]<>(p1 v @ n2 (p1 <--> <>p3)))
                 ->
                 (<>p1 <--> []<>(@n2 (n3 & P4)))
              )
   )

   ->

   (
      @ n2 ([]<>(p1 v @ n2 (p1 <--> <>p3)))
      ->
      @ n1 (<>p1 <--> []<>(@ n2 (n3 & P4)))
   )
)

end