signature { automatic } theory

{
 !((P1 & P2) -> ( ((P4 <--> !P7) | !P9) --> ((P1 & P2) | (P2 | !P2)) ));
 P1 | P2;
 P4 <--> ! P5
}