resolution in clause sets. Standard notions like completeness do not adequately cover the new phenomena and problems introduced by clause graph resolution, and standard proof techniques do not work for clause graphs, which are the major reasons why important questions have been open for years. This work defines a series of relevant properties in precise terms and answers several of the open questions. The clause graph inference system is refutation complete and refutation confluent if the insertion of a single additional variant of a clause into the graph is allowed. Compared to clause set resolution, clause graph resolution does not increase the complexity of the simplest refutations, again provided that one additional variant may be inserted. A number of well-known restriction strategies are refutation complete, but most are not refutation confluent for clause graph resolution, which renders them useless. Exhaustive ordering strategies do not exist and contrary to a widespread conjecture the plausible approximations of exhaustiveness do not ensure the detection of a refutation.

Hide more