Bachmair and Ganzinger, ordering of equations
A short answer to your question is to use the definition of multiset extension of a partial ordering.

We have the following:


Let $M = \{s,\bot\}$ and $N=\{s\}$. We have  $M\succ M$ since $M(\bot) &gt; N(\bot)$ and there does not exist $x$ such that $N(x)&gt; M(x)$.
Let $M=\{\{s,\bot\},\{u,\bot\}\}$ and $N=\{\{s\},\{t\}\}$. We have $M(\{s,\bot\})&gt;N(\{s,\bot\})$ and by (1) $\{s,\bot\}\succ\{s\}$. Therefore $M\succ N$.


It would be interesting to see examples where the two ways of extending an ordering on equations to clauses disagree and discuss how that might affect the properties or performance of a rewrite-based prover.