signature { automatic } theory

{
 !(P1 & P1) & (P3 -> P2);
 !(!P5 ->(P3 | !!P4))
}