resolution の完全性についての疑問

一階述語論理の resolution の規則って， l \in C, \neg l' \in C' として \theta を l, l' の MGU としたときに
C, C' \vdash (C\theta \setminus \{l\theta\}) \cup (C'\theta \setminus\{\neg l \theta\})
と書けて(resolution に \vdash を使うのはあまり普通ではないかもしれないけど)，これだけで反駁完全なのだと思っていました。しかしどうもそうではないようだという気がしてきて，どうやったら本当に完全になるんだろうかということを最近考えました。

まず完全でないと思う理由ですが，例えば \{ \{p(x), p(y)\}, \{ \neg p(u), \neg p(v) \} \} (p は述語記号，x, y, u, v は変数)という節集合を考えます。これが充足不能なのは，論理式で書くと (\forall x y. p(x) \lor p(y)) \land (\forall u v. \neg p(u) \lor \neg p(v)) だから明らかでしょう。一方，この節集合からは上の規則を使っても \{ p(z), \neg p(w) \} しか(変数の名前の違いを除いて)新しい節は出てきません。だから空節を導くことはできません。

いくつか見てみた本の中で「論理と計算のしくみ」では違う規則を採用していて，この本では一つずつではなく複数のリテラルをまとめて取り出して unify してよいことになっています。具体的には \theta を C' \cup D' の MGU として
C \cup C', D \cup \neg D' \vdash (C \cup D)\theta
のようにしています。これだとさっきの例は p(x), p(y), p(u), p(v) をまとめて unify してやれば空節が出てくるので OK，ということになります。この形の規則だと確かに反駁完全性が成り立つようです。

でもそういう形の規則になっている本は他に見かけないので，これはどういうことだろうかと疑問に思い調べてみました。以下の記述は "Handbook of Automated Reasoning" の Chapter 2 の冒頭(を読んだ記憶)に基づいています。どうやら resolution の手法を最初に考えた Robinson は，確かに最初の形を resolution として定式化していたようですが，それに加えて別にもう一つ規則を用意していたらしいです。その規則は factoring といって， \theta を D の unifier として
C \cup D \vdash (C \cup D)\theta
という形をしています(たぶん)。これがあると，
\{ \{p(x), p(y)\}, \{ \neg p(u), \neg p(v) \} \} \vdash \{ \{p(x)\}, \{ \neg p(u) \} \}
なので，最初の形の resolution と合わせて空節が導けます。厳密には確かめていませんが，こちらも反駁完全性が成り立ちそうです。

ということは，もともとは resolution と factoring を合わせて反駁完全であるという話だったのに，factoring の方は何らかの理由であまり教科書に書かれなくなってしまったのでしょうか(実際，handbook を読むまで factoring という名前を知らなかった)。https://en.wikipedia.org/wiki/Resolution_(logic) には "The resolution rule, as defined by Robinson, also incorporated factoring, .... The resulting inference rule is refutation-complete, ...." と書いてあるので，そんなに知られていない事実でもなくて，たまたま僕がそのあたりのことが書いてある教科書を読まなかっただけかもしれませんが。