HTab-1.5.4: examples/unsat/test04.frm

signature { automatic } theory

{
!(((P3 | (!P4 & P5)) <--> (P7 | (P4 --> P2))) <--> (((P3 | (!P4 & P5)) --> (P7 |
(P4 --> P2))) & ((P7 | (P4 --> P2)) --> (P3 | (!P4 & P5)))))
}