HTab-1.5.4: examples/sat/test07.frm

signature { automatic } theory

{
 !(P1 & P1) & (P3 -> P2);
 N1 : !(!P5 ->(P3 | !!P4));
 N2 :  (N3 :  P3)
}