\begin{thebibliography}{xx}

\harvarditem{Bachmair \harvardand\ Ganzinger}{1994{\em
  a}}{BachmairGanzinger-94-cade}
Bachmair, L. \harvardand\ Ganzinger, H.  \harvardyearleft 1994{\em
  a}\harvardyearright , Ordered chaining for total orderings, {\em in} `Proc.\
  12$th$ International Conference on Automated Deduction', Vol. 814 of {\em
  Lecture Notes in Artificial Intelligence}, Springer-Verlag, Berlin,
  pp.~435--450.

\harvarditem{Bachmair \harvardand\ Ganzinger}{1994{\em
  b}}{BachmairGanzinger-94-jlc}
Bachmair, L. \harvardand\ Ganzinger, H.  \harvardyearleft 1994{\em
  b}\harvardyearright , `Rewrite-based equational theorem proving with
  selection and simplification', {\em J.\ Logic and Computation} {\bf
  4}(3),~217--247.
\newblock Revised version of Technical Report MPI-I-91-208, 1991.

\harvarditem{Bachmair \harvardand\ Ganzinger}{1994{\em
  c}}{BachmairGanzinger-94-lics}
Bachmair, L. \harvardand\ Ganzinger, H.  \harvardyearleft 1994{\em
  c}\harvardyearright , Rewrite techniques for transitive relations, {\em in}
  `Proc.\ 9th IEEE Symposium on Logic in Computer Science', IEEE Computer
  Society Press, pp.~384--393.
\newline\harvardurl{http://www.mpi-sb.mpg.de/\~{}hg/pca.html\#LICS94}

\harvarditem{Bachmair \harvardand\ Ganzinger}{1995{\em
  a}}{BachmairGanzinger-95-ctrs}
Bachmair, L. \harvardand\ Ganzinger, H.  \harvardyearleft 1995{\em
  a}\harvardyearright , Associative-commutative superposition, {\em in}
  N.~Dershowitz \harvardand\ N.~Lindenstrauss, eds, `Proc.\ 4th Int'l Workshop
  on Conditional and Typed Rewrite Systems, {\rm Jerusalem}', Vol. 968 of {\em
  Lecture Notes in Computer Science}, Springer-Verlag, Berlin, pp.~1--14.
\newblock Revised version of MPI-I-93-267, 1993.

\harvarditem{Bachmair \harvardand\ Ganzinger}{1995{\em
  b}}{BachmairGanzinger-95-mpii2-009}
Bachmair, L. \harvardand\ Ganzinger, H.  \harvardyearleft 1995{\em
  b}\harvardyearright , Ordered chaining calculi for first-order theories of
  binary relations, Research Report MPI-I-95-2-009, Max-Planck-Institut f{\"u}r
  Informatik, Saarbr{\"u}cken, Saarbr{\"u}cken.
\newblock Revised version to appear in JACM.
\newline\harvardurl{http://www.mpi-sb.mpg.de/\~{}hg/pra.html\#MPI-I-95-2-009}

\harvarditem{Basin \harvardand\ Ganzinger}{1995}{BasinGanzinger-95-mpii2-006}
Basin, D. \harvardand\ Ganzinger, H.  \harvardyearleft 1995\harvardyearright ,
  Automated complexity analysis based on ordered resolution, Research Report
  MPI-I-95-2-006, Max-Planck-Institut f{\"u}r Informatik, Saarbr{\"u}cken,
  Saarbr{\"u}cken.
\newblock Full version of LICS'96 paper.
\newline\harvardurl{http://www.mpi-sb.mpg.de/\~{}hg/pra.html\#MPI-I-95-2-006}

\harvarditem{Basin \harvardand\ Ganzinger}{1996}{BasinGanzinger-96-lics}
Basin, D. \harvardand\ Ganzinger, H.  \harvardyearleft 1996\harvardyearright ,
  Complexity analysis based on ordered resolution, {\em in} `Proc.\ 11th IEEE
  Symposium on Logic in Computer Science', IEEE Computer Society Press,
  pp.~456--465.
\newline\harvardurl{http://www.mpi-sb.mpg.de/\~{}hg/pca.html\#LICS96}

\harvarditem{Nieuwenhuis \harvardand\ Rubio}{1992{\em
  a}}{NieuwenhuisRubio-92-esop}
Nieuwenhuis, R. \harvardand\ Rubio, A.  \harvardyearleft 1992{\em
  a}\harvardyearright , Basic superposition is complete, {\em in} `ESOP'92',
  Vol. 582 of {\em Lecture Notes in Computer Science}, Springer-Verlag, Berlin,
  pp.~371--389.

\harvarditem{Nieuwenhuis \harvardand\ Rubio}{1992{\em
  b}}{NieuwenhuisRubio-92-cade}
Nieuwenhuis, R. \harvardand\ Rubio, A.  \harvardyearleft 1992{\em
  b}\harvardyearright , Theorem proving with ordering constrained clauses, {\em
  in} `Automated Deduction --- CADE'11', Vol. 607 of {\em Lecture Notes in
  Computer Science}, Springer-Verlag, Berlin, pp.~477--491.

\end{thebibliography}
