docs: public Set<Explanation<E>> computePreciseJustsOptimised(E entailment, int limit) throws OWLException {
          this.limit = limit;
          foundLaconicJustifications.clear();
          ExplanationGenerator<E> gen = explanationGeneratorFactory.createExplanationGenerator(axioms, this);
          Set<Explanation<E>> regularJusts = null;
          try {
              regularJusts = gen.getExplanations(entailment);
          }
          catch (ExplanationGeneratorInterruptedException e) {
              // We have interrupted the generator via our progress monitor
              return foundLaconicJustifications;
          }
          if (isCancelled()) {
              return foundLaconicJustifications;
          }
          lastRegularJusts.clear();
  
          // Initialise the current set of justifications with the regular justifications.
          allPreviouslyFoundJustifications = new HashSet<Explanation<E>>();
          allPreviouslyFoundJustifications.addAll(regularJusts);
  
  //        Set<Explanation<E>> nonLaconicJusts = new HashSet<Explanation<E>>();
  //        Set<Explanation<E>> laconicJusts = new HashSet<Explanation<E>>();
  
          Set<OWLAxiom> axiomsInPreviousOntology = new HashSet<OWLAxiom>();
  
          // We compute justifications until we can't find anymore
          while (true) {
  
              if (isCancelled()) {
                  return getReconstitutedLaconicJustifications();
              }
              // Now we take the union of our current set of justifications and compute
              // O+ from this set.
  
              Set<OWLAxiom> unionOfAllJustifications = new HashSet<OWLAxiom>();
              for (Explanation<E> exp : allPreviouslyFoundJustifications) {
                  unionOfAllJustifications.addAll(exp.getAxioms());
              }
              Set<OWLAxiom> oPlus = computeOPlus(unionOfAllJustifications);
  
              // Create our new ontology.
              Set<OWLAxiom> augmentedAxioms = new HashSet<OWLAxiom>(oPlus);
  
              ///////////////////////////////////////////////////////////////////////////
              // OPTIMISATION
              //////////////////////////////////////////////////////////////////////////
  
              // Exactly which axioms to we add the ontology?  We need to
              // limit the axioms that we add to O+ to limit the number of
              // intermediate justifications.  Without limiting the performance impact
              // can be HUGE.
              // Basically, if an checker at some stage appeared in a justification that we
              // found, but it never appears in O+ then we don't add it to the ontology.
              // The rationale behind this is that certain axioms such as equivalent classes
              // checker will never ever appear in O+ or in a precise justification.
              for (OWLAxiom ax : ont.getLogicalAxioms()) {
                  // If we have found the checker previously in a justification
                  // but our O+ doesn't contain it then we don't add it.
                  if (unionOfAllJustifications.contains(ax) && !oPlus.contains(ax)) {
                      continue;
                  }
                  augmentedAxioms.add(ax);
              }
  
              //////////////////////////////////////////////////////////////////////////
              //////////////////////////////////////////////////////////////////////////
  
              // Next optimisation
  
  
              if (augmentedAxioms.equals(axiomsInPreviousOntology)) {
                  break;
              }
  
              ExplanationGenerator<E> gen2 = explanationGeneratorFactory.createExplanationGenerator(augmentedAxioms, this);
  
              axiomsInPreviousOntology.clear();
              axiomsInPreviousOntology.addAll(augmentedAxioms);
  
              Set<Explanation> allPrevJustsCopy = new HashSet<Explanation>(allPreviouslyFoundJustifications);
  
              // Create a generator that gets ALL explanations from OPlus
              Set<Explanation<E>> currentJustifications = null;
              try {
                  currentJustifications = gen2.getExplanations(entailment);
              }
              catch (ExplanationGeneratorInterruptedException e) {
                  return getReconstitutedLaconicJustifications();
              }
              if (isCancelled()) {
                  return getReconstitutedLaconicJustifications();
              }
              allPreviouslyFoundJustifications.addAll(currentJustifications);
              if (allPreviouslyFoundJustifications.equals(allPrevJustsCopy)) {
                  break;
              }
              // The following code used to check if we had found enough laconic justifcations.  We don't need this
              // anymore - I don't think
  //            for (Explanation<E> e : currentJustifications) {
  //                if (nonLaconicJusts.contains(e)) {
  //                    continue;
  //                }
  //                if (laconicJusts.contains(e)) {
  //                    continue;
  //                }
  //                if (isLaconic(e)) {
  //                    laconicJusts.add(e);
  //                }
  //                else {
  //                    nonLaconicJusts.add(e);
  //                }
  //                if (laconicJusts.size() == limit) {
  //                    return getReconstitutedLaconicJustifications(laconicJusts);
  //                }
  //            }
          }
  
  //        Set<Explanation<E>> laconicJustifications = new HashSet<Explanation<E>>();
  //
  //        // We should now have our justifications that contain the set of precise justifications.
  //        // We just need to know which ones are the precise justifications.
  //        for (Explanation<E> justification : allPreviouslyFoundJustifications) {
  //            if (nonLaconicJusts.contains(justification)) {
  //                continue;
  //            }
  //            if (laconicJusts.contains(justification)) {
  //                laconicJustifications.add(justification);
  //            } else {
  //                if (isLaconic(justification)) {
  //                    laconicJustifications.add(justification);
  //                }
  //            }
  //        }
  
          return getReconstitutedLaconicJustifications();
      }