Found by running verify-el over all 1,920 ORE ontologies on the post-#81 engine. Of the 366 it can actually check, 358 are Verified and 8 are Violated — and all 8 adjudicate to false positives of the instrument, from two mechanisms. No new engine defect was found. Full write-up: docs/benchmarks/2026-08-30-corpus-wide-d10-hunt.md.
This matters because the crate's headline claim is that a Violated is a real engine defect. On the corpus as it stands, 100% of Violated verdicts are the instrument's own, so the two bugs below are what stand between it and being usable unattended.
F4 — SubClassOf(owl:Thing, C) is never applied to model elements
Affects ore_ont_11522, ore_ont_14128, ore_ont_14826, ore_ont_7270.
⊤ ⊑ C requires every element to be a C. build_model never propagates it, so the checker reports the very axiom that should have closed the label. The violation count equals the ontology's owl:Thing-LHS axiom count exactly:
| ontology |
SubClassOf(owl:Thing, …) axioms |
violations |
| ore_ont_14128 |
2 |
2 |
| ore_ont_7270 |
2 |
2 |
| ore_ont_11522 |
8 |
8 |
| ore_ont_14826 |
19 |
19 |
The reported element is a Tseitin synthetic carrying only itself, e.g. Element(79)={<synthetic#80>}.
The engine is right. rustdl subclass-expr <ont> "owl:Thing" "<C>" returns yes on every probed pair (5/5). rustdl simply omits owl:Thing from classification output — a reporting convention, not a completeness gap.
Worth flagging beyond this crate: against Konclude these four show MISSED=8/2/19/2 with EXTRA=0, all of the form Thing ⊑ C. Any oracle comparison that counts Thing rows will report spurious MISSED on any ontology asserting ⊤ ⊑ C. The project has hit this before — 73% of an apparent ~1,795-row gap against Kobayashi-MaRust was the same ⊤-equivalence convention artifact.
F5 — BoundTripped produces Violated instead of Unresolved
Affects ore_ont_12317, ore_ont_13220, ore_ont_15249, ore_ont_283 — all 50k–60k classes, all exceeding Bounds::max_elements = 50_000:
verdict: violated domain: 50738 violations: 25369
unresolved: ['BoundTripped { bound: "max_elements", limit: Some(50000) }', ...]
Violations run to the order of the domain size (25,369 / 20,292 / 54,304 / 92,573). The model was truncated, so most axioms cannot be witnessed and the violations are artifacts of the cut.
This is an asymmetry in owl-dl-cli's fold_build_reasons: the Verified arm downgrades to Unresolved whenever build reasons are non-empty (the arm that stops a false all-clear), while the Violated arm appends the reasons and keeps the verdict. That is right for a complete model with a minor residual, and wrong for BoundTripped, where the model is known-incomplete by construction. A truncated model should exit 3 (no verdict), not 2 (real defect).
Note F5 is the cheaper fix and removes half the false positives on its own.
Coverage, stated as measured
| verdict |
count |
| unresolved (off-fragment/refused) |
1,357 |
| verified |
358 |
| timeout at 60 s — UNMEASURED, not passing |
196 |
| violated |
8 |
| I/O or parse error |
1 |
The instrument covers 19% of the corpus, and the largest single obstacle is the pure-EL fragment restriction rather than defect density.
Found by running
verify-elover all 1,920 ORE ontologies on the post-#81 engine. Of the 366 it can actually check, 358 areVerifiedand 8 areViolated— and all 8 adjudicate to false positives of the instrument, from two mechanisms. No new engine defect was found. Full write-up:docs/benchmarks/2026-08-30-corpus-wide-d10-hunt.md.This matters because the crate's headline claim is that a
Violatedis a real engine defect. On the corpus as it stands, 100% ofViolatedverdicts are the instrument's own, so the two bugs below are what stand between it and being usable unattended.F4 —
SubClassOf(owl:Thing, C)is never applied to model elementsAffects
ore_ont_11522,ore_ont_14128,ore_ont_14826,ore_ont_7270.⊤ ⊑ Crequires every element to be aC.build_modelnever propagates it, so the checker reports the very axiom that should have closed the label. The violation count equals the ontology'sowl:Thing-LHS axiom count exactly:SubClassOf(owl:Thing, …)axiomsThe reported element is a Tseitin synthetic carrying only itself, e.g.
Element(79)={<synthetic#80>}.The engine is right.
rustdl subclass-expr <ont> "owl:Thing" "<C>"returnsyeson every probed pair (5/5). rustdl simply omitsowl:Thingfrom classification output — a reporting convention, not a completeness gap.Worth flagging beyond this crate: against Konclude these four show
MISSED=8/2/19/2withEXTRA=0, all of the formThing ⊑ C. Any oracle comparison that countsThingrows will report spurious MISSED on any ontology asserting⊤ ⊑ C. The project has hit this before — 73% of an apparent ~1,795-row gap against Kobayashi-MaRust was the same ⊤-equivalence convention artifact.F5 —
BoundTrippedproducesViolatedinstead ofUnresolvedAffects
ore_ont_12317,ore_ont_13220,ore_ont_15249,ore_ont_283— all 50k–60k classes, all exceedingBounds::max_elements = 50_000:Violations run to the order of the domain size (25,369 / 20,292 / 54,304 / 92,573). The model was truncated, so most axioms cannot be witnessed and the violations are artifacts of the cut.
This is an asymmetry in
owl-dl-cli'sfold_build_reasons: theVerifiedarm downgrades toUnresolvedwhenever build reasons are non-empty (the arm that stops a false all-clear), while theViolatedarm appends the reasons and keeps the verdict. That is right for a complete model with a minor residual, and wrong forBoundTripped, where the model is known-incomplete by construction. A truncated model should exit 3 (no verdict), not 2 (real defect).Note F5 is the cheaper fix and removes half the false positives on its own.
Coverage, stated as measured
The instrument covers 19% of the corpus, and the largest single obstacle is the pure-EL fragment restriction rather than defect density.