HTab-1.6.1: examples/unsat/test07.frm

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