Fix proof OOM by actually counting all neighbors

[pavpanchekha]

This PR fixes the root cause behind herbie-fp/herbie#1084. Basically, Herbie will sometimes build a truly enormous egraph. The proofs code is supposed to early-exit in cases like this but it doesn't due to a bug. I don't really understand the bug, @oflatt helped on fixing it, but it takes memory usage on this benchmark from about ~24GB to about 0.

[oflatt]

Great!
For more context:
There can be many different extra congruence edges between terms in the egraph (n^2 many)
This code was supposed to early exit after it hit too many, but it was miscounting the number of edges