HTab-1.5.4: examples/unsat/test10.frm

signature { automatic } theory

{
   !(((<R1>P1) | (<R1>P2)) --> (<R1>(P1 | P2)))
}