HTab-1.5.4: examples/unsat/test13.frm

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