move CNF out of resolution method. add DPLL.