HTab-1.6.1: examples/unsat/test02.frm

begin
 P1 | P2 | P3 | P4;
 !P1 | !P2;
 !(P1 --> ((P3 <--> P4) --> P1))
end