HTab-1.6.1: examples/sat/test37.frm

begin
N1;
<><>(N2 & P1);
E false v [](N1 v E true);
[](!P1 v N2:(N1 & !P1))
end