Example that sends tree tool into nirwana

[Jean-Luc-Picard-2021]

I tried this here:

∀x(m(e,x)=x)∧∀x(m(i(x),x)=e)∧∀x∀y∀z(m(m(x,y),z)=m(x,m(y,z)))→∀x(m(x,e)=x) https://www.umsu.de/trees/#~6x(m(e,x)=x)~1~6x(m(i(x),x)=e)~1~6x~6y~6z(m(m(x,y),z)=m(x,m(y,z)))~5~6x(m(x,e)=x)

But it gets very quickly into a state where stop buttion doesn't work anymore.

Bug or feature?

[wo]

Can confirm. The equality reasoner appears to get stuck in step 4350.

[Jean-Luc-Picard-2021]

Howdy? Ever managed to prove this (Pelletier 53):

(∃X∃Y(¬ (X = Y) ∧ ∀Z(Z = X ∨ Z = Y)) → (∃T∀U(∃V∀W(f(U, W) ↔ W = V) ↔ U = T) ↔ ∃V∀W(∃T∀U(f(U, W) ↔ U = T) ↔ W = V)))

Its not sending the prover to nirvana, but somehow I have the feeling it is more busy with counter model finding than proving.

[wo]

Right. If I turn off the model search, it still runs up to step 335,000 at which point my computer runs out of memory.