HTab-1.6.1: examples/unsat/test28.frm

begin
n1:<>(n1 v (p1 & !p1));
n1:(<>true  --> p1);
!(n1:<>p1) 
end