signature { automatic } theory

{
 !(P1 & P1)
}