gt:             if (!hasType) {
context: /* Copyright 2008, 2009, 2010 by the Oxford University Computing Laboratory
  
     This file is part of HermiT.
  
     HermiT is free software: you can redistribute it and/or modify
     it under the terms of the GNU Lesser General Public License as published by
     the Free Software Foundation, either version 3 of the License, or
     (at your option) any later version.
  
     HermiT is distributed in the hope that it will be useful,
     but WITHOUT ANY WARRANTY; without even the implied warranty of
     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
     GNU Lesser General Public License for more details.
  
     You should have received a copy of the GNU Lesser General Public License
     along with HermiT.  If not, see <http://www.gnu.org/licenses/>.
   */
  
  package org.semanticweb.HermiT.hierarchy;
  
  import java.util.ArrayList;
  import java.util.Arrays;
  import java.util.Collections;
  import java.util.HashMap;
  import java.util.HashSet;
  import java.util.LinkedList;
  import java.util.List;
  import java.util.Map;
  import java.util.Queue;
  import java.util.Set;
  
  import org.semanticweb.HermiT.Prefixes;
  import org.semanticweb.HermiT.Reasoner;
  import org.semanticweb.HermiT.graph.Graph;
  import org.semanticweb.HermiT.hierarchy.DeterministicClassification.GraphNode;
  import org.semanticweb.HermiT.hierarchy.RoleElementManager.RoleElement;
  import org.semanticweb.HermiT.model.Atom;
  import org.semanticweb.HermiT.model.AtomicConcept;
  import org.semanticweb.HermiT.model.AtomicRole;
  import org.semanticweb.HermiT.model.DLClause;
  import org.semanticweb.HermiT.model.DLOntology;
  import org.semanticweb.HermiT.model.DLPredicate;
  import org.semanticweb.HermiT.model.Individual;
  import org.semanticweb.HermiT.model.Inequality;
  import org.semanticweb.HermiT.model.InverseRole;
  import org.semanticweb.HermiT.model.Role;
  import org.semanticweb.HermiT.monitor.TableauMonitor;
  import org.semanticweb.HermiT.tableau.ExtensionManager;
  import org.semanticweb.HermiT.tableau.ExtensionTable;
  import org.semanticweb.HermiT.tableau.InterruptFlag;
  import org.semanticweb.HermiT.tableau.Node;
  import org.semanticweb.HermiT.tableau.NodeType;
  import org.semanticweb.HermiT.tableau.ReasoningTaskDescription;
  import org.semanticweb.HermiT.tableau.Tableau;
  import org.semanticweb.owlapi.model.IRI;
  import org.semanticweb.owlapi.model.OWLAxiom;
  import org.semanticweb.owlapi.model.OWLClass;
  import org.semanticweb.owlapi.model.OWLClassExpression;
  import org.semanticweb.owlapi.model.OWLDataFactory;
  import org.semanticweb.owlapi.model.OWLNamedIndividual;
  import org.semanticweb.owlapi.model.OWLObjectProperty;
  import org.semanticweb.owlapi.reasoner.ReasonerProgressMonitor;
  
  public class InstanceManager {
      public static final int thresholdForAdditionalAxioms=10000;
  
      protected final InterruptFlag m_interruptFlag;
      protected final Reasoner m_reasoner;
      protected final TableauMonitor m_tableauMonitor;
      protected final Individual[] m_individuals;
      protected final HashSet<AtomicRole> m_complexRoles;
      protected final Map<AtomicConcept,AtomicConceptElement> m_conceptToElement;
      protected final AtomicConcept m_topConcept;
      protected final AtomicConcept m_bottomConcept;
      protected Hierarchy<AtomicConcept> m_currentConceptHierarchy;
      protected final RoleElementManager m_roleElementManager;
      protected final RoleElement m_topRoleElement;
      protected final RoleElement m_bottomRoleElement;
      protected Hierarchy<RoleElement> m_currentRoleHierarchy;
      protected final boolean m_usesInverseRoles;
      protected final Map<Individual, Node> m_nodesForIndividuals;
      protected final Map<Node,Individual> m_individualsForNodes;
      protected final Map<Node,Set<Node>> m_canonicalNodeToDetMergedNodes;
      protected final Map<Node,Set<Node>> m_canonicalNodeToNonDetMergedNodes;
      protected boolean m_isInconsistent;
      protected boolean m_realizationCompleted;
      protected boolean m_roleRealizationCompleted;
      protected boolean m_usesClassifiedConceptHierarchy;
      protected boolean m_usesClassifiedObjectRoleHierarchy;
      protected boolean m_classesInitialised;
      protected boolean m_propertiesInitialised;
      protected boolean m_readingOffFoundPossibleConceptInstance;
      protected boolean m_readingOffFoundPossiblePropertyInstance;
      protected final Map<Individual,Set<Individual>> m_individualToEquivalenceClass;
      protected Map<Set<Individual>,Set<Set<Individual>>> m_individualToPossibleEquivalenceClass;
      protected final ExtensionTable.Retrieval m_binaryRetrieval0Bound;
      protected final ExtensionTable.Retrieval m_binaryRetrieval1Bound;
      protected final ExtensionTable.Retrieval m_binaryRetrieval01Bound;
      protected final ExtensionTable.Retrieval m_ternaryRetrieval1Bound;
      protected final ExtensionTable.Retrieval m_ternaryRetrieval0Bound;
      protected final ExtensionTable.Retrieval m_ternaryRetrieval012Bound;
      protected int m_currentIndividualIndex=0;
  
      public InstanceManager(InterruptFlag interruptFlag,Reasoner reasoner,Hierarchy<AtomicConcept> atomicConceptHierarchy,Hierarchy<Role> objectRoleHierarchy) {
          m_interruptFlag=interruptFlag;
          m_interruptFlag.startTask();
          try {
              m_reasoner=reasoner;
              m_tableauMonitor=m_reasoner.getTableau().getTableauMonitor();
              DLOntology dlo=m_reasoner.getDLOntology();
              m_individuals=new ArrayList<Individual>(dlo.getAllIndividuals()).toArray(new Individual[0]);
              m_complexRoles=new HashSet<AtomicRole>();
              m_individualToEquivalenceClass=new HashMap<Individual, Set<Individual>>();
              m_nodesForIndividuals=new HashMap<Individual,Node>();
              for (Individual individual : m_individuals) {
                  m_nodesForIndividuals.put(individual,null);
                  Set<Individual> equivalentIndividuals=new HashSet<Individual>();
                  equivalentIndividuals.add(individual);
                  m_individualToEquivalenceClass.put(individual, equivalentIndividuals);
                  m_interruptFlag.checkInterrupt();
              }
              m_individualsForNodes=new HashMap<Node,Individual>();
              m_canonicalNodeToDetMergedNodes=new HashMap<Node,Set<Node>>();
              m_canonicalNodeToNonDetMergedNodes=new HashMap<Node,Set<Node>>();
              m_individualToPossibleEquivalenceClass=null;
  
              m_topConcept=AtomicConcept.THING;
              m_bottomConcept=AtomicConcept.NOTHING;
              m_conceptToElement=new HashMap<AtomicConcept, AtomicConceptElement>();
              m_conceptToElement.put(m_topConcept, new AtomicConceptElement(null, null));
              Graph<AtomicConcept> knownConceptSubsumptions=null;
              Set<AtomicConcept> atomicConcepts=null;
              if (atomicConceptHierarchy!=null)
                  setToClassifiedConceptHierarchy(atomicConceptHierarchy);
              else {
                  knownConceptSubsumptions=new Graph<AtomicConcept>();
                  atomicConcepts=new HashSet<AtomicConcept>();
                  atomicConcepts.add(m_topConcept);
                  atomicConcepts.add(m_bottomConcept);
                  for (AtomicConcept atomicConcept : dlo.getAllAtomicConcepts()) {
                      if (!Prefixes.isInternalIRI(atomicConcept.getIRI())) {
                          atomicConcepts.add(atomicConcept);
                          addKnownConceptSubsumption(knownConceptSubsumptions,atomicConcept,atomicConcept);
                          addKnownConceptSubsumption(knownConceptSubsumptions,atomicConcept,m_topConcept);
                          addKnownConceptSubsumption(knownConceptSubsumptions,m_bottomConcept,atomicConcept);
                      }
                      m_interruptFlag.checkInterrupt();
                  }
                  addKnownConceptSubsumption(knownConceptSubsumptions,m_bottomConcept,m_bottomConcept);
              }
  
              m_roleElementManager=new RoleElementManager();
              Graph<Role> knownRoleSubsumptions=null;
              m_topRoleElement=m_roleElementManager.getRoleElement(AtomicRole.TOP_OBJECT_ROLE);
              m_bottomRoleElement=m_roleElementManager.getRoleElement(AtomicRole.BOTTOM_OBJECT_ROLE);
              m_usesInverseRoles=dlo.hasInverseRoles();
              Set<Role> roles=null;
              Set<Role> complexRoles=dlo.getAllComplexObjectRoles();
              if (objectRoleHierarchy!=null) {
                  setToClassifiedRoleHierarchy(objectRoleHierarchy);
                  for (Role role : complexRoles)
                      if (role instanceof AtomicRole && role!=AtomicRole.TOP_OBJECT_ROLE && role!=AtomicRole.BOTTOM_OBJECT_ROLE)
                          m_complexRoles.add((AtomicRole)role);
              }
              else {
                  knownRoleSubsumptions=new Graph<Role>();
                  roles=new HashSet<Role>();
                  roles.add(AtomicRole.TOP_OBJECT_ROLE);
                  roles.add(AtomicRole.BOTTOM_OBJECT_ROLE);
                  roles.addAll(dlo.getAllAtomicObjectRoles());
                  for (Role role : roles) {
                      addKnownRoleSubsumption(knownRoleSubsumptions,role,role);
                      addKnownRoleSubsumption(knownRoleSubsumptions,role,AtomicRole.TOP_OBJECT_ROLE);
                      addKnownRoleSubsumption(knownRoleSubsumptions,AtomicRole.BOTTOM_OBJECT_ROLE,role);
                      if (complexRoles.contains(role) && role instanceof AtomicRole && role!=AtomicRole.TOP_OBJECT_ROLE && role!=AtomicRole.BOTTOM_OBJECT_ROLE)
                          m_complexRoles.add((AtomicRole)role);
                      m_interruptFlag.checkInterrupt();
                  }
                  addKnownRoleSubsumption(knownRoleSubsumptions,AtomicRole.BOTTOM_OBJECT_ROLE,AtomicRole.BOTTOM_OBJECT_ROLE);
              }
              if (atomicConceptHierarchy==null || objectRoleHierarchy==null) {
                  updateKnownSubsumptionsUsingToldSubsumers(dlo.getDLClauses(),knownConceptSubsumptions,atomicConcepts,knownRoleSubsumptions,roles);
              }
              if (atomicConceptHierarchy==null)
                  m_currentConceptHierarchy=buildTransitivelyReducedConceptHierarchy(knownConceptSubsumptions);
              if (objectRoleHierarchy==null)
                  m_currentRoleHierarchy=buildTransitivelyReducedRoleHierarchy(knownRoleSubsumptions);
              ExtensionManager extensionManager=m_reasoner.getTableau().getExtensionManager();
              m_binaryRetrieval0Bound=extensionManager.getBinaryExtensionTable().createRetrieval(new boolean[] { true, false }, ExtensionTable.View.TOTAL);
              m_binaryRetrieval1Bound=extensionManager.getBinaryExtensionTable().createRetrieval(new boolean[] { false, true }, ExtensionTable.View.TOTAL);
              m_binaryRetrieval01Bound=extensionManager.getBinaryExtensionTable().createRetrieval(new boolean[] { true, true }, ExtensionTable.View.TOTAL);
              m_ternaryRetrieval1Bound=extensionManager.getTernaryExtensionTable().createRetrieval(new boolean[] { false,true,false }, ExtensionTable.View.TOTAL);
              m_ternaryRetrieval0Bound=extensionManager.getTernaryExtensionTable().createRetrieval(new boolean[] { true,false,false }, ExtensionTable.View.TOTAL);
              m_ternaryRetrieval012Bound=extensionManager.getTernaryExtensionTable().createRetrieval(new boolean[] { true,true,true }, ExtensionTable.View.TOTAL);
          }
          finally {
              m_interruptFlag.endTask();
          }
      }
      protected void addKnownConceptSubsumption(Graph<AtomicConcept> knownSubsumptions,AtomicConcept subConcept,AtomicConcept superConcept) {
          knownSubsumptions.addEdge(subConcept,superConcept);
      }
      protected void addKnownRoleSubsumption(Graph<Role> knownSubsumptions,Role subRole,Role superRole) {
          knownSubsumptions.addEdge(subRole,superRole);
          if (m_usesInverseRoles)
              knownSubsumptions.addEdge(subRole.getInverse(),superRole.getInverse());
      }
      protected void updateKnownSubsumptionsUsingToldSubsumers(Set<DLClause> dlClauses, Graph<AtomicConcept> knownConceptSubsumptions,Set<AtomicConcept> concepts,Graph<Role> knownRoleSubsumptions,Set<Role> roles) {
          boolean requiresConceptSubsumers=knownConceptSubsumptions!=null;
          boolean requiresRoleSubsumers=knownRoleSubsumptions!=null;
          if (requiresConceptSubsumers || requiresRoleSubsumers) {
              for (DLClause dlClause : dlClauses) {
                  if (dlClause.getHeadLength()==1 && dlClause.getBodyLength()==1) {
                      DLPredicate headPredicate=dlClause.getHeadAtom(0).getDLPredicate();
                      DLPredicate bodyPredicate=dlClause.getBodyAtom(0).getDLPredicate();
                      if (requiresConceptSubsumers && headPredicate instanceof AtomicConcept && bodyPredicate instanceof AtomicConcept) {
                          AtomicConcept headConcept=(AtomicConcept)headPredicate;
                          AtomicConcept bodyConcept=(AtomicConcept)bodyPredicate;
                          if (concepts.contains(headConcept) && concepts.contains(bodyConcept))
                              addKnownConceptSubsumption(knownConceptSubsumptions,bodyConcept,headConcept);
                      }
                      else if (requiresRoleSubsumers && headPredicate instanceof AtomicRole && bodyPredicate instanceof AtomicRole) {
                          AtomicRole headRole=(AtomicRole)headPredicate;
                          AtomicRole bodyRole=(AtomicRole)bodyPredicate;
                          if (roles.contains(headRole) && roles.contains(bodyRole)) {
                              if (dlClause.getBodyAtom(0).getArgument(0)!=dlClause.getHeadAtom(0).getArgument(0))
                                  // r -> s^- and r^- -> s
                                  addKnownRoleSubsumption(knownRoleSubsumptions,InverseRole.create(bodyRole),headRole);
                              else
                                  // r-> s and r^- -> s^-
                                  addKnownRoleSubsumption(knownRoleSubsumptions,bodyRole,headRole);
                          }
                      }
                  }
                  m_interruptFlag.checkInterrupt();
              }
          }
      }
      protected Hierarchy<AtomicConcept> buildTransitivelyReducedConceptHierarchy(Graph<AtomicConcept> knownSubsumptions) {
          final Map<AtomicConcept,GraphNode<AtomicConcept>> allSubsumers=new HashMap<AtomicConcept,GraphNode<AtomicConcept>>();
          for (AtomicConcept element : knownSubsumptions.getElements())
              allSubsumers.put(element,new GraphNode<AtomicConcept>(element,knownSubsumptions.getSuccessors(element)));
          m_interruptFlag.checkInterrupt();
          return DeterministicClassification.buildHierarchy(m_topConcept,m_bottomConcept,allSubsumers);
      }
      public void setToClassifiedConceptHierarchy(Hierarchy<AtomicConcept> atomicConceptHierarchy) {
          if (atomicConceptHierarchy!=m_currentConceptHierarchy) {
              m_currentConceptHierarchy=atomicConceptHierarchy;
              if (m_classesInitialised && m_individuals.length>0) {
                  for (HierarchyNode<AtomicConcept> node : m_currentConceptHierarchy.getAllNodesSet()) {
                      if (node.m_representative!=m_bottomConcept) {
                          AtomicConcept representativeConcept=node.getRepresentative();
                          Set<Individual> known=new HashSet<Individual>();
                          Set<Individual> possible=null;
                          for (AtomicConcept concept : node.getEquivalentElements()) {
                              if (m_conceptToElement.containsKey(concept)) {
                                  AtomicConceptElement element=m_conceptToElement.get(concept);
                                  known.addAll(element.m_knownInstances);
                                  if (possible==null)
                                      possible=new HashSet<Individual>(element.m_possibleInstances);
                                  else
                                      possible.retainAll(element.m_possibleInstances);
                                  m_conceptToElement.remove(concept);
                              }
                          }
                          if (possible!=null)
                              possible.removeAll(known);
                          if (!known.isEmpty()||possible!=null||representativeConcept==m_topConcept)
                              m_conceptToElement.put(representativeConcept, new AtomicConceptElement(known, possible));
                      }
                  }
                  // clean up known and possibles
                  Queue<HierarchyNode<AtomicConcept>> toProcess=new LinkedList<HierarchyNode<AtomicConcept>>();
                  toProcess.addAll(m_currentConceptHierarchy.m_bottomNode.m_parentNodes);
                  while (!toProcess.isEmpty()) {
                      HierarchyNode<AtomicConcept> current=toProcess.remove();
                      AtomicConcept currentConcept=current.getRepresentative();
                      AtomicConceptElement currentElement=m_conceptToElement.get(currentConcept);
                      if (currentElement!=null) {
                          Set<HierarchyNode<AtomicConcept>> ancestors=current.getAncestorNodes();
                          ancestors.remove(current);
                          for (HierarchyNode<AtomicConcept> ancestor : ancestors) {
                              AtomicConcept ancestorConcept=ancestor.getRepresentative();
                              AtomicConceptElement ancestorElement=m_conceptToElement.get(ancestorConcept);
                              if (ancestorElement!=null) {
                                  ancestorElement.m_knownInstances.removeAll(currentElement.m_knownInstances);
                                  ancestorElement.m_possibleInstances.removeAll(currentElement.m_knownInstances);
                                  ancestorElement.m_possibleInstances.removeAll(currentElement.m_possibleInstances);
                              }
                          }
                          for (HierarchyNode<AtomicConcept> parent : current.getParentNodes())
                              if (!toProcess.contains(parent))
                                  toProcess.add(parent);
                      }
                      m_interruptFlag.checkInterrupt();
                  }
              }
              m_usesClassifiedConceptHierarchy=true;
          }
      }
      protected Hierarchy<RoleElement> buildTransitivelyReducedRoleHierarchy(Graph<Role> knownSubsumptions) {
          final Map<Role,GraphNode<Role>> allSubsumers=new HashMap<Role,GraphNode<Role>>();
          for (Role role : knownSubsumptions.getElements())
              allSubsumers.put(role,new GraphNode<Role>(role,knownSubsumptions.getSuccessors(role)));
          m_interruptFlag.checkInterrupt();
          return transformRoleHierarchy(DeterministicClassification.buildHierarchy(AtomicRole.TOP_OBJECT_ROLE,AtomicRole.BOTTOM_OBJECT_ROLE,allSubsumers));
      }
      /**
       * Removes the inverses from the given hierarchy and then converts Role hierarchy nodes to RoleElement hierarchy nodes, which can store
       * known and possible instances.
       * @param roleHierarchy
       * @return a hierarchy containing role element nodes and no inverses
       */
      protected Hierarchy<RoleElement> transformRoleHierarchy(final Hierarchy<Role> roleHierarchy) {
          Hierarchy<AtomicRole> newHierarchy=removeInverses(roleHierarchy);
          Hierarchy.Transformer<Role,RoleElement> transformer=new Hierarchy.Transformer<Role,RoleElement>() {
              public RoleElement transform(Role role) {
                  m_interruptFlag.checkInterrupt();
                  if (!(role instanceof AtomicRole))
                      throw new IllegalArgumentException("Internal error: The instance manager should only use atomic roles, but here we got a hierarchy element for an inverse role:" + role);
                  return m_roleElementManager.getRoleElement((AtomicRole)role);
              }
              public RoleElement determineRepresentative(Role oldRepresentative,Set<RoleElement> newEquivalentElements) {
                  RoleElement representative=transform(oldRepresentative);
                  for (RoleElement newEquiv : newEquivalentElements) {
                      if (!newEquiv.equals(representative)) {
                          for (Individual individual : newEquiv.m_knownRelations.keySet()) {
                              Set<Individual> successors=representative.m_knownRelations.get(individual);
                              if (successors==null) {
                                  successors=new HashSet<Individual>();
                                  representative.m_knownRelations.put(individual, successors);
                              }
                              successors.addAll(newEquiv.m_knownRelations.get(individual));
                          }
                          for (Individual individual : newEquiv.m_possibleRelations.keySet()) {
                              Set<Individual> successors=representative.m_possibleRelations.get(individual);
                              if (successors!=null) {
                                  successors.retainAll(newEquiv.m_possibleRelations.get(individual));
                              }
                          }
                          newEquiv.m_knownRelations.clear();
                          newEquiv.m_possibleRelations.clear();
                      }
                  }
                  m_interruptFlag.checkInterrupt();
                  return representative;
              }
          };
          return newHierarchy.transform(transformer,null);
      }
      protected Hierarchy<AtomicRole> removeInverses(Hierarchy<Role> hierarchy) {
          final Map<AtomicRole,GraphNode<AtomicRole>> allSubsumers=new HashMap<AtomicRole,GraphNode<AtomicRole>>();
          Set<AtomicRole> toProcess=new HashSet<AtomicRole>();
          Set<AtomicRole> visited=new HashSet<AtomicRole>();
          toProcess.add(m_bottomRoleElement.m_role);
          while (!toProcess.isEmpty()) {
              AtomicRole current=toProcess.iterator().next();
              visited.add(current);
              HierarchyNode<Role> currentNode=hierarchy.getNodeForElement(current);
              Set<AtomicRole> atomicRepresentatives=new HashSet<AtomicRole>();
              findNextHierarchyNodeWithAtomic(atomicRepresentatives, currentNode);
              allSubsumers.put(current,new GraphNode<AtomicRole>(current,atomicRepresentatives));
              toProcess.addAll(atomicRepresentatives);
              toProcess.removeAll(visited);
              m_interruptFlag.checkInterrupt();
          }
          Hierarchy<AtomicRole> newHierarchy=DeterministicClassification.buildHierarchy(m_topRoleElement.m_role,m_bottomRoleElement.m_role,allSubsumers);
          for (AtomicRole element : newHierarchy.m_nodesByElements.keySet()) {
              HierarchyNode<Role> oldNode=hierarchy.getNodeForElement(element);
              HierarchyNode<AtomicRole> newNode=newHierarchy.getNodeForElement(element);
              for (Role equivalent : oldNode.m_equivalentElements) {
                  if (equivalent instanceof AtomicRole)
                      newNode.m_equivalentElements.add((AtomicRole)equivalent);
              }
              m_interruptFlag.checkInterrupt();
          }
          return newHierarchy;
      }
      public void setToClassifiedRoleHierarchy(final Hierarchy<Role> roleHierarchy) {
          m_currentRoleHierarchy=transformRoleHierarchy(roleHierarchy);
          // clean up known and possibles
          if (m_propertiesInitialised && m_individuals.length>0) {
              Queue<HierarchyNode<RoleElement>> toProcess=new LinkedList<HierarchyNode<RoleElement>>();
              toProcess.add(m_currentRoleHierarchy.m_bottomNode);
              while (!toProcess.isEmpty()) {
                  HierarchyNode<RoleElement> current=toProcess.remove();
                  RoleElement currentRepresentative=current.getRepresentative();
                  Set<HierarchyNode<RoleElement>> ancestors=current.getAncestorNodes();
                  ancestors.remove(current);
                  for (HierarchyNode<RoleElement> ancestor : ancestors) {
                      RoleElement ancestorRepresentative=ancestor.m_representative;
                      Map<Individual,Set<Individual>> ancestorKnowRelations=ancestorRepresentative.m_knownRelations;
                      Map<Individual,Set<Individual>> ancestorPossibleRelations=ancestorRepresentative.m_possibleRelations;
                      for (Individual individual : currentRepresentative.m_knownRelations.keySet()) {
                          Set<Individual> successors=ancestorKnowRelations.get(individual);
                          if (successors!=null) {
                              successors.removeAll(currentRepresentative.m_knownRelations.get(individual));
                              if (successors.isEmpty())
                                  ancestorKnowRelations.remove(individual);
                          }
                          successors=ancestorPossibleRelations.get(individual);
                          if (successors!=null) {
                              successors.removeAll(currentRepresentative.m_knownRelations.get(individual));
                              if (successors.isEmpty())
                                  ancestorPossibleRelations.remove(individual);
                          }
                      }
                      for (Individual individual : currentRepresentative.m_possibleRelations.keySet()) {
                          Set<Individual> successors=ancestorPossibleRelations.get(individual);
                          if (successors!=null) {
                              successors.removeAll(currentRepresentative.m_possibleRelations.get(individual));
                              if (successors.isEmpty())
                                  ancestorPossibleRelations.remove(individual);
                          }
                      }
                  }
                  for (HierarchyNode<RoleElement> parent : current.getParentNodes())
                      if (!toProcess.contains(parent))
                          toProcess.add(parent);
                  m_interruptFlag.checkInterrupt();
              }
          }
          m_usesClassifiedObjectRoleHierarchy=true;
      }
      protected void findNextHierarchyNodeWithAtomic(Set<AtomicRole> atomicRepresentatives, HierarchyNode<Role> current) {
          for (HierarchyNode<Role> successor : current.getParentNodes()) {
              Set<AtomicRole> suitable=new HashSet<AtomicRole>();
              for (Role role : successor.getEquivalentElements()) {
                  if (role instanceof AtomicRole)
                      suitable.add((AtomicRole)role);
              }
              if (!suitable.isEmpty())
                  atomicRepresentatives.add(suitable.iterator().next());
              else if (successor!=current)
                  findNextHierarchyNodeWithAtomic(atomicRepresentatives, successor);
          }
      }
      public OWLAxiom[] getAxiomsForReadingOffCompexProperties(OWLDataFactory factory, ReasonerProgressMonitor monitor, int completedSteps, int steps) {
          if (m_complexRoles.size()>0) {
              int noAdditionalAxioms=0;
              List<OWLAxiom> additionalAxioms=new ArrayList<OWLAxiom>();
              m_interruptFlag.startTask();
              try {
                  for (;m_currentIndividualIndex<m_individuals.length && noAdditionalAxioms < thresholdForAdditionalAxioms;m_currentIndividualIndex++) {
                      Individual ind=m_individuals[m_currentIndividualIndex];
                      for (AtomicRole objectRole : m_complexRoles) {
                          completedSteps++;
                          if (monitor!=null)
                              monitor.reasonerTaskProgressChanged(completedSteps,steps);
                          OWLObjectProperty objectProperty=factory.getOWLObjectProperty(IRI.create(objectRole.getIRI()));
                          String indIRI=ind.getIRI();
                          OWLClass classForIndividual=factory.getOWLClass(IRI.create("internal:individual-concept#"+indIRI));
                          OWLAxiom axiom=factory.getOWLClassAssertionAxiom(classForIndividual,factory.getOWLNamedIndividual(IRI.create(indIRI)));
                          additionalAxioms.add(axiom); // A_a(a)
                          AtomicConcept conceptForRole=AtomicConcept.create("internal:individual-concept#"+objectRole.getIRI()+"#"+indIRI);
                          OWLClass classForRoleAndIndividual=factory.getOWLClass(IRI.create(conceptForRole.getIRI()));
                          axiom=factory.getOWLSubClassOfAxiom(classForIndividual,factory.getOWLObjectAllValuesFrom(objectProperty,classForRoleAndIndividual));
                          additionalAxioms.add(axiom); // A_a implies forall r.A_a^r
                          noAdditionalAxioms+=2;
                          m_interruptFlag.checkInterrupt();
                      }
                  }
              } finally {
                  m_interruptFlag.endTask();
              }
              OWLAxiom[] additionalAxiomsArray=new OWLAxiom[additionalAxioms.size()];
              return additionalAxioms.toArray(additionalAxiomsArray);
          }
          else {
              m_currentIndividualIndex=m_individuals.length-1;
              return new OWLAxiom[0];
          }
      }
      public void initializeKnowAndPossibleClassInstances(Tableau tableau, ReasonerProgressMonitor monitor, int completedSteps, int steps) {
          if (!m_classesInitialised) {
              m_interruptFlag.startTask();
              try {
                  initializeIndividualsForNodes();
                  if (!m_propertiesInitialised) {
                      // nothing has been read-off yet
                      initializeSameAs();
                  }
                  completedSteps=readOffClassInstancesByIndividual(tableau, monitor, completedSteps, steps);
                  if (!m_readingOffFoundPossibleConceptInstance && m_usesClassifiedConceptHierarchy)
                      m_realizationCompleted=true;
                  m_classesInitialised=true;
                  m_individualsForNodes.clear();
                  m_canonicalNodeToDetMergedNodes.clear();
                  m_canonicalNodeToNonDetMergedNodes.clear();
              } finally {
                  m_interruptFlag.endTask();
              }
          }
      }
      protected int readOffClassInstancesByIndividual(Tableau tableau, ReasonerProgressMonitor monitor, int completedSteps, int steps) {
          for (Individual ind : m_individuals) {
              Node nodeForIndividual=m_nodesForIndividuals.get(ind);
              // read of concept instances and normal role instances only once, we don't slice that
              boolean hasType=readOffTypes(ind,nodeForIndividual);
  