HTab-1.6.1: examples/unsat/test38.frm

begin
p1 v <><><><>p1 v down(N1 <>(N1:[]p1));
A !p1
end