HTab-1.5.4: examples/unsat/test17.frm
signature { automatic } theory
{
!(n1:(n1 & n2:(n2 & ([](p1 -->((!(p1 -> (p2 --> p1))) v p2)) --> ([]p1 --> []p2)))))
}
signature { automatic } theory
{
!(n1:(n1 & n2:(n2 & ([](p1 -->((!(p1 -> (p2 --> p1))) v p2)) --> ([]p1 --> []p2)))))
}