HTab-1.6.1: examples/sat/spy.frm

begin
down (N1 []([]( down( N2 (N1:<>(N2))))));
[]<>true;
[] (down (N1 (!<>N1)))
end