Polynomial-Delay Enumeration of Fixed-Endpoint Vertex-Regular Paths in Skew-Symmetric Digraphs

Let G = (V,E) be a finite skew-symmetric digraph with a fixed-point-free vertex involution. A directed path is vertex-regular if it contains no vertex together with its mate. For prescribed vertices s and t, this paper gives a depth-first algorithm that enumerates every vertex-regular s–t path exactly once with delay O(n²(n+m)) and polynomial space. The extension test deletes the vertices of the current prefix and their mates and invokes linear-time regular reachability, obtained from the arc-regular algorithm of Goldberg and Karzanov by vertex splitting. This establishes the fixed-endpoint variant needed for the two-unit-clause consequence stated after Conjecture 8.1 of Kullmann and Clewer. Via their regular-path bijection, it also yields O(ℓ(F)³)-delay enumeration of the minimally unsatisfiable subsets of a 2-CNF containing two prescribed distinct unit clauses. This record contains the venue-neutral preprint and LaTeX source together with a reproducibility artifact containing a dependency-free Python implementation, an independent exponential specification, regression and exhaustive tests, and a pinned Lean 4 companion. The Lean companion checks the vertex-splitting model, involution and skew-edge laws, alternating-walk lift, list-regularity join/deletion equivalence, induced reachability, and key abstract prefix-oracle lemmas. The Lean companion is intentionally not an end-to-end formalization of the endpoint gadget, the published Goldberg–Karzanov implementation, the Python matching oracle, the recursive enumerator, or the asymptotic analysis. AI disclosure: OpenAI Codex and Anthropic Claude were used as agentic research assistants. The author independently checked the claims, proofs, computations, sources, and final text, accepts full responsibility, and confirms that neither system is an author.