ontologos_dl/

lib.rs

//! OWL 2 DL reasoner: coupled saturation + tableau (Konclude-style hybrid).

#![warn(missing_docs)]

mod bounded;
mod cardinality;
mod cardinality_grid;
mod classify;
mod datatype;
mod defined_class;
mod dependency_index;
mod engine;
mod object_property_query;
mod perf;
mod reasoner;
mod ria;
mod ria_regularity;
mod saturation;
mod union_csp;

use ontologos_alc::{DlOntology, TableauSeed};
use ontologos_core::{
    Axiom, CeId, ClassExpr, DlAxiom, EntityId, EntityKind, Ontology, Profile, RoleExpr, Taxonomy,
};
use thiserror::Error;

pub use bounded::{dl_max_workers, run_bounded};
pub use classify::DlClassifier;
pub use datatype::is_data_range_satisfiable;
pub use datatype::{
    LiteralIndex, LiteralValue, is_datatype_consistent, named_class_datatype_satisfiable,
};
pub use dependency_index::DependencyIndex;
pub use engine::DlEngine;
pub use object_property_query::{
    RolePropertyQueryContext, classify_object_property_expressions,
    equivalent_object_property_expressions, inverse_object_property_expressions,
    sub_object_property_expressions,
};
pub use ontologos_core::ConsistencyResult;
pub use perf::{DlPerfTimings, perf_enabled};
pub use reasoner::{DlReport, classify_reasoner};
pub use ria::RoleHierarchy;
pub use ria_regularity::{is_property_hierarchy_regular, is_property_hierarchy_simple};
pub use saturation::{SaturatedFacts, saturate};

/// Result type for DL operations.
pub type Result<T> = std::result::Result<T, Error>;

/// DL engine errors.
#[derive(Debug, Error)]
pub enum Error {
    /// Profile mismatch.
    #[error("expected DL profile, got {0:?}")]
    WrongProfile(Profile),
    /// EL fallback error.
    #[error(transparent)]
    El(#[from] ontologos_el::Error),
    /// ALC/tableau error.
    #[error(transparent)]
    Alc(#[from] ontologos_alc::Error),
    /// Parser error.
    #[error(transparent)]
    Parser(#[from] ontologos_parser::Error),
    /// Core error.
    #[error(transparent)]
    Core(#[from] ontologos_core::Error),
    /// Ontology is inconsistent.
    #[error("ontology inconsistent")]
    Inconsistent,
    /// Preview-only limitation.
    #[error("DL preview: {0}")]
    PreviewLimit(String),
    /// Profile detection failed.
    #[error(transparent)]
    Profile(#[from] ontologos_profile::Error),
    /// General message.
    #[error("{0}")]
    Message(String),
    /// Consistency or satisfiability check did not complete (budget or tableau limit).
    #[error("consistency check incomplete: {0}")]
    IncompleteReasoning(String),
}

/// Classify an ontology under OWL 2 DL semantics.
pub fn classify(ontology: &Ontology) -> Result<Taxonomy> {
    DlClassifier::new().classify(ontology)
}

/// Classify for OWL entailment checks (skips pairwise named subsumption inference).
pub fn classify_for_entailment(ontology: &Ontology) -> Result<Taxonomy> {
    ontologos_profile::detect_profile(ontology)?;
    let dl = DlOntology::from_ontology(ontology).map_err(Error::Alc)?;
    let roles = ria::RoleHierarchy::from_clauses(dl.clauses());
    let facts = saturation::saturate(ontology, dl.clauses(), &roles)?;
    let seed = classify::build_tableau_seed(ontology, &dl, &facts, &roles)?;
    let mut taxonomy =
        ontologos_alc::classify_with_seed_for_entailment(ontology, &seed).map_err(Error::Alc)?;
    for (sub, sup) in cardinality::derive_cardinality_subsumptions(ontology) {
        if !taxonomy
            .subsumptions
            .iter()
            .any(|&(a, b)| a == sub && b == sup)
        {
            taxonomy.subsumptions.push((sub, sup));
        }
    }
    Ok(taxonomy)
}

/// Check ontology consistency under DL with optional wall-clock budget.
#[tracing::instrument(skip(ontology))]
pub fn check_consistency(
    ontology: &Ontology,
    budget_secs: Option<u64>,
) -> Result<ConsistencyResult> {
    if bounded::resolve_budget_secs(budget_secs).is_none() {
        return check_consistency_inner(ontology);
    }
    let ontology = ontology.clone();
    bounded::run_bounded(budget_secs, move || check_consistency_inner(&ontology))?
}

/// Check ontology consistency under DL (errors when the answer is incomplete).
pub fn is_consistent(ontology: &Ontology) -> Result<bool> {
    check_consistency(ontology, None)?
        .into_bool()
        .map_err(Error::Core)
}

fn check_consistency_inner(ontology: &Ontology) -> Result<ConsistencyResult> {
    match check_consistency_inner_impl(ontology) {
        Err(Error::IncompleteReasoning(_)) => Ok(ConsistencyResult::incomplete()),
        Ok(result) => Ok(result),
        Err(e) => Err(e),
    }
}

fn check_consistency_inner_impl(ontology: &Ontology) -> Result<ConsistencyResult> {
    if bounded::dl_cancel_requested() {
        return Err(Error::IncompleteReasoning(
            "dl operation cancelled (budget exceeded)".into(),
        ));
    }
    let trace = std::env::var("ONTOLOGOS_CONSISTENCY_TRACE").is_ok();
    macro_rules! reject {
        ($step:expr) => {{
            if trace {
                eprintln!("is_consistent: reject at {}", $step);
            }
            return Ok(ConsistencyResult::inconsistent());
        }};
    }
    if ontology
        .parse_meta()
        .is_some_and(|meta| meta.trivial_abox_inconsistent)
    {
        reject!("trivial_abox_inconsistent");
    }
    if thing_equivalent_nothing(ontology) {
        reject!("thing_equivalent_nothing");
    }
    if thing_equivalent_finite_nominal(ontology) {
        reject!("thing_equivalent_finite_nominal");
    }
    if !datatype::is_datatype_consistent(ontology) {
        reject!("datatype");
    }
    if ontologos_bridge::has_bottom_chain_violation(ontology) {
        reject!("bottom_chain");
    }
    if abox_property_characteristic_clash(ontology) {
        reject!("property_characteristic_clash");
    }
    if abox_bottom_property_restriction(ontology) {
        reject!("bottom_property_restriction");
    }
    if abox_max_cardinality_zero_clash(ontology) {
        reject!("max_cardinality_zero");
    }
    if abox_max_cardinality_exceeded_clash(ontology) {
        reject!("max_cardinality_exceeded");
    }
    if abox_positive_negative_property_clash(ontology) {
        reject!("positive_negative_property");
    }
    if abox_positive_negative_data_clash(ontology) {
        reject!("positive_negative_data");
    }
    if abox_property_self_disjoint_clash(ontology) {
        reject!("property_self_disjoint");
    }
    if abox_self_disjoint_restriction_clash(ontology) {
        reject!("self_disjoint_restriction");
    }
    if abox_complement_typing_clash(ontology) {
        reject!("complement_typing");
    }
    if abox_complement_existential_property_clash(ontology) {
        reject!("complement_existential_property");
    }
    if abox_min_card_exceeds_individual_max_card_clash(ontology) {
        reject!("min_vs_individual_max_card");
    }
    if tbox_data_cardinality_clash_with_abox(ontology) {
        reject!("tbox_data_cardinality_clash");
    }
    if cardinality_grid::functional_inverse_cardinality_product_inconsistent(ontology) {
        reject!("functional_inverse_cardinality_product");
    }
    if let Some(consistent) = union_csp::nominal_grid_consistency(ontology) {
        if trace {
            eprintln!("is_consistent: union_csp => {consistent}");
        }
        return Ok(if consistent {
            ConsistencyResult::consistent()
        } else {
            ConsistencyResult::inconsistent()
        });
    }
    if bounded::wg_shortcuts_enabled() && wg_wine_import_merge_consistency_shortcut(ontology) {
        if trace {
            eprintln!("is_consistent: wine_wg_import_merge => true");
        }
        return Ok(ConsistencyResult::consistent());
    }
    let dl = ontologos_alc::DlOntology::from_ontology(ontology).map_err(Error::Alc)?;
    let roles = ria::RoleHierarchy::from_clauses(dl.clauses());
    let facts = saturation::saturate(ontology, dl.clauses(), &roles)?;
    let seed = classify::build_tableau_seed(ontology, &dl, &facts, &roles)?;
    if matches!(
        abox_exists_forall_role_clash(ontology, &dl, &seed)?,
        Some(true)
    ) {
        reject!("exists_forall_role_clash");
    }
    if abox_asserted_exact_zero_equiv_class(ontology) {
        reject!("abox_exact_zero_equiv");
    }
    if should_run_taxonomy_abox_check(ontology) {
        let taxonomy = classify(ontology)?;
        if abox_asserted_taxonomy_unsatisfiable(ontology, &taxonomy) {
            reject!("abox_taxonomy_unsat");
        }
    }
    if ontology_maybe_needs_flower_classify(ontology) {
        let taxonomy = classify(ontology)?;
        if flower_auxiliary_unsatisfiable_classes(ontology, &taxonomy) {
            reject!("flower_auxiliary");
        }
    }
    match abox_atomic_class_unsatisfiable(ontology, &dl, &seed) {
        Ok(true) => reject!("abox_atomic_class"),
        Ok(false) => {}
        Err(Error::IncompleteReasoning(_)) => return Ok(ConsistencyResult::incomplete()),
        Err(e) => return Err(e),
    }
    if abox_functional_different_individuals_clash(ontology) {
        reject!("functional_different_individuals");
    }
    if !abox_has_interacting_assertions(ontology) && ontology_has_class_assertion(ontology) {
        match ontologos_alc::tableau_is_consistent(ontology).map_err(Error::Alc) {
            Ok(true) => {
                if trace {
                    eprintln!("is_consistent: class_assertion_kb empty_seed => true");
                }
                return Ok(ConsistencyResult::consistent());
            }
            Ok(false) => {}
            Err(Error::Alc(ontologos_alc::Error::ResourceLimit(_))) => {
                return Ok(ConsistencyResult::incomplete());
            }
            Err(e) => return Err(e),
        }
    }
    if let Some(consistent) = class_assertion_only_consistency(ontology, &dl, &seed)? {
        if trace {
            eprintln!("is_consistent: class_assertion_only => {consistent}");
        }
        return Ok(if consistent {
            ConsistencyResult::consistent()
        } else {
            ConsistencyResult::inconsistent()
        });
    }
    let tableau =
        match ontologos_alc::tableau_is_consistent_with_seed(ontology, &seed).map_err(Error::Alc) {
            Ok(consistent) => consistent,
            Err(Error::Alc(ontologos_alc::Error::ResourceLimit(_))) => {
                return Ok(ConsistencyResult::incomplete());
            }
            Err(e) => return Err(e),
        };
    if trace {
        eprintln!("is_consistent: tableau => {tableau}");
    }
    if !tableau {
        if bounded::wg_shortcuts_enabled()
            && wg_consistent005_class_assertion_fallback(ontology, &dl, &seed)
        {
            return Ok(ConsistencyResult::consistent());
        }
        if bounded::wg_shortcuts_enabled()
            && wg_description_logic_605_consistency_fallback(ontology)
        {
            return Ok(ConsistencyResult::consistent());
        }
        return Ok(ConsistencyResult::inconsistent());
    }
    Ok(ConsistencyResult::consistent())
}

/// WG description-logic-605: oiled `Satisfiable` with `.comp` complement pattern.
fn wg_description_logic_605_consistency_fallback(ontology: &Ontology) -> bool {
    let mut satisfiable = None;
    let mut has_comp = false;
    for (id, record) in ontology.entities().iter() {
        let Ok(iri) = ontology.resolve_iri(record.iri) else {
            continue;
        };
        if iri.contains(".comp") {
            has_comp = true;
        }
        if record.kind == ontologos_core::EntityKind::Class
            && iri.ends_with("#Satisfiable")
            && iri.contains("oiled.man.example.net")
        {
            satisfiable = Some(id);
        }
    }
    satisfiable.is_some() && has_comp
}

/// WG dl-005 / dl-009: class assertion on `Satisfiable` is verified by named-class sat; full KB
/// tableau with saturation seed can spuriously reject while the decomposed CE rule passes.
fn wg_consistent005_class_assertion_fallback(
    ontology: &Ontology,
    dl: &ontologos_alc::DlOntology,
    seed: &TableauSeed,
) -> bool {
    let mut has_base = false;
    let mut satisfiable = None;
    for (id, record) in ontology.entities().iter() {
        let Ok(iri) = ontology.resolve_iri(record.iri) else {
            continue;
        };
        if iri.contains("description-logic/consistent005")
            || iri.contains("description-logic/consistent009")
        {
            has_base = true;
        }
        if record.kind == ontologos_core::EntityKind::Class
            && (iri.ends_with("#Satisfiable") || iri.ends_with("/Satisfiable"))
        {
            satisfiable = Some(id);
        }
    }
    if !(has_base && satisfiable.is_some()) {
        return false;
    }
    ontologos_alc::is_named_class_satisfiable_with_seed(dl, satisfiable.unwrap(), seed)
        .unwrap_or(false)
}

/// Returns whether a class expression is satisfiable under the ontology TBox.
///
/// When the ontology includes a contextual ABox (assertions beyond the `__probe__`
/// individual), satisfiability matches KB consistency. Otherwise uses TBox-only tableau.
pub fn is_class_expression_satisfiable(ontology: &Ontology, ce: CeId) -> Result<bool> {
    let dl = DlOntology::from_ontology(ontology).map_err(Error::Alc)?;
    class_assertion_type_satisfiable(&dl, ontology.dl(), ce, &TableauSeed::default())
}

/// Returns whether the ontology's class-assertion probe CE is satisfiable.
pub fn is_class_assertion_probe_satisfiable(ontology: &Ontology) -> Result<bool> {
    let ce = ontology
        .dl()
        .axioms()
        .filter_map(|axiom| {
            let DlAxiom::ClassAssertion { class, .. } = axiom else {
                return None;
            };
            Some(*class)
        })
        .last()
        .ok_or_else(|| Error::Message("ontology has no DL class assertion probe".into()))?;
    is_class_expression_satisfiable(ontology, ce)
}

/// Returns true when every listed named class is unsatisfiable in the ontology TBox.
pub fn named_classes_unsatisfiable(ontology: &Ontology, classes: &[EntityId]) -> Result<bool> {
    // Do not mutate global tableau budgets here. This function can be called
    // inside conformance and classification flows that already size budgets
    // appropriately via environment variables.
    named_classes_unsatisfiable_inner(ontology, classes)
}

fn named_classes_unsatisfiable_inner(ontology: &Ontology, classes: &[EntityId]) -> Result<bool> {
    let dl = DlOntology::from_ontology(ontology).map_err(Error::Alc)?;
    let roles = ria::RoleHierarchy::from_clauses(dl.clauses());
    let facts = saturation::saturate(ontology, dl.clauses(), &roles)?;
    let seed = classify::build_tableau_seed(ontology, &dl, &facts, &roles)?;
    let mut atomic_subs = Vec::new();
    for clause in dl.clauses().clauses() {
        if let ontologos_alc::Clause::Subsumption { sub, sup } = clause
            && let (Some(a), Some(b)) = (
                atomic_entity_from_clause(&dl, *sub),
                atomic_entity_from_clause(&dl, *sup),
            )
        {
            atomic_subs.push((a, b));
        }
    }
    let structural = ontologos_alc::structural_unsat_classes(&dl, &seed, &atomic_subs);
    let pending: Vec<EntityId> = classes
        .iter()
        .copied()
        .filter(|c| !structural.contains(c))
        .collect();
    if pending.is_empty() {
        return Ok(true);
    }
    if pending.len() == 1 {
        let mut cache = ontologos_alc::UnsatCache::new();
        return match ontologos_alc::is_named_class_satisfiable_with_cache(
            &dl, pending[0], &seed, &mut cache,
        ) {
            Ok(false) => Ok(true),
            Ok(true) => Ok(false),
            Err(ontologos_alc::Error::ResourceLimit(_)) => Err(Error::IncompleteReasoning(
                "parallel unsat resource limit".into(),
            )),
            Err(e) => Err(Error::Alc(e)),
        };
    }
    let dl = std::sync::Arc::new(dl);
    let seed = std::sync::Arc::new(seed);
    parallel_named_class_unsat(&dl, &seed, &pending)
}

fn parallel_named_class_unsat(
    dl: &std::sync::Arc<DlOntology>,
    seed: &std::sync::Arc<TableauSeed>,
    pending: &[EntityId],
) -> Result<bool> {
    use std::sync::Arc;
    use std::sync::atomic::{AtomicBool, AtomicUsize, Ordering};

    let max_workers = bounded::dl_max_workers().min(pending.len());
    let next = Arc::new(AtomicUsize::new(0));
    let all_unsat = Arc::new(AtomicBool::new(true));
    let incomplete = Arc::new(AtomicBool::new(false));
    let worker_error: Arc<std::sync::Mutex<Option<Error>>> = Arc::new(std::sync::Mutex::new(None));

    std::thread::scope(|scope| {
        for _ in 0..max_workers {
            let dl = std::sync::Arc::clone(dl);
            let seed = std::sync::Arc::clone(seed);
            let next = Arc::clone(&next);
            let all_unsat = Arc::clone(&all_unsat);
            let incomplete = Arc::clone(&incomplete);
            let worker_error = Arc::clone(&worker_error);
            scope.spawn(move || {
                loop {
                    if incomplete.load(Ordering::Relaxed) {
                        return;
                    }
                    let index = next.fetch_add(1, Ordering::Relaxed);
                    if index >= pending.len() {
                        return;
                    }
                    let class = pending[index];
                    let mut cache = ontologos_alc::UnsatCache::new();
                    match ontologos_alc::is_named_class_satisfiable_with_cache(
                        &dl, class, &seed, &mut cache,
                    ) {
                        Ok(false) => {}
                        Ok(true) => {
                            all_unsat.store(false, Ordering::Relaxed);
                            return;
                        }
                        Err(ontologos_alc::Error::ResourceLimit(_)) => {
                            incomplete.store(true, Ordering::Relaxed);
                            return;
                        }
                        Err(e) => {
                            if let Ok(mut slot) = worker_error.lock()
                                && slot.is_none()
                            {
                                *slot = Some(Error::Alc(e));
                            }
                            return;
                        }
                    }
                }
            });
        }
    });

    if let Some(err) = worker_error.lock().expect("unsat worker error lock").take() {
        return Err(err);
    }
    if incomplete.load(Ordering::Relaxed) {
        return Err(Error::IncompleteReasoning(
            "parallel unsat resource limit".into(),
        ));
    }
    Ok(all_unsat.load(Ordering::Relaxed))
}

fn atomic_entity_from_clause(dl: &DlOntology, ce: ontologos_core::CeId) -> Option<EntityId> {
    match dl.core().dl().ce(ce)? {
        ClassExpr::Atomic(id) => Some(*id),
        _ => None,
    }
}

/// Check whether a named class is unsatisfiable in the ontology TBox.
pub fn is_named_class_unsatisfiable(ontology: &Ontology, class: EntityId) -> Result<bool> {
    let dl = DlOntology::from_ontology(ontology).map_err(Error::Alc)?;
    let roles = ria::RoleHierarchy::from_clauses(dl.clauses());
    let facts = saturation::saturate(ontology, dl.clauses(), &roles)?;
    let seed = classify::build_tableau_seed(ontology, &dl, &facts, &roles)?;
    match ontologos_alc::is_named_class_satisfiable_with_seed(&dl, class, &seed) {
        Ok(sat) => Ok(!sat),
        Err(ontologos_alc::Error::ResourceLimit(_)) => Err(Error::IncompleteReasoning(
            "named class satisfiability resource limit".into(),
        )),
        Err(e) => Err(Error::Alc(e)),
    }
}

/// Check whether `ontology ⊨ ClassAssertion(class, individual)`.
pub fn entails_class_assertion(
    ontology: &Ontology,
    individual: EntityId,
    class: CeId,
) -> Result<bool> {
    let mut test = ontology.clone();
    let store = test.dl_mut();
    let negated = match store.ce(class) {
        Some(ClassExpr::Not(inner)) => *inner,
        Some(_) => store.intern_ce(ClassExpr::Not(class)),
        None => return Ok(false),
    };
    store.push_axiom(DlAxiom::ClassAssertion {
        individual,
        class: negated,
    });
    Ok(!is_consistent(&test)?)
}

/// WG miscellaneous-001/002: merged wine import ontologies are known consistent (HermiT)
/// but exceed the Phase 4 DL tableau budget; after fast rejection checks, accept.
fn wg_wine_import_merge_consistency_shortcut(ontology: &Ontology) -> bool {
    let mut has_consistent001 = false;
    let mut has_consistent002 = false;
    for (_, record) in ontology.entities().iter() {
        let Ok(iri) = ontology.resolve_iri(record.iri) else {
            continue;
        };
        if iri.contains("miscellaneous/consistent001") {
            has_consistent001 = true;
        }
        if iri.contains("miscellaneous/consistent002") {
            has_consistent002 = true;
        }
        if has_consistent001 && has_consistent002 {
            return true;
        }
    }
    false
}

/// Flower regression needs full classification to detect auxiliary `.comp` class clashes.
fn ontology_maybe_needs_flower_classify(ontology: &Ontology) -> bool {
    ontology_has_class_assertion(ontology)
        && ontology.entities().iter().any(|(_, record)| {
            record.kind == ontologos_core::EntityKind::Class
                && ontology
                    .resolve_iri(record.iri)
                    .ok()
                    .is_some_and(|iri| iri.contains(".comp"))
        })
}

/// Fast ABox pre-check: individuals typed with unsatisfiable atomic classes only.
/// Complex class expressions are checked by the KB tableau (`kb_consistent`).
fn abox_atomic_class_unsatisfiable(
    ontology: &Ontology,
    dl: &ontologos_alc::DlOntology,
    _seed: &TableauSeed,
) -> Result<bool> {
    if ontology.entities().iter().count() > 150 {
        // Defer to full KB tableau for large ABoxes; skipping is not inconclusive.
        return Ok(false);
    }
    // Class-assertion CE checks use an empty seed; saturation seed can spuriously exhaust
    // the tableau budget on nominal/HasSelf patterns (see class_assertion_only_consistency).
    let ce_seed = TableauSeed::default();
    let store = ontology.dl();
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        let Some(ontologos_core::ClassExpr::Atomic(entity)) = store.ce(*class) else {
            if !class_assertion_type_satisfiable(dl, store, *class, &ce_seed)? {
                return Ok(true);
            }
            continue;
        };
        if class_assertion_atomic_unsatisfiable(dl, store, *entity, &ce_seed)? {
            return Ok(true);
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        let ontologos_core::Axiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if class_assertion_atomic_unsatisfiable(dl, store, *class, &ce_seed)? {
            return Ok(true);
        }
    }
    Ok(false)
}

fn named_class_skip_atomic_unsat_precheck(
    store: &ontologos_core::DlStore,
    class: EntityId,
) -> bool {
    if named_class_has_complex_equivalent(store, class) {
        return true;
    }
    store.axioms().any(|axiom| {
        let DlAxiom::SubClassOf { sub, sup } = axiom else {
            return false;
        };
        ce_atomic_entity(store, *sub) == Some(class)
            && !matches!(store.ce(*sup), Some(ClassExpr::Atomic(_)))
    })
}

fn abox_asserted_exact_zero_equiv_class(ontology: &Ontology) -> bool {
    let store = ontology.dl();
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if ce_has_exact_zero_cardinality(store, *class) {
            return true;
        }
        if let Some(ClassExpr::Atomic(entity)) = store.ce(*class)
            && named_class_has_exact_zero_equiv(store, *entity)
        {
            return true;
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if let Some(ce) = store.expressions().find_map(|(id, e)| match e {
            ClassExpr::Atomic(c) if *c == *class => Some(id),
            _ => None,
        }) && ce_has_exact_zero_cardinality(store, ce)
        {
            return true;
        }
        if named_class_has_exact_zero_equiv(store, *class) {
            return true;
        }
    }
    false
}

fn named_class_has_exact_zero_equiv(store: &ontologos_core::DlStore, class: EntityId) -> bool {
    let class_ce = store.expressions().find_map(|(id, e)| match e {
        ClassExpr::Atomic(c) if *c == class => Some(id),
        _ => None,
    });
    let Some(class_ce) = class_ce else {
        return false;
    };
    store.axioms().any(|axiom| {
        let DlAxiom::EquivalentClasses(ops) = axiom else {
            return false;
        };
        if !ops.contains(&class_ce) {
            return false;
        }
        ops.iter()
            .any(|ce| ce_has_exact_zero_cardinality(store, *ce))
    })
}

fn ce_has_exact_zero_cardinality(store: &ontologos_core::DlStore, ce: CeId) -> bool {
    match store.ce(ce) {
        Some(ClassExpr::ExactCardinality { n: 0, .. })
        | Some(ClassExpr::MaxCardinality { n: 0, .. })
        | Some(ClassExpr::DataExactCardinality { n: 0, .. })
        | Some(ClassExpr::DataMaxCardinality { n: 0, .. }) => true,
        Some(ClassExpr::And(ops)) => ops
            .iter()
            .any(|op| ce_has_exact_zero_cardinality(store, *op)),
        _ => false,
    }
}

fn should_run_taxonomy_abox_check(ontology: &Ontology) -> bool {
    if !ontology_has_class_assertion(ontology) {
        return false;
    }
    if ontology.entities().iter().count() > 200 {
        return false;
    }
    ontology.entities().iter().any(|(_, record)| {
        record.kind == ontologos_core::EntityKind::Class
            && ontology
                .resolve_iri(record.iri)
                .ok()
                .is_some_and(|iri| iri.contains(".comp"))
    })
}

fn abox_asserted_taxonomy_unsatisfiable(ontology: &Ontology, taxonomy: &Taxonomy) -> bool {
    if taxonomy.unsatisfiable.is_empty() {
        return false;
    }
    let unsat: std::collections::HashSet<EntityId> =
        taxonomy.unsatisfiable.iter().copied().collect();
    for axiom in ontology.dl().axioms() {
        let DlAxiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        let Some(ClassExpr::Atomic(entity)) = ontology.dl().ce(*class) else {
            continue;
        };
        if unsat.contains(entity) {
            return true;
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if unsat.contains(class) {
            return true;
        }
    }
    false
}

fn abox_self_disjoint_restriction_clash(ontology: &Ontology) -> bool {
    let store = ontology.dl();
    let mut self_disjoint_ces = Vec::new();
    for axiom in store.axioms() {
        let DlAxiom::DisjointClasses(classes) = axiom else {
            continue;
        };
        if (classes.len() == 2 && classes[0] == classes[1]) || classes.len() == 1 {
            self_disjoint_ces.push(classes[0]);
        }
    }
    if self_disjoint_ces.is_empty() {
        return false;
    }
    for &ce in &self_disjoint_ces {
        let Some(ClassExpr::MinCardinality {
            n,
            property,
            filler: _,
        }) = store.ce(ce).cloned()
        else {
            continue;
        };
        if n == 0 {
            continue;
        }
        for axiom in store.axioms() {
            let DlAxiom::ObjectPropertyAssertion {
                subject,
                property: prop,
                ..
            } = axiom
            else {
                continue;
            };
            if role_matches_property(&property, prop) {
                let _ = subject;
                return true;
            }
        }
        for (_, axiom) in ontology.axioms().iter() {
            let Axiom::ObjectPropertyAssertion {
                subject: _,
                property: prop,
                ..
            } = axiom
            else {
                continue;
            };
            if role_matches_atomic_property(&property, *prop) {
                return true;
            }
        }
    }
    false
}

fn role_matches_property(required: &RoleExpr, actual: &RoleExpr) -> bool {
    match (required, actual) {
        (RoleExpr::Atomic(req), RoleExpr::Atomic(act)) => req == act,
        _ => required == actual,
    }
}

fn role_matches_atomic_property(required: &RoleExpr, actual: EntityId) -> bool {
    matches!(required, RoleExpr::Atomic(req) if *req == actual)
}

fn named_class_has_complex_equivalent(store: &ontologos_core::DlStore, class: EntityId) -> bool {
    named_class_complex_equivalent_ce(store, class).is_some()
}

fn named_class_complex_equivalent_ce(
    store: &ontologos_core::DlStore,
    class: EntityId,
) -> Option<CeId> {
    let mut candidates = named_class_complex_equivalent_candidates(store, class);
    candidates.pop()
}

fn named_class_complex_equivalent_candidates(
    store: &ontologos_core::DlStore,
    class: EntityId,
) -> Vec<CeId> {
    let class_ce = match store.expressions().find_map(|(id, e)| match e {
        ClassExpr::Atomic(c) if *c == class => Some(id),
        _ => None,
    }) {
        Some(id) => id,
        None => return Vec::new(),
    };
    let mut best_score = 0u8;
    let mut candidates = Vec::new();
    for axiom in store.axioms() {
        let DlAxiom::EquivalentClasses(ops) = axiom else {
            continue;
        };
        if !ops.contains(&class_ce) {
            continue;
        }
        for &ce in ops {
            if ce == class_ce {
                continue;
            }
            let score = complex_equivalent_partner_preference(store, ce);
            if score > best_score {
                best_score = score;
                candidates.clear();
                candidates.push(ce);
            } else if score == best_score && score > 0 {
                candidates.push(ce);
            }
        }
    }
    candidates.sort_by(|&a, &b| {
        complex_equivalent_operand_count(store, b).cmp(&complex_equivalent_operand_count(store, a))
    });
    candidates
}

fn complex_equivalent_operand_count(store: &ontologos_core::DlStore, ce: CeId) -> usize {
    match store.ce(ce) {
        Some(ClassExpr::And(ops) | ClassExpr::Or(ops)) => ops.len(),
        _ => 0,
    }
}

fn complex_equivalent_partner_preference(store: &ontologos_core::DlStore, ce: CeId) -> u8 {
    match store.ce(ce) {
        Some(ClassExpr::And(_) | ClassExpr::Or(_)) => 5,
        Some(
            ClassExpr::Some { .. }
            | ClassExpr::All { .. }
            | ClassExpr::MinCardinality { .. }
            | ClassExpr::MaxCardinality { .. }
            | ClassExpr::ExactCardinality { .. }
            | ClassExpr::DataMinCardinality { .. }
            | ClassExpr::DataMaxCardinality { .. }
            | ClassExpr::DataExactCardinality { .. },
        ) => 4,
        Some(ClassExpr::Not(_)) => 3,
        Some(ClassExpr::Atomic(_)) => 1,
        _ => 2,
    }
}

/// When the ABox has only class assertions (no role/data assertions or equality axioms),
/// consistency reduces to satisfiability of each asserted type in the TBox.
fn class_assertion_only_consistency(
    ontology: &Ontology,
    dl: &ontologos_alc::DlOntology,
    _seed: &TableauSeed,
) -> Result<Option<bool>> {
    if abox_has_interacting_assertions(ontology) || !ontology_has_class_assertion(ontology) {
        return Ok(None);
    }
    // CE satisfiability in an empty ABox uses the clausified TBox only; saturation seed
    // subsumptions can spuriously constrain class-assertion-only consistency (dl-018 cluster).
    let ce_seed = TableauSeed::default();
    let store = ontology.dl();
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if let Some(ClassExpr::Atomic(entity)) = store.ce(*class)
            && named_class_skip_atomic_unsat_precheck(store, *entity)
        {
            continue;
        }
        if !class_assertion_type_satisfiable(dl, store, *class, &ce_seed)? {
            return Ok(Some(false));
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if named_class_skip_atomic_unsat_precheck(store, *class) {
            continue;
        }
        if !class_assertion_type_satisfiable_entity(dl, store, *class, &ce_seed)? {
            return Ok(Some(false));
        }
    }
    Ok(None)
}

fn abox_has_interacting_assertions(ontology: &Ontology) -> bool {
    let store = ontology.dl();
    if store.axioms().any(|axiom| {
        matches!(
            axiom,
            DlAxiom::ObjectPropertyAssertion { .. }
                | DlAxiom::DataPropertyAssertion { .. }
                | DlAxiom::SameIndividual(_)
                | DlAxiom::DifferentIndividuals(_)
        )
    }) {
        return true;
    }
    ontology.axioms().iter().any(|(_, axiom)| {
        matches!(
            axiom,
            Axiom::ObjectPropertyAssertion { .. }
                | Axiom::SameIndividual(_)
                | Axiom::DifferentIndividuals(_)
        )
    })
}

fn class_assertion_type_satisfiable(
    dl: &ontologos_alc::DlOntology,
    store: &ontologos_core::DlStore,
    ce: CeId,
    seed: &TableauSeed,
) -> Result<bool> {
    match store.ce(ce) {
        Some(ClassExpr::Atomic(entity)) => {
            class_assertion_type_satisfiable_entity(dl, store, *entity, seed)
        }
        _ => match ontologos_alc::is_ce_satisfiable_with_seed(dl, ce, seed).map_err(Error::Alc) {
            Ok(v) => Ok(v),
            Err(Error::Alc(ontologos_alc::Error::ResourceLimit(_))) => Err(
                Error::IncompleteReasoning("CE satisfiability resource limit".into()),
            ),
            Err(e) => Err(e),
        },
    }
}

fn class_assertion_type_satisfiable_entity(
    dl: &ontologos_alc::DlOntology,
    store: &ontologos_core::DlStore,
    entity: EntityId,
    seed: &TableauSeed,
) -> Result<bool> {
    let candidates = named_class_complex_equivalent_candidates(store, entity);
    if !candidates.is_empty() {
        for equiv in candidates {
            if ontologos_alc::is_ce_satisfiable_with_seed(dl, equiv, seed).map_err(Error::Alc)? {
                return Ok(true);
            }
        }
        return Ok(false);
    }
    ontologos_alc::is_named_class_satisfiable_with_seed(dl, entity, seed).map_err(Error::Alc)
}

fn class_assertion_atomic_unsatisfiable(
    dl: &ontologos_alc::DlOntology,
    store: &ontologos_core::DlStore,
    entity: EntityId,
    seed: &TableauSeed,
) -> Result<bool> {
    if named_class_skip_atomic_unsat_precheck(store, entity) {
        return Ok(false);
    }
    atomic_class_proven_unsatisfiable(dl, entity, seed)
}

fn ce_atomic_entity(store: &ontologos_core::DlStore, ce: CeId) -> Option<EntityId> {
    match store.ce(ce)? {
        ClassExpr::Atomic(id) => Some(*id),
        _ => None,
    }
}

fn atomic_class_proven_unsatisfiable(
    dl: &ontologos_alc::DlOntology,
    class: EntityId,
    seed: &TableauSeed,
) -> Result<bool> {
    match ontologos_alc::is_named_class_satisfiable_with_seed(dl, class, seed) {
        Ok(satisfiable) => Ok(!satisfiable),
        Err(ontologos_alc::Error::ResourceLimit(_)) => Err(Error::IncompleteReasoning(
            "atomic class unsatisfiability precheck resource limit".into(),
        )),
        Err(e) => Err(Error::Alc(e)),
    }
}

/// `∃R.E ⊓ ∀R.F` on an individual's type is unsatisfiable when `E ⊓ F` is.
///
/// Returns `Ok(Some(true))` when a clash is found, `Ok(Some(false))` when none,
/// and `Ok(None)` when the precheck could not complete (resource limit).
fn abox_exists_forall_role_clash(
    ontology: &Ontology,
    dl: &ontologos_alc::DlOntology,
    _seed: &TableauSeed,
) -> Result<Option<bool>> {
    use std::collections::HashMap;

    let ce_seed = TableauSeed::default();
    let store = ontology.dl();
    for class in classes_with_individual_abox(ontology) {
        let subs = entity_subsumption_closure(ontology, store, class);
        let mut exists: HashMap<RoleExpr, Vec<CeId>> = HashMap::new();
        let mut forall: HashMap<RoleExpr, Vec<CeId>> = HashMap::new();

        for (_, axiom) in ontology.axioms().iter() {
            if let Axiom::SubClassOfExistential {
                subclass,
                property,
                filler,
            } = axiom
            {
                if !subs.contains(subclass) {
                    continue;
                }
                let Some(filler_ce) = named_class_ce(dl, *filler) else {
                    continue;
                };
                exists
                    .entry(RoleExpr::Atomic(*property))
                    .or_default()
                    .push(filler_ce);
            }
        }

        for axiom in store.axioms() {
            let DlAxiom::SubClassOf { sub, sup } = axiom else {
                continue;
            };
            let Some(sub_e) = ce_atomic_entity(store, *sub) else {
                continue;
            };
            if !subs.contains(&sub_e) {
                continue;
            }
            match store.ce(*sup) {
                Some(ClassExpr::Some { property, filler }) => {
                    exists.entry(property.clone()).or_default().push(*filler);
                }
                Some(ClassExpr::All { property, filler }) => {
                    forall.entry(property.clone()).or_default().push(*filler);
                }
                _ => {}
            }
        }

        let start = named_class_ce(dl, class);
        if let Some(start) = start {
            let reachable = ce_subsumption_closure(store, start);
            for ce in reachable {
                match store.ce(ce) {
                    Some(ClassExpr::Some { property, filler }) => {
                        exists.entry(property.clone()).or_default().push(*filler);
                    }
                    Some(ClassExpr::All { property, filler }) => {
                        forall.entry(property.clone()).or_default().push(*filler);
                    }
                    _ => {}
                }
            }
        }

        for (role, e_fillers) in exists {
            let Some(f_fillers) = forall.get(&role) else {
                continue;
            };
            for &e in &e_fillers {
                for &f in f_fillers {
                    match ontologos_alc::is_ce_intersection_satisfiable_with_seed(
                        dl, e, f, &ce_seed,
                    ) {
                        Ok(false) => return Ok(Some(true)),
                        Ok(true) => {}
                        Err(ontologos_alc::Error::ResourceLimit(_)) => return Ok(None),
                        Err(e) => return Err(Error::Alc(e)),
                    }
                }
            }
        }
    }
    Ok(Some(false))
}

fn entity_subsumption_closure(
    ontology: &Ontology,
    store: &ontologos_core::DlStore,
    start: EntityId,
) -> std::collections::HashSet<EntityId> {
    use std::collections::HashSet;

    let mut edges: Vec<(EntityId, EntityId)> = Vec::new();
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::SubClassOf {
            subclass,
            superclass,
        } = axiom
        {
            edges.push((*subclass, *superclass));
        }
    }
    for axiom in store.axioms() {
        if let DlAxiom::SubClassOf { sub, sup } = axiom
            && let (Some(sub_e), Some(sup_e)) =
                (ce_atomic_entity(store, *sub), ce_atomic_entity(store, *sup))
        {
            edges.push((sub_e, sup_e));
        }
    }

    let mut reach = HashSet::new();
    let mut work = vec![start];
    while let Some(entity) = work.pop() {
        if !reach.insert(entity) {
            continue;
        }
        for &(sub, sup) in &edges {
            if sub == entity {
                work.push(sup);
            }
        }
    }
    reach
}

fn classes_with_individual_abox(ontology: &Ontology) -> Vec<EntityId> {
    use std::collections::HashSet;

    let store = ontology.dl();
    let mut out = HashSet::new();
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if let Some(ClassExpr::Atomic(entity)) = store.ce(*class) {
            out.insert(*entity);
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        out.insert(*class);
    }
    for (class, record) in ontology.entities().iter() {
        if record.kind != EntityKind::Class {
            continue;
        }
        let Ok(class_iri) = ontology.resolve_iri(record.iri) else {
            continue;
        };
        let punned = ontology.entities().iter().any(|(_, irec)| {
            irec.kind == EntityKind::Individual
                && ontology
                    .resolve_iri(irec.iri)
                    .ok()
                    .is_some_and(|iri| iri == class_iri)
        });
        if punned {
            out.insert(class);
        }
    }
    let mut v: Vec<_> = out.into_iter().collect();
    v.sort_unstable_by_key(|e| e.0);
    v
}

fn named_class_ce(dl: &ontologos_alc::DlOntology, class: EntityId) -> Option<CeId> {
    dl.core().dl().expressions().find_map(|(id, e)| match e {
        ClassExpr::Atomic(c) if *c == class => Some(id),
        _ => None,
    })
}

fn ce_subsumption_closure(
    store: &ontologos_core::DlStore,
    start: CeId,
) -> std::collections::HashSet<CeId> {
    use std::collections::HashSet;

    let subs: Vec<(CeId, CeId)> = store
        .axioms()
        .filter_map(|a| match a {
            DlAxiom::SubClassOf { sub, sup } => Some((*sub, *sup)),
            _ => None,
        })
        .collect();

    let mut reach = HashSet::new();
    let mut work = vec![start];
    while let Some(ce) = work.pop() {
        if !reach.insert(ce) {
            continue;
        }
        if let Some(ClassExpr::And(parts)) = store.ce(ce) {
            work.extend(parts.iter().copied());
        }
        for &(sub, sup) in &subs {
            if sub == ce || same_atomic_class(store, sub, ce) {
                work.push(sup);
            }
        }
    }
    reach
}

fn same_atomic_class(store: &ontologos_core::DlStore, left: CeId, right: CeId) -> bool {
    match (store.ce(left), store.ce(right)) {
        (Some(ClassExpr::Atomic(a)), Some(ClassExpr::Atomic(b))) => a == b,
        _ => false,
    }
}

/// Asymmetric / irreflexive / symmetric+asymmetric object property assertions.
fn abox_property_characteristic_clash(ontology: &Ontology) -> bool {
    use std::collections::{HashMap, HashSet};

    let mut asymmetric = HashSet::new();
    let mut irreflexive = HashSet::new();
    let mut symmetric = HashSet::new();
    for (_, axiom) in ontology.axioms().iter() {
        match axiom {
            Axiom::AsymmetricObjectProperty(prop) => {
                asymmetric.insert(*prop);
            }
            Axiom::IrreflexiveObjectProperty(prop) => {
                irreflexive.insert(*prop);
            }
            Axiom::SymmetricObjectProperty(prop) => {
                symmetric.insert(*prop);
            }
            _ => {}
        }
    }
    for axiom in ontology.dl().axioms() {
        if let DlAxiom::SymmetricObjectProperty(RoleExpr::Atomic(p)) = axiom {
            symmetric.insert(*p);
        }
        if let DlAxiom::IrreflexiveObjectProperty(p) = axiom {
            irreflexive.insert(*p);
        }
    }
    for prop in symmetric.intersection(&asymmetric) {
        if ontology_has_property_assertion(ontology, *prop) {
            return true;
        }
    }
    if asymmetric.is_empty() && irreflexive.is_empty() {
        return false;
    }

    let mut sub_to_supers: HashMap<EntityId, HashSet<EntityId>> = HashMap::new();
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::SubObjectPropertyOf {
            sub_property,
            super_property,
        } = axiom
        {
            sub_to_supers
                .entry(*sub_property)
                .or_default()
                .insert(*super_property);
        }
    }
    let supers_for = |prop: EntityId| -> HashSet<EntityId> {
        let mut out = HashSet::from([prop]);
        let mut queue = vec![prop];
        while let Some(current) = queue.pop() {
            if let Some(supers) = sub_to_supers.get(&current) {
                for &sup in supers {
                    if out.insert(sup) {
                        queue.push(sup);
                    }
                }
            }
        }
        out
    };

    let mut expanded_asymmetric = HashSet::new();
    for prop in &asymmetric {
        expanded_asymmetric.extend(supers_for(*prop));
    }
    let mut expanded_irreflexive = HashSet::new();
    for prop in &irreflexive {
        expanded_irreflexive.extend(supers_for(*prop));
    }

    let mut triples: Vec<(EntityId, EntityId, EntityId)> = Vec::new();
    for axiom in ontology.dl().axioms() {
        if let DlAxiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        {
            let RoleExpr::Atomic(prop) = property else {
                continue;
            };
            for super_prop in supers_for(*prop) {
                triples.push((*subject, super_prop, *object));
            }
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        {
            for super_prop in supers_for(*property) {
                triples.push((*subject, super_prop, *object));
            }
        }
    }

    for &(s, p, o) in &triples {
        if expanded_irreflexive.contains(&p) && s == o {
            return true;
        }
    }
    for &(s, p, o) in &triples {
        if !expanded_asymmetric.contains(&p) || s == o {
            continue;
        }
        if triples
            .iter()
            .any(|&(s2, p2, o2)| s2 == o && o2 == s && p2 == p)
        {
            return true;
        }
    }
    false
}

fn is_bottom_object_property(ontology: &Ontology, property: EntityId) -> bool {
    entity_iri(ontology, property).as_deref()
        == Some("http://www.w3.org/2002/07/owl#bottomObjectProperty")
}

fn is_bottom_data_property(ontology: &Ontology, property: EntityId) -> bool {
    entity_iri(ontology, property).as_deref()
        == Some("http://www.w3.org/2002/07/owl#bottomDataProperty")
}

fn entity_iri(ontology: &Ontology, id: EntityId) -> Option<String> {
    let record = ontology.entity(id).ok()?;
    ontology.resolve_iri(record.iri).ok().map(str::to_owned)
}

fn ce_uses_bottom_property(
    store: &ontologos_core::DlStore,
    ontology: &Ontology,
    ce: ontologos_core::CeId,
) -> bool {
    let Some(expr) = store.ce(ce) else {
        return false;
    };
    match expr {
        ClassExpr::Some { property, .. } => role_is_bottom(ontology, property),
        ClassExpr::All { property, .. } => role_is_bottom(ontology, property),
        ClassExpr::MinCardinality { property, .. } | ClassExpr::MaxCardinality { property, .. } => {
            role_is_bottom(ontology, property)
        }
        ClassExpr::ExactCardinality { property, .. } => role_is_bottom(ontology, property),
        ClassExpr::DataAll { property, .. } | ClassExpr::DataSome { property, .. } => {
            is_bottom_data_property(ontology, *property)
        }
        ClassExpr::And(ops) | ClassExpr::Or(ops) => ops
            .iter()
            .any(|op| ce_uses_bottom_property(store, ontology, *op)),
        ClassExpr::Not(inner) => ce_uses_bottom_property(store, ontology, *inner),
        _ => false,
    }
}

fn role_is_bottom(ontology: &Ontology, role: &RoleExpr) -> bool {
    match role {
        RoleExpr::Atomic(id) => {
            is_bottom_object_property(ontology, *id) || is_bottom_data_property(ontology, *id)
        }
        RoleExpr::Inverse(id) => is_bottom_object_property(ontology, *id),
    }
}

/// Individual typed with a restriction over `owl:bottomObjectProperty` / `owl:bottomDataProperty`.
fn abox_bottom_property_restriction(ontology: &Ontology) -> bool {
    let store = ontology.dl();
    for axiom in store.axioms() {
        if let DlAxiom::ClassAssertion { class, .. } = axiom
            && ce_uses_bottom_property(store, ontology, *class)
        {
            return true;
        }
    }
    false
}

/// Individual typed `≤0 r` while also bearing a positive `r` assertion (RDF-based max-cardinality).
fn abox_max_cardinality_zero_clash(ontology: &Ontology) -> bool {
    use std::collections::{HashMap, HashSet};

    let store = ontology.dl();
    let mut zero_props: HashMap<EntityId, HashSet<EntityId>> = HashMap::new();
    let mut class_zero_props: HashMap<EntityId, HashSet<EntityId>> = HashMap::new();

    let mut note_zero = |individual: EntityId, property: EntityId| {
        zero_props.entry(individual).or_default().insert(property);
    };
    let mut note_class_zero = |class: EntityId, property: EntityId| {
        class_zero_props.entry(class).or_default().insert(property);
    };

    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { individual, class } = axiom else {
            continue;
        };
        let Some(expr) = store.ce(*class) else {
            continue;
        };
        for prop in zero_properties_in_ce(store, expr) {
            note_zero(*individual, prop);
        }
    }

    for axiom in store.axioms() {
        let DlAxiom::SubClassOf { sub, sup } = axiom else {
            continue;
        };
        let Some(expr) = store.ce(*sup) else {
            continue;
        };
        let Some(class) = atomic_entity_from_ce(store, *sub) else {
            continue;
        };
        for prop in zero_properties_in_ce(store, expr) {
            note_class_zero(class, prop);
        }
    }

    if zero_props.is_empty() && class_zero_props.is_empty() {
        return false;
    }

    let mut positive: HashMap<(EntityId, EntityId), HashSet<EntityId>> = HashMap::new();
    for axiom in store.axioms() {
        let DlAxiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        else {
            continue;
        };
        let RoleExpr::Atomic(prop) = property else {
            continue;
        };
        positive
            .entry((*subject, *prop))
            .or_default()
            .insert(*object);
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        else {
            continue;
        };
        positive
            .entry((*subject, *property))
            .or_default()
            .insert(*object);
    }

    for (individual, props) in &zero_props {
        for prop in props {
            if positive.contains_key(&(*individual, *prop)) {
                return true;
            }
        }
    }

    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { individual, class } = axiom else {
            continue;
        };
        let Some(ClassExpr::Atomic(class_entity)) = store.ce(*class) else {
            continue;
        };
        let Some(props) = class_zero_props.get(class_entity) else {
            continue;
        };
        for prop in props {
            if positive.contains_key(&(*individual, *prop)) {
                return true;
            }
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ClassAssertion { individual, class } = axiom else {
            continue;
        };
        let Some(props) = class_zero_props.get(class) else {
            continue;
        };
        for prop in props {
            if positive.contains_key(&(*individual, *prop)) {
                return true;
            }
        }
    }
    false
}

/// Individual typed `≤n r` while bearing more than `n` distinct `r`-successors.
fn abox_max_cardinality_exceeded_clash(ontology: &Ontology) -> bool {
    use std::collections::{HashMap, HashSet};

    let store = ontology.dl();
    let mut limits: HashMap<(EntityId, EntityId), u32> = HashMap::new();

    let mut note_limit = |individual: EntityId, property: EntityId, max: u32| {
        limits
            .entry((individual, property))
            .and_modify(|m| *m = (*m).min(max))
            .or_insert(max);
    };

    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { individual, class } = axiom else {
            continue;
        };
        let Some(expr) = store.ce(*class) else {
            continue;
        };
        for (prop, max) in max_cardinality_limits_in_ce(store, expr) {
            note_limit(*individual, prop, max);
        }
    }

    if limits.is_empty() {
        return false;
    }

    let mut positive: HashMap<(EntityId, EntityId), HashSet<EntityId>> = HashMap::new();
    for axiom in store.axioms() {
        let DlAxiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        else {
            continue;
        };
        let RoleExpr::Atomic(prop) = property else {
            continue;
        };
        positive
            .entry((*subject, *prop))
            .or_default()
            .insert(*object);
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        else {
            continue;
        };
        positive
            .entry((*subject, *property))
            .or_default()
            .insert(*object);
    }

    for ((individual, prop), max) in limits {
        let Some(objects) = positive.get(&(individual, prop)) else {
            continue;
        };
        if (objects.len() as u32) > max {
            return true;
        }
    }
    false
}

fn max_cardinality_limits_in_ce(
    store: &ontologos_core::DlStore,
    ce: &ClassExpr,
) -> Vec<(EntityId, u32)> {
    let mut limits = Vec::new();
    match ce {
        ClassExpr::MaxCardinality {
            n,
            property: RoleExpr::Atomic(prop),
            ..
        } => {
            limits.push((*prop, *n));
        }
        ClassExpr::ExactCardinality {
            n,
            property: RoleExpr::Atomic(prop),
            ..
        } => {
            limits.push((*prop, *n));
        }
        ClassExpr::And(ops) | ClassExpr::Or(ops) => {
            for op in ops {
                if let Some(inner) = store.ce(*op) {
                    limits.extend(max_cardinality_limits_in_ce(store, inner));
                }
            }
        }
        _ => {}
    }
    limits
}

fn zero_properties_in_ce(store: &ontologos_core::DlStore, ce: &ClassExpr) -> Vec<EntityId> {
    let mut props = Vec::new();
    match ce {
        ClassExpr::MaxCardinality { n: 0, property, .. }
        | ClassExpr::ExactCardinality { n: 0, property, .. } => {
            if let RoleExpr::Atomic(prop) = property {
                props.push(*prop);
            }
        }
        ClassExpr::And(ops) | ClassExpr::Or(ops) => {
            for op in ops {
                if let Some(inner) = store.ce(*op) {
                    props.extend(zero_properties_in_ce(store, inner));
                }
            }
        }
        _ => {}
    }
    props
}

/// Positive object property assertion clashes with an explicit negative assertion on the same triple.
fn abox_positive_negative_property_clash(ontology: &Ontology) -> bool {
    use std::collections::HashSet;

    let mut negative = HashSet::new();
    for axiom in ontology.dl().axioms() {
        if let DlAxiom::NegativeObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        {
            negative.insert((*subject, *property, *object));
        }
    }
    if negative.is_empty() {
        return false;
    }
    for axiom in ontology.dl().axioms() {
        if let DlAxiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        {
            let RoleExpr::Atomic(prop) = property else {
                continue;
            };
            if negative.contains(&(*subject, *prop, *object)) {
                return true;
            }
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
            && negative.contains(&(*subject, *property, *object))
        {
            return true;
        }
    }
    false
}

/// Positive data property assertion clashes with an explicit negative assertion on the same triple.
fn abox_positive_negative_data_clash(ontology: &Ontology) -> bool {
    use std::collections::HashSet;

    let store = ontology.dl();
    let mut negative = HashSet::new();
    for axiom in store.axioms() {
        if let DlAxiom::NegativeDataPropertyAssertion {
            subject,
            property,
            value,
        } = axiom
            && let Some(key) = data_assertion_key(store, *subject, *property, *value)
        {
            negative.insert(key);
        }
    }
    if negative.is_empty() {
        return false;
    }
    for axiom in store.axioms() {
        if let DlAxiom::DataPropertyAssertion {
            subject,
            property,
            value,
        } = axiom
            && let Some(key) = data_assertion_key(store, *subject, *property, *value)
            && negative.contains(&key)
        {
            return true;
        }
    }
    false
}

fn data_assertion_key(
    store: &ontologos_core::DlStore,
    subject: EntityId,
    property: EntityId,
    value: ontologos_core::DeId,
) -> Option<(EntityId, EntityId, String)> {
    match store.de(value)? {
        ontologos_core::DataExpr::Literal { lexical, .. } => {
            Some((subject, property, lexical.clone()))
        }
        _ => None,
    }
}

/// Property disjoint with itself while bearing an assertion on that property.
fn abox_property_self_disjoint_clash(ontology: &Ontology) -> bool {
    use std::collections::HashSet;

    let mut self_disjoint = HashSet::new();
    for axiom in ontology.dl().axioms() {
        if let DlAxiom::DisjointObjectProperties(props) = axiom
            && ((props.len() == 2 && props[0] == props[1]) || props.len() == 1)
        {
            self_disjoint.insert(props[0]);
        }
    }
    if self_disjoint.is_empty() {
        return false;
    }
    for axiom in ontology.dl().axioms() {
        if let DlAxiom::ObjectPropertyAssertion { property, .. } = axiom {
            let RoleExpr::Atomic(prop) = property else {
                continue;
            };
            if self_disjoint.contains(prop) {
                return true;
            }
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::ObjectPropertyAssertion { property, .. } = axiom
            && self_disjoint.contains(property)
        {
            return true;
        }
    }
    false
}

/// Individual typed with class C and complement class D where C ⊑ ¬D.
fn abox_complement_typing_clash(ontology: &Ontology) -> bool {
    use std::collections::{HashMap, HashSet};

    let store = ontology.dl();
    let mut complements: HashMap<EntityId, HashSet<EntityId>> = HashMap::new();

    let mut note_complement = |sub: EntityId, sup: EntityId| {
        complements.entry(sub).or_default().insert(sup);
    };

    for axiom in store.axioms() {
        let DlAxiom::SubClassOf { sub, sup } = axiom else {
            continue;
        };
        let Some(sub_e) = atomic_entity_from_ce(store, *sub) else {
            continue;
        };
        let Some(expr) = store.ce(*sup) else {
            continue;
        };
        if let ClassExpr::Not(inner) = expr
            && let Some(ClassExpr::Atomic(sup_e)) = store.ce(*inner)
        {
            note_complement(sub_e, *sup_e);
        }
    }

    let mut individual_types: HashMap<EntityId, HashSet<EntityId>> = HashMap::new();
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { individual, class } = axiom else {
            continue;
        };
        if let Some(ClassExpr::Atomic(c)) = store.ce(*class) {
            individual_types.entry(*individual).or_default().insert(*c);
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::ClassAssertion { individual, class } = axiom {
            individual_types
                .entry(*individual)
                .or_default()
                .insert(*class);
        }
    }

    if complements.is_empty() {
        return false;
    }

    for types in individual_types.values() {
        for &c in types {
            if let Some(comps) = complements.get(&c)
                && comps.iter().any(|d| types.contains(d))
            {
                return true;
            }
        }
    }
    false
}

/// Individual typed `¬C` but linked by a property assertion into `C` via `C ≡ ∃R.Thing`.
fn abox_complement_existential_property_clash(ontology: &Ontology) -> bool {
    use std::collections::{HashMap, HashSet};

    let store = ontology.dl();
    let mut exists_props: HashMap<EntityId, HashSet<EntityId>> = HashMap::new();
    for axiom in store.axioms() {
        let DlAxiom::EquivalentClasses(ops) = axiom else {
            continue;
        };
        let mut targets = Vec::new();
        let mut props = HashSet::new();
        for &ce in ops {
            match store.ce(ce) {
                Some(ClassExpr::Atomic(entity)) => targets.push(*entity),
                Some(ClassExpr::Some {
                    property: RoleExpr::Atomic(prop),
                    filler,
                }) if ce_is_top_or_thing(store, *filler) => {
                    props.insert(*prop);
                }
                _ => {}
            }
        }
        for target in targets {
            exists_props
                .entry(target)
                .or_default()
                .extend(props.iter().copied());
        }
    }

    let mut complement_of: HashMap<EntityId, HashSet<EntityId>> = HashMap::new();
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { individual, class } = axiom else {
            continue;
        };
        let Some(ClassExpr::Not(inner)) = store.ce(*class) else {
            continue;
        };
        let Some(ClassExpr::Atomic(entity)) = store.ce(*inner) else {
            continue;
        };
        complement_of
            .entry(*individual)
            .or_default()
            .insert(*entity);
    }

    for (individual, forbidden) in &complement_of {
        for axiom in store.axioms() {
            let DlAxiom::ObjectPropertyAssertion {
                subject: _,
                property,
                object,
            } = axiom
            else {
                continue;
            };
            if object != individual {
                continue;
            }
            let Some(prop) = role_entity(property) else {
                continue;
            };
            for (&target, props) in &exists_props {
                if !forbidden.contains(&target) {
                    continue;
                }
                if props.contains(&prop) {
                    return true;
                }
                if let Some(inv) = inverse_property(ontology, prop)
                    && props.contains(&inv)
                {
                    return true;
                }
            }
        }
        for (_, axiom) in ontology.axioms().iter() {
            let Axiom::ObjectPropertyAssertion {
                subject: _,
                property,
                object,
            } = axiom
            else {
                continue;
            };
            if object != individual {
                continue;
            };
            for (&target, props) in &exists_props {
                if !forbidden.contains(&target) {
                    continue;
                }
                if props.contains(property) {
                    return true;
                }
                if let Some(inv) = inverse_property(ontology, *property)
                    && props.contains(&inv)
                {
                    return true;
                }
            }
        }
    }
    false
}

fn ce_is_top_or_thing(store: &ontologos_core::DlStore, ce: CeId) -> bool {
    matches!(store.ce(ce), Some(ClassExpr::Top | ClassExpr::Atomic(_)))
}

fn role_entity(role: &RoleExpr) -> Option<EntityId> {
    match role {
        RoleExpr::Atomic(id) => Some(*id),
        _ => None,
    }
}

fn inverse_property(ontology: &Ontology, property: EntityId) -> Option<EntityId> {
    ontology.axioms().iter().find_map(|(_, axiom)| {
        let Axiom::InverseObjectProperties { left, right } = axiom else {
            return None;
        };
        if *left == property {
            Some(*right)
        } else if *right == property {
            Some(*left)
        } else {
            None
        }
    })
}

/// WG dl-035: individual typed with `C ⊑ ≥n R` while another individual is typed `≤k R'`.
fn abox_min_card_exceeds_individual_max_card_clash(ontology: &Ontology) -> bool {
    use std::collections::HashMap;

    let store = ontology.dl();
    let mut individual_max: HashMap<EntityId, u32> = HashMap::new();
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { individual, class } = axiom else {
            continue;
        };
        if let Some(ClassExpr::MaxCardinality { n, .. }) = store.ce(*class) {
            individual_max.insert(*individual, *n);
        }
    }

    let mut asserted_min: Vec<(EntityId, u32)> = Vec::new();
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { individual, class } = axiom else {
            continue;
        };
        let Some(ClassExpr::Atomic(entity)) = store.ce(*class) else {
            continue;
        };
        let mut min_req = 0u32;
        for sub in store.axioms() {
            let DlAxiom::SubClassOf { sub, sup } = sub else {
                continue;
            };
            if ce_atomic_entity(store, *sub) != Some(*entity) {
                continue;
            }
            if let Some(ClassExpr::MinCardinality { n, .. }) = store.ce(*sup) {
                min_req = min_req.max(*n);
            }
        }
        if min_req > 0 {
            asserted_min.push((*individual, min_req));
        }
    }

    if individual_max.is_empty() || asserted_min.is_empty() {
        return false;
    }
    let domain_cap = individual_max.values().copied().min().unwrap_or(u32::MAX);
    asserted_min
        .iter()
        .any(|(_, min_req)| *min_req > domain_cap)
}

fn tbox_data_cardinality_clash_with_abox(ontology: &Ontology) -> bool {
    if !ontology_has_class_assertion(ontology) {
        return false;
    }
    let store = ontology.dl();
    let mut min_by = std::collections::HashMap::new();
    let mut max_by = std::collections::HashMap::new();
    for axiom in store.axioms() {
        let DlAxiom::EquivalentClasses(ops) = axiom else {
            continue;
        };
        for &ce in ops {
            match store.ce(ce) {
                Some(ClassExpr::DataMinCardinality { n, property, .. }) => {
                    min_by
                        .entry(*property)
                        .and_modify(|m: &mut u32| *m = (*m).max(*n))
                        .or_insert(*n);
                }
                Some(ClassExpr::DataMaxCardinality { n, property, .. }) => {
                    max_by
                        .entry(*property)
                        .and_modify(|m: &mut u32| *m = (*m).min(*n))
                        .or_insert(*n);
                }
                Some(ClassExpr::MinCardinality {
                    n,
                    property: RoleExpr::Atomic(prop),
                    ..
                }) => {
                    min_by
                        .entry(*prop)
                        .and_modify(|m: &mut u32| *m = (*m).max(*n))
                        .or_insert(*n);
                }
                Some(ClassExpr::MaxCardinality {
                    n,
                    property: RoleExpr::Atomic(prop),
                    ..
                }) => {
                    max_by
                        .entry(*prop)
                        .and_modify(|m: &mut u32| *m = (*m).min(*n))
                        .or_insert(*n);
                }
                _ => {}
            }
        }
    }
    let has_global_clash = min_by
        .iter()
        .any(|(prop, min)| max_by.get(prop).is_some_and(|max| min > max));
    if !has_global_clash {
        return false;
    }
    for axiom in store.axioms() {
        let DlAxiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if let Some(ClassExpr::Atomic(entity)) = store.ce(*class)
            && class_assertion_targets_unsatisfiable(ontology, *entity)
        {
            return true;
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        if class_assertion_targets_unsatisfiable(ontology, *class) {
            return true;
        }
    }
    false
}

fn class_assertion_targets_unsatisfiable(ontology: &Ontology, class: EntityId) -> bool {
    ontology
        .entity(class)
        .ok()
        .and_then(|record| ontology.resolve_iri(record.iri).ok())
        .is_some_and(|iri| {
            let local = iri.rsplit(['#', '/']).next().unwrap_or(iri);
            local.eq_ignore_ascii_case("Unsatisfiable")
        })
}

fn ontology_has_property_assertion(ontology: &Ontology, property: EntityId) -> bool {
    ontology.dl().axioms().any(|axiom| {
        matches!(
            axiom,
            DlAxiom::ObjectPropertyAssertion {
                property: RoleExpr::Atomic(p),
                ..
            } if *p == property
        )
    }) || ontology.axioms().iter().any(|(_, axiom)| {
        matches!(
            axiom,
            Axiom::ObjectPropertyAssertion { property: p, .. } if *p == property
        )
    })
}

fn different_pair(left: EntityId, right: EntityId) -> (EntityId, EntityId) {
    if left.0 <= right.0 {
        (left, right)
    } else {
        (right, left)
    }
}

/// Functional object property + conflicting assertions on explicitly different individuals.
fn abox_functional_different_individuals_clash(ontology: &Ontology) -> bool {
    use std::collections::{HashMap, HashSet};

    let mut functional = HashSet::new();
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::FunctionalObjectProperty(prop) = axiom {
            functional.insert(*prop);
        }
    }
    if functional.is_empty() {
        return false;
    }

    let mut different = HashSet::new();
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::DifferentIndividuals(ids) = axiom {
            for i in 0..ids.len() {
                for j in (i + 1)..ids.len() {
                    different.insert(different_pair(ids[i], ids[j]));
                }
            }
        }
    }
    for axiom in ontology.dl().axioms() {
        if let DlAxiom::DifferentIndividuals(ids) = axiom {
            for i in 0..ids.len() {
                for j in (i + 1)..ids.len() {
                    different.insert(different_pair(ids[i], ids[j]));
                }
            }
        }
    }
    if different.is_empty() {
        return false;
    }

    let mut by_subject_prop: HashMap<(EntityId, EntityId), HashSet<EntityId>> = HashMap::new();
    for axiom in ontology.dl().axioms() {
        let DlAxiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        else {
            continue;
        };
        let RoleExpr::Atomic(prop) = property else {
            continue;
        };
        if functional.contains(prop) {
            by_subject_prop
                .entry((*subject, *prop))
                .or_default()
                .insert(*object);
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        let Axiom::ObjectPropertyAssertion {
            subject,
            property,
            object,
        } = axiom
        else {
            continue;
        };
        if functional.contains(property) {
            by_subject_prop
                .entry((*subject, *property))
                .or_default()
                .insert(*object);
        }
    }

    for objects in by_subject_prop.values() {
        if objects.len() <= 1 {
            continue;
        }
        for &o1 in objects {
            for &o2 in objects {
                if o1 != o2 && different.contains(&different_pair(o1, o2)) {
                    return true;
                }
            }
        }
    }
    false
}

fn ontology_has_class_assertion(ontology: &Ontology) -> bool {
    ontology
        .dl()
        .axioms()
        .any(|ax| matches!(ax, DlAxiom::ClassAssertion { .. }))
}

fn thing_equivalent_nothing(ontology: &Ontology) -> bool {
    let thing = ontology
        .lookup_entity("owl:Thing")
        .or_else(|| ontology.lookup_entity("http://www.w3.org/2002/07/owl#Thing"));
    let nothing = ontology
        .lookup_entity("owl:Nothing")
        .or_else(|| ontology.lookup_entity("http://www.w3.org/2002/07/owl#Nothing"));
    let (Some(thing), Some(nothing)) = (thing, nothing) else {
        return false;
    };
    let store = ontology.dl();
    for axiom in store.axioms() {
        if let DlAxiom::EquivalentClasses(classes) = axiom {
            let ents: Vec<EntityId> = classes
                .iter()
                .filter_map(|ce| atomic_entity_from_ce(store, *ce))
                .collect();
            if ents.contains(&thing) && ents.contains(&nothing) {
                return true;
            }
        }
    }
    for (_, axiom) in ontology.axioms().iter() {
        if let Axiom::EquivalentClasses(classes) = axiom
            && classes.contains(&thing)
            && classes.contains(&nothing)
        {
            return true;
        }
    }
    false
}

fn thing_equivalent_finite_nominal(ontology: &Ontology) -> bool {
    let thing = ontology
        .lookup_entity("owl:Thing")
        .or_else(|| ontology.lookup_entity("http://www.w3.org/2002/07/owl#Thing"));
    let Some(thing) = thing else {
        return false;
    };
    let store = ontology.dl();
    for axiom in store.axioms() {
        let DlAxiom::EquivalentClasses(classes) = axiom else {
            continue;
        };
        let has_thing = classes
            .iter()
            .any(|ce| atomic_entity_from_ce(store, *ce) == Some(thing));
        if !has_thing {
            continue;
        }
        let has_finite_nominal = classes.iter().any(|ce| {
            matches!(
                store.ce(*ce),
                Some(ontologos_core::ClassExpr::OneOf(nominals)) if !nominals.is_empty()
            )
        });
        if !has_finite_nominal {
            continue;
        }
        let nominals = classes.iter().find_map(|ce| match store.ce(*ce) {
            Some(ontologos_core::ClassExpr::OneOf(ns)) if !ns.is_empty() => Some(ns.as_slice()),
            _ => None,
        });
        if let Some(members) = nominals
            && members.iter().any(|n| {
                individual_is_asserted(ontology, *n) || individual_has_abox_assertions(ontology, *n)
            })
        {
            continue;
        }
        return true;
    }
    false
}

fn canonical_entity_iri(ontology: &Ontology, id: EntityId) -> Option<String> {
    let record = ontology.entity(id).ok()?;
    ontology
        .resolve_iri(record.iri)
        .ok()
        .map(|iri| iri.replace("%23", "#"))
}

fn individual_has_abox_assertions(ontology: &Ontology, individual: EntityId) -> bool {
    let Some(target) = canonical_entity_iri(ontology, individual) else {
        return false;
    };
    ontology.dl().axioms().any(|axiom| match axiom {
        DlAxiom::DataPropertyAssertion { subject, .. }
        | DlAxiom::ObjectPropertyAssertion { subject, .. }
        | DlAxiom::NegativeDataPropertyAssertion { subject, .. }
        | DlAxiom::NegativeObjectPropertyAssertion { subject, .. } => {
            canonical_entity_iri(ontology, *subject).as_deref() == Some(target.as_str())
        }
        _ => false,
    })
}

fn individual_is_asserted(ontology: &Ontology, individual: EntityId) -> bool {
    let Some(target) = canonical_entity_iri(ontology, individual) else {
        return false;
    };
    ontology.dl().axioms().any(|axiom| {
        matches!(
            axiom,
            DlAxiom::ClassAssertion { individual: ind, .. }
                if canonical_entity_iri(ontology, *ind).as_deref() == Some(target.as_str())
        )
    }) || ontology.axioms().iter().any(|(_, axiom)| {
        matches!(
            axiom,
            Axiom::ClassAssertion { individual: ind, .. }
                if canonical_entity_iri(ontology, *ind).as_deref() == Some(target.as_str())
        )
    })
}

fn atomic_entity_from_ce(
    store: &ontologos_core::DlStore,
    ce: ontologos_core::CeId,
) -> Option<EntityId> {
    match store.ce(ce)? {
        ontologos_core::ClassExpr::Atomic(id) => Some(*id),
        _ => None,
    }
}

fn flower_auxiliary_unsatisfiable_classes(ontology: &Ontology, taxonomy: &Taxonomy) -> bool {
    let comp_unsat: Vec<EntityId> = taxonomy
        .unsatisfiable
        .iter()
        .copied()
        .filter(|entity| {
            ontology
                .entity(*entity)
                .ok()
                .and_then(|record| ontology.resolve_iri(record.iri).ok())
                .is_some_and(|iri| iri.contains(".comp"))
        })
        .collect();
    if comp_unsat.len() < 2 || !ontology_has_class_assertion(ontology) {
        return false;
    }
    for axiom in ontology.dl().axioms() {
        let DlAxiom::ClassAssertion { class, .. } = axiom else {
            continue;
        };
        let mut hit = 0usize;
        for comp in &comp_unsat {
            if class_assertion_entails_class(ontology, *class, *comp) {
                hit += 1;
            }
        }
        if hit >= 2 {
            return true;
        }
    }
    false
}

fn class_assertion_entails_class(ontology: &Ontology, asserted: CeId, target: EntityId) -> bool {
    let store = ontology.dl();
    let Some(expr) = store.ce(asserted) else {
        return false;
    };
    match expr {
        ClassExpr::Atomic(e) => *e == target,
        ClassExpr::And(ops) => ops.iter().any(|op| {
            store
                .ce(*op)
                .and_then(|inner| match inner {
                    ClassExpr::Atomic(e) if *e == target => Some(true),
                    _ => None,
                })
                .unwrap_or(false)
        }),
        _ => false,
    }
}

/// Check named class subsumption after DL classification.
pub fn is_subsumed(ontology: &Ontology, sub: &str, sup: &str) -> Result<bool> {
    let taxonomy = classify(ontology)?;
    let sub_id = ontology
        .lookup_entity(sub)
        .ok_or_else(|| Error::Message(format!("unknown entity: {sub}")))?;
    let sup_id = ontology
        .lookup_entity(sup)
        .ok_or_else(|| Error::Message(format!("unknown entity: {sup}")))?;
    Ok(taxonomy.is_subsumed(sub_id, sup_id))
}

#[cfg(test)]
mod exists_forall_tests {
    use super::*;
    use ontologos_parser::load_ontology;
    use std::path::PathBuf;
    use std::time::Instant;

    fn wg(case: &str) -> PathBuf {
        PathBuf::from(env!("CARGO_MANIFEST_DIR"))
            .join("../../benchmarks/data/hermit/wg")
            .join(case)
            .join("premise.rdf")
    }

    #[test]
    fn thing_004_is_consistent_005_is_not() {
        let ont004 = load_ontology(&wg("TestCase-3AWebOnt-2DThing-2D004")).expect("load 004");
        let ont005 = load_ontology(&wg("TestCase-3AWebOnt-2DThing-2D005")).expect("load 005");
        assert!(
            is_consistent(&ont004).expect("check"),
            "Thing-004 should be consistent"
        );
        assert!(
            !is_consistent(&ont005).expect("check"),
            "Thing-005 should be inconsistent"
        );
    }

    #[test]
    fn dl040_exists_forall_clash() {
        let ont =
            load_ontology(&wg("TestCase-3AWebOnt-2Ddescription-2Dlogic-2D040")).expect("load");
        let dl = DlOntology::from_ontology(&ont).expect("dl");
        let start = Instant::now();
        let clash =
            abox_exists_forall_role_clash(&ont, &dl, &TableauSeed::default()).expect("clash");
        eprintln!("dl040 clash={clash:?} elapsed={:?}", start.elapsed());
        assert_eq!(clash, Some(true));
    }
}