Two statements sharing a name.
Names identify formulae, and an inference record refers to its parents by name, so a shared name renders a derivation ambiguous and a formula selection indeterminate.
A warning rather than an error, and noisy over parts of the TPTP library: the
machine-generated ITP axiom sets repeat declarations across files, so a problem
including thirty of them defines one name thirty times. The finding is correct —
the derivation is ambiguous — but a caller may reasonably :suppress it.
One diagnostic is emitted per name rather than per occurrence. related carries
the remaining occurrences, so the count is available without a diagnostic for
each.