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