K. Subramani, Piotr Wojciechowski, Ying Sheng: Read-once refutations in Horn constraint systems: an algorithmic approach. J. Log. Comput. 32(4): 667-696 (2022)