signature { automatic } theory
{
n1:<>(n1 v (p1 & !p1));
n1:(<>true  --> p1);
!(n1:<>p1) 
}