HTab-1.5.5: examples/sat/blockable1.frm

begin
@ N1 <> true;
@ N1 []<> (down (X1 @ N1 <> X1))
end