HTab-1.6.1: examples/unsat/interpol.frm

begin
!((<>p1 & <>!p1) --> (([](p2 --> N1) --> <>!p2)))
end