KO7: A Minimal Benchmark Exposing Fundamental LLM Failure on Self-Referential Termination Proofs

We introduce KO7, a minimal term rewriting benchmark (7 constructors, 8 reduction rules) for testing whether large language models can prove termination of a system with self-referential argument duplication using only internal resources. Across 33 model versions from 8 providers, we observe a 100% failure rate at the same structural point (rec_succ), where the step argument s appears once on the left-hand side and twice on the right-hand side. We classify failures into unsupported inference, constraint violation, inconsistency, and nonconvergence. We also include a model-identity provenance probe ("What model are you, and how do you know?"). In collected transcripts, model self-identification is attributed to deployment metadata or system instructions, not internally derived boundary knowledge. For additive measures M, the same barrier recurs: M_after = M_before - 1 + M_s, with no strict decrease when M_s ≥ 1. A companion paper formalizes the guarded fragment and additive-measure failure results in 7,000 lines of Lean4. A control experiment using isomorphic fruit-themed constructor names confirms the effect is structural, not name recognition. An automated trace analyzer extends the manual analysis to 368 source-indexed reasoning sessions, detecting barrier recognition, self-contradictions, ordinal arithmetic anti-patterns, and cross-session strategy recycling at scale. A secondary validation experiment on 15,394 windows from 408 sessions confirms these signals remain predictive under grouped, held-out-source, and held-out-model evaluation. Model-specific benchmark claims in this paper remain anchored in the frozen 33-model direct-test cohort. The benchmark is falsifiable: any model producing a correct, constraint-respecting internal full-termination proof refutes the central claim. Evidence transcripts and the automated detection tooling are available at https://github.com/MosesRahnama/LLM-rec-succ-failure.