begin
!(((P3 | (!P4 & P5)) <--> (P7 | (P4 --> P2))) <--> (((P3 | (!P4 & P5)) --> (P7 |
(P4 --> P2))) & ((P7 | (P4 --> P2)) --> (P3 | (!P4 & P5)))))
end