HTab-1.6.1: examples/unsat/test13.frm

begin
!([R1](P1 --> P2) --> [R1]P1 --> [R1]P2)
end