Eval literals in formulas and CNF to invert evaluation order.

For some reason, that doesn't work well.

The following table shows number of Setup::Entails() calls and the
milliseconds that took for test_formula.cc's morri_regression test and
the total test time. The first columns refer to debug mode, the last
ones to production mode.

Old w/o min.: 199  2686 ms   6592 ms total  198   77 ms  136 ms total
Old w/  min.: 200  2545 ms   6490 ms total  199   58 ms  120 ms total
New w/o min.: 432  6854 ms  10301 ms total  437  152 ms  215 ms total
New w/  min.: 138  6899 ms  10587 ms total  131  131 ms  193 ms total