test16.frm

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