Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', section 5.2, 'Simplification and Deletion Techniques', page 17, 'Elimination of redundant atoms', discusses the question of when, having used one clause to derive another, you can throw away the first clause instead of ending up with both. As discussed in Redundancy elimination in the superposition calculus you cannot do this in the general case, but you can do it in some particular cases, such as when discarding tautologies or subsumed clauses.
"Let C = Γ, u ≈ v → ∆ be a clause in N. If N |= Γ → u ≈ v, ∆, then N |= Γ → ∆, so that C can be simplified to Γ → ∆. A particular case is the elimination of multiple occurrences of atoms in the antecedent. For example, if C = Γ, u ≈ v, u ≈ v → ∆, then the clause Γ, u ≈ v → u ≈ v, ∆ is a tautology and hence trivially implied by N. Redundant atoms in the succedent can be eliminated in a similar way."
Hang on. "elimination of multiple occurrences of atoms in the antecedent", "Redundant atoms in the succedent can be eliminated" - it would certainly be nice if you could do this, but as I understand it, as discussed in https://stackoverflow.com/questions/29164610/why-are-clauses-multisets you have to treat clauses as multisets, not sets, you cannot just throw away multiple occurrences of the same atom. What am I missing?
And "then the clause Γ, u ≈ v → u ≈ v, ∆ is a tautology" - as I understand it, this is true, a clause which contains both an item and its negation is indeed a tautology and you really can promptly discard tautologies, but what does that have to do with multiple occurrences of the same atom with the same polarity? How is that sentence connected to the rest of the paragraph?