HTab-1.6.1: examples/sat/test09.frm

begin
(P1 & (P1 & (P1 & P1))) & (P3 & (P2 & P1) & (P1 & (P2 & P3)))
end