reduce chooses an equivalence clique's representative inconsistently across identical subclasses (Whelk, after relax)

[jamesamcl]

robot reduce — in the standard reason → relax → reduce release pipeline with the Whelk reasoner — picks the representative of a satisfiable equivalence clique inconsistently across otherwise-identical subclasses. Some subclasses reduce to one clique member, some to the other, from the same asserted structure.

Minimal, self-contained reproduction (4 axioms): https://github.com/jamesamcl/robot-clique-reduce-bug

Minimal input

EquivalentClasses(obo:CHEBI_36080 obo:PR_000000001)   # a 2-member equivalence clique
SubClassOf(obo:PR_000000001 obo:PR_000018263)         # the clique has a superclass

SubClassOf(obo:PR_000001002 obo:PR_000000001)         # two subclasses, asserted
SubClassOf(obo:PR_000001338 obo:PR_000000001)         # IDENTICALLY under the clique

PR_000001002 and PR_000001338 are declared and asserted the same way — each is simply ⊑ PR_000000001. Nothing distinguishes them.

Command

robot reason --reasoner WHELK \
             --equivalent-classes-allowed asserted-only \
             --exclude-tautologies structural \
             --input ontology.ofn \
      relax \
      reduce --reasoner WHELK \
      --output reduced.ofn

Expected

Both subclasses reduce to the same clique representative — either both PR_000000001 or both CHEBI_36080.

Actual

SubClassOf(obo:PR_000001002 obo:PR_000000001)   <- kept PR
SubClassOf(obo:PR_000001338 obo:CHEBI_36080)    <- kept CHEBI

Two structurally identical subclasses get different representatives. The result is deterministic (identical across repeated runs) but is not a consistent function of the ontology — it tracks the reasoner's internal class ordering rather than a single clique representative.

Versions

Confirmed on ROBOT 1.9.7 and ROBOT 1.9.10 (latest, Feb 2026) — identical output on both.

Why it happens

relax rewrites EquivalentClasses(CHEBI_36080 PR_000000001) into the pair CHEBI_36080 ⊑ PR_000000001 and PR_000000001 ⊑ CHEBI_36080. For a subclass C ⊑ PR_000000001, reasoning then also entails C ⊑ CHEBI_36080, and the two edges are mutually redundant (each derivable from the other via the clique). reduce must drop one, and its choice is made per-subclass from the reasoner's superclass iteration order rather than from a single clique representative — so identical subclasses can diverge.

The clique needs a superclass to trigger it: if PR_000000001 is a root (remove the SubClassOf(PR_000000001 PR_000018263) line), reduction is consistent (both keep PR_000000001).

Scope

• Whelk (--reasoner WHELK): inconsistent — the bug shown here.
• ELK (--reasoner ELK): keeps edges to both clique members for every subclass — consistent, but arguably wrong (a transitive reduction should not retain a redundant edge to an equivalent class).
• Plain robot reduce with no preceding relax does not exhibit it (the PR ⊑ CHEBI direction that makes the edges mutually redundant is not present).

Real-world impact

Observed building the Cell Ontology (cl.obo), where CHEBI:36080 ≡ PR:000000001 and ~216 protein classes are subclasses of the clique. In the released cl-base/cl.obo, 8 of those 216 come out with CHEBI:36080 (6 of them) or with both CHEBI:36080 and PR:000000001 (2 of them), while the other 208 get PR:000000001 — from identical asserted structure.

[matentzn]

@cmungall things this problem is not a reasoner problem, and @balhoff agrees.

choice is made per-subclass from the reasoner’s superclass iteration order rather than from a single clique representative

@balhoff: It seems like robot reduce should make that deterministic somehow.

@matentzn: ok, I will try to take a stab at it next week.