Abstract
[Bogaerts, Gocht, McCreesh, Nordstrom, AAII-22] introduces a proof system which can be thought of as extended Frege plus a novel "dominance-based strengthening rule", as a tool to certify correctness of runs of a symmetry-breaking SAT solver. We observe that this rule simulates, in a certain sense, polynomial local search and thus show, via known results in bounded arithmetic, that the system is equivalent to the quantified propositional proof system G_1. As such it is likely to be strictly stronger than extended Frege. This is joint work with Leszek Kolodziejczyk.