Fixed: two and a half bugs in Formula::Flatten().

1.   term_to_var mixed up term and var, which led to the same terms
     being flattened twice.
2.   when multiple argument terms are flattened, each intermediate
     literal would have been stored (eventually the procedure should
     have converged against the same result though).
2.5. NF[] was nondeterministic wrt different executions because
     when in (t = t') both t and t' are functions, their memory
     addresses determine which is lhs and which is rhs; now we always
     try to keep the higher-arity term in the equality.