Drastically restricted ewffs.

An ewff is now only a conjunction of inequalities: x /= y or x /= n.
All equalities x = n shall be represented by just using n in the
literal and likewise x = y shall be represented by using x or y in the
literal.

We couldn't simplify Ewff::Conj in a similar manner in the old version
because an ewff was a disjunction of conjunction, and some of them
could have bound x and others might not.

The idea is that this simplification leads to less complex code at the
cost of more clauses. Considering that most ewffs in reality are just
short conjunctions, we may even save memory because of the smaller
footprint of the new Ewffs.