HTab-1.5.4: examples/sat/test05.frm

signature { automatic } theory

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