Zhang, G. Q. PB-277 Literal Resolution: A Simple Proof of Resolution Completeness. DPB 1989, 18.