Triangular Unit Clause Generation: Enhancing Proving Capacity in Saturation-Based Deduction

Automated theorem proving in first-order logic forms the backbone of both formal verification and artificial intelligence. Modern theorem provers commonly use saturation-based inference, in which unit clauses are particularly useful because they can substantially reduce the search space. However, traditional binary resolution combines only two clauses at a time, and this pairwise interaction is prone to a combinatorial explosion of redundant clauses when logic is deeply nested or few unit clauses are initially available. To address this bottleneck, this paper proposes two synergistic strategies for deriving unit clauses from multiple clauses at once: triangle-based unit extraction (tbue), which arranges several clauses into a specialized topological configuration to identify and separate multiple contradiction paths in one step, and equality synergy (es), which integrates E-unification and rewriting into this construction so that equational reasoning avoids search-space explosion. Combining tbue and es yields the triangular unit clause generation (TUCG) algorithm, an efficient implementation of the standard contradiction separation (S-CS) rule. Integrated into the prover Vampire and evaluated on the CASC FOF benchmarks (2021–2025) and on TPTP problems with a rating of 1.0 (the hardest class in the library), the resulting system, Vampire_TUCG, achieved higher solve counts than both Vampire and E in every tested CASC year, and solved 75 of the rating-1.0 problems versus 13 for Vampire, resolving 70 problems that Vampire alone could not. These results indicate that coordinating multiple clauses via triangle construction effectively compresses inferential paths and expands the range of high-complexity problems solvable by saturation-based provers.