Maybe fixed bug in internalisation.

12 files changed, 335 insertions, 250 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/endomorph/Endomorph.java b/src/uk/ac/ox/cs/pagoda/endomorph/Endomorph.java
index cde0895..1c853d7 100644
--- a/src/uk/ac/ox/cs/pagoda/endomorph/Endomorph.java
+++ b/src/uk/ac/ox/cs/pagoda/endomorph/Endomorph.java
@@ -85,10 +85,18 @@ public class Endomorph extends Checker {
         }
 
         @Override
+        public int getNoOfCalls() {
+                return fullReasoner.getNoOfCalls();
+        }
+
+        @Override
         public void dispose() {
                 super.dispose();
 
-                fullReasoner.dispose();
+                if(fullReasoner != null) {
+//                      Utility.logInfo("Hermit was called " + fullReasoner.getNoOfCalls() + " times");
+                        fullReasoner.dispose();
+                }
         }
         
         public Graph getGraph() {
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
index 2471c80..33f9f03 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageQueryEngine.java
@@ -83,21 +83,6 @@ public class MultiStageQueryEngine extends StageQueryEngine {
         return materialise(program, treatment, gap);
     }
 
-    /**
-     * delta-chase with fixed mad term depth
-     */
-    @Override
-    public int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap) {
-        if(isDisposed()) throw new DisposedException();
-
-        materialise("lower program", dProgram.getLower().toString());
-        Program generalProgram = dProgram.getGeneral();
-        LimitedSkolemisationApplication program =
-                new LimitedSkolemisationApplication(generalProgram, dProgram.getUpperBottomStrategy());
-        Treatment treatment = new Pick4NegativeConceptNaive(this, program);
-        return materialise(program, treatment, gap);
-    }
-
     public int materialise4SpecificQuery(Program generalProgram, QueryRecord record, BottomStrategy upperBottom) {
         if(isDisposed()) throw new DisposedException();
 
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java b/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java
index ffca55a..65184ee 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/StageQueryEngine.java
@@ -21,8 +21,6 @@ public abstract class StageQueryEngine extends BasicQueryEngine {
 
         public abstract int materialiseRestrictedly(DatalogProgram dProgram, GapByStore4ID gap);
 
-        public abstract int materialiseSkolemly(DatalogProgram dProgram, GapByStore4ID gap);
-
         public boolean isValid() {
                 if (!checkValidity) return true; 
                 if (validMaterialisation != null) return validMaterialisation; 
diff --git a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
index 5878a57..291af27 100644
--- a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
+++ b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
@@ -188,6 +188,10 @@ public class QueryRecord extends Disposable {
         return new AnswerTuplesImp(answerVariables[0], gapAnswerTuples);
     }
 
+    public int getGapAnswersCount() {
+        return gapAnswerTuples.size();
+    }
+
     public String toString() {
         if(isDisposed()) throw new DisposedException();
 
diff --git a/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java b/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java
index a567699..a09cf5b 100644
--- a/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java
+++ b/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java
@@ -81,6 +81,44 @@ public class QueryGraph {
                 return axioms;
         }
 
+//      public Set<OWLClassExpression> getExistentialConditions(Map<Variable, Term> assignment) {
+//              if(!rollable_edges.isEmpty()) return null;
+//
+//              OWLIndividual sub;
+//              Visitor visitor = new Visitor(factory, assignment);
+//              Set<OWLClassExpression> axioms = new HashSet<>();
+//              for(Map.Entry<Term, Set<OWLClassExpression>> entry : concepts.map.entrySet()) {
+//                      // TODO check correctness!!!
+//                      if(existVars.contains(entry.getKey())) {
+//                              OWLClassExpression conjunction =
+//                                              factory.getOWLObjectIntersectionOf(factory.getOWLThing());
+//                              for(OWLClassExpression owlClassExpression : entry.getValue()) {
+//                                      conjunction = factory.getOWLObjectIntersectionOf(conjunction, owlClassExpression.accept(visitor));
+//                              }
+//                              axioms.add(conjunction);
+////                            continue; // previously the "then" contained only this
+//                      }
+//              }
+//              return axioms;
+//      }
+
+        public Set<OWLAxiom> getExistentialAxioms() {
+                if(!rollable_edges.isEmpty()) return null;
+
+                Set<OWLAxiom> axioms = new HashSet<>();
+                for(Map.Entry<Term, Set<OWLClassExpression>> entry : concepts.map.entrySet()) {
+                        if(existVars.contains(entry.getKey())) {
+                                OWLClassExpression conjunction =
+                                                factory.getOWLObjectIntersectionOf(factory.getOWLThing());
+                                for(OWLClassExpression owlClassExpression : entry.getValue()) {
+                                        conjunction = factory.getOWLObjectIntersectionOf(conjunction, owlClassExpression);
+                                }
+                                axioms.add(factory.getOWLSubClassOfAxiom(conjunction, factory.getOWLNothing()));
+                        }
+                }
+                return axioms;
+        }
+
         public Set<OWLAxiom> getAssertions(Map<Variable, Term> assignment) {
                 if(!rollable_edges.isEmpty()) return null;
 
@@ -88,10 +126,21 @@ public class QueryGraph {
                 Visitor visitor = new Visitor(factory, assignment);
                 Set<OWLAxiom> axioms = getPropertyAssertions(assignment);
                 for(Map.Entry<Term, Set<OWLClassExpression>> entry : concepts.map.entrySet()) {
-                        if(existVars.contains(entry.getKey())) continue;
-                        sub = factory.getOWLNamedIndividual(IRI.create(getIndividual(entry.getKey(), assignment).getIRI()));
-                        for(OWLClassExpression clsExp : entry.getValue()) {
-                                axioms.add(factory.getOWLClassAssertionAxiom(clsExp.accept(visitor), sub));
+                        // TODO check correctness!!!
+                        if(existVars.contains(entry.getKey())) {
+//                              OWLClassExpression conjunction =
+//                                              factory.getOWLObjectIntersectionOf(factory.getOWLThing());
+//                              for(OWLClassExpression owlClassExpression : entry.getValue()) {
+//                                      conjunction = factory.getOWLObjectIntersectionOf(conjunction, owlClassExpression.accept(visitor));
+//                              }
+//                              axioms.add(factory.getOWLSubClassOfAxiom(conjunction, factory.getOWLNothing()));
+                                continue; // previously the "then" contained only this
+                        }
+                        else {
+                                sub = factory.getOWLNamedIndividual(IRI.create(getIndividual(entry.getKey(), assignment).getIRI()));
+                                for(OWLClassExpression clsExp : entry.getValue()) {
+                                        axioms.add(factory.getOWLClassAssertionAxiom(clsExp.accept(visitor), sub));
+                                }
                         }
                 }
                 return axioms;
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
index 93fbc98..51cb44d 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -10,7 +10,6 @@ import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
 import uk.ac.ox.cs.pagoda.query.GapByStore4ID2;
 import uk.ac.ox.cs.pagoda.query.QueryRecord;
 import uk.ac.ox.cs.pagoda.query.QueryRecord.Step;
-import uk.ac.ox.cs.pagoda.reasoner.full.Checker;
 import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
 import uk.ac.ox.cs.pagoda.reasoner.light.KarmaQueryEngine;
 import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
@@ -189,19 +188,21 @@ class MyQueryReasoner extends QueryReasoner {
             return;
 
         OWLOntology relevantOntologySubset = extractRelevantOntologySubset(queryRecord);
-//        queryRecord.saveRelevantOntology("./fragment_query" + queryRecord.getQueryID() + ".owl");
+//        queryRecord.saveRelevantOntology("/home/alessandro/Desktop/test-relevant-ontology.owl");
 
         if(properties.getUseSkolemUpperBound() &&
-                querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord))
+                querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord)) {
             return;
+        }
 
         Timer t = new Timer();
-        Checker summarisedChecker = new HermitSummaryFilter(queryRecord, properties.getToCallHermiT());
+        HermitSummaryFilter summarisedChecker = new HermitSummaryFilter(queryRecord, properties.getToCallHermiT());
         summarisedChecker.check(queryRecord.getGapAnswers());
-        summarisedChecker.dispose();
+//        summarisedChecker.checkByFullReasoner(queryRecord.getGapAnswers());
         Utility.logDebug("Total time for full reasoner: " + t.duration());
+
         queryRecord.markAsProcessed();
-        Utility.logDebug("Difficulty of this query: " + queryRecord.getDifficulty());
+        summarisedChecker.dispose();
     }
 
     @Override
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java
index 3a057ec..e8daa3b 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java
@@ -206,7 +206,7 @@ public abstract class QueryReasoner extends Disposable {
                    if you call twice, you will end up with a json file with multiple roots */
         if(answerWriter != null) gson.toJson(queryRecords, answerWriter);
 //              queryRecords.stream().forEach(record -> Utility.logDebug(gson.toJson(record)));
-        queryRecords.stream().forEach(record -> record.dispose());
+        queryRecords.stream().forEach(QueryRecord::dispose);
     }
 
     @Override
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java b/src/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java
index fd620a5..07adc6d 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java
@@ -12,4 +12,6 @@ public abstract class Checker extends Disposable {
 
         public abstract boolean isConsistent();
 
+        public abstract int getNoOfCalls();
+
 }
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java b/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
index 35db0f2..cfae88b 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
@@ -24,228 +24,255 @@ import java.util.Map;
 import java.util.Set;
 
 public class HermitChecker extends Checker {
-        
-        protected OWLDataFactory factory;
-        protected String[][] answerVariable;
-        protected OWLOntology ontology;
-        protected QueryRecord record;
-        protected QueryGraph qGraph = null;
-        boolean toCheck = true;
-        AnswerTuple topAnswerTuple = null, botAnswerTuple = null;
-        private String queryText;
-        private DLClause queryClause;
-        private Reasoner hermit;
-        private int tag = 0;
-        private int counter = 0;
-        private DependencyGraph dGraph = null;
-        public HermitChecker(Checker checker) {
-                if (checker instanceof HermitChecker) {
-                        HermitChecker other = (HermitChecker) checker;
-                        factory = other.factory;
-                        queryText = other.queryText;
-                        queryClause = other.queryClause;
-                        answerVariable = other.answerVariable;
-                        ontology = other.ontology;
+
+    protected OWLDataFactory factory;
+    protected String[][] answerVariable;
+    protected OWLOntology ontology;
+    protected QueryRecord record;
+    protected QueryGraph qGraph = null;
+    boolean toCheck = true;
+    AnswerTuple topAnswerTuple = null, botAnswerTuple = null;
+    private String queryText;
+    private DLClause queryClause;
+    private Reasoner hermit;
+    private int tag = 0;
+
+    public int getNoOfCalls() {
+        if(isDisposed()) throw new DisposedException();
+        return noOfCalls;
+    }
+
+    private int noOfCalls = 0;
+    private DependencyGraph dGraph = null;
+
+    public HermitChecker(Checker checker) {
+        if(checker instanceof HermitChecker) {
+            HermitChecker other = (HermitChecker) checker;
+            factory = other.factory;
+            queryText = other.queryText;
+            queryClause = other.queryClause;
+            answerVariable = other.answerVariable;
+            ontology = other.ontology;
 //                      record = other.record;
-                }
+        }
 
-                hermit = new Reasoner(ontology);
-        }
+        hermit = new Reasoner(ontology);
+    }
 
-        public HermitChecker(OWLOntology ontology, QueryRecord record, boolean toCheck) {
-                this.ontology = ontology;
-                queryText = record.getQueryText();
-                answerVariable = record.getVariables();
-                queryClause = record.getClause();
+    public HermitChecker(OWLOntology ontology, QueryRecord record, boolean toCheck) {
+        this.ontology = ontology;
+        queryText = record.getQueryText();
+        answerVariable = record.getVariables();
+        queryClause = record.getClause();
 //              this.record = record;
-                this.toCheck = toCheck;
-        }
-
-        public HermitChecker(OWLOntology ontology, String queryText) {
-                this.ontology = ontology;
-                this.queryText = queryText;
-                answerVariable = queryText == null ? null : ConjunctiveQueryHelper.getAnswerVariables(queryText);
-                queryClause = DLClauseHelper.getQuery(queryText, null);
+        this.toCheck = toCheck;
+    }
+
+    public HermitChecker(OWLOntology ontology, String queryText) {
+        this.ontology = ontology;
+        this.queryText = queryText;
+        answerVariable = queryText == null ? null : ConjunctiveQueryHelper.getAnswerVariables(queryText);
+        queryClause = DLClauseHelper.getQuery(queryText, null);
 //              this.record = null;
-        }
-
-        @Override
-        public int check(AnswerTuples answers) {
-                if(isDisposed()) throw new DisposedException();
-
-                if(hermit == null) initialiseReasoner();
-                int answerCounter = 0, counter = 0;
-                for(; answers.isValid(); answers.moveNext()) {
-                        ++counter;
-                        if(check(answers.getTuple())) ++answerCounter;
-                }
-                answers.dispose();
-
-                Utility.logDebug("The number of individuals to be checked by HermiT: " + counter,
-                                                 "The number of correct answers: " + answerCounter);
-                return answerCounter;
-        }
-
-        @Override
-        public boolean check(AnswerTuple answerTuple) {
-                if(isDisposed()) throw new DisposedException();
-
-                if(!toCheck) return false;
-
-                if(hermit == null) initialiseReasoner();
-                if(tag != 0) return tag == 1;
-                ++counter;
-                Timer t = new Timer();
-                Map<Variable, Term> sub = answerTuple.getAssignment(answerVariable[1]);
-                Set<OWLAxiom> toCheckAxioms = qGraph.getAssertions(sub);
+    }
+
+    @Override
+    public int check(AnswerTuples answers) {
+        if(isDisposed()) throw new DisposedException();
+
+        if(hermit == null) initialiseReasoner();
+        int answerCounter = 0, counter = 0;
+        for(; answers.isValid(); answers.moveNext()) {
+            ++counter;
+            if(check(answers.getTuple())) ++answerCounter;
+        }
+        answers.dispose();
+
+        Utility.logDebug("The number of individuals to be checked by HermiT: " + counter,
+                         "The number of correct answers: " + answerCounter);
+        return answerCounter;
+    }
+
+    @Override
+    public boolean check(AnswerTuple answerTuple) {
+        if(isDisposed()) throw new DisposedException();
+
+        if(!toCheck) return false;
+        ++noOfCalls;
+
+        if(tag != 0) return tag == 1;
+        if(hermit == null) initialiseReasoner();
+
+        Timer t = new Timer();
+        Map<Variable, Term> sub = answerTuple.getAssignment(answerVariable[1]);
+        Set<OWLAxiom> toCheckAxioms = qGraph.getAssertions(sub);
+
+        // TODO complete
+        Set<OWLAxiom> toCheckExistentialAxioms = qGraph.getExistentialAxioms();
+
+        // TODO possibly inefficient
+        for(OWLAxiom subclassAxiom : toCheckExistentialAxioms) {
+            Utility.logDebug("Checking consistency of ontology union " + subclassAxiom);
+            ontology.getOWLOntologyManager().addAxiom(ontology, subclassAxiom);
+            if(hermit.isConsistent()) {
+                Utility.logDebug("@TIME to check one tuple: " + t.duration());
+                return false;
+            }
+            ontology.getOWLOntologyManager().removeAxiom(ontology, subclassAxiom);
+        }
+
 
 //              for (OWLAxiom axiom: toCheckAxioms)     System.out.println(axiom.toString());
 
-                if(hermit.isEntailed(toCheckAxioms)) {
-                        Utility.logDebug("@TIME to check one tuple: " + t.duration());
-                        return true;
-                }
-                Utility.logDebug("@TIME to check one tuple: " + t.duration());
-                return false;
-        }
-        
-        @Override
-        public boolean isConsistent() {
-                if(isDisposed()) throw new DisposedException();
-
-                if(hermit == null) initialiseReasoner();
-                return hermit.isConsistent();
-        }
-
-        public void dispose() {
-                super.dispose();
-
-                Utility.logInfo("Hermit was called " + counter + " times.");
-                if(hermit != null) hermit.dispose();
-                hermit = null;
-        }
-
-        public void setDependencyGraph(DependencyGraph dGraph) {
-                if(isDisposed()) throw new DisposedException();
-
-                this.dGraph = dGraph;
-        }
-
-        private void initialiseReasoner() {
-                qGraph = new QueryGraph(queryClause.getBodyAtoms(), answerVariable[1], ontology);
-                OWLOntologyManager manager = ontology.getOWLOntologyManager();
-                factory = manager.getOWLDataFactory();
-
-                if(hermit != null) hermit.dispose();
-
-                if(dGraph != null && answerVariable[1].length == 1 && (dGraph.getExits().size() > 1 || dGraph.getEntrances()
-                                                                                                                                                                                                         .size() > 1)) {
-                        Set<OWLAxiom> topAxioms = new HashSet<OWLAxiom>();
-                        Set<OWLAxiom> botAxioms = new HashSet<OWLAxiom>();
-                        addTopAndBotTuple(topAxioms, botAxioms);
-                        manager.addAxioms(ontology, topAxioms);
-                        manager.addAxioms(ontology, botAxioms);
-                        hermit = new Reasoner(ontology);
-                        boolean topValid = true;
-                        if(!hermit.isConsistent() || topAnswerTuple != null && (topValid = check(topAnswerTuple))) {
-                                hermit.dispose();
-                                manager.removeAxioms(ontology, topAxioms);
-                                hermit = new Reasoner(ontology);
-                        }
-                        else {
-                                if(!topValid) tag = -1;
-                                else if(botAnswerTuple != null && check(botAnswerTuple)) tag = 1;
-                        }
-                }
-                else
-                        hermit = new Reasoner(ontology);
-        }
-
-        private void addTopAndBotTuple(Set<OWLAxiom> topAxioms, Set<OWLAxiom> botAxioms) {
-                String top_str = Namespace.PAGODA_ANONY + "top", bot_str = Namespace.PAGODA_ANONY + "bot";
-                topAnswerTuple =
-                                new AnswerTuple(new uk.ac.ox.cs.JRDFox.model.Individual[]{uk.ac.ox.cs.JRDFox.model.Individual.create(top_str)});
-                botAnswerTuple =
-                                new AnswerTuple(new uk.ac.ox.cs.JRDFox.model.Individual[]{uk.ac.ox.cs.JRDFox.model.Individual.create(bot_str)});
-                OWLIndividual top_ind = factory.getOWLNamedIndividual(IRI.create(top_str)), bot_ind =
-                                factory.getOWLNamedIndividual(IRI.create(bot_str));
-                Map<OWLAxiom, Integer> counter = new HashMap<OWLAxiom, Integer>();
-
-                Set<String> topAnswers = new HashSet<String>(), botAnswers = new HashSet<String>();
-                OWLIndividual sub, obj;
-                if(dGraph.getExits().size() > 1) {
-                        for(Clique answerClique : dGraph.getExits())
-                                topAnswers.add(((uk.ac.ox.cs.JRDFox.model.Individual) answerClique.getRepresentative()
-                                                                                                                                                                  .getAnswerTuple()
-                                                                                                                                                                  .getGroundTerm(0)).getIRI());
-                }
-                else topAnswerTuple = null;
-
-                if(dGraph.getEntrances().size() > 1) {
-                        for(Clique answerClique : dGraph.getEntrances())
-                                botAnswers.add(((uk.ac.ox.cs.JRDFox.model.Individual) answerClique.getRepresentative()
-                                                                                                                                                                  .getAnswerTuple()
-                                                                                                                                                                  .getGroundTerm(0)).getIRI());
-                }
-                else botAnswerTuple = null;
-
-                for(OWLAxiom axiom : ontology.getABoxAxioms(true))
-                        if(axiom instanceof OWLClassAssertionAxiom) {
-                                OWLClassAssertionAxiom ca = (OWLClassAssertionAxiom) axiom;
-                                sub = ca.getIndividual();
-                                if(topAnswers.contains(sub.toStringID()))
-                                        topAxioms.add(factory.getOWLClassAssertionAxiom(ca.getClassExpression(), top_ind));
-                                if(botAnswers.contains(sub.toStringID()))
-                                        inc(counter, factory.getOWLClassAssertionAxiom(ca.getClassExpression(), bot_ind));
-                        }
-                        else if(axiom instanceof OWLObjectPropertyAssertionAxiom) {
-                                OWLObjectPropertyAssertionAxiom oa = (OWLObjectPropertyAssertionAxiom) axiom;
-                                sub = oa.getSubject();
-                                obj = oa.getObject();
-                                if(topAnswers.contains(sub.toStringID()))
-                                        if(topAnswers.contains(obj.toStringID()))
-                                                topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), top_ind, top_ind));
-                                        else
-                                                topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), top_ind, obj));
-                                else {
-                                        if(topAnswers.contains(obj.toStringID()))
-                                                topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), sub, top_ind));
-                                }
-
-                                if(botAnswers.contains(sub.toStringID()))
-                                        if(botAnswers.contains(obj.toStringID()))
-                                                inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), bot_ind, bot_ind));
-                                        else
-                                                inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), bot_ind, obj));
-                                else {
-                                        if(botAnswers.contains(obj.toStringID()))
-                                                inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), sub, bot_ind));
-                                }
-
-                        }
-                        else if(axiom instanceof OWLDataPropertyAssertionAxiom) {
-                                OWLDataPropertyAssertionAxiom da = (OWLDataPropertyAssertionAxiom) axiom;
-                                sub = da.getSubject();
-                                if(topAnswers.contains(sub.toStringID()))
-                                        topAxioms.add(factory.getOWLDataPropertyAssertionAxiom(da.getProperty(), top_ind, da.getObject()));
-
-                                if(botAnswers.contains(sub.toStringID()))
-                                        inc(counter, factory.getOWLDataPropertyAssertionAxiom(da.getProperty(), bot_ind, da.getObject()));
-                        }
-
-                int number = botAnswers.size();
-                for(Map.Entry<OWLAxiom, Integer> entry : counter.entrySet()) {
-                        if(entry.getValue() == number)
-                                botAxioms.add(entry.getKey());
-                }
-        }
-
-        private void inc(Map<OWLAxiom, Integer> counter, OWLAxiom newAxiom) {
-                if(isDisposed()) throw new DisposedException();
-
-                Integer number = counter.get(newAxiom);
-                if(number == null) counter.put(newAxiom, 1);
-                else counter.put(newAxiom, number + 1);
-        }
+//              Utility.logInfo(toCheckAxioms);
+
+        if(hermit.isEntailed(toCheckAxioms)) {
+            Utility.logDebug("@TIME to check one tuple: " + t.duration());
+            return true;
+        }
+        Utility.logDebug("@TIME to check one tuple: " + t.duration());
+        return false;
+    }
+
+    @Override
+    public boolean isConsistent() {
+        if(isDisposed()) throw new DisposedException();
+
+        if(hermit == null) initialiseReasoner();
+        return hermit.isConsistent();
+    }
+
+    public void dispose() {
+        super.dispose();
+
+        Utility.logDebug("Disposing of an instance of Hermit after " + noOfCalls + " calls");
+        if(hermit != null) hermit.dispose();
+        hermit = null;
+    }
+
+    public void setDependencyGraph(DependencyGraph dGraph) {
+        if(isDisposed()) throw new DisposedException();
+
+        this.dGraph = dGraph;
+    }
+
+    private void initialiseReasoner() {
+        qGraph = new QueryGraph(queryClause.getBodyAtoms(), answerVariable[1], ontology);
+        OWLOntologyManager manager = ontology.getOWLOntologyManager();
+        factory = manager.getOWLDataFactory();
+
+        if(hermit != null) hermit.dispose();
+
+        if(dGraph != null && answerVariable[1].length == 1 && (dGraph.getExits().size() > 1 || dGraph.getEntrances()
+                                                                                                     .size() > 1)) {
+            Set<OWLAxiom> topAxioms = new HashSet<OWLAxiom>();
+            Set<OWLAxiom> botAxioms = new HashSet<OWLAxiom>();
+            addTopAndBotTuple(topAxioms, botAxioms);
+            manager.addAxioms(ontology, topAxioms);
+            manager.addAxioms(ontology, botAxioms);
+            hermit = new Reasoner(ontology);
+            boolean topValid = true;
+            if(!hermit.isConsistent() || topAnswerTuple != null && (topValid = check(topAnswerTuple))) {
+                hermit.dispose();
+                manager.removeAxioms(ontology, topAxioms);
+                hermit = new Reasoner(ontology);
+            }
+            else {
+                if(!topValid) tag = -1;
+                else if(botAnswerTuple != null && check(botAnswerTuple)) tag = 1;
+            }
+        }
+        else
+            hermit = new Reasoner(ontology);
+    }
+
+    private void addTopAndBotTuple(Set<OWLAxiom> topAxioms, Set<OWLAxiom> botAxioms) {
+        String top_str = Namespace.PAGODA_ANONY + "top", bot_str = Namespace.PAGODA_ANONY + "bot";
+        topAnswerTuple =
+                new AnswerTuple(
+                        new uk.ac.ox.cs.JRDFox.model.Individual[]{uk.ac.ox.cs.JRDFox.model.Individual.create(top_str)});
+        botAnswerTuple =
+                new AnswerTuple(
+                        new uk.ac.ox.cs.JRDFox.model.Individual[]{uk.ac.ox.cs.JRDFox.model.Individual.create(bot_str)});
+        OWLIndividual top_ind = factory.getOWLNamedIndividual(IRI.create(top_str)), bot_ind =
+                factory.getOWLNamedIndividual(IRI.create(bot_str));
+        Map<OWLAxiom, Integer> counter = new HashMap<OWLAxiom, Integer>();
+
+        Set<String> topAnswers = new HashSet<String>(), botAnswers = new HashSet<String>();
+        OWLIndividual sub, obj;
+        if(dGraph.getExits().size() > 1) {
+            for(Clique answerClique : dGraph.getExits())
+                topAnswers.add(((uk.ac.ox.cs.JRDFox.model.Individual) answerClique.getRepresentative()
+                                                                                  .getAnswerTuple()
+                                                                                  .getGroundTerm(0)).getIRI());
+        }
+        else topAnswerTuple = null;
+
+        if(dGraph.getEntrances().size() > 1) {
+            for(Clique answerClique : dGraph.getEntrances())
+                botAnswers.add(((uk.ac.ox.cs.JRDFox.model.Individual) answerClique.getRepresentative()
+                                                                                  .getAnswerTuple()
+                                                                                  .getGroundTerm(0)).getIRI());
+        }
+        else botAnswerTuple = null;
+
+        for(OWLAxiom axiom : ontology.getABoxAxioms(true))
+            if(axiom instanceof OWLClassAssertionAxiom) {
+                OWLClassAssertionAxiom ca = (OWLClassAssertionAxiom) axiom;
+                sub = ca.getIndividual();
+                if(topAnswers.contains(sub.toStringID()))
+                    topAxioms.add(factory.getOWLClassAssertionAxiom(ca.getClassExpression(), top_ind));
+                if(botAnswers.contains(sub.toStringID()))
+                    inc(counter, factory.getOWLClassAssertionAxiom(ca.getClassExpression(), bot_ind));
+            }
+            else if(axiom instanceof OWLObjectPropertyAssertionAxiom) {
+                OWLObjectPropertyAssertionAxiom oa = (OWLObjectPropertyAssertionAxiom) axiom;
+                sub = oa.getSubject();
+                obj = oa.getObject();
+                if(topAnswers.contains(sub.toStringID()))
+                    if(topAnswers.contains(obj.toStringID()))
+                        topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), top_ind, top_ind));
+                    else
+                        topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), top_ind, obj));
+                else {
+                    if(topAnswers.contains(obj.toStringID()))
+                        topAxioms.add(factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), sub, top_ind));
+                }
+
+                if(botAnswers.contains(sub.toStringID()))
+                    if(botAnswers.contains(obj.toStringID()))
+                        inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), bot_ind, bot_ind));
+                    else
+                        inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), bot_ind, obj));
+                else {
+                    if(botAnswers.contains(obj.toStringID()))
+                        inc(counter, factory.getOWLObjectPropertyAssertionAxiom(oa.getProperty(), sub, bot_ind));
+                }
+
+            }
+            else if(axiom instanceof OWLDataPropertyAssertionAxiom) {
+                OWLDataPropertyAssertionAxiom da = (OWLDataPropertyAssertionAxiom) axiom;
+                sub = da.getSubject();
+                if(topAnswers.contains(sub.toStringID()))
+                    topAxioms.add(factory.getOWLDataPropertyAssertionAxiom(da.getProperty(), top_ind, da.getObject()));
+
+                if(botAnswers.contains(sub.toStringID()))
+                    inc(counter, factory.getOWLDataPropertyAssertionAxiom(da.getProperty(), bot_ind, da.getObject()));
+            }
+
+        int number = botAnswers.size();
+        for(Map.Entry<OWLAxiom, Integer> entry : counter.entrySet()) {
+            if(entry.getValue() == number)
+                botAxioms.add(entry.getKey());
+        }
+    }
+
+    private void inc(Map<OWLAxiom, Integer> counter, OWLAxiom newAxiom) {
+        if(isDisposed()) throw new DisposedException();
+
+        Integer number = counter.get(newAxiom);
+        if(number == null) counter.put(newAxiom, 1);
+        else counter.put(newAxiom, number + 1);
+    }
 
 }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/Program.java b/src/uk/ac/ox/cs/pagoda/rules/Program.java
index afc32d4..85000e3 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/Program.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/Program.java
@@ -119,7 +119,7 @@ protected PredicateDependency dependencyGraph;
                 } catch(IOException e) {
                         e.printStackTrace();
                 }
-                Utility.logDebug("The rules are saved in " + getOutputPath() + ".");
+                Utility.logInfo("The rules are saved in " + getOutputPath() + ".");
         }
 
         @Override
diff --git a/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java b/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
index f3f08e9..95f2cbb 100644
--- a/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
+++ b/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
@@ -111,6 +111,11 @@ public class HermitSummaryFilter extends Checker {
         }
 
         @Override
+        public int getNoOfCalls() {
+                return summarisedHermiT.getNoOfCalls() + endomorphismChecker.getNoOfCalls();
+        }
+
+        @Override
         public int check(AnswerTuples answers) {
                 if(isDisposed()) throw new DisposedException();
 
@@ -183,8 +188,14 @@ public class HermitSummaryFilter extends Checker {
         public void dispose() {
                 super.dispose();
 
-                if(summarisedHermiT != null) summarisedHermiT.dispose();
-                endomorphismChecker.dispose();
+                if(summarisedHermiT != null) {
+                        Utility.logInfo("SummarisedHermit was called " + summarisedHermiT.getNoOfCalls() + " times");
+                        summarisedHermiT.dispose();
+                }
+                if(endomorphismChecker != null) {
+                        Utility.logInfo("Hermit was called " + endomorphismChecker.getNoOfCalls() + " times");
+                        endomorphismChecker.dispose();
+                }
         }
 
         private void initialiseSummarisedReasoner() {
diff --git a/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java b/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
index e501821..4991d0d 100644
--- a/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
+++ b/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
@@ -43,14 +43,14 @@ public class PagodaProperties {
                                 defaultUseAlwaysSimpleUpperBound =
                                                 Boolean.parseBoolean(config.getProperty("useAlwaysSimpleUpperBound"));
                                 if(defaultUseAlwaysSimpleUpperBound)
-                                        logger.info("By default the simple upper bound is always used");
+                                        logger.debug("By default the simple upper bound is always used");
                         }
                         if(config.containsKey("useSkolemUpperBound")) {
                                 defaultUseSkolemUpperBound = Boolean.parseBoolean(config.getProperty("useSkolemUpperBound"));
                                 if(defaultUseSkolemUpperBound)
-                                        logger.info("By default the Skolem upper bound is enabled");
+                                        logger.debug("By default the Skolem upper bound is enabled");
                                 else
-                                        logger.info("By default the Skolem upper bound is disabled");
+                                        logger.debug("By default the Skolem upper bound is disabled");
                         }
 
                 } catch(IOException e) {