Is unification modulo the theory of allegories decidable?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Let \textit{ALL} be the equational theory of Allegories. Is unification modulo \textit{ALL} decidable?

Background:

The notion of "Allegory" has defined by Peter Freyd and Andre Scedrov in their monograph [Dougherty, 2000]. Allegories are to binary relations between sets as categories are to functions between sets. By ALL we refer to the untyped version of the theory (see page 195 of [Dougherty, 2000]).

Validity in this equational theory is decidable (Guti'errez' dissertation, Wesleyan University 1999, also see [Dougherty, 2000]). The universal-existential theory over these axioms is undecidable (reduction from the universal-existential theory of free semigroups with constants).