Robert Anderson, W. W. Bledsoe: A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness. J. ACM 17(3): 525-534 (1970)