Many little changes.

24 files changed, 435 insertions, 95 deletions

diff --git a/src/resources/pagoda.properties b/src/resources/pagoda.properties
index 64de225..98f8628 100644
--- a/src/resources/pagoda.properties
+++ b/src/resources/pagoda.properties
@@ -1,5 +1,6 @@
 debug=true
 useAlwaysSimpleUpperBound=false
 useSkolemUpperBound=true
+toCallHermit=true
 
 statisticsDir=/home/alessandro/Dropbox/Oxford/PAGOdA/statistics
\ No newline at end of file
diff --git a/src/uk/ac/ox/cs/pagoda/Pagoda.java b/src/uk/ac/ox/cs/pagoda/Pagoda.java
index f5dce15..7d2317d 100644
--- a/src/uk/ac/ox/cs/pagoda/Pagoda.java
+++ b/src/uk/ac/ox/cs/pagoda/Pagoda.java
@@ -1,12 +1,21 @@
 package uk.ac.ox.cs.pagoda;
 
 import org.apache.commons.cli.*;
+import org.apache.commons.io.FilenameUtils;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
 import uk.ac.ox.cs.pagoda.reasoner.QueryReasoner;
 import uk.ac.ox.cs.pagoda.util.PagodaProperties;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
 
+import java.io.BufferedWriter;
+import java.io.IOException;
+import java.nio.file.Files;
 import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.Map;
 
 /**
  * Executable command line user interface.
@@ -23,7 +32,7 @@ public class Pagoda implements Runnable {
 
     /**
      * Do not use it
-     * */
+     */
     private Pagoda() {
         properties = new PagodaProperties();
     }
@@ -85,7 +94,7 @@ public class Pagoda implements Runnable {
 
     /**
      * Get a builder.
-     * */
+     */
     public static PagodaBuilder builder() {
         return new PagodaBuilder();
     }
@@ -102,21 +111,48 @@ public class Pagoda implements Runnable {
         try {
             Timer t = new Timer();
             pagoda = QueryReasoner.getInstance(properties);
-            if (pagoda == null) return;
-
-            Utility.logInfo("Preprocessing Done in " + t.duration()     + " seconds.");
-
-            if (properties.getQueryPath() != null)
-                for (String queryFile: properties.getQueryPath().split(";"))
-                    pagoda.evaluate(pagoda.getQueryManager().collectQueryRecords(queryFile));
+            if(pagoda == null) return;
+
+            Utility.logInfo("Preprocessing Done in " + t.duration() + " seconds.");
+
+            if(properties.getQueryPath() != null) {
+                for(String queryFile : properties.getQueryPath().split(";")) {
+                    Collection<QueryRecord> queryRecords = pagoda.getQueryManager().collectQueryRecords(queryFile);
+                    pagoda.evaluate(queryRecords);
+
+                    if(PagodaProperties.isDebuggingMode()) {
+                        HashMap<String, Map<String, String>> statistics = new HashMap<>();
+                        for(QueryRecord queryRecord : queryRecords) {
+                            statistics.put(queryRecord.getQueryID(), queryRecord.getStatistics());
+                        }
+                        String statisticsFilename = getStatisticsFilename(properties, queryFile);
+                        try(BufferedWriter writer = Files.newBufferedWriter(Paths.get(statisticsFilename))) {
+                            QueryRecord.GsonCreator.getInstance().toJson(statistics, writer);
+                        } catch(IOException e) {
+                            Utility.logError("Unable to save statistics");
+                        }
+                    }
+                }
+            }
         } finally {
-            if (pagoda != null) pagoda.dispose();
+            if(pagoda != null) pagoda.dispose();
         }
     }
 
+    private String getStatisticsFilename(PagodaProperties properties, String queryFile) {
+        String statisticsFilename = "statistics_" +
+                FilenameUtils.removeExtension(FilenameUtils.getName(properties.getOntologyPath().replaceAll("_", "-")));
+        statisticsFilename += "_" + FilenameUtils.removeExtension(FilenameUtils.getName(queryFile).replaceAll("_", "-"));
+        statisticsFilename += "_" + ((properties.getUseSkolemUpperBound()) ? "skolem" : "");
+        statisticsFilename += ".json";
+        statisticsFilename = FilenameUtils.concat(properties.getStatisticsDir().toString(),
+                                                  statisticsFilename);
+        return statisticsFilename;
+    }
+
     /**
      * Allows to set the parameters before creating a Pagoda instance.
-     * */
+     */
     public static class PagodaBuilder {
 
         private Pagoda instance;
diff --git a/src/uk/ac/ox/cs/pagoda/endomorph/plan/OpenEndPlan.java b/src/uk/ac/ox/cs/pagoda/endomorph/plan/OpenEndPlan.java
index 73a27bf..a46da85 100644
--- a/src/uk/ac/ox/cs/pagoda/endomorph/plan/OpenEndPlan.java
+++ b/src/uk/ac/ox/cs/pagoda/endomorph/plan/OpenEndPlan.java
@@ -7,6 +7,7 @@ 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.summary.NodeTuple;
+import uk.ac.ox.cs.pagoda.util.SimpleProgressBar;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
 
@@ -40,7 +41,11 @@ public class OpenEndPlan implements CheckPlan {
                 Timer t = new Timer(); 
                 
                 AnswerTuple answerTuple;
-                while (!topo.isEmpty()) { 
+                int initialTopoSize = topo.size();
+                // TODO test progress bar
+                SimpleProgressBar progressBar = new SimpleProgressBar("Checking", initialTopoSize);
+                while (!topo.isEmpty()) {
+                        progressBar.update(initialTopoSize - topo.size());
                         if (flag) {
                                 clique = topo.removeFirst();
                                 if (redundant(clique)) continue; 
@@ -70,6 +75,8 @@ public class OpenEndPlan implements CheckPlan {
                                 }
                         }
                 }
+                progressBar.update(initialTopoSize - topo.size());
+                progressBar.dispose();
                 
 //              Utility.logDebug("HermiT was called " + times + " times."); 
                 
diff --git a/src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java b/src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java
index 530b97f..81c99a4 100644
--- a/src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java
+++ b/src/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java
@@ -37,7 +37,7 @@ public class RuleHelper {
                 boolean lastSpace = true;
                 for (Atom headAtom: clause.getHeadAtoms()) {
                         if ((atomText = getText(headAtom)) == null) continue; 
-                        if (!lastSpace) buf.append(" | ");
+                        if (!lastSpace) buf.append(" v ");
                         buf.append(atomText);
                         lastSpace = false;
                 }
diff --git a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
index 291af27..d88376f 100644
--- a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
+++ b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
@@ -171,14 +171,10 @@ public class QueryRecord extends Disposable {
     }
 
     public String getQueryText() {
-        if(isDisposed()) throw new DisposedException();
-
         return queryText;
     }
 
     public String getQueryID() {
-        if(isDisposed()) throw new DisposedException();
-
         return stringQueryID;
     }
 
@@ -193,8 +189,6 @@ public class QueryRecord extends Disposable {
     }
 
     public String toString() {
-        if(isDisposed()) throw new DisposedException();
-
         return queryText;
     }
 
@@ -281,6 +275,20 @@ public class QueryRecord extends Disposable {
         }
     }
 
+    public Map<String, String> getStatistics() {
+        HashMap<String, String> result = new HashMap<>();
+
+        double totalTime = 0.0;
+        for(Step step : Step.values()) {
+            result.put(step.toString(), Double.toString(timer[step.ordinal()]));
+            totalTime += timer[step.ordinal()];
+        }
+        result.put("totalTime", Double.toString(totalTime));
+        result.put("difficulty", difficulty.toString());
+
+        return result;
+    }
+
     public String outputSoundAnswerTuple() {
         if(isDisposed()) throw new DisposedException();
 
@@ -359,6 +367,8 @@ public class QueryRecord extends Disposable {
                 Utility.logError("The answer (" + answer + ") cannot be removed, because it is not in the upper bound.");
             gapAnswerTuples.remove(answer);
         }
+        int numOfUpperBoundAnswers = soundAnswerTuples.size() + gapAnswerTuples.size();
+        Utility.logInfo("Upper bound answers updated: " + numOfUpperBoundAnswers);
     }
 
     public void addLowerBoundAnswers(Collection<AnswerTuple> answers) {
@@ -722,7 +732,9 @@ public class QueryRecord extends Disposable {
 
         @Override
         public String toString() {
-            return WordUtils.capitalizeFully(super.toString(), new char[]{'_'}).replace("_", "");
+            String s = super.toString();
+            if(s == null) return null;
+            return WordUtils.capitalizeFully(s, new char[]{'_'}).replace("_", "");
         }
     }
 
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 a09cf5b..116e724 100644
--- a/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java
+++ b/src/uk/ac/ox/cs/pagoda/query/rollup/QueryGraph.java
@@ -102,16 +102,17 @@ public class QueryGraph {
 //              return axioms;
 //      }
 
-        public Set<OWLAxiom> getExistentialAxioms() {
+        public Set<OWLAxiom> getExistentialAxioms(Map<Variable, Term> assignment) {
                 if(!rollable_edges.isEmpty()) return null;
 
+                Visitor visitor = new Visitor(factory, assignment);
                 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);
+                                        conjunction = factory.getOWLObjectIntersectionOf(conjunction, owlClassExpression.accept(visitor));
                                 }
                                 axioms.add(factory.getOWLSubClassOfAxiom(conjunction, factory.getOWLNothing()));
                         }
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
index e5074d5..b419289 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -68,9 +68,9 @@ class MyQueryReasoner extends QueryReasoner {
 
         ontology = o;
         program = new DatalogProgram(ontology, properties.getToClassify());
-                program.getLower().save();
-                program.getUpper().save();
-                program.getGeneral().save();
+//              program.getLower().save();
+//              program.getUpper().save();
+//              program.getGeneral().save();
 
         if(!program.getGeneral().isHorn())
             lazyUpperStore = new MultiStageQueryEngine("lazy-upper-bound", true);
@@ -195,19 +195,24 @@ class MyQueryReasoner extends QueryReasoner {
 
         Utility.logInfo("Summarisation...");
         HermitSummaryFilter summarisedChecker = new HermitSummaryFilter(queryRecord, properties.getToCallHermiT());
-        if(summarisedChecker.check(queryRecord.getGapAnswers()) == 0)
+        if(summarisedChecker.check(queryRecord.getGapAnswers()) == 0) {
+            summarisedChecker.dispose();
             return;
+        }
 
         if(properties.getUseSkolemUpperBound() &&
-                querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord))
+                querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord)) {
+            summarisedChecker.dispose();
             return;
+        }
 
         Utility.logInfo("Full reasoning...");
         Timer t = new Timer();
         summarisedChecker.checkByFullReasoner(queryRecord.getGapAnswers());
         Utility.logDebug("Total time for full reasoner: " + t.duration());
 
-        queryRecord.markAsProcessed();
+        if(properties.getToCallHermiT())
+            queryRecord.markAsProcessed();
         summarisedChecker.dispose();
     }
 
@@ -377,7 +382,7 @@ class MyQueryReasoner extends QueryReasoner {
         relevantStore.importDataFromABoxOf(relevantSubset);
         String relevantOriginalMarkProgram = OWLHelper.getOriginalMarkProgram(relevantSubset);
 
-        int queryDependentMaxTermDepth = 5; // TODO make it dynamic
+        int queryDependentMaxTermDepth = 1; // TODO make it dynamic
         relevantStore.materialise("Mark original individuals", relevantOriginalMarkProgram);
         int materialisationTag = relevantStore.materialiseSkolemly(relevantProgram, null,
                                                                    queryDependentMaxTermDepth);
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 cfae88b..9574845 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
@@ -99,7 +99,6 @@ public class HermitChecker extends Checker {
 
         if(!toCheck) return false;
         ++noOfCalls;
-
         if(tag != 0) return tag == 1;
         if(hermit == null) initialiseReasoner();
 
@@ -107,19 +106,19 @@ public class HermitChecker extends Checker {
         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);
-        }
+//        // TODO complete
+//        Set<OWLAxiom> toCheckExistentialAxioms = qGraph.getExistentialAxioms(sub);
+//
+//        // TODO possibly inefficient
+//        for(OWLAxiom subclassAxiom : toCheckExistentialAxioms) {
+//            Utility.logInfo("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());
diff --git a/src/uk/ac/ox/cs/pagoda/rules/Program.java b/src/uk/ac/ox/cs/pagoda/rules/Program.java
index 85000e3..a0edf85 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/Program.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/Program.java
@@ -316,9 +316,10 @@ protected PredicateDependency dependencyGraph;
         private Atom getAtom(OWLObjectPropertyExpression exp, Variable x, Variable y) {
                 if(exp instanceof OWLObjectProperty)
                         return Atom.create(AtomicRole.create(((OWLObjectProperty) exp).toStringID()), x, y);
-                OWLObjectInverseOf inverseOf;
-                if(exp instanceof OWLObjectInverseOf && (inverseOf =
-                                (OWLObjectInverseOf) exp).getInverse() instanceof OWLObjectProperty)
+                // TODO fixed, test it
+                OWLObjectPropertyExpression inverseOf;
+                if(exp instanceof OWLObjectInverseOf && (inverseOf = (
+                                (OWLObjectInverseOf) exp).getInverse()) instanceof OWLObjectProperty)
                         return Atom.create(AtomicRole.create(((OWLObjectProperty) inverseOf).toStringID()), x, y);
                 return null;
         }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
index dfe1e59..d694b61 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -64,14 +64,14 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
 
     private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
         ArrayList<DLClause> result = new ArrayList<>();
-        for(Tuple<Individual> violationTuple : violationTuples)
+        for(Tuple<Individual> violationTuple : violationTuples) {
             if(getMaxDepth(violationTuple) < maxTermDepth) {
                 result.addAll(getGroundSkolemisation(clause, originalClause, violationTuple));
                 Utility.logDebug("Approximating maximal individual by a constant in rule:" + originalClause);
             }
             else
                 result.addAll(alternativeApproximator.convert(clause, originalClause, null));
-
+        }
 
         return result;
     }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java b/src/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java
new file mode 100644
index 0000000..2adb66b
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/clauses/Clause.java
@@ -0,0 +1,100 @@
+package uk.ac.ox.cs.pagoda.rules.clauses;
+
+public class Clause {
+
+//    public static final String IF = ":-";
+//    public static final String OR = "|";
+//    public static final String AND = ",";
+//
+//    protected final List<List<Atom>> head;
+//    protected final List<Atom> body;
+//
+//    protected Clause(Atom[] headAtoms, Atom[] bodyAtoms) {
+//        this.head = Collections.singletonList(Arrays.asList(headAtoms));
+//        this.body= Arrays.asList(bodyAtoms);
+//    }
+//
+//    protected Clause(String s) {
+//        this.headAtoms = null;
+//        this.bodyAtoms = null;
+//    }
+//
+//    public int getHeadLength() {
+//        return headAtoms.length;
+//    }
+//
+//    public Atom getHeadAtom(int atomIndex) {
+//        return headAtoms[atomIndex];
+//    }
+//
+//    public Atom[] getHeadAtoms() {
+//        return headAtoms.clone();
+//    }
+//
+//    public int getBodyLength() {
+//        return bodyAtoms.length;
+//    }
+//
+//    public Atom getBodyAtom(int atomIndex) {
+//        return bodyAtoms[atomIndex];
+//    }
+//
+//    public Atom[] getBodyAtoms() {
+//        return bodyAtoms.clone();
+//    }
+//
+//    public String toString(Prefixes prefixes) {
+//        StringBuilder buffer = new StringBuilder();
+//        for(int headIndex = 0; headIndex < headAtoms.length; headIndex++) {
+//            if(headIndex != 0)
+//                buffer.append(" ").append(OR).append(" ");
+//            buffer.append(headAtoms[headIndex].toString(prefixes));
+//        }
+//        buffer.append(" ").append(IF).append(" ");
+//        for(int bodyIndex = 0; bodyIndex < bodyAtoms.length; bodyIndex++) {
+//            if(bodyIndex != 0)
+//                buffer.append(AND).append(" ");
+//            buffer.append(bodyAtoms[bodyIndex].toString(prefixes));
+//        }
+//        return buffer.toString();
+//    }
+//
+//    public String toString() {
+//        return toString(Prefixes.STANDARD_PREFIXES);
+//    }
+//
+//    protected static InterningManager<? extends Clause> s_interningManager = new InterningManager<Clause>() {
+//        protected boolean equal(Clause object1, Clause object2) {
+//            if(object1.head.length != object2.headAtoms.length
+//                    || object1.bodyAtoms.length != object2.bodyAtoms.length)
+//                return false;
+//            for(int index = object1.headAtoms.length - 1; index >= 0; --index)
+//                if(object1.headAtoms[index] != object2.headAtoms[index])
+//                    return false;
+//            for(int index = object1.bodyAtoms.length - 1; index >= 0; --index)
+//                if(object1.bodyAtoms[index] != object2.bodyAtoms[index])
+//                    return false;
+//            return true;
+//        }
+//
+//        protected int getHashCode(Clause object) {
+//            int hashCode = 0;
+//            for(int index = object.bodyAtoms.length - 1; index >= 0; --index)
+//                hashCode += object.bodyAtoms[index].hashCode();
+//            for(int index = object.headAtoms.length - 1; index >= 0; --index)
+//                hashCode += object.headAtoms[index].hashCode();
+//            return hashCode;
+//        }
+//    };
+//
+//    /**
+//     * Creates a clause from a string.
+//     *
+//     * @param s
+//     * @return
+//     */
+//    public static Clause create(String s) {
+//        return s_interningManager.intern(new Clause(s));
+//    }
+
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/clauses/Conjunction.java b/src/uk/ac/ox/cs/pagoda/rules/clauses/Conjunction.java
new file mode 100644
index 0000000..91bb3e7
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/clauses/Conjunction.java
@@ -0,0 +1,4 @@
+package uk.ac.ox.cs.pagoda.rules.clauses;
+
+public class Conjunction {
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/clauses/DLClause.java b/src/uk/ac/ox/cs/pagoda/rules/clauses/DLClause.java
new file mode 100644
index 0000000..7394be0
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/clauses/DLClause.java
@@ -0,0 +1,12 @@
+package uk.ac.ox.cs.pagoda.rules.clauses;
+
+public class DLClause extends Clause {
+
+//    private DLClause(Atom[] headAtoms, Atom[] bodyAtoms) {
+//        super(headAtoms, bodyAtoms);
+//    }
+//
+//    public static DLClause create(Atom[] headAtoms, Atom[] bodyAtoms) {
+//        return s_interningManager.intern(new DLClause(headAtoms, bodyAtoms));
+//    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java b/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
index 2d2198f..6fcf887 100644
--- a/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
+++ b/src/uk/ac/ox/cs/pagoda/summary/HermitSummaryFilter.java
@@ -6,12 +6,12 @@ import uk.ac.ox.cs.pagoda.endomorph.Endomorph;
 import uk.ac.ox.cs.pagoda.owl.OWLHelper;
 import uk.ac.ox.cs.pagoda.query.AnswerTuple;
 import uk.ac.ox.cs.pagoda.query.AnswerTuples;
-import uk.ac.ox.cs.pagoda.query.AnswerTuplesImp;
 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.full.HermitChecker;
 import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoder;
+import uk.ac.ox.cs.pagoda.util.SimpleProgressBar;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
 import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
@@ -122,12 +122,12 @@ public class HermitSummaryFilter extends Checker {
                 if(m_record.isProcessed())
                         return 0;
 
-                Utility.logDebug("The number of answers to be checked with HermiT: " + passed.size() + "/" + counter);
+//              Utility.logDebug("The number of answers to be checked with HermiT: " + passed.size() + "/" + counter);
                 m_record.setDifficulty(Step.FULL_REASONING);
 
-                if(summarisedConsistency)
-                        return endomorphismChecker.check(new AnswerTuplesImp(m_record.getAnswerVariables(), passed));
-                else
+//              if(summarisedConsistency)
+//                      return endomorphismChecker.check(new AnswerTuplesImp(m_record.getAnswerVariables(), passed));
+//              else
                         return endomorphismChecker.check(answers);
         }
 
@@ -145,9 +145,17 @@ public class HermitSummaryFilter extends Checker {
                         Set<AnswerTuple> succ = new HashSet<AnswerTuple>();
                         Set<AnswerTuple> falsified = new HashSet<AnswerTuple>(), fail = new HashSet<AnswerTuple>();
 
+                        int numOfAnswers = 0;
+                        for(; answers.isValid(); answers.moveNext()) {
+                                numOfAnswers++;
+                        }
+                        answers.reset();
+
                         counter = 0;
                         AnswerTuple representative;
+                        SimpleProgressBar progressBar = new SimpleProgressBar("Summarised checking", numOfAnswers);
                         for(AnswerTuple answer; answers.isValid(); answers.moveNext()) {
+                                progressBar.update(counter);
                                 ++counter;
                                 answer = answers.getTuple();
                                 representative = summary.getSummary(answer);
@@ -164,6 +172,7 @@ public class HermitSummaryFilter extends Checker {
                                         falsified.add(answer);
                                 }
                         }
+                        progressBar.dispose();
                         answers.dispose();
 
                         Utility.logDebug("@TIME to filter out non-answers by summarisation: " + t.duration());
diff --git a/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java b/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
index 4991d0d..7b68400 100644
--- a/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
+++ b/src/uk/ac/ox/cs/pagoda/util/PagodaProperties.java
@@ -15,6 +15,7 @@ public class PagodaProperties {
         public static final boolean DEFAULT_DEBUG = false;
         private static final boolean DEFAULT_USE_ALWAYS_SIMPLE_UPPER_BOUND;
         private static final boolean DEFAULT_USE_SKOLEM_UPPER_BOUND;
+        private static final boolean DEFAULT_TO_CALL_HERMIT;
         private static final Path DEFAULT_STATISTICS_DIR;
 
         public static boolean shellModeDefault = false;
@@ -23,6 +24,7 @@ public class PagodaProperties {
         static {
                 boolean defaultUseAlwaysSimpleUpperBound = false;
                 boolean defaultUseSkolemUpperBound = true;
+                boolean toCallHermit = true;
                 Path defaultStatisticsDir = null;
 
                 try(InputStream in = PagodaProperties.class.getClassLoader().getResourceAsStream(CONFIG_FILE)) {
@@ -52,12 +54,20 @@ public class PagodaProperties {
                                 else
                                         logger.debug("By default the Skolem upper bound is disabled");
                         }
+                        if(config.containsKey("toCallHermit")) {
+                                toCallHermit = Boolean.parseBoolean(config.getProperty("toCallHermit"));
+                                if(toCallHermit)
+                                        logger.debug("By default Hermit is enabled");
+                                else
+                                        logger.debug("By default Hermit is disabled");
+                        }
 
                 } catch(IOException e) {
                         e.printStackTrace();
                 }
                 DEFAULT_USE_ALWAYS_SIMPLE_UPPER_BOUND = defaultUseAlwaysSimpleUpperBound;
                 DEFAULT_USE_SKOLEM_UPPER_BOUND = defaultUseSkolemUpperBound;
+                DEFAULT_TO_CALL_HERMIT = toCallHermit;
                 DEFAULT_STATISTICS_DIR = defaultStatisticsDir;
         }
 
@@ -66,7 +76,7 @@ public class PagodaProperties {
         String queryPath = null;
         String answerPath = null;
         boolean toClassify = true;
-        boolean toCallHermiT = true;
+        boolean toCallHermiT = DEFAULT_TO_CALL_HERMIT;
         boolean shellMode = shellModeDefault;
         private boolean useAlwaysSimpleUpperBound = DEFAULT_USE_ALWAYS_SIMPLE_UPPER_BOUND;
         private boolean useSkolemUpperBound = DEFAULT_USE_SKOLEM_UPPER_BOUND;
diff --git a/src/uk/ac/ox/cs/pagoda/util/SimpleProgressBar.java b/src/uk/ac/ox/cs/pagoda/util/SimpleProgressBar.java
new file mode 100644
index 0000000..3c4aad7
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/util/SimpleProgressBar.java
@@ -0,0 +1,48 @@
+package uk.ac.ox.cs.pagoda.util;
+
+import uk.ac.ox.cs.pagoda.util.disposable.Disposable;
+
+public class SimpleProgressBar extends Disposable {
+
+    private final String name;
+    private int lastPercent;
+    private int maxValue;
+
+    public SimpleProgressBar() {
+        this("");
+    }
+
+    public SimpleProgressBar(String name) {
+        this(name, 100);
+    }
+
+    public SimpleProgressBar(String name, int maxValue) {
+        this.name = name;
+        this.maxValue = maxValue;
+    }
+
+    public void update(int value) {
+        int percent = value * 100 / maxValue;
+        StringBuilder template = new StringBuilder("\r" + name + " [");
+        for (int i = 0; i < 50; i++) {
+            if (i < percent * .5) {
+                template.append("=");
+            } else if (i == percent * .5) {
+                template.append(">");
+            } else {
+                template.append(" ");
+            }
+        }
+        template.append("] %s   ");
+        System.out.printf(template.toString(), percent + "%");
+        System.out.flush();
+        lastPercent = percent;
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+
+        System.out.println();
+    }
+}
diff --git a/test/resources/BugTests.xml b/test/resources/BugTests.xml
index 5782bd4..c7a80ba 100644
--- a/test/resources/BugTests.xml
+++ b/test/resources/BugTests.xml
@@ -4,13 +4,8 @@
 <suite name="BugTests">
 
     <test name="BugTest">
-        <groups>
-            <run>
-                <include name="BugTesters"/>
-            </run>
-        </groups>
         <classes>
-            <class name="uk.ac.ox.cs.pagoda.global_tests.MinimumCardinalityTest"/>
+            <class name="uk.ac.ox.cs.pagoda.global_tests.BugTests"/>
         </classes>
     </test>
 
diff --git a/test/resources/LightTests.xml b/test/resources/MainTests.xml
index bcdc4af..255b68e 100644
--- a/test/resources/LightTests.xml
+++ b/test/resources/MainTests.xml
@@ -1,21 +1,25 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE suite SYSTEM "http://testng.org/testng-1.0.dtd" >
 
-<suite name="LightTests">
-    <test name="light">
+<suite name="MainTests">
+    <test name="main">
         <groups>
             <run>
-                <include name="light"/>
+                <!--<include name="correctness"/>-->
+                <!--<include name="light"/>-->
                 <!--<include name="justExecute"/>-->
-                <exclude name="nonOriginal"/>
+                <!--&lt;!&ndash;<include name="heavy"/>&ndash;&gt;-->
+                <include name="nonOriginal"/>
             </run>
         </groups>
         <classes>
             <!--<class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaReactome"/>-->
-            <class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaUOBM"/>
-            <class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaLUBM"/>
+            <!--<class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaUOBM"/>-->
+            <!--<class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaLUBM"/>-->
             <!--Fly does not terminate: query-5 looks really hard-->
-            <!--<class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaFLY"/>-->
+            <class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaFLY"/>
+            <!--<class name="uk.ac.ox.cs.pagoda.global_tests.SkolemisationTests"/>-->
+            <!--<class name="uk.ac.ox.cs.pagoda.util.SimpleProgressBarTester" />-->
         </classes>
     </test>
 </suite>
\ No newline at end of file
diff --git a/test/resources/SygeniaTests.xml b/test/resources/SygeniaTests.xml
index 01c4eab..4daecf5 100644
--- a/test/resources/SygeniaTests.xml
+++ b/test/resources/SygeniaTests.xml
@@ -11,9 +11,10 @@
         </groups>
 
         <classes>
-            <!--<class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaUOBM"/>-->
+            <class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaUOBM"/>
             <class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaLUBM"/>
-            <!--<class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaFLY"/>-->
+            <class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaFLY"/>
+            <class name="uk.ac.ox.cs.pagoda.global_tests.TestPagodaReactome"/>
         </classes>
     </test>
 
diff --git a/test/uk/ac/ox/cs/pagoda/global_tests/MinimumCardinalityTest.java b/test/uk/ac/ox/cs/pagoda/global_tests/BugTests.java
index 71c20c1..19e0b2a 100644
--- a/test/uk/ac/ox/cs/pagoda/global_tests/MinimumCardinalityTest.java
+++ b/test/uk/ac/ox/cs/pagoda/global_tests/BugTests.java
@@ -6,6 +6,7 @@ import org.testng.Assert;
 import org.testng.annotations.Test;
 import uk.ac.ox.cs.pagoda.query.AnswerTuple;
 import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
 import uk.ac.ox.cs.pagoda.reasoner.QueryReasoner;
 import uk.ac.ox.cs.pagoda.util.TestUtil;
 
@@ -13,7 +14,7 @@ import java.io.IOException;
 import java.nio.file.Files;
 import java.nio.file.Paths;
 
-public class MinimumCardinalityTest {
+public class BugTests {
 
     public static final String NS = "http://example.org/test#%s";
 
@@ -21,8 +22,8 @@ public class MinimumCardinalityTest {
         return IRI.create(String.format(NS, name));
     }
 
-    @Test(groups = {"BugTesters"})
-    public void test() throws OWLOntologyCreationException, IOException, OWLOntologyStorageException {
+    @Test
+    public void minimumCardinalityAxiom() throws OWLOntologyCreationException, IOException, OWLOntologyStorageException {
 
         /*
          * Build test ontology
@@ -98,4 +99,86 @@ public class MinimumCardinalityTest {
         }
         pagoda.dispose();
     }
+
+    /**
+     * Bug: the relevant ontology is not a subset of the original one.
+     *
+     * @throws OWLOntologyCreationException
+     * @throws IOException
+     * @throws OWLOntologyStorageException
+     */
+    @Test
+    public void rTest() throws OWLOntologyCreationException, IOException, OWLOntologyStorageException {
+
+        /*
+         * Build test ontology
+         * */
+
+        OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
+        OWLDataFactory factory = manager.getOWLDataFactory();
+        OWLOntology ontology = manager.createOntology();
+
+        OWLClass classA = factory.getOWLClass(getEntityIRI("A"));
+        manager.addAxiom(ontology, factory.getOWLDeclarationAxiom(classA));
+        OWLClass classB = factory.getOWLClass(getEntityIRI("B"));
+        manager.addAxiom(ontology, factory.getOWLDeclarationAxiom(classB));
+        OWLNamedIndividual a = factory.getOWLNamedIndividual(getEntityIRI("a"));
+        OWLNamedIndividual b = factory.getOWLNamedIndividual(getEntityIRI("b"));
+        OWLNamedIndividual c = factory.getOWLNamedIndividual(getEntityIRI("c"));
+        OWLObjectProperty roleR = factory.getOWLObjectProperty(IRI.create(String.format(NS, "R")));
+        manager.addAxiom(ontology, factory.getOWLDeclarationAxiom(roleR));
+        OWLObjectProperty roleP = factory.getOWLObjectProperty(IRI.create(String.format(NS, "P")));
+        manager.addAxiom(ontology, factory.getOWLDeclarationAxiom(roleP));
+
+        // Class assertions
+        manager.addAxiom(ontology, factory.getOWLClassAssertionAxiom(classA, a));    // A(a)
+        manager.addAxiom(ontology, factory.getOWLClassAssertionAxiom(classA, b));    // A(b)
+        manager.addAxiom(ontology, factory.getOWLObjectPropertyAssertionAxiom(roleP, c, a)); // P(c,a)
+
+        // Axioms
+        // subsetOf(A someValuesFrom(R owl:Thing))
+        manager.addAxiom(ontology,
+                         factory.getOWLSubClassOfAxiom(classA,
+                                                       factory.getOWLObjectSomeValuesFrom(roleR,
+                                                                                          factory.getOWLThing())));
+
+        // inverseFunctional(R)
+        manager.addAxiom(ontology,
+                         factory.getOWLInverseFunctionalObjectPropertyAxiom(roleR));
+
+        // subsetOf(someValuesFrom(inverseOf(P) owl:thing) B)
+        manager.addAxiom(ontology,
+                         factory.getOWLSubClassOfAxiom(factory.getOWLObjectSomeValuesFrom(roleP.getInverseProperty(),
+                                                                                          factory.getOWLThing()),
+                                                       classB));
+        /*
+         * Save the ontology
+         * */
+
+//        manager.saveOntology(ontology, Files.newOutputStream(Paths.get("/home/alessandro/Desktop/test-ontology.owl")));
+
+        /*
+         * Test one query
+         * */
+
+        QueryReasoner pagoda = QueryReasoner.getInstance(ontology);
+        pagoda.loadOntology(ontology);
+        if(pagoda.preprocess()) {
+            String queryStr = "PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> " +
+                    "select distinct ?x" +
+                    " where { "
+                    + " ?x rdf:type " + classB +
+                    " }";
+            QueryRecord queryRecord = pagoda.getQueryManager().create(queryStr);
+            System.out.println(queryRecord);
+            pagoda.evaluate(queryRecord);
+            AnswerTuples answers = queryRecord.getAnswers();
+            System.out.println("Difficulty: " + queryRecord.getDifficulty());
+            for(AnswerTuple ans; answers.isValid(); answers.moveNext()) {
+                ans = answers.getTuple();
+                TestUtil.logInfo(ans);
+            }
+        }
+        pagoda.dispose();
+    }
 }
diff --git a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java
index 31d2eac..0ce3d69 100644
--- a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java
+++ b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java
@@ -25,7 +25,6 @@ public class TestPagodaFLY {
                               .query(Paths.get(ontoDir, "fly/queries/fly.sparql"))
                               .answer(answers)
                               .classify(false)
-                              .hermit(true)
                               .build();
 
         pagoda.run();
@@ -45,7 +44,6 @@ public class TestPagodaFLY {
                               .answer(answers)
 //                              .answer(Paths.get("/home/alessandro/Desktop/answers.json"))
                               .classify(false)
-                              .hermit(true)
                               .build();
 
         pagoda.run();
@@ -57,8 +55,8 @@ public class TestPagodaFLY {
         String ontoDir = TestUtil.getConfig().getProperty("ontoDir");
 
         Pagoda.builder()
-                .ontology(Paths.get(ontoDir, "fly/fly_rolledUp.owl"))
-//                        .ontology(Paths.get(ontoDir, "fly/fly_anatomy_XP_with_GJ_FC_individuals.owl"))
+//                .ontology(Paths.get(ontoDir, "fly/fly_rolledUp.owl"))
+                          .ontology(Paths.get(ontoDir, "fly/fly_anatomy_XP_with_GJ_FC_individuals.owl"))
                 .query(Paths.get(ontoDir, "fly/queries/new_queries.sparql"))
 //                        .answer(Paths.get("/home/alessandro/Desktop/answers.json"))
                 .classify(false)
diff --git a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaLUBM.java b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaLUBM.java
index fdbfc42..c893f96 100644
--- a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaLUBM.java
+++ b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaLUBM.java
@@ -23,8 +23,6 @@ public class TestPagodaLUBM {
                                                           .data(Paths.get(ontoDir, "lubm/data/lubm" + number + ".ttl"))
                                                           .query(Paths.get(ontoDir, "lubm/queries/test.sparql"))
                                                           .answer(answers)
-                                                          .classify(true)
-                                                          .hermit(true)
                                                           .build();
 
                 pagoda.run();
@@ -45,11 +43,9 @@ public class TestPagodaLUBM {
                 Pagoda pagoda = Pagoda.builder()
                                                           .ontology(Paths.get(ontoDir, "lubm/univ-bench.owl"))
                                                           .data(Paths.get(ontoDir, "lubm/data/lubm" + number + ".ttl"))
-                                .query(Paths.get(ontoDir, "lubm/queries/lubm_sygenia.sparql"))
+                                              .query(Paths.get(ontoDir, "lubm/queries/lubm_sygenia.sparql"))
 //                                                        .answer(answers)
-                                .classify(true)
-                                .hermit(true)
-                                .build();
+                                              .build();
 
                 pagoda.run();
 //              CheckAnswers.assertSameAnswers(answers, givenAnswers);
@@ -71,8 +67,6 @@ public class TestPagodaLUBM {
                                                           .data(Paths.get(ontoDir, "lubm/data/lubm" + number + ".ttl"))
                                 .query(Paths.get(ontoDir, "lubm/queries/lubm_sygenia_all-blanks.sparql"))
 //                                                        .answer(answers)
-                                .classify(true)
-                                .hermit(true)
                                 .build();
 
                 pagoda.run();
diff --git a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaUOBM.java b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaUOBM.java
index 9fb6cbe..c5b272c 100644
--- a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaUOBM.java
+++ b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaUOBM.java
@@ -41,8 +41,6 @@ public class TestPagodaUOBM {
                                                           .data(Paths.get(ontoDir, "uobm/data/uobm" + number + ".ttl"))
                                                           .query(Paths.get(ontoDir, "uobm/queries/test.sparql"))
                                                           .answer(answers)
-                                                          .classify(true)
-                                                          .hermit(true)
                                                           .build();
 
                 pagoda.run();
@@ -65,8 +63,6 @@ public class TestPagodaUOBM {
                                                           .ontology(Paths.get(ontoDir, "uobm/univ-bench-dl.owl"))
                                                           .data(Paths.get(ontoDir, "uobm/data/uobm" + number + ".ttl"))
                                 .query(Paths.get(ontoDir, "uobm/queries/uobm_sygenia.sparql"))
-                                .classify(true)
-                                .hermit(true)
                                 .build();
 
                 pagoda.run();
@@ -85,22 +81,30 @@ public class TestPagodaUOBM {
                           .ontology(Paths.get(ontoDir, "uobm/univ-bench-dl.owl"))
                           .data(Paths.get(ontoDir, "uobm/data/uobm" + number + ".ttl"))
                           .query(Paths.get(ontoDir, "uobm/queries/uobm_sygenia_all-blanks.sparql"))
-                          .classify(true)
-                          .hermit(true)
+                          .build()
+                          .run();
+        }
+
+        @Test(groups = {"justExecute", "heavy", "nonOriginal"})
+        public void justExecute_modifiedUOBM() throws IOException {
+                String ontoDir = TestUtil.getConfig().getProperty("ontoDir");
+
+                Pagoda.builder()
+                          .ontology(Paths.get(ontoDir, "uobm_modified/univ-bench-dl-modified.owl"))
+                          .data(Paths.get(ontoDir, "uobm_modified/data/uobm1.ttl"))
+                          .query(Paths.get(ontoDir, "uobm_modified/queries/additional_queries.sparql"))
                           .build()
                           .run();
         }
 
         @Test(groups = {"justExecute"})
-        public void justExecute_existentialQueries() throws IOException {
+        public void justExecute_additionalQueries() throws IOException {
                 String ontoDir = TestUtil.getConfig().getProperty("ontoDir");
 
                 Pagoda.builder()
-                          .ontology(Paths.get(ontoDir, "uobm/univ-bench-dl-modified.owl"))
+                          .ontology(Paths.get(ontoDir, "uobm/univ-bench-dl.owl"))
                           .data(Paths.get(ontoDir, "uobm/data/uobm1.ttl"))
-                          .query(Paths.get(ontoDir, "uobm/queries/existential_queries.sparql"))
-                          .classify(true)
-                          .hermit(true)
+                          .query(Paths.get(ontoDir, "uobm/queries/additional_queries.sparql"))
                           .build()
                           .run();
         }
diff --git a/test/uk/ac/ox/cs/pagoda/util/SimpleProgressBarTester.java b/test/uk/ac/ox/cs/pagoda/util/SimpleProgressBarTester.java
new file mode 100644
index 0000000..3de30e4
--- /dev/null
+++ b/test/uk/ac/ox/cs/pagoda/util/SimpleProgressBarTester.java
@@ -0,0 +1,16 @@
+package uk.ac.ox.cs.pagoda.util;
+
+import org.testng.annotations.Test;
+
+public class SimpleProgressBarTester {
+
+    @Test
+    public void test() throws InterruptedException {
+        SimpleProgressBar simpleProgressBar = new SimpleProgressBar("TestBar", 1000);
+        for(int i = 0; i < 1000; i++) {
+            simpleProgressBar.update(i);
+            Thread.sleep(10);
+        }
+        simpleProgressBar.dispose();
+    }
+}