,
Springer
Lecture Notes in Computer Science
International Conference on Automated Deduction

de Nivelle, H. (1997). A classification of non-liftable orders for resolution. Automated Deduction - CADE-14, 336–350.