HTab-1.5.4: examples/sat/test09.frm

signature { automatic } theory
{
(P1 & (P1 & (P1 & P1))) & (P3 & (P2 & P1) & (P1 & (P2 & P3)))
}