I went down the rabbit hole way to long ago (decades), but it is definitely fun there.
No, actually found it many years ago when trying to solve another problem. It is one of those things that once you learn about, you never forget.
While I am familiar with proof systems (Coq), I have yet to actually work with them to a level I would like, but the concepts and burdens you noted are what keep me from adding them to my tool box because of the steep learning curve.
Every time that part of the problem enters my mind, the axiom of choice comes to mind.
Confusion is also my companion whom with serendipity will introduce me to ideas. So having one without the other makes life dull.
I didn’t know how far the cognitive distance was between Unification and Knuth-Bendix for your work, and if it was too great, an answer would have required more time than necessary.
It is like when I see some questions on StackOverflow and the OP needs a full class in programming just to explain Hello, World!; just not something I can devote the time to answer.
Not at all. It is actually nice to converse with other that know about areas I partially know about so that I can learn more.