Paramodulation and Knuth–Bendix Completion with Nontotal and Nonmonotonic Orderings | Publicación