test20.frm

signature { automatic } theory
{
n1:(p1 -> <>p2);
n2:(p2 -> []p3);
n1:!n2;
n3:<>n1;
n3:<>n2;
n1:<>n2;
n2:<>n1;
n1:!p3;
n3:<>(n2 & p2)
}