signature { automatic } theory
{
A(P1 v P2);
N1:(!P1 & !P2)
}