test25.frm

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