HTab-1.5.4: examples/unsat/test09.frm

signature { automatic } theory

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