Bachmair and Ganzinger, ordering of equations Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical one in the overall attempt to get to the point where equations can be applied in one direction, thereby dramatically improving the performance of automated reasoning on problems involving equality.)

If $s \succ t \succ u$

Let $s\approx t$ have the multiset representation $\{\{s\},\{t\}\}$

Let $s\not\approx t$ have the multiset representation $\{\{s,\bot\},\{t,\bot\}\}$ where $\bot$ is a new symbol such that every existing symbol is greater than $\bot$.

Then $s\not\approx u \succ s\approx t$ even though $t \succ u$.

... wait, how? Sure, $s\not\approx u$ also contains a couple of occurrences of $\bot$, but what of that? $t \succ u \succ \bot$, so the comparison should be decided by $t$ vs. $u$; $\bot$ should not have enough weight to tip the balance, so to speak.

What am I missing?

(I have seen later writing that gives $s\not\approx t$ the multiset representation $\{\{s,s\},\{t,t\}\}$, and I see how this solves the problem, but I don't see how it is solved in the original version.)
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.