HTab-1.5.4: examples/sat/test08.frm

signature { automatic } theory

{
   (<>(<>(<>(P1 <--> P2))));
   ([]P3);
   ([](P3 -> (P5 | P2)))
}