signature { automatic } theory
{
N1:!N2;
E B !(N1 v N2)
}