HTab-1.5.4: examples/unsat/test07.frm

signature { automatic } theory

{
  !(([R1](P1 --> P2)) --> (([R1] P1) --> ([R1] P2)))
}