Konclude not seeing pigeonhole principle

[mpomarlan]

Hello,

I encountered a situation in which HermiT arrives at a (correct) conclusion which Konclude misses. The OWL file is as follows:

Prefix(:=<http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/>)
Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
Prefix(rdf:=<http://www.w3.org/1999/02/22-rdf-syntax-ns#>)
Prefix(xml:=<http://www.w3.org/XML/1998/namespace>)
Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>)
Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>)


Ontology(<http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole>

############################
#   Object Properties
############################

# Object Property: :sitsAt (:sitsAt)
SubObjectPropertyOf(:sitsAt owl:topObjectProperty)


############################
#   Classes
############################

# Class: :CrowdedHole (:CrowdedHole)
EquivalentClasses(:CrowdedHole ObjectIntersectionOf(:Hole ObjectMinCardinality(2 ObjectInverseOf(:sitsAt) :Pigeon)))
SubClassOf(:CrowdedHole :Hole)

# Class: :CrowdedScene (:CrowdedScene)
EquivalentClasses(:CrowdedScene ObjectIntersectionOf(:Scene ObjectSomeValuesFrom(ObjectInverseOf(:inScene) :CrowdedHole)))
SubClassOf(:CrowdedScene :Scene)

# Class: :Hole (:Hole)
EquivalentClasses(:Hole ObjectOneOf(:h1 :h2))
SubClassOf(:Hole ObjectSomeValuesFrom(:inScene :Scene))

# Class: :Pigeon (:Pigeon)
EquivalentClasses(:Pigeon ObjectOneOf(:p1 :p2 :p3))
SubClassOf(:Pigeon ObjectExactCardinality(1 :sitsAt :Hole))

# Class: :Scene (:Scene)
EquivalentClasses(:Scene ObjectOneOf(:s))


############################
#   Named Individuals
############################

SubClassOf(ObjectIntersectionOf(:Hole :Pigeon) owl:Nothing)
SubClassOf(ObjectIntersectionOf(:Hole :Scene) owl:Nothing)
SubClassOf(ObjectIntersectionOf(:Pigeon :Scene) owl:Nothing)
DifferentIndividuals(:p1 :p2 :p3)
)

With the above file called pigeonhole.owl, I run the command

Konclude classification -i pigeonhole.owl -o output.owl

The contents of output.owl are as follows:

<?xml version="1.0" encoding="UTF-8"?>
<Ontology xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns="http://www.w3.org/2002/07/owl#" xmlns:xml="http://www.w3.org/XML/1998/namespace" xmlns:xsd="http://www.w3.org/2001/XMLSchema#">
    <Prefix name="" IRI="http://www.w3.org/2002/07/owl#"/>
    <Prefix name="owl" IRI="http://www.w3.org/2002/07/owl#"/>
    <Prefix name="rdf" IRI="http://www.w3.org/1999/02/22-rdf-syntax-ns#"/>
    <Prefix name="xml" IRI="http://www.w3.org/XML/1998/namespace"/>
    <Prefix name="xsd" IRI="http://www.w3.org/2001/XMLSchema#"/>
    <Prefix name="rdfs" IRI="http://www.w3.org/2000/01/rdf-schema#"/>
    <Declaration>
        <Class IRI="http://www.w3.org/2002/07/owl#Nothing"/>
    </Declaration>
    <Declaration>
        <Class IRI="http://www.w3.org/2002/07/owl#Thing"/>
    </Declaration>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Scene"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Scene"/>
        <Class IRI="http://www.w3.org/2002/07/owl#Thing"/>
    </SubClassOf>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Hole"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Hole"/>
        <Class IRI="http://www.w3.org/2002/07/owl#Thing"/>
    </SubClassOf>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Pigeon"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Pigeon"/>
        <Class IRI="http://www.w3.org/2002/07/owl#Thing"/>
    </SubClassOf>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/CrowdedScene"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/CrowdedScene"/>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Scene"/>
    </SubClassOf>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/CrowdedHole"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/CrowdedHole"/>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Hole"/>
    </SubClassOf>
</Ontology>

The Konclude I used is version 0.7.0 (from the activity log: Reasoner for the SROIQV(D) Description Logic, 64-bit, Version v0.7.0-1135 - 91b3e331 (Mar 16 2021)).

The missing conclusion (which HermiT finds) is that CrowdedScene and Scene are equivalent.

I tried realization as well, and the individual s is discovered to be a Scene and a Thing, but it is not discovered to be a CrowdedScene.