begin
 !(P1 & P1);
 !(P1 & P1);
 P2 | P1;
 !(P1 & P1) & (P3 -> P2);
 !(!P5 -->(P3 | !!P4));
 (P1 & P1 & P1 ) --> (P3 | P4);
 (P3 --> (!P2 | (P5 --> P6)));
 P6 | P7 | !P8;
 !(P1 & P2) <--> P7 | P3;
 P5 & P3 --> (P8 | !(P10 -> P9));
 (P3 | P6) --> (P4 | !P16);
 (P7 | !P8);
 (N1:P1) & (N2:!P1);
 !(P1 & P1) & (P3 --> P2);
 N1 : !(!P5 -->(P3 | !!P4));
 N2 :  (N3 :  P3);
 <><><>(P1 <--> P2); 
 ([]P3);
 ([](P3 --> (P5 | P2)));
 (P10 & (P10 & (P10 & P10))) & (P30 & (P20 & P10) & (P10 & (P20 & P30)))
end