signature { automatic } theory
{
N1 & B N1;
E P1;
E !P1
}