Suppose, we have a first-order logic theory over a signature {=, $\times$} (where $\times$ is a binary function symbol, and = is the equality symbol), that contains following axioms: $$\forall x \forall y ( x \times (y \times y) = (x \times y) \times y)$$ $$\exists o \forall x (x \times o = o)$$ $$\exists e \forall x (x \times e = x)$$ $$\forall x \forall y \exists z (x \times z = y)$$ $$\exists x \exists y (\neg(x = y))$$ Is this theory consistent?
It is quite easy to prove that if it is, then every its model has to be infinite. Also, it is quite obvious that the following statements are logically implied by this theory: $$\neg \forall x \forall y ((y \times y) \times x = y \times(y \times x))$$ $$\neg \exists a \forall x (a \times x = a)$$ $$\neg \forall x \forall y \exists z (z \times x = y)$$ $$\neg \forall x \forall y (x \times y = y \times x)$$
However, I do not know how to proceed further…
Any help will be appreciated.
Your theory is consistent. Here is a model. I will write $*$ instead of $\times$ because it's easier to type.
The universe is the set $\{0,1,2,3,\dots\}$ of all nonnegative integers; $x*1=x$ for all $x;$ for $y\ne1$ we define $$x*y=\begin{cases} \ \ \ y\ \ \ \ \ \text{ if }\ x=y,\\ \lfloor y/2\rfloor\ \text{ if }\ x\ne y. \end{cases}$$
Clearly $x*1=x$ and $x*0=0$ for all $x.$
Given $x$ and $y,$ we can find $z$ such that $x*z=y;$ namely, if $y=0$ take $z=0;$ if $y\ne0$ choose $z\in\{2y,2y+1\}$ so that $z\ne x.$
To verify $x*(y*y)=(x*y)*y$ we consider three cases:
If $y=1$ then $x*(y*y)=x*(1*1)=x*1=x$ and $(x*y)*y=(x*1)*1=x*1=x.$
If $x=y$ then $x*(y*y)=y*(y*y)=y*y=y$ and $(x*y)*y=(y*y)*y=y*y=y.$
If $y\ne1$ and $x\ne y$ then $x*(y*y)=x*y=\lfloor y/2\rfloor$ and $(x*y)*y=\lfloor y/2\rfloor*y=\lfloor y/2\rfloor.$