Disunification is the problem of deciding satisfiability of a system of equations and disequations w.r.t. a given equational theory. In this paper we study the disunification problem in the context of ACI1 equational theories. We provide a characterization of the interpretation structures suitable to model the axioms in ACI1 theories. The satisfiability problem is solved using known techniques for the equality constraints and novel methodologies to transform disequation constraints into solved forms. We propose three solved forms, offering an increasingly more precise characterization of the set of solutions. Two of them can be computed and tested in polynomial time. The novel results achieved open new possibilities in the practical and efficient manipulation of ACI1 constraints.
