To be clear, the problem in issue771 is that we could get a *quadratic* number
of mutexes, not an exponential one. With N ground facts, there can never be more
than N^2 mutexes.

An algorithm that would "multiply out" multiple representations of atoms in a
mutex group would be exponential, but that just means that this would be an
unreasonable way to represent these mutexes. The problem here is that O(N^2) is
already too large.

In the full encoding, an atom can be represented by more than one variable-value
pair. If this happens, there can be exponentially many mutex groups, so we do
not generate them (see issue771). However, we could generate information of the
type "var1=val4 is equivalent to var3=val0" which might be useful for some
heuristics.