signature { automatic } theory
{
P1  v N2:N1;
!N2 v (!N2 & B false);
!P1 v <>false;
N1  v []true
}