begin !(P1 & P2) <--> P7 | P3; P5 & P3 -> (P8 | !(P10 -> P9)); (P3 | P6) -> (P4 | !P16); (P7 | !P8) end