Constraints of the form X:a & X \dom Y are
automatically unsatisfiable if X and Y are different
variables. The Bodirsky et al. paper calls constraints
of this form "non-well-formed". Utool happily solves them.
Implement a check at the beginning of the solver that
checks whether a constraint is non-well-formed and
returns unsolvability in this case. Condition: In the
compact version of the graph, every upper end of a
dominance edge tree-dominates a hole.