HTab-1.6.1: examples/sat/test15.frm

begin
[](n1 <--> [](n2 <--> [](n3 <--> []n4)));
<>[]<>(p1 <--> p2);
[](p3 -> n1:!p1);
(n1:n2)
end