We consider cut-elimination in the sequent calculus for classical

first-order logic. It is well known that this system, in its most

general form, is neither confluent nor strongly normalizing. In this

work we take a coarser (and mathematically more realistic) look at

cut-free proofs. We analyze which witnesses they choose for which

quantifiers, or in other words: we only consider the

Herbrand-disjunction of a cut-free proof. Our main theorem is a

confluence result for a natural class of proofs: all (possibly

infinitely many) normal forms of the non-erasing reduction lead to the

same Herbrand-disjunction.