signature { automatic } theory

{
 (N1:P1) & (N2:!P1)
}