pub fn nnf_complement(cid: ConceptId, pool: &mut ConceptPool) -> ConceptIdExpand description
Compute nnf(¬C) given C (already assumed NNF or convertible).
Exposed for the tableau’s choose rule, which needs the NNF
complement of a concept when branching on ≤n R.C.