HTab-1.5.4: examples/sat/test14.frm

signature { automatic } theory
{
<>p1 & <>(p1 & <>p1) & [](p1 & <>p1 & <>(<>!p1 & []p2));
[]!p2 & (p1 <--> p3) & [](p1 <--> p3);
p11 v p12 v p13 v p14 v p15;
!p11 v !p12 v !p13;
[][][](p11 <--> p12)
}