Unsoudness on a bunch of problems in equality reasoning

[jrosain]

Description of the issue

The equality reasoning makes us prove countertheorems. See attached file.

I've checked on the fix-deskolemization branch to get the Rocq output, and it is indeed the equality that fails at some point in the proof.

Flags used

-dmt

Small problem file to reproduce the bug

• MGT038+1.p from TPTP
• NLP014+1.p from TPTP
• NLP015+1.p from TPTP
• NLP016+1.p from TPTP
• NLP017+1.p from TPTP
• NLP018+1.p from TPTP
• NLP019+1.p from TPTP
• NLP022+1.p from TPTP
• NUM374+4.p from TPTP
• PUZ153+1.p from TPTP
• SWW863+1.p from TPTP
• SWW866+1.p from TPTP
• SWW868+1.p from TPTP (takes more time)
• SWW876+1.p from TPTP
• SWW882+1.p from TPTP
• SWW883+1.p from TPTP
• SWW899+1.p from TPTP
• SWW911+1.p from TPTP
• SWW918+1.p from TPTP
• SWW942+1.p from TPTP

Version of Goéland where the issue occurs

from master up to the most up-to-date branch