Fixed: regression base case and recursive call. Added unit test.

* Fixed: regression should stop if z = <> instead of returning Nothing.
* Fixed: the RHS obtained from RegressOneStep() needs to be regressed.
* Added naive optimization of CNFs. Should be improved to actually
  compute a minimal CNF.
* Added unit test the ESL example as unit test using regression.