Bernhard Gleiss, Laura Kovács, Jakob Rath: Subsumption Demodulation in First-Order Theorem Proving. IJCAR (1) 2020: 297-315