In rewrite theory, you often want confluence of your system: if $$ u_1\leftarrow t\rightarrow u_2$$

Then there is some term $v$ such that $$ u_1\rightarrow v\leftarrow u_2$$

It is possible to tell whether a set of rewrite rules is confluent by examining the critical pairs: pairs of rules $t_1\rightarrow u_1,t_2\rightarrow u_2$ and an instance $\theta$ such that

1. $t'_1\theta = t_2\theta$
2. $t'_1$ is a subterm of $t_1$ at position $p$.

You can then add the equation $u_1\theta = t_1[u_2\theta]_p$ to make the system confluent.

This suggest an approach to your problem: look at your equations as rewrite rules, then consider the critical pairs: they tell you which equations need to hold to make your system confluent.

In rewrite theory, you often want confluence of your system: if $$ u_1\leftarrow t\rightarrow u_2$$

Then there is some term $v$ such that $$ u_1\rightarrow v\leftarrow u_2$$

It is possible to tell whether a set of rewrite rules is confluent by examining the critical pairs: pairs of rules $t_1\rightarrow u_1,t_2\rightarrow u_2$ and an instance $\theta$ such that

1. $t'_1\theta = t_2\theta$
2. $t'_1$ is a subterm of $t_1$ at position $p$.

You can then add the equation $u_1\theta = t_1[u_2\theta]_p$ to make the system confluent.

This suggest an approach to your problem: look at your equations as rewrite rules, then consider the critical pairs: they tell you which equations need to hold to make your system unifiable.