HTab-1.5.4: examples/sat/test04.frm

signature { automatic } theory

{
 (P1 & P1 & P1 ) -> (P3 | P4);
 (P3 -> (!P2 | (P5 -> P6)));
 P6 | P7 | !P8
}