Are there semi-decision procedures for this theory?
It looks to me that you can encode the word problem for groups within the theory of categories in the following way. Pick an object $X$, and then for each generator of the group introduce two morphisms $x,x&#39; : X \to X$, and assume the equalities $x \circ x&#39; = 1_X$ and $x&#39; \circ x = 1_X$. Then you can define the unit to be the identity map, the composition to be the group multiplication, and the negation of a string $x\circ y\circ z$ to be the reverse primed string $z&#39; \circ y&#39; \circ x&#39;$. Hence this problem is undecidable.

However, the word problem is solvable for many specific groups, so if you have more details about the problem this may help. In particular, one idea from the theory of groups which might help you a lot is that absolute presentations of finitely generated groups are solvable -- the inequations can prune the search space enough to make the theory decidable.

EDIT: One additional thought I had is that adding irrelations might still be a useful tool for you, even if the concrete models you're interested validate the equations. This is because in categorical situations you often only want "nice" equations, for some value of nice, and you can use the inequations to rule out solutions that are too evil for you. Your decision procedure might still be incomplete, but you might get a more natural characterization of the solutions it can find than "we search possible proof-trees to a depth of 7". 

Good luck; that functor thing you're doing looks pretty cool!