We present an equality saturation engine with three contributions. First, pervasive semi-persistence built from a single vector primitive with O(1) snapshots and O($k$) restore, enabling equality saturation inside backtracking search algorithms. Second, native support for associative~(A), associative-commutative~(AC), and AC-idempotent~(ACI) operators with an extension of leapfrog triejoin to multiset matching using maximum partition semantics. Third, proof logging via copy-on-first-re-canonization with Euler-tour LCA for batch extraction. Both semi-persistence and proof logging are compile-time opt-out with zero residual overhead.