Rewrite tableau_dnf().

This really fixes the bug in previous. Also, handle the cases in which a DNF
(sub)formula is a literal or a conjunction of literals.