KO7: A Minimal Benchmark Exposing fundamental LLM Failure at 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 Lean 4. A control experiment using isomorphic fruit-themed constructor names confirms the effect is structural, not name recognition. The benchmark is falsifiable: any model producing a correct, constraint-respecting internal full-termination proof refutes the central claim.