Several kinds of orderings, such as polynomial orderings, lexicographic path orderings and Knuth-Bendix orderings, are widely used in term rewriting and theorem proving. In term rewriting, these orderings are powerful tools in proving termination of rewriting systems. In theorem proving, they are key instruments to prune search space without compromising refutational completeness. Solving ordering constraints is therefore essential to the successful application of ordered rewriting and ordered resolution. Besides the needs for decision procedures for existential theories, situations arise in constrained deduction where the satisfiability of arbitrarily quantified formulas need be decided. Unfortunately, the first-order theory of lexicographic path orderings is undecidable, so is existential theory of polynomial orderings. This leaves an open question whether the first-order theory of Knuth-Bendix orderings is decidable (RTA problem 99). In this talk, we give a positive answer to this question using quantifier elimination on a complex structure containing term algebras and integer arithmetic. In fact, we shall show the decidability of a theory that is more expressive than the theory of Knuth-Bendix orderings.