HTab-1.6.1: examples/unsat/test05.frm

begin
 !((P1 & P2) -> ( ((P4 <--> !P7) | !P9) --> ((P1 & P2) | (P2 | !P2)) ));
 P1 | P2;
 P4 <--> ! P5
end