I guess not, because SAT is propositional so just substituting variables for terms would yield a ground propositional clause. Actually I wasn't even sure we say "clause" in propositional logic. Anyway Plotkin's subsumption is really based off Robinson's unification algorithm and it makes a lot more sense in that context and in the context of resolution theorem proving. Or I'm just hopelessly stuck forever thinking in the first order.
Do you know if Codish et al. were based on an earlier paper for their definition of subsumption? It really sounds like they are simply describing it, rather than introducing it as a new concept.
Edit: of course, the obvious question in my mind now is whether it would be possible to learn sorting networks using one of the ILP approaches that build on Plotkin's work and don't have to perform an expensive search of a large hypothesis space.