Specifically, on the ground level equational literals are simplified, until they are in a sufficiently simplified form. For each of these forms one derives a symmetrization, that is a set of rules such that critical pairs with the theory converge. One then considers overlaps between symmetrizations. Since their structure is know, one can exploit this by showing that only a few critical pairs need to be tested to obtain convergence.
To lift this to the non-ground level, each step of the simplification becomes an inference. These are either carefully controlled superpositions with theory axioms or derived inferences like cancellation. Then, for inferences between sufficiently simplified non-theory clauses, one distinguished between overlaps of two extended rules and overlaps where at least one rule is not extended. The former correspond to the critical pairs obtained above; the latter are similar to superposition inferences, except that they take the extended rules in the symmetrization into account.
The technique is quite general, but it seems most useful for theories which have abelian groups as a subtheory. In that case a single term of a sum can be isolated on the left-hand side. The inference systems obtained are extensions of the corresponding Gröbner base algorithms.
