HTab-1.5.5: examples/unsat/trans01.frm

{unsat}
begin
N1 & P1;
<*>(N1 & [*](-P1 v -N1));
[](N1 v Etrue)
end