G. Q. Zhang, “PB-277 Literal resolution: A Simple Proof of Resolution Completeness”, DPB, vol. 18, no. 277, Jan. 1989.