 There are several automated reasoning programs that are based on resolution, or refinements of resolution. Otter (succeeded by Prover4) was a driving force in the development of automated reasoning (Wos, Overbeek, Lusk &amp; Boyle 1984) but it has been superseded by more capable programs like Vampire (Voronkov 1995, Kovács &amp; Voronkov 2013). Resolution also provides the underlying logico-computational mechanism for the popular logic programming language Prolog (Clocksin &amp; Mellish 1981).