started on pure cnf version, see sec6 of formulas.pdf