I had a similar thought when I learned about e-graphs. I'm not sure yet, but I think congruence closure is a slightly different problem from the one Prolog unification solves. In particular, if you tell an e-graph that `f(x) = g(y)`, it will take you at your word -- while Prolog would give a unification error. (An e-graph should also handle `X = f(X)`, while this would fail Prolog's admittedly often-ignored occurs check.)