As I was digging into computational group theory for string Knuth Bendix completion goodness I noted that coset enumeration aka Todd-Coxeter, one of the mainstay algorithms of computational group theory, mechanically looks quite a bit like equality saturation. This is interesting in its own right but also as a source of controlled benchmarks for equality saturation systems.
