The efficiency of Satisfiability Modulo Theories (SMT) solvers is crucially dependent on the capability of theory reasoners to provide small conflict sets, i.e. small unsatisfiable subsets from unsatisfiable sets of literals. Decision procedures for uninterpreted symbols (i.e. congruence closure algorithms) date back from the very early days of SMT, and their complexity is well-known. Nevertheless, to our best knowledge, the complexity of the smallest conflict set generation for sets of literals with uninterpreted symbols and equalities was unknown, although it was believed to be NP-complete. We provide a proof of NP-hardness, using a simple reduction from SAT. This is a joint work with Andreas Fellner and Bruno Woltzenlogel Paleo.