HTab-1.5.4: examples/unsat/test38.frm

signature { automatic } theory
{
p1 v <><><><>p1 v down(N1 <>(N1:[]p1));
A !p1
}