Fixed: Formula::Minimize() and ResolveLiterals().

* Formula::Minimize() generated all prime implicates, which included
  non-essential ones. For example, the CNF of (p ^ q) v (~p ^ r) is
  (p v ~p) ^ (~p v q) ^ (p v r) ^ (q v r). Then (p v ~p) is tautologous
  and (q v r) is not essential because it is the result of resolving
  (~p v q) and (p v r).
* ResolveLiterals() forgot to add the literals from the RHS.