[pagoda] Move project to Scala

This commit includes a few changes:
- The repository still uses Maven to manage dependency but it is now a
  Scala project.
- The code has been ported from OWLAPI 3.4.10 to 5.1.20
- A proof of concept program using both RSAComb and PAGOdA has been
  added.

19 files changed, 3302 insertions, 0 deletions

diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
new file mode 100644
index 0000000..3fd2fbd
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java
@@ -0,0 +1,314 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import org.semanticweb.HermiT.model.Atom;
+import org.semanticweb.HermiT.model.AtomicConcept;
+import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.HermiT.model.Variable;
+import org.semanticweb.owlapi.model.OWLOntology;
+import org.semanticweb.owlapi.model.OWLOntologyCreationException;
+import org.semanticweb.owlapi.model.OWLOntologyManager;
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.store.DataStore;
+import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType;
+import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.QueryManager;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
+import uk.ac.ox.cs.pagoda.reasoner.full.Checker;
+import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
+import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
+import uk.ac.ox.cs.pagoda.summary.HermitSummaryFilter;
+import uk.ac.ox.cs.pagoda.tracking.QueryTracker;
+import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoder;
+import uk.ac.ox.cs.pagoda.util.Timer;
+import uk.ac.ox.cs.pagoda.util.Utility;
+import uk.ac.ox.cs.pagoda.util.disposable.Disposable;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
+
+import java.util.LinkedList;
+
+public class ConsistencyManager extends Disposable {
+
+        protected MyQueryReasoner m_reasoner;
+        protected QueryManager m_queryManager;  
+        
+        Timer t = new Timer();
+        QueryRecord fullQueryRecord;
+        QueryRecord[] botQueryRecords;
+        LinkedList<DLClause> toAddClauses;
+        boolean fragmentExtracted = false;
+        
+        public ConsistencyManager(MyQueryReasoner reasoner) {
+                m_reasoner = reasoner;
+                m_queryManager = reasoner.getQueryManager();
+        }
+
+        @Override
+        public void dispose() {
+                super.dispose();
+                fullQueryRecord.dispose();
+        }
+
+        public void extractBottomFragment() {
+                if(isDisposed()) throw new DisposedException();
+
+                if(fragmentExtracted) return;
+                fragmentExtracted = true;
+
+                UpperDatalogProgram upperProgram = m_reasoner.program.getUpper();
+                int number = upperProgram.getBottomNumber();
+
+                if(number <= 1) {
+                        botQueryRecords = new QueryRecord[]{fullQueryRecord};
+                }
+                else {
+                        QueryRecord[] tempQueryRecords = new QueryRecord[number - 1];
+                        QueryRecord record;
+                        for(int i = 0; i < number - 1; ++i) {
+                                tempQueryRecords[i] = record =
+                                                m_queryManager.create(QueryRecord.botQueryText.replace("Nothing", "Nothing" + (i + 1)), 0, i + 1);
+                                AnswerTuples iter = null;
+                                try {
+                                        iter = m_reasoner.trackingStore.evaluate(record.getQueryText(), record.getAnswerVariables());
+                                        record.updateUpperBoundAnswers(iter);
+                                } finally {
+                                        if(iter != null) iter.dispose();
+                                        iter = null;
+                                }
+                        }
+
+                        int bottomNumber = 0;
+                        int[] group = new int[number - 1];
+                        for(int i = 0; i < number - 1; ++i) group[i] = i;
+                        for(int i = 0; i < number - 1; ++i)
+                                if(tempQueryRecords[i].isProcessed()) tempQueryRecords[i].dispose();
+                                else if(group[i] == i) {
+                                        ++bottomNumber;
+                                        record = tempQueryRecords[i];
+                                        for(int j = i + 1; j < number - 1; ++j)
+                                                if(record.hasSameGapAnswers(tempQueryRecords[j]))
+                                                        group[j] = i;
+                                }
+
+                        Utility.logInfo("There are " + bottomNumber + " different bottom fragments.");
+                        toAddClauses = new LinkedList<DLClause>();
+                        int bottomCounter = 0;
+                        botQueryRecords = new QueryRecord[bottomNumber];
+                        Variable X = Variable.create("X");
+                        for(int i = 0; i < number - 1; ++i)
+                                if(!tempQueryRecords[i].isDisposed() && !tempQueryRecords[i].isProcessed())
+                                        if(group[i] == i) {
+                                                botQueryRecords[bottomCounter] = record = tempQueryRecords[i];
+                                                record.resetInfo(QueryRecord.botQueryText.replace("Nothing", "Nothing_final" + (++bottomCounter)), 0,
+                                                                                 group[i] = bottomCounter);
+                                                toAddClauses.add(
+                                                                DLClause.create(
+                                                                                new Atom[]{Atom.create(AtomicConcept.create(AtomicConcept.NOTHING.getIRI() + "_final" + bottomCounter), X)},
+                                                                                new Atom[]{Atom.create(AtomicConcept.create(AtomicConcept.NOTHING.getIRI() + (i + 1)), X)}));
+                                        }
+                                        else {
+                                                toAddClauses.add(
+                                                                DLClause.create(
+                                                                                new Atom[]{Atom.create(AtomicConcept.create(AtomicConcept.NOTHING.getIRI() + "_final" + group[group[i]]), X)},
+                                                                                new Atom[]{Atom.create(AtomicConcept.create(AtomicConcept.NOTHING.getIRI() + (i + 1)), X)}));
+                                                tempQueryRecords[i].dispose();
+                                        }
+
+                        upperProgram.updateDependencyGraph(toAddClauses);
+                }
+
+                String[] programs = collectTrackingProgramAndImport();
+                if(programs.length == 0)
+                        return;
+
+                DataStore store = m_reasoner.trackingStore.getDataStore();
+                long oldTripleCount, tripleCount;
+                try {
+                        Timer t1 = new Timer();
+                        oldTripleCount = store.getTriplesCount();
+                        for(String program : programs)
+                                store.importRules(program, UpdateType.ScheduleForAddition);
+                        store.applyReasoning(true);
+                        tripleCount = store.getTriplesCount();
+
+                        Utility.logDebug("tracking store after materialising tracking program: " + tripleCount + " (" + (tripleCount - oldTripleCount) + " new)",
+                                                        "tracking store finished the materialisation of tracking program in " + t1.duration() + " seconds.");
+
+                        extractAxioms();
+                        store.clearRulesAndMakeFactsExplicit();
+                } catch(JRDFStoreException e) {
+                        e.printStackTrace();
+                } catch(OWLOntologyCreationException e) {
+                        e.printStackTrace();
+                }
+        }
+
+        public QueryRecord[] getQueryRecords() {
+                if(isDisposed()) throw new DisposedException();
+
+                return botQueryRecords;
+        }
+
+        boolean checkRLLowerBound() {
+                if(isDisposed()) throw new DisposedException();
+
+                fullQueryRecord = m_queryManager.create(QueryRecord.botQueryText, 0);
+                AnswerTuples iter = null;
+
+                try {
+                        iter = m_reasoner.rlLowerStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables());
+                        fullQueryRecord.updateLowerBoundAnswers(iter);
+                } finally {
+                        iter.dispose();
+                }
+
+                if (fullQueryRecord.getNoOfSoundAnswers() > 0) {
+                        Utility.logInfo("Answers to bottom in the lower bound: ", fullQueryRecord.outputSoundAnswerTuple());
+                        return false;
+                }
+                return true;
+        }
+
+//      protected boolean unsatisfiability(double duration) {
+//              fullQueryRecord.dispose();
+//              Utility.logDebug("The ontology and dataset is unsatisfiable.");
+//              return false;
+//      }
+
+//      protected boolean satisfiability(double duration) {
+//              fullQueryRecord.dispose();
+//              Utility.logDebug("The ontology and dataset is satisfiable.");
+//              return true;
+//      }
+
+        boolean checkELLowerBound() {
+                if(isDisposed()) throw new DisposedException();
+
+                fullQueryRecord.updateLowerBoundAnswers(m_reasoner.elLowerStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord
+                                .getAnswerVariables()));
+                if(fullQueryRecord.getNoOfSoundAnswers() > 0) {
+                        Utility.logInfo("Answers to bottom in the lower bound: ", fullQueryRecord.outputSoundAnswerTuple());
+                        return true;
+                }
+                return true;
+        }
+
+        boolean checkUpper(BasicQueryEngine upperStore) {
+                if(isDisposed()) throw new DisposedException();
+
+                if(upperStore != null) {
+                        AnswerTuples tuples = null;
+                        try {
+                                tuples = upperStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables());
+                                if(!tuples.isValid()) {
+                                        Utility.logInfo("There are no contradictions derived in " + upperStore.getName() + " materialisation.");
+                                        Utility.logDebug("The ontology and dataset is satisfiable.");
+                                        return true;
+                                }
+                        } finally {
+                                if(tuples != null) tuples.dispose();
+                        }
+                }
+                return false;
+        }
+
+        boolean check() {
+                if(isDisposed()) throw new DisposedException();
+
+//              if (!checkRLLowerBound()) return false;
+//              if (!checkELLowerBound()) return false;
+//              if (checkLazyUpper()) return true;
+                AnswerTuples iter = null;
+
+                try {
+                        iter =
+                                        m_reasoner.trackingStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables());
+                        fullQueryRecord.updateUpperBoundAnswers(iter);
+                } finally {
+                        if(iter != null) iter.dispose();
+                }
+
+                if(fullQueryRecord.getNoOfCompleteAnswers() == 0)
+                        return true;
+
+                extractBottomFragment();
+
+                try {
+                        extractAxioms4Full();
+                } catch(OWLOntologyCreationException e) {
+                        e.printStackTrace();
+                }
+//              fullQueryRecord.saveRelevantClause();
+
+                boolean satisfiability;
+
+                Checker checker;
+                for(QueryRecord r : getQueryRecords()) {
+                        // TODO to be removed ...
+//                      r.saveRelevantOntology("bottom" + r.getQueryID() + ".owl");
+                        checker = new HermitSummaryFilter(r, true); // m_reasoner.factory.getSummarisedReasoner(r);
+                        satisfiability = checker.isConsistent();
+                        checker.dispose();
+                        if(!satisfiability) return false;
+                }
+
+//              Checker checker = m_reasoner.factory.getSummarisedReasoner(fullQueryRecord);
+//              boolean satisfiable = checker.isConsistent();
+//              checker.dispose();
+//              if (!satisfiable) return unsatisfiability(t.duration());
+
+                return true;
+        }
+
+        private void extractAxioms4Full() throws OWLOntologyCreationException {
+                OWLOntologyManager manager = m_reasoner.encoder.getProgram().getOntology().getOWLOntologyManager();
+                OWLOntology fullOntology = manager.createOntology();
+                for (QueryRecord record: botQueryRecords) {
+                        for (DLClause clause: record.getRelevantClauses()) {
+                                fullQueryRecord.addRelevantClauses(clause);
+                        }
+                        manager.addAxioms(fullOntology, record.getRelevantOntology().getAxioms());
+                }
+                fullQueryRecord.setRelevantOntology(fullOntology);
+        }
+
+        private void extractAxioms() throws OWLOntologyCreationException {
+                OWLOntologyManager manager = m_reasoner.encoder.getProgram().getOntology().getOWLOntologyManager();
+                for (QueryRecord record: botQueryRecords) {
+                        record.setRelevantOntology(manager.createOntology());
+                        QueryTracker tracker = new QueryTracker(m_reasoner.encoder, m_reasoner.rlLowerStore, record);
+                        m_reasoner.encoder.setCurrentQuery(record);
+                        tracker.extractAxioms(m_reasoner.trackingStore);
+//                      record.saveRelevantClause();
+//                      record.saveRelevantOntology("bottom" + record.getQueryID() + ".owl");
+                        Utility.logInfo("finish extracting axioms for bottom " + record.getQueryID());
+                }
+        }
+
+        private String[] collectTrackingProgramAndImport() {
+                String[] programs = new String[botQueryRecords.length];
+                TrackingRuleEncoder encoder = m_reasoner.encoder;
+
+                StringBuilder builder;
+                LinkedList<DLClause> currentClauses = new LinkedList<DLClause>();
+
+                for (int i = 0; i < botQueryRecords.length; ++i) {
+                        encoder.setCurrentQuery(botQueryRecords[i]);
+                        builder = new StringBuilder(encoder.getTrackingProgram());
+//                      encoder.saveTrackingRules("tracking_bottom" + (i + 1) + ".dlog");
+
+                        for (DLClause clause: toAddClauses)
+                                if (clause.getHeadAtom(0).getDLPredicate().toString().contains("_final" + (i + 1)))
+                                        currentClauses.add(clause);
+
+                        builder.append(DLClauseHelper.toString(currentClauses));
+                        programs[i] = builder.toString();
+
+                        currentClauses.clear();
+                }
+
+                return programs;
+        }
+
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java
new file mode 100644
index 0000000..29754ce
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ELHOQueryReasoner.java
@@ -0,0 +1,101 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import org.semanticweb.karma2.profile.ELHOProfile;
+import org.semanticweb.owlapi.model.OWLOntology;
+import uk.ac.ox.cs.pagoda.constraints.UnaryBottom;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
+import uk.ac.ox.cs.pagoda.query.QueryRecord.Step;
+import uk.ac.ox.cs.pagoda.reasoner.light.KarmaQueryEngine;
+import uk.ac.ox.cs.pagoda.rules.LowerDatalogProgram;
+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;
+
+public class ELHOQueryReasoner extends QueryReasoner {
+
+    LowerDatalogProgram program;
+
+    OWLOntology elho_ontology;
+    KarmaQueryEngine elLowerStore = null;
+
+    private Timer t = new Timer();
+
+    public ELHOQueryReasoner() {
+        elLowerStore = new KarmaQueryEngine("el");
+    }
+
+    @Override
+    public void evaluate(QueryRecord queryRecord) {
+        if(isDisposed()) throw new DisposedException();
+        AnswerTuples elAnswer = null;
+        t.reset();
+        try {
+            elAnswer = elLowerStore.evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+            queryRecord.updateLowerBoundAnswers(elAnswer);
+        } finally {
+            if(elAnswer != null) elAnswer.dispose();
+        }
+        queryRecord.addProcessingTime(Step.EL_LOWER_BOUND, t.duration());
+
+        queryRecord.setDifficulty(Step.EL_LOWER_BOUND);
+        queryRecord.markAsProcessed();
+    }
+
+    @Override
+    public void evaluateUpper(QueryRecord queryRecord) {
+        if(isDisposed()) throw new DisposedException();
+        evaluate(queryRecord);
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+        if(elLowerStore != null) elLowerStore.dispose();
+    }
+
+    @Override
+    public void loadOntology(OWLOntology ontology) {
+        if(isDisposed()) throw new DisposedException();
+        program = new LowerDatalogProgram(properties.getToClassify());
+        program.load(ontology, new UnaryBottom());
+        program.transform();
+
+        importData(program.getAdditionalDataFile());
+
+        elho_ontology = new ELHOProfile().getFragment(ontology);
+        elLowerStore.processOntology(elho_ontology);
+    }
+
+    @Override
+    public boolean preprocess() {
+        if(isDisposed()) throw new DisposedException();
+        elLowerStore.importRDFData("data", getImportedData());
+        String rlLowerProgramText = program.toString();
+//              program.save();
+        elLowerStore.materialise("lower program", rlLowerProgramText);
+        elLowerStore.initialiseKarma();
+
+        if(!isConsistent()) {
+            Utility.logDebug("The dataset is not consistent with the ontology.");
+            return false;
+        }
+        return true;
+    }
+
+    @Override
+    public boolean isConsistent() {
+        if(isDisposed()) throw new DisposedException();
+        String[] X = new String[]{"X"};
+        AnswerTuples ans = null;
+        try {
+            ans = elLowerStore.evaluate(QueryRecord.botQueryText, X);
+            if(ans.isValid()) return false;
+        } finally {
+            if(ans != null) ans.dispose();
+        }
+
+        return true;
+    }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java
new file mode 100644
index 0000000..15dfa03
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/ELHOUQueryReasoner.java
@@ -0,0 +1,199 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import org.semanticweb.karma2.profile.ELHOProfile;
+import org.semanticweb.owlapi.model.OWLOntology;
+import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine;
+import uk.ac.ox.cs.pagoda.owl.EqualitiesEliminator;
+import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
+import uk.ac.ox.cs.pagoda.query.QueryRecord.Step;
+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;
+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;
+
+class ELHOUQueryReasoner extends QueryReasoner {
+
+    DatalogProgram program;
+
+    BasicQueryEngine rlLowerStore;
+    BasicQueryEngine rlUpperStore;
+
+    OWLOntology elho_ontology;
+    KarmaQueryEngine elLowerStore = null;
+
+    boolean multiStageTag, equalityTag;
+    String originalMarkProgram;
+    private Timer t = new Timer();
+
+    public ELHOUQueryReasoner(boolean multiStageTag, boolean considerEqualities) {
+        this.multiStageTag = multiStageTag;
+        this.equalityTag = considerEqualities;
+        rlLowerStore = new BasicQueryEngine("rl-lower-bound");
+        elLowerStore = new KarmaQueryEngine("el-lower-bound");
+
+        if(!multiStageTag)
+            rlUpperStore = new BasicQueryEngine("rl-upper-bound");
+        else
+            rlUpperStore = new MultiStageQueryEngine("rl-upper-bound", false);
+    }
+
+    @Override
+    public void evaluate(QueryRecord queryRecord) {
+        if(isDisposed()) throw new DisposedException();
+        AnswerTuples rlAnswer = null;
+        t.reset();
+        try {
+            rlAnswer = rlLowerStore.evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+            queryRecord.updateLowerBoundAnswers(rlAnswer);
+        } finally {
+            if(rlAnswer != null) rlAnswer.dispose();
+        }
+        queryRecord.addProcessingTime(Step.LOWER_BOUND, t.duration());
+
+        String extendedQueryText = queryRecord.getExtendedQueryText().get(0);
+        String[] toQuery = queryRecord.getQueryText().equals(extendedQueryText) ?
+                new String[]{queryRecord.getQueryText()} :
+                new String[]{queryRecord.getQueryText(), extendedQueryText};
+
+        for(String queryText : toQuery) {
+            rlAnswer = null;
+            t.reset();
+            try {
+                rlAnswer = rlUpperStore.evaluate(queryText, queryRecord.getAnswerVariables());
+                queryRecord.updateUpperBoundAnswers(rlAnswer);
+            } finally {
+                if(rlAnswer != null) rlAnswer.dispose();
+            }
+            queryRecord.addProcessingTime(Step.UPPER_BOUND, t.duration());
+
+            if(queryRecord.isProcessed()) {
+                queryRecord.setDifficulty(Step.UPPER_BOUND);
+                return;
+            }
+        }
+
+        AnswerTuples elAnswer = null;
+        t.reset();
+        try {
+            elAnswer =
+                    elLowerStore.evaluate(extendedQueryText, queryRecord.getAnswerVariables(), queryRecord.getLowerBoundAnswers());
+            queryRecord.updateLowerBoundAnswers(elAnswer);
+        } finally {
+            if(elAnswer != null) elAnswer.dispose();
+        }
+        queryRecord.addProcessingTime(Step.EL_LOWER_BOUND, t.duration());
+    }
+
+    @Override
+    public void evaluateUpper(QueryRecord queryRecord) {
+        if(isDisposed()) throw new DisposedException();
+        AnswerTuples rlAnswer = null;
+        try {
+            rlAnswer = rlUpperStore.evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+            queryRecord.updateUpperBoundAnswers(rlAnswer, true);
+        } finally {
+            if(rlAnswer != null) rlAnswer.dispose();
+        }
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+        if(elLowerStore != null) elLowerStore.dispose();
+        if(rlUpperStore != null) rlUpperStore.dispose();
+    }
+
+    @Override
+    public void loadOntology(OWLOntology o) {
+        if(isDisposed()) throw new DisposedException();
+        if(!equalityTag) {
+            EqualitiesEliminator eliminator = new EqualitiesEliminator(o);
+            o = eliminator.getOutputOntology();
+            eliminator.save();
+        }
+
+        OWLOntology ontology = o;
+        program = new DatalogProgram(ontology);
+
+        importData(program.getAdditionalDataFile());
+
+        elho_ontology = new ELHOProfile().getFragment(ontology);
+        elLowerStore.processOntology(elho_ontology);
+        originalMarkProgram = OWLHelper.getOriginalMarkProgram(ontology);
+    }
+
+    @Override
+    public boolean preprocess() {
+        if(isDisposed()) throw new DisposedException();
+        String name = "data", datafile = getImportedData();
+
+        String lowername = "lower program";
+        String rlLowerProgramText = program.getLower().toString();
+
+        rlUpperStore.importRDFData(name, datafile);
+        rlUpperStore.materialise("saturate named individuals", originalMarkProgram);
+
+        int flag = rlUpperStore.materialiseRestrictedly(program, null);
+        if(flag != 1) {
+            if(flag == -1) return false;
+            rlUpperStore.dispose();
+
+            if(!multiStageTag)
+                rlUpperStore = new BasicQueryEngine("rl-upper-bound");
+            else
+                rlUpperStore = new MultiStageQueryEngine("rl-upper-bound", false);
+            rlUpperStore.importRDFData(name, datafile);
+            rlUpperStore.materialise("saturate named individuals", originalMarkProgram);
+            rlUpperStore.materialiseFoldedly(program, null);
+        }
+        Utility.logInfo("upper store ready.");
+
+        rlLowerStore.importRDFData(name, datafile);
+        rlLowerStore.materialise(lowername, rlLowerProgramText);
+        Utility.logInfo("lower store ready.");
+
+        elLowerStore.importRDFData(name, datafile);
+        elLowerStore.materialise("saturate named individuals", originalMarkProgram);
+        elLowerStore.materialise(lowername, rlLowerProgramText);
+
+        elLowerStore.initialiseKarma();
+        Utility.logInfo("EL lower store ready.");
+
+        if(!isConsistent()) {
+            Utility.logInfo("The dataset is not consistent with the ontology.");
+            return false;
+        }
+        Utility.logInfo("The dataset is consistent.");
+        return true;
+    }
+
+    @Override
+    public boolean isConsistent() {
+        if(isDisposed()) throw new DisposedException();
+        Utility.logInfo("Start checking consistency... ");
+        String[] X = new String[]{"X"};
+        AnswerTuples ans = null;
+        try {
+            ans = rlUpperStore.evaluate(QueryRecord.botQueryText, X);
+            if(!ans.isValid()) return true;
+        } finally {
+            if(ans != null) ans.dispose();
+        }
+
+        ans = null;
+        try {
+            ans = elLowerStore.evaluate(QueryRecord.botQueryText, X);
+            if(ans.isValid()) return false;
+        } finally {
+            if(ans != null) ans.dispose();
+        }
+
+        Utility.logDebug("The consistency of the data has not been determined yet.");
+        return true;
+    }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java
new file mode 100644
index 0000000..ac62488
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/HermiTReasoner.java
@@ -0,0 +1,122 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import org.semanticweb.HermiT.Reasoner;
+import org.semanticweb.owlapi.model.*;
+import uk.ac.ox.cs.JRDFox.model.Individual;
+import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine;
+import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.owl.QueryRoller;
+import uk.ac.ox.cs.pagoda.query.*;
+import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
+import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
+import uk.ac.ox.cs.pagoda.util.Utility;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
+
+import java.io.File;
+import java.io.IOException;
+import java.util.HashSet;
+import java.util.Set;
+
+class HermiTReasoner extends QueryReasoner {
+
+    Reasoner hermit;
+
+    BasicQueryEngine upperStore = null;
+
+    OWLOntology onto;
+    OWLDataFactory factory;
+
+    String importedOntologyPath = null;
+
+    QueryRoller roller;
+    boolean toCheckSatisfiability;
+
+    public HermiTReasoner(boolean toCheckSatisfiability) {
+        this.toCheckSatisfiability = toCheckSatisfiability;
+    }
+
+    @Override
+    public void loadOntology(OWLOntology ontology) {
+        if(isDisposed()) throw new DisposedException();
+        onto = ontology;
+    }
+
+    @Override
+    public boolean preprocess() {
+        if(isDisposed()) throw new DisposedException();
+        OWLOntology tbox = onto;
+        try {
+            onto = OWLHelper.getImportedOntology(tbox, getImportedData().split(ImportDataFileSeparator));
+            importedOntologyPath = OWLHelper.getOntologyPath(onto);
+        } catch(OWLOntologyCreationException | OWLOntologyStorageException | IOException e) {
+            e.printStackTrace();
+        }
+
+        DatalogProgram datalogProgram = new DatalogProgram(tbox);
+        importData(datalogProgram.getAdditionalDataFile());
+        upperStore = new MultiStageQueryEngine("rl-upper", false);
+        upperStore.importRDFData("data", getImportedData());
+        GapByStore4ID gap = new GapByStore4ID(upperStore);
+        upperStore.materialiseFoldedly(datalogProgram, gap);
+        gap.clear();
+
+        factory = onto.getOWLOntologyManager().getOWLDataFactory();
+        roller = new QueryRoller(factory);
+
+        hermit = new Reasoner(onto);
+        return isConsistent();
+    }
+
+    @Override
+    public boolean isConsistent() {
+        if(isDisposed()) throw new DisposedException();
+        if(toCheckSatisfiability)
+            return hermit.isConsistent();
+        return true;
+    }
+
+    @Override
+    public void evaluate(QueryRecord record) {
+        if(isDisposed()) throw new DisposedException();
+        String[] disVars = record.getDistinguishedVariables();
+        Set<OWLNamedIndividual> individuals = onto.getIndividualsInSignature(true);
+        if(disVars.length == 1) {
+            OWLClassExpression clsExp = roller.rollUp(record.getClause(), record.getAnswerVariables()[0]);
+            Set<AnswerTuple> answers = new HashSet<AnswerTuple>();
+            for(OWLNamedIndividual individual : individuals) {
+                Utility.logDebug("checking ... " + individual);
+                if(hermit.isEntailed(factory.getOWLClassAssertionAxiom(clsExp, individual))) {
+                    answers.add(new AnswerTuple(new Individual[]{Individual.create(individual.toStringID())}));
+                }
+            }
+            record.updateLowerBoundAnswers(new AnswerTuplesImp(record.getAnswerVariables(), answers));
+            record.markAsProcessed();
+        }
+        else {
+            // FIXME join here
+            record.markAsProcessed();
+        }
+    }
+
+    @Override
+    public void evaluateUpper(QueryRecord record) {
+        if(isDisposed()) throw new DisposedException();
+        AnswerTuples rlAnswer = null;
+        try {
+            rlAnswer = upperStore.evaluate(record.getQueryText(), record.getAnswerVariables());
+            record.updateUpperBoundAnswers(rlAnswer, true);
+        } finally {
+            if(rlAnswer != null) rlAnswer.dispose();
+        }
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+        if(importedOntologyPath != null) {
+            File tmp = new File(importedOntologyPath);
+            if(tmp.exists()) tmp.delete();
+        }
+    }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/IterativeRefinement.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/IterativeRefinement.java
new file mode 100644
index 0000000..7847e7c
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/IterativeRefinement.java
@@ -0,0 +1,117 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import org.semanticweb.owlapi.model.OWLOntology;
+import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
+import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom;
+import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
+import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
+import uk.ac.ox.cs.pagoda.rules.GeneralProgram;
+import uk.ac.ox.cs.pagoda.tracking.QueryTracker;
+import uk.ac.ox.cs.pagoda.util.Utility;
+
+import java.io.File;
+
+public class IterativeRefinement {
+        
+        private static final int depthLimit = 1; 
+        
+        QueryRecord m_record;
+        QueryTracker m_tracker; 
+        BasicQueryEngine m_trackingStore;
+        QueryRecord[] botQueryRecords;  
+        
+        int m_depth = 0;
+        String tempDataFile = "temp.ttl";
+        
+        public IterativeRefinement(QueryRecord queryRecord, QueryTracker tracker, BasicQueryEngine trackingStore, QueryRecord[] botQueryRecords) {
+                m_record = queryRecord;
+                m_tracker = tracker;
+                m_trackingStore = trackingStore;
+                this.botQueryRecords = botQueryRecords;
+        }
+
+        public OWLOntology extractWithFullABox(String dataset, BottomStrategy upperBottom) {
+                GeneralProgram program; 
+                boolean update; 
+                while (m_depth < depthLimit) {
+                        ++m_depth;
+                        program = new GeneralProgram(m_record.getRelevantClauses(), m_record.getRelevantOntology());
+                        
+                        MultiStageQueryEngine tEngine = new MultiStageQueryEngine("query-tracking", true);
+                        try {
+                                tEngine.importRDFData("data", dataset);
+                                if (tEngine.materialise4SpecificQuery(program, m_record, upperBottom) != 1) {
+                                        return m_record.getRelevantOntology(); 
+                                }
+                                
+                                AnswerTuples ans = null; 
+                                try {
+                                        ans = tEngine.evaluate(m_record.getQueryText());
+                                        update = m_record.updateUpperBoundAnswers(ans);
+                                } finally {
+                                        if (ans != null) ans.dispose();
+                                }                               
+                        } finally {
+                                tEngine.dispose();
+                        }
+
+                        if(m_record.isProcessed())
+                                return null;
+                        
+                        if (!update) break; 
+                        
+                        m_record.updateSubID();
+                        m_tracker.extract(m_trackingStore, botQueryRecords, true); 
+                }
+                
+                return m_record.getRelevantOntology(); 
+        }
+        
+        public OWLOntology extract(UpperUnaryBottom upperBottom) {
+                GeneralProgram program; 
+                boolean update; 
+                while (m_depth < depthLimit) {
+                        m_record.saveABoxInTurtle(tempDataFile); 
+                        program = new GeneralProgram(m_record.getRelevantClauses(), m_record.getRelevantOntology());
+                        
+                        MultiStageQueryEngine tEngine = new MultiStageQueryEngine("query-tracking", true);
+                        try {
+                                tEngine.importRDFData("fragment abox", tempDataFile);
+                                if (tEngine.materialise4SpecificQuery(program, m_record, upperBottom) != 1) {
+                                        return m_record.getRelevantOntology(); 
+                                }
+                                
+                                AnswerTuples ans = null; 
+                                try {
+                                        ans = tEngine.evaluate(m_record.getQueryText()); 
+                                        update = m_record.updateUpperBoundAnswers(ans);
+                                } finally {
+                                        if (ans != null) ans.dispose();
+                                }
+                        } finally {
+                                tEngine.dispose();
+                        }
+
+                        if(m_record.isProcessed())
+                                return null;
+                        
+                        if (!update) break; 
+                        
+                        m_record.updateSubID();
+                        m_tracker.extract(m_trackingStore, botQueryRecords, true); 
+                }
+                
+                return m_record.getRelevantOntology(); 
+        }
+        
+        public void dispose() {
+                File file = new File(tempDataFile);  
+                if (file.exists()) {
+                        file.delete(); 
+                        Utility.logDebug(file.getAbsolutePath() + " is deleted.");
+                }
+        }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
new file mode 100644
index 0000000..f2e29f2
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -0,0 +1,473 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import org.semanticweb.karma2.profile.ELHOProfile;
+import org.semanticweb.owlapi.model.OWLOntology;
+import org.semanticweb.owlapi.model.parameters.Imports;
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine;
+import uk.ac.ox.cs.pagoda.owl.EqualitiesEliminator;
+import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+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.light.BasicQueryEngine;
+import uk.ac.ox.cs.pagoda.reasoner.light.KarmaQueryEngine;
+import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
+import uk.ac.ox.cs.pagoda.summary.HermitSummaryFilter;
+import uk.ac.ox.cs.pagoda.tracking.QueryTracker;
+import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoder;
+import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoderDisjVar1;
+import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoderWithGap;
+import uk.ac.ox.cs.pagoda.util.ExponentialInterpolation;
+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 uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
+import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
+
+import java.util.Collection;
+import java.util.LinkedList;
+
+public class MyQueryReasoner extends QueryReasoner {
+
+    OWLOntology ontology;
+    OWLOntology elho_ontology;
+    DatalogProgram program;
+
+    BasicQueryEngine rlLowerStore = null;
+    KarmaQueryEngine elLowerStore = null;
+    MultiStageQueryEngine lazyUpperStore = null;
+    MultiStageQueryEngine trackingStore = null;
+    TrackingRuleEncoder encoder;
+
+    private boolean equalityTag;
+    private Timer t = new Timer();
+
+    private Collection<String> predicatesWithGap = null;
+    private ConsistencyStatus isConsistent;
+    private ConsistencyManager consistency = new ConsistencyManager(this);
+//    private int relevantOntologiesCounter = 0;
+
+    public MyQueryReasoner() {
+        setup(true);
+    }
+
+    public MyQueryReasoner(boolean multiStageTag, boolean considerEqualities) {
+        if(!multiStageTag)
+            throw new IllegalArgumentException(
+                    "Value \"true\" for parameter \"multiStageTag\" is no longer supported");
+
+        setup(considerEqualities);
+    }
+
+    @Override
+    public void loadOntology(OWLOntology o) {
+        if(isDisposed()) throw new DisposedException();
+        if(!equalityTag) {
+            EqualitiesEliminator eliminator = new EqualitiesEliminator(o);
+            o = eliminator.getOutputOntology();
+            eliminator.save();
+        }
+
+        ontology = o;
+        program = new DatalogProgram(ontology);
+//              program.getLower().save();
+//              program.getUpper().save();
+                program.getGeneral().save();
+
+        if(!program.getGeneral().isHorn())
+            lazyUpperStore = new MultiStageQueryEngine("lazy-upper-bound", true);
+
+        importData(program.getAdditionalDataFile());
+
+        elho_ontology = new ELHOProfile().getFragment(ontology);
+        elLowerStore.processOntology(elho_ontology);
+    }
+
+    public Collection<String> getPredicatesWithGap() {
+        if(isDisposed()) throw new DisposedException();
+        return predicatesWithGap;
+    }
+
+    @Override
+    public boolean preprocess() {
+        if(isDisposed()) throw new DisposedException();
+
+        t.reset();
+        Utility.logInfo("Preprocessing (and checking satisfiability)...");
+
+        String name = "data", datafile = getImportedData();
+        rlLowerStore.importRDFData(name, datafile);
+        rlLowerStore.materialise("lower program", program.getLower().toString());
+//              program.getLower().save();
+        if(!consistency.checkRLLowerBound()) {
+            Utility.logDebug("time for satisfiability checking: " + t.duration());
+            isConsistent = ConsistencyStatus.INCONSISTENT;
+            return false;
+        }
+        Utility.logDebug("The number of sameAs assertions in RL lower store: " + rlLowerStore.getSameAsNumber());
+
+        String originalMarkProgram = OWLHelper.getOriginalMarkProgram(ontology);
+
+        elLowerStore.importRDFData(name, datafile);
+        elLowerStore.materialise("saturate named individuals", originalMarkProgram);
+        elLowerStore.materialise("lower program", program.getLower().toString());
+        elLowerStore.initialiseKarma();
+        if(!consistency.checkELLowerBound()) {
+            Utility.logDebug("time for satisfiability checking: " + t.duration());
+            isConsistent = ConsistencyStatus.INCONSISTENT;
+            return false;
+        }
+
+        if(lazyUpperStore != null) {
+            lazyUpperStore.importRDFData(name, datafile);
+            lazyUpperStore.materialise("saturate named individuals", originalMarkProgram);
+            int tag = lazyUpperStore.materialiseRestrictedly(program, null);
+            if(tag == -1) {
+                Utility.logDebug("time for satisfiability checking: " + t.duration());
+                isConsistent = ConsistencyStatus.INCONSISTENT;
+                return false;
+            }
+            else if(tag != 1) {
+                lazyUpperStore.dispose();
+                lazyUpperStore = null;
+            }
+        }
+        if(consistency.checkUpper(lazyUpperStore)) {
+            isConsistent = ConsistencyStatus.CONSISTENT;
+            Utility.logDebug("time for satisfiability checking: " + t.duration());
+        }
+
+        trackingStore.importRDFData(name, datafile);
+        trackingStore.materialise("saturate named individuals", originalMarkProgram);
+
+//              materialiseFullUpper();
+//              GapByStore4ID gap = new GapByStore4ID(trackingStore);
+        GapByStore4ID gap = new GapByStore4ID2(trackingStore, rlLowerStore);
+        trackingStore.materialiseFoldedly(program, gap);
+        predicatesWithGap = gap.getPredicatesWithGap();
+        gap.clear();
+
+        if(program.getGeneral().isHorn())
+            encoder = new TrackingRuleEncoderWithGap(program.getUpper(), trackingStore);
+        else
+            encoder = new TrackingRuleEncoderDisjVar1(program.getUpper(), trackingStore);
+//                      encoder = new TrackingRuleEncoderDisj1(program.getUpper(), trackingStore);
+//                      encoder = new TrackingRuleEncoderDisjVar2(program.getUpper(), trackingStore);
+//                      encoder = new TrackingRuleEncoderDisj2(program.getUpper(), trackingStore);
+
+        // TODO? add consistency check by Skolem-upper-bound
+
+        if(!isConsistent())
+            return false;
+
+        consistency.extractBottomFragment();
+
+        return true;
+    }
+
+    @Override
+    public boolean isConsistent() {
+        if(isDisposed()) throw new DisposedException();
+
+        if(isConsistent == ConsistencyStatus.UNCHECKED) {
+            isConsistent = consistency.check() ? ConsistencyStatus.CONSISTENT : ConsistencyStatus.INCONSISTENT;
+            Utility.logDebug("time for satisfiability checking: " + t.duration());
+        }
+        if(isConsistent == ConsistencyStatus.CONSISTENT) {
+            Utility.logInfo("The ontology is consistent!");
+            return true;
+        }
+        else {
+            Utility.logInfo("The ontology is inconsistent!");
+            return false;
+        }
+    }
+
+    @Override
+    public void evaluate(QueryRecord queryRecord) {
+        if(isDisposed()) throw new DisposedException();
+
+        if(queryLowerAndUpperBounds(queryRecord))
+            return;
+
+        OWLOntology relevantOntologySubset = extractRelevantOntologySubset(queryRecord);
+
+//        queryRecord.saveRelevantOntology("/home/alessandro/Desktop/test-relevant-ontology-"+relevantOntologiesCounter+".owl");
+//        relevantOntologiesCounter++;
+
+        if(properties.getSkolemUpperBound() == PagodaProperties.SkolemUpperBoundOptions.BEFORE_SUMMARISATION
+                && querySkolemisedRelevantSubset(relevantOntologySubset, queryRecord)) {
+            return;
+        }
+
+        Utility.logInfo(">> Summarisation <<");
+        HermitSummaryFilter summarisedChecker = new HermitSummaryFilter(queryRecord, properties.getToCallHermiT());
+        if(summarisedChecker.check(queryRecord.getGapAnswers()) == 0) {
+            summarisedChecker.dispose();
+            return;
+        }
+
+        if(properties.getSkolemUpperBound() == PagodaProperties.SkolemUpperBoundOptions.AFTER_SUMMARISATION
+                && 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());
+
+        if(properties.getToCallHermiT())
+            queryRecord.markAsProcessed();
+        summarisedChecker.dispose();
+    }
+
+    @Override
+    public void evaluateUpper(QueryRecord queryRecord) {
+        if(isDisposed()) throw new DisposedException();
+        // TODO? add new upper store
+        AnswerTuples rlAnswer = null;
+        boolean useFull = queryRecord.isBottom() || lazyUpperStore == null;
+        try {
+            rlAnswer =
+                    (useFull ? trackingStore : lazyUpperStore).evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+            queryRecord.updateUpperBoundAnswers(rlAnswer, true);
+        } finally {
+            if(rlAnswer != null) rlAnswer.dispose();
+        }
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+
+        if(encoder != null) encoder.dispose();
+        if(rlLowerStore != null) rlLowerStore.dispose();
+        if(lazyUpperStore != null) lazyUpperStore.dispose();
+        if(elLowerStore != null) elLowerStore.dispose();
+        if(trackingStore != null) trackingStore.dispose();
+        if(consistency != null) consistency.dispose();
+        if(program != null) program.dispose();
+    }
+
+    private void setup(boolean considerEqualities) {
+        if(isDisposed()) throw new DisposedException();
+
+        isConsistent = ConsistencyStatus.UNCHECKED;
+        this.equalityTag = considerEqualities;
+
+        rlLowerStore = new BasicQueryEngine("rl-lower-bound");
+        elLowerStore = new KarmaQueryEngine("elho-lower-bound");
+
+        trackingStore = new MultiStageQueryEngine("tracking", false);
+    }
+
+    protected void internal_importDataFile(String name, String datafile) {
+//              addDataFile(datafile);
+        rlLowerStore.importRDFData(name, datafile);
+        if(lazyUpperStore != null)
+            lazyUpperStore.importRDFData(name, datafile);
+        elLowerStore.importRDFData(name, datafile);
+        trackingStore.importRDFData(name, datafile);
+    }
+
+    /**
+     * It deals with blanks nodes differently from variables
+     * according to SPARQL semantics for OWL2 Entailment Regime.
+     * <p>
+     * In particular variables are matched only against named individuals,
+     * and blank nodes against named and anonymous individuals.
+     */
+    private boolean queryUpperStore(BasicQueryEngine upperStore, QueryRecord queryRecord,
+                                    Tuple<String> extendedQuery, Step step) {
+        t.reset();
+
+        Utility.logDebug("First query type");
+        queryUpperBound(upperStore, queryRecord, queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+        if(!queryRecord.isProcessed() && !queryRecord.getQueryText().equals(extendedQuery.get(0))) {
+            Utility.logDebug("Second query type");
+            queryUpperBound(upperStore, queryRecord, extendedQuery.get(0), queryRecord.getAnswerVariables());
+        }
+        if(!queryRecord.isProcessed() && queryRecord.hasNonAnsDistinguishedVariables()) {
+            Utility.logDebug("Third query type");
+            queryUpperBound(upperStore, queryRecord, extendedQuery.get(1), queryRecord.getDistinguishedVariables());
+        }
+
+        queryRecord.addProcessingTime(step, t.duration());
+        if(queryRecord.isProcessed()) {
+            queryRecord.setDifficulty(step);
+            return true;
+        }
+        return false;
+    }
+
+    /**
+     * Returns the part of the ontology relevant for Hermit, while computing the bound answers.
+     */
+    private boolean queryLowerAndUpperBounds(QueryRecord queryRecord) {
+
+        Utility.logInfo(">> Base bounds <<");
+
+        AnswerTuples rlAnswer = null, elAnswer = null;
+
+        t.reset();
+        try {
+            rlAnswer = rlLowerStore.evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+            Utility.logDebug(t.duration());
+            queryRecord.updateLowerBoundAnswers(rlAnswer);
+        } finally {
+            if(rlAnswer != null) rlAnswer.dispose();
+        }
+        queryRecord.addProcessingTime(Step.LOWER_BOUND, t.duration());
+
+        Tuple<String> extendedQueryTexts = queryRecord.getExtendedQueryText();
+
+        if(properties.getUseAlwaysSimpleUpperBound() || lazyUpperStore == null) {
+            Utility.logDebug("Tracking store");
+            if(queryUpperStore(trackingStore, queryRecord, extendedQueryTexts, Step.SIMPLE_UPPER_BOUND))
+                return true;
+        }
+
+        if(!queryRecord.isBottom()) {
+            Utility.logDebug("Lazy store");
+            if(lazyUpperStore != null && queryUpperStore(lazyUpperStore, queryRecord, extendedQueryTexts, Step.LAZY_UPPER_BOUND))
+                return true;
+        }
+
+        t.reset();
+        try {
+            elAnswer = elLowerStore.evaluate(extendedQueryTexts.get(0),
+                                             queryRecord.getAnswerVariables(),
+                                             queryRecord.getLowerBoundAnswers());
+            Utility.logDebug(t.duration());
+            queryRecord.updateLowerBoundAnswers(elAnswer);
+        } finally {
+            if(elAnswer != null) elAnswer.dispose();
+        }
+        queryRecord.addProcessingTime(Step.EL_LOWER_BOUND, t.duration());
+
+        if(queryRecord.isProcessed()) {
+            queryRecord.setDifficulty(Step.EL_LOWER_BOUND);
+            return true;
+        }
+
+        return false;
+    }
+
+    private OWLOntology extractRelevantOntologySubset(QueryRecord queryRecord) {
+        Utility.logInfo(">> Relevant ontology-subset extraction <<");
+
+        t.reset();
+
+        QueryTracker tracker = new QueryTracker(encoder, rlLowerStore, queryRecord);
+        OWLOntology relevantOntologySubset = tracker.extract(trackingStore, consistency.getQueryRecords(), true);
+
+        queryRecord.addProcessingTime(Step.FRAGMENT, t.duration());
+
+        int numOfABoxAxioms = relevantOntologySubset.getABoxAxioms(Imports.INCLUDED).size();
+        int numOfTBoxAxioms = relevantOntologySubset.getAxiomCount() - numOfABoxAxioms;
+        Utility.logInfo("Relevant ontology-subset has been extracted: |ABox|="
+                                + numOfABoxAxioms + ", |TBox|=" + numOfTBoxAxioms);
+
+        return relevantOntologySubset;
+    }
+
+    private void queryUpperBound(BasicQueryEngine upperStore, QueryRecord queryRecord, String queryText, String[] answerVariables) {
+        AnswerTuples rlAnswer = null;
+        try {
+            Utility.logDebug(queryText);
+            rlAnswer = upperStore.evaluate(queryText, answerVariables);
+            Utility.logDebug(t.duration());
+            queryRecord.updateUpperBoundAnswers(rlAnswer);
+        } finally {
+            if(rlAnswer != null) rlAnswer.dispose();
+        }
+    }
+
+    private boolean querySkolemisedRelevantSubset(OWLOntology relevantSubset, QueryRecord queryRecord) {
+        Utility.logInfo(">> Semi-Skolemisation <<");
+        t.reset();
+
+        DatalogProgram relevantProgram = new DatalogProgram(relevantSubset);
+
+        MultiStageQueryEngine relevantStore =
+                new MultiStageQueryEngine("Relevant-store", true); // checkValidity is true
+
+        relevantStore.importDataFromABoxOf(relevantSubset);
+        String relevantOriginalMarkProgram = OWLHelper.getOriginalMarkProgram(relevantSubset);
+
+        relevantStore.materialise("Mark original individuals", relevantOriginalMarkProgram);
+
+        boolean isFullyProcessed = false;
+        LinkedList<Tuple<Long>> lastTwoTriplesCounts = new LinkedList<>();
+        for (int currentMaxTermDepth = 1; !isFullyProcessed; currentMaxTermDepth++) {
+
+            if(currentMaxTermDepth > properties.getSkolemDepth()) {
+                Utility.logInfo("Maximum term depth reached");
+                break;
+            }
+
+            if(lastTwoTriplesCounts.size() == 2) {
+                if(lastTwoTriplesCounts.get(0).get(1).equals(lastTwoTriplesCounts.get(1).get(1)))
+                    break;
+
+                ExponentialInterpolation interpolation = new ExponentialInterpolation(lastTwoTriplesCounts.get(0).get(0),
+                        lastTwoTriplesCounts.get(0).get(1),
+                        lastTwoTriplesCounts.get(1).get(0),
+                        lastTwoTriplesCounts.get(1).get(1));
+                double triplesEstimate = interpolation.computeValue(currentMaxTermDepth);
+
+                Utility.logDebug("Estimate of the number of triples:" + triplesEstimate);
+
+                // exit condition if the query is not fully answered
+                if(triplesEstimate > properties.getMaxTriplesInSkolemStore()) {
+                    Utility.logInfo("Interrupting Semi-Skolemisation because of triples count limit");
+                    break;
+                }
+            }
+
+            Utility.logInfo("Trying with maximum depth " + currentMaxTermDepth);
+
+            int materialisationTag = relevantStore.materialiseSkolemly(relevantProgram, null,
+                    currentMaxTermDepth);
+            queryRecord.addProcessingTime(Step.SKOLEM_UPPER_BOUND, t.duration());
+            if(materialisationTag == -1) {
+                relevantStore.dispose();
+                throw new Error("A consistent ontology has turned out to be " +
+                                        "inconsistent in the Skolemises-relevant-upper-store");
+            }
+            else if(materialisationTag != 1) {
+                Utility.logInfo("Semi-Skolemised relevant upper store cannot be employed");
+                break;
+            }
+
+            Utility.logInfo("Querying semi-Skolemised upper store...");
+            isFullyProcessed = queryUpperStore(relevantStore, queryRecord,
+                    queryRecord.getExtendedQueryText(),
+                    Step.SKOLEM_UPPER_BOUND);
+
+            try {
+                lastTwoTriplesCounts.add
+                        (new Tuple<>((long) currentMaxTermDepth, relevantStore.getStoreSize()));
+            } catch (JRDFStoreException e) {
+                e.printStackTrace();
+                break;
+            }
+            if(lastTwoTriplesCounts.size() > 2)
+                lastTwoTriplesCounts.remove();
+
+            Utility.logDebug("Last two triples counts:" + lastTwoTriplesCounts);
+        }
+
+        relevantStore.dispose();
+        Utility.logInfo("Semi-Skolemised relevant upper store has been evaluated");
+        return isFullyProcessed;
+    }
+
+    private enum ConsistencyStatus {CONSISTENT, INCONSISTENT, UNCHECKED}
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/QueryEngine.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/QueryEngine.java
new file mode 100644
index 0000000..3200216
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/QueryEngine.java
@@ -0,0 +1,15 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.util.disposable.Disposable;
+
+import java.util.Collection;
+
+public abstract class QueryEngine extends Disposable {
+
+        public abstract void evaluate(Collection<String> queryTexts, String answerFile);
+
+        public abstract AnswerTuples evaluate(String queryText);
+
+        public abstract AnswerTuples evaluate(String queryText, String[] answerVariables);
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java
new file mode 100644
index 0000000..e8daa3b
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/QueryReasoner.java
@@ -0,0 +1,266 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import com.google.gson.Gson;
+import org.semanticweb.owlapi.model.OWLOntology;
+import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.QueryManager;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
+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 uk.ac.ox.cs.pagoda.util.disposable.Disposable;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
+
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Paths;
+import java.util.Collection;
+
+// TODO clean APIs
+public abstract class QueryReasoner extends Disposable {
+
+    public static final String ImportDataFileSeparator = ";";
+    private static final boolean DEFAULT_MULTI_STAGES = true;
+    private static final boolean DEFAULT_EQUALITIES = true;
+    public boolean fullReasoner = this instanceof MyQueryReasoner;
+    //  protected boolean forSemFacet = false;
+    PagodaProperties properties;
+    BufferedWriter answerWriter = null;
+    private StringBuilder importedData = new StringBuilder();
+    private QueryManager m_queryManager = new QueryManager();
+
+    public static QueryReasoner getInstance(PagodaProperties p) {
+        OWLOntology ontology = OWLHelper.loadOntology(p.getOntologyPath());
+        QueryReasoner pagoda = getInstance(ontology, p);
+        pagoda.properties = p;
+        pagoda.loadOntology(ontology);
+        pagoda.importData(p.getDataPath());
+        if(pagoda.preprocess()) {
+            Utility.logInfo("The ontology is consistent!");
+            return pagoda;
+        }
+        else {
+            System.out.println("The ontology is inconsistent!");
+            pagoda.dispose();
+            return null;
+        }
+    }
+
+    public static QueryReasoner getInstance(OWLOntology o) {
+        QueryReasoner pagoda = getInstance(Type.Full, o, DEFAULT_MULTI_STAGES, DEFAULT_EQUALITIES);
+        pagoda.properties = new PagodaProperties();
+        return pagoda;
+    }
+
+    private static QueryReasoner getInstance(OWLOntology o, PagodaProperties p) {
+        return getInstance(Type.Full, o, DEFAULT_MULTI_STAGES, DEFAULT_EQUALITIES);
+    }
+
+    public static QueryReasoner getInstance(Type type, OWLOntology o, boolean performMultiStages, boolean considerEqualities) {
+//              Utility.initialise();
+        QueryReasoner reasoner;
+        if(OWLHelper.isInOWL2RL(o)) reasoner = new RLQueryReasoner();
+        else if(OWLHelper.isInELHO(o)) reasoner = new ELHOQueryReasoner();
+        else
+            switch(type) {
+                case RLU:
+                    reasoner = new RLUQueryReasoner(performMultiStages, considerEqualities);
+                    break;
+                case ELHOU:
+                    reasoner = new ELHOUQueryReasoner(performMultiStages, considerEqualities);
+                    break;
+                default:
+                    reasoner = new MyQueryReasoner(performMultiStages, considerEqualities);
+            }
+        return reasoner;
+    }
+
+    public static QueryReasoner getHermiTReasoner(boolean toCheckSatisfiability) {
+        return new HermiTReasoner(toCheckSatisfiability);
+    }
+
+    public void setToClassify(boolean flag) {
+        if(isDisposed()) throw new DisposedException();
+        properties.setToClassify(flag);
+    }
+
+    public void setToCallHermiT(boolean flag) {
+        if(isDisposed()) throw new DisposedException();
+        properties.setToCallHermiT(flag);
+    }
+
+    public void importData(String datafile) {
+        if(isDisposed()) throw new DisposedException();
+        if(datafile != null && !datafile.equalsIgnoreCase("null"))
+            importData(datafile.split(ImportDataFileSeparator));
+    }
+
+    public void importData(String[] datafiles) {
+        if(isDisposed()) throw new DisposedException();
+        if(datafiles != null) {
+            for(String datafile : datafiles) {
+                File file = new File(datafile);
+                if(file.exists()) {
+                    if(file.isFile()) importDataFile(file);
+                    else importDataDirectory(file);
+                }
+                else {
+                    Utility.logError("warning: file " + datafile + " doesn't exists.");
+                }
+            }
+        }
+    }
+
+    public abstract void loadOntology(OWLOntology ontology);
+
+    public abstract boolean preprocess();
+
+    public abstract boolean isConsistent();
+
+    public abstract void evaluate(QueryRecord record);
+
+    public abstract void evaluateUpper(QueryRecord record);
+
+    public AnswerTuples evaluate(String queryText, boolean forFacetGeneration) {
+        if(isDisposed()) throw new DisposedException();
+        if(forFacetGeneration) {
+            QueryRecord record = m_queryManager.create(queryText);
+            Utility.logInfo("---------- start evaluating upper bound for Query " + record.getQueryID() + " ----------", queryText);
+            if(!record.isProcessed())
+                evaluateUpper(record);
+//                      AnswerTuples tuples = record.getUpperBoundAnswers();
+//                      for (AnswerTuple tuple; tuples.isValid(); tuples.moveNext()) {
+//                              tuple = tuples.getTuple();
+//                              if (tuple.toString().contains("NC"))
+//                                      System.out.println(tuple.toString());
+//                      }
+            return record.getUpperBoundAnswers();
+        }
+        else
+            return evaluate(queryText);
+    }
+
+    public AnswerTuples evaluate(String queryText) {
+        if(isDisposed()) throw new DisposedException();
+        QueryRecord record = m_queryManager.create(queryText);
+        Utility.logInfo("---------- start evaluating Query " + record.getQueryID() + " ----------", queryText);
+        if(!record.isProcessed())
+            evaluate(record);
+        AnswerTuples answer = record.getAnswers();
+        record.dispose();
+        return answer;
+
+    }
+
+    public void evaluate_shell(String queryText) {
+        if(isDisposed()) throw new DisposedException();
+        QueryRecord record = m_queryManager.create(queryText);
+        Utility.logInfo("---------- start evaluating Query " + record.getQueryID() + " ----------", queryText);
+        if(!record.isProcessed())
+            evaluate(record);
+        Utility.logInfo("Answers to this query: ", record.outputSoundAnswerTuple());
+        record.dispose();
+
+    }
+
+    public void evaluate(Collection<QueryRecord> queryRecords) {
+        if(isDisposed()) throw new DisposedException();
+        if(!isConsistent()) {
+            Utility.logDebug("The ontology and dataset is inconsistent.");
+            return;
+        }
+
+        if(properties.getAnswerPath() != null && answerWriter == null) {
+            try {
+                answerWriter = Files.newBufferedWriter(Paths.get(properties.getAnswerPath()));
+            } catch(IOException e) {
+                Utility.logError("The answer path is not valid!");
+                e.printStackTrace();
+            }
+        }
+
+        Timer t = new Timer();
+        Gson gson = QueryRecord.GsonCreator.getInstance();
+        for(QueryRecord record : queryRecords) {
+//                      if (Integer.parseInt(record.getQueryID()) != 218) continue;
+            Utility.logInfo("---------- start evaluating Query " + record.getQueryID() + " ----------",
+                            record.getQueryText());
+            if(!record.isProcessed()) {
+                t.reset();
+                if(!record.isProcessed())
+                    evaluate(record);
+                Utility.logInfo("Total time to answer this query: " + t.duration());
+                Utility.logInfo("Difficulty of this query: " + record.getDifficulty());
+                if(!fullReasoner && !record.isProcessed()) {
+                    Utility.logInfo("The query has not been fully answered in " + t.duration() + " seconds.");
+                    continue;
+                }
+            }
+            record.outputAnswerStatistics();
+            record.outputTimes();
+        }
+        /* TODO it can handle one call only
+                   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(QueryRecord::dispose);
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+        if(answerWriter != null) {
+            try {
+                answerWriter.close();
+            } catch(IOException e) {
+                e.printStackTrace();
+            }
+        }
+//              Utility.cleanup();
+    }
+
+//      public void evaluate(Collection<QueryRecord> queryRecords) {
+//              evaluate(queryRecords);
+//      }
+
+    public QueryManager getQueryManager() {
+        if(isDisposed()) throw new DisposedException();
+        return m_queryManager;
+    }
+
+    protected String getImportedData() {
+        return importedData.toString();
+    }
+
+    private void importDataDirectory(File file) {
+        for(File child : file.listFiles())
+            if(child.isFile()) importDataFile(child);
+            else importDataDirectory(child);
+    }
+
+    private void importDataFile(File file) {
+        String datafile;
+        try {
+            datafile = file.getCanonicalPath();
+        } catch(IOException e) {
+            e.printStackTrace();
+            return;
+        }
+        importDataFile(datafile);
+    }
+
+    protected final void importDataFile(String datafile) {
+        if(importedData.length() == 0)
+            importedData.append(datafile);
+        else
+            importedData.append(ImportDataFileSeparator).append(datafile);
+
+    }
+
+
+    public enum Type {Full, RLU, ELHOU}
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java
new file mode 100644
index 0000000..32f5541
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/RLQueryReasoner.java
@@ -0,0 +1,86 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import org.semanticweb.owlapi.model.OWLOntology;
+import uk.ac.ox.cs.pagoda.constraints.UnaryBottom;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
+import uk.ac.ox.cs.pagoda.query.QueryRecord.Step;
+import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
+import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxQueryEngine;
+import uk.ac.ox.cs.pagoda.rules.LowerDatalogProgram;
+import uk.ac.ox.cs.pagoda.util.Timer;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
+
+public class RLQueryReasoner extends QueryReasoner {
+        
+        RDFoxQueryEngine rlLowerStore = null;
+
+        LowerDatalogProgram program;
+        Timer t = new Timer();
+
+        public RLQueryReasoner() {
+                rlLowerStore = new BasicQueryEngine("rl");
+        }
+        
+        @Override
+        public void evaluate(QueryRecord queryRecord) {
+                if(isDisposed()) throw new DisposedException();
+                AnswerTuples rlAnswer = null; 
+                t.reset();
+                try {
+                        rlAnswer = rlLowerStore.evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+                        queryRecord.updateLowerBoundAnswers(rlAnswer);
+                } finally {
+                        if (rlAnswer != null) rlAnswer.dispose();
+                }
+                queryRecord.addProcessingTime(Step.LOWER_BOUND, t.duration());
+                queryRecord.setDifficulty(Step.LOWER_BOUND);
+                queryRecord.markAsProcessed();
+        }
+
+        @Override
+        public void dispose() {
+                super.dispose();
+                if(rlLowerStore != null) rlLowerStore.dispose();
+        }
+
+        @Override
+        public void loadOntology(OWLOntology ontology) {
+                if(isDisposed()) throw new DisposedException();
+                program = new LowerDatalogProgram(); 
+                program.load(ontology, new UnaryBottom());
+                program.transform();
+                
+                importData(program.getAdditionalDataFile());
+        }
+
+        @Override
+        public boolean preprocess() {
+                if(isDisposed()) throw new DisposedException();
+                rlLowerStore.importRDFData("data", getImportedData());
+                rlLowerStore.materialise("lower program", program.toString());
+
+                return isConsistent();
+        }
+
+        @Override
+        public boolean isConsistent() {
+                if(isDisposed()) throw new DisposedException();
+                AnswerTuples ans = null; 
+                try {
+                        ans = rlLowerStore.evaluate(QueryRecord.botQueryText, new String[] {"X"});
+                        return !ans.isValid(); 
+                } finally {
+                        if (ans != null) ans.dispose();
+                                
+                }
+                
+        }
+
+        @Override
+        public void evaluateUpper(QueryRecord record) {
+                if(isDisposed()) throw new DisposedException();
+                evaluate(record); 
+        }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java
new file mode 100644
index 0000000..368fbb2
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/RLUQueryReasoner.java
@@ -0,0 +1,135 @@
+package uk.ac.ox.cs.pagoda.reasoner;
+
+import org.semanticweb.owlapi.model.OWLOntology;
+import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine;
+import uk.ac.ox.cs.pagoda.owl.EqualitiesEliminator;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.QueryRecord;
+import uk.ac.ox.cs.pagoda.query.QueryRecord.Step;
+import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
+import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
+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;
+
+class RLUQueryReasoner extends QueryReasoner {
+
+        DatalogProgram program; 
+        
+        BasicQueryEngine rlLowerStore, rlUpperStore;
+        
+        boolean multiStageTag, equalityTag;
+        Timer t = new Timer();
+
+        public RLUQueryReasoner(boolean multiStageTag, boolean considerEqualities) {
+                this.multiStageTag = multiStageTag;
+                this.equalityTag = considerEqualities;
+                rlLowerStore = new BasicQueryEngine("rl-lower-bound");
+                if(!multiStageTag)
+                        rlUpperStore = new BasicQueryEngine("rl-upper-bound");
+                else
+                        rlUpperStore = new MultiStageQueryEngine("rl-upper-bound", false);
+        }
+        
+        @Override
+        public void evaluate(QueryRecord queryRecord) {
+                if(isDisposed()) throw new DisposedException();
+                AnswerTuples ans = null;
+                t.reset(); 
+                try {
+                        ans = rlLowerStore.evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+                        Utility.logDebug(t.duration());
+                        queryRecord.updateLowerBoundAnswers(ans); 
+                } finally {
+                        if (ans != null) ans.dispose();
+                }
+                queryRecord.addProcessingTime(Step.LOWER_BOUND, t.duration());
+                
+                ans = null; 
+                t.reset(); 
+                try {
+                        ans = rlUpperStore.evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+                        Utility.logDebug(t.duration());
+                        queryRecord.updateUpperBoundAnswers(ans); 
+                } finally {
+                        if (ans != null) ans.dispose();
+                }
+                queryRecord.addProcessingTime(Step.UPPER_BOUND, t.duration());
+
+                if(queryRecord.isProcessed())
+                        queryRecord.setDifficulty(Step.UPPER_BOUND);
+        }
+        
+        @Override
+        public void evaluateUpper(QueryRecord queryRecord) {
+                if(isDisposed()) throw new DisposedException();
+                AnswerTuples ans = null; 
+                try {
+                        ans = rlUpperStore.evaluate(queryRecord.getQueryText(), queryRecord.getAnswerVariables());
+                        Utility.logDebug(t.duration());
+                        queryRecord.updateUpperBoundAnswers(ans, true); 
+                } finally {
+                        if (ans != null) ans.dispose();
+                }
+        }
+
+        @Override
+        public void dispose() {
+                super.dispose();
+                if (rlLowerStore != null) rlLowerStore.dispose();
+                if (rlUpperStore != null) rlUpperStore.dispose();
+        }
+
+        @Override
+        public void loadOntology(OWLOntology o) {
+                if(isDisposed()) throw new DisposedException();
+                if (!equalityTag) {
+                        EqualitiesEliminator eliminator = new EqualitiesEliminator(o);
+                        o = eliminator.getOutputOntology();
+                        eliminator.save();
+                }                       
+
+                OWLOntology ontology = o; 
+                program = new DatalogProgram(ontology);
+                importData(program.getAdditionalDataFile());
+        }
+
+        @Override
+        public boolean preprocess() {
+                if(isDisposed()) throw new DisposedException();
+                String datafile = getImportedData();
+                rlLowerStore.importRDFData("data", datafile);
+                rlLowerStore.materialise("lower program", program.getLower().toString());
+                
+                rlUpperStore.importRDFData("data", datafile);
+                rlUpperStore.materialiseRestrictedly(program, null);
+
+                return isConsistent();
+
+        }
+
+        @Override
+        public boolean isConsistent() {
+                if(isDisposed()) throw new DisposedException();
+                String[] X = new String[] { "X" }; 
+                AnswerTuples ans = null; 
+                try {
+                        ans = rlLowerStore.evaluate(QueryRecord.botQueryText, X);
+                        if (ans.isValid()) return false; 
+                } finally {
+                        if (ans != null) ans.dispose();
+                }
+
+                ans = null; 
+                try {
+                        ans = rlUpperStore.evaluate(QueryRecord.botQueryText, X);
+                        if (!ans.isValid()) return true; 
+                } finally { 
+                        if (ans != null) ans.dispose();
+                }
+                
+                Utility.logDebug("The consistency of the data has not been determined yet.");
+                return true; 
+        }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java
new file mode 100644
index 0000000..07adc6d
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/full/Checker.java
@@ -0,0 +1,17 @@
+package uk.ac.ox.cs.pagoda.reasoner.full;
+
+import uk.ac.ox.cs.pagoda.query.AnswerTuple;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.util.disposable.Disposable;
+
+public abstract class Checker extends Disposable {
+
+        public abstract int check(AnswerTuples answers);
+
+        public abstract boolean check(AnswerTuple answer);
+
+        public abstract boolean isConsistent();
+
+        public abstract int getNoOfCalls();
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
new file mode 100644
index 0000000..3f3c22d
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/full/HermitChecker.java
@@ -0,0 +1,282 @@
+package uk.ac.ox.cs.pagoda.reasoner.full;
+
+import org.semanticweb.HermiT.Reasoner;
+import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.HermiT.model.Term;
+import org.semanticweb.HermiT.model.Variable;
+import org.semanticweb.owlapi.model.*;
+import org.semanticweb.owlapi.model.parameters.Imports;
+import uk.ac.ox.cs.pagoda.endomorph.Clique;
+import uk.ac.ox.cs.pagoda.endomorph.DependencyGraph;
+import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
+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.query.rollup.QueryGraph;
+import uk.ac.ox.cs.pagoda.util.ConjunctiveQueryHelper;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+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;
+
+import java.util.HashMap;
+import java.util.HashSet;
+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;
+
+    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);
+    }
+
+    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.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;
+        ++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(sub);
+
+        // TODO possibly inefficient
+        for(OWLAxiom subclassAxiom : toCheckExistentialAxioms) {
+            Utility.logDebug("Checking consistency of ontology union " + subclassAxiom);
+            ontology.getOWLOntologyManager().addAxiom(ontology, subclassAxiom);
+            hermit.flush();
+            if(hermit.isConsistent()) {
+                ontology.getOWLOntologyManager().removeAxiom(ontology, subclassAxiom);
+                hermit.flush();
+                Utility.logDebug("@TIME to check one tuple: " + t.duration());
+                return false;
+            }
+            ontology.getOWLOntologyManager().removeAxiom(ontology, subclassAxiom);
+            hermit.flush();
+        }
+
+
+//              for (OWLAxiom axiom: toCheckAxioms)     System.out.println(axiom.toString());
+
+//              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(Imports.INCLUDED))
+            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/main/java/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java
new file mode 100644
index 0000000..034827e
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/BasicQueryEngine.java
@@ -0,0 +1,422 @@
+package uk.ac.ox.cs.pagoda.reasoner.light;
+
+import org.semanticweb.HermiT.model.DLClause;
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.store.DataStore;
+import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType;
+import uk.ac.ox.cs.JRDFox.store.Parameters;
+import uk.ac.ox.cs.JRDFox.store.TripleStatus;
+import uk.ac.ox.cs.JRDFox.store.TupleIterator;
+import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
+import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
+import uk.ac.ox.cs.pagoda.rules.Program;
+import uk.ac.ox.cs.pagoda.util.*;
+import uk.ac.ox.cs.pagoda.util.Timer;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
+
+import java.util.*;
+
+public class BasicQueryEngine extends RDFoxQueryEngine {
+
+    protected DataStore store;
+    protected Parameters parameters = new Parameters();
+    Set<DLClause> materialisedRules = new HashSet<DLClause>();
+    private UFS<String> equalityGroups = null;
+
+    public BasicQueryEngine(String name) {
+        super(name);
+        store = RDFoxQueryEngine.createDataStore();
+        parameters.m_allAnswersInRoot = true;
+        parameters.m_useBushy = true;
+    }
+
+    /***
+     * @return Overall number of triples.
+     */
+    public long getStoreSize() throws JRDFStoreException {
+        return store.getTriplesCount();
+    }
+
+    public void materialiseFoldedly(DatalogProgram dProgram, GapByStore4ID gap) {
+        if(isDisposed()) throw new DisposedException();
+        if(gap != null) {
+            materialise("lower program", dProgram.getLower().toString());
+            String program = dProgram.getUpper().toString();
+            try {
+                gap.compile(program);
+                gap.addBackTo();
+                getDataStore().clearRulesAndMakeFactsExplicit();
+            } catch(JRDFStoreException e) {
+                e.printStackTrace();
+            } finally {
+                gap.clear();
+            }
+        }
+        else
+            materialise("upper program", dProgram.getUpper().toString());
+    }
+
+    public int materialiseRestrictedly(DatalogProgram dProgram, GapByStore4ID gap) {
+        if(isDisposed()) throw new DisposedException();
+        if(gap != null) {
+            materialise("lower program", dProgram.getLower().toString());
+            String program = dProgram.getUpper().toString();
+            try {
+                gap.compile(program);
+                gap.addBackTo();
+                getDataStore().clearRulesAndMakeFactsExplicit();
+            } catch(JRDFStoreException e) {
+                e.printStackTrace();
+            } finally {
+                gap.clear();
+            }
+        }
+        else
+            materialise("upper program", dProgram.getUpper().toString());
+
+        return 1;
+    }
+
+    @Override
+    public AnswerTuples evaluate(String queryText) {
+        if(isDisposed()) throw new DisposedException();
+        return evaluate(queryText, ConjunctiveQueryHelper.getAnswerVariables(queryText)[0]);
+    }
+
+    @Override
+    public AnswerTuples evaluate(String queryText, String[] answerVars) {
+        if(isDisposed()) throw new DisposedException();
+        TupleIterator tupleIterator;
+        try {
+            tupleIterator = store.compileQuery(queryText.replace("_:", "?"), prefixes, parameters);
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+            return null;
+        }
+        return new RDFoxAnswerTuples(answerVars, tupleIterator);
+    }
+
+    @Override
+    public DataStore getDataStore() {
+        if(isDisposed()) throw new DisposedException();
+        return store;
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+        store.dispose();
+    }
+
+    public void outputInstance4BinaryPredicate(String iri, String filename) {
+        if(isDisposed()) throw new DisposedException();
+
+        Utility.redirectCurrentOut(filename);
+        outputInstance4BinaryPredicate(iri);
+        Utility.closeCurrentOut();
+    }
+
+    public void outputInstance4BinaryPredicate(String iri) {
+        if(isDisposed()) throw new DisposedException();
+
+        outputAnswers("select ?x ?y where { ?x <" + iri + "> ?y . }");
+    }
+
+    public void outputInstanceNumbers(String filename) {
+        if(isDisposed()) throw new DisposedException();
+
+        TupleIterator predicateTuples = null;
+        TupleIterator instanceTuples;
+        Set<String> number = new HashSet<String>();
+        String predicate;
+        try {
+            predicateTuples =
+                    getDataStore().compileQuery("SELECT DISTINCT ?Y WHERE { ?X <" + Namespace.RDF_TYPE + "> ?Y }", prefixes, parameters);
+            for(long multi = predicateTuples.open(); multi != 0; multi = predicateTuples.getNext()) {
+                predicate = RDFoxTripleManager.getQuotedTerm(predicateTuples.getResource(0));
+                instanceTuples = null;
+                try {
+                    instanceTuples =
+                            getDataStore().compileQuery("SELECT ?X WHERE { ?X <" + Namespace.RDF_TYPE + "> " + predicate + " }", prefixes, parameters);
+                    long totalCount = 0;
+                    for(long multi1 = instanceTuples.open(); multi1 != 0; multi1 = instanceTuples.getNext()) {
+                        totalCount += instanceTuples.getMultiplicity();
+                    }
+                    number.add(predicate + " * " + totalCount);
+                } finally {
+                    if(instanceTuples != null) instanceTuples.dispose();
+                }
+            }
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        } finally {
+            if(predicateTuples != null) predicateTuples.dispose();
+            predicateTuples = null;
+        }
+
+        try {
+            predicateTuples =
+                    getDataStore().compileQuery("SELECT DISTINCT ?Y WHERE { ?X ?Y ?Z }", prefixes, parameters);
+            for(long multi = predicateTuples.open(); multi != 0; multi = predicateTuples.getNext()) {
+                predicate = RDFoxTripleManager.getQuotedTerm(predicateTuples.getResource(0));
+                instanceTuples = null;
+                try {
+                    instanceTuples =
+                            getDataStore().compileQuery("SELECT ?X ?Z WHERE { ?X " + predicate + " ?Z }", prefixes, parameters);
+                    long totalCount = 0;
+                    for(long multi1 = instanceTuples.open(); multi1 != 0; multi1 = instanceTuples.getNext())
+                        totalCount += instanceTuples.getMultiplicity();
+                    number.add(predicate + " * " + totalCount);
+                } finally {
+                    if(instanceTuples != null) instanceTuples.dispose();
+                }
+            }
+
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        } finally {
+            if(predicateTuples != null) predicateTuples.dispose();
+            predicateTuples = null;
+        }
+
+        Utility.redirectCurrentOut(filename);
+        String[] ordered = number.toArray(new String[0]);
+        Arrays.sort(ordered, new DLPredicateComparator());
+        for(String line : ordered) System.out.println(line);
+        Utility.closeCurrentOut();
+
+    }
+
+    public TupleIterator internal_evaluateAgainstIDBs(String queryText) throws JRDFStoreException {
+        if(isDisposed()) throw new DisposedException();
+
+        TupleIterator iter =
+                store.compileQuery(queryText, prefixes, parameters, TripleStatus.TUPLE_STATUS_IDB.union(TripleStatus.TUPLE_STATUS_EDB), TripleStatus.TUPLE_STATUS_IDB);
+//              iter.open();
+        return iter;
+    }
+
+    public TupleIterator internal_evaluate(String queryText) throws JRDFStoreException {
+        if(isDisposed()) throw new DisposedException();
+
+        TupleIterator iter = store.compileQuery(queryText, prefixes, parameters);
+//              iter.open();
+        return iter;
+    }
+
+    public void setExpandEquality(boolean flag) {
+        if(isDisposed()) throw new DisposedException();
+
+        parameters.m_expandEquality = flag;
+    }
+
+    public TupleIterator internal_evaluateNotExpanded(String queryText) throws JRDFStoreException {
+        if(isDisposed()) throw new DisposedException();
+
+        parameters.m_expandEquality = false;
+        TupleIterator iter = store.compileQuery(queryText, prefixes, parameters);
+//              iter.open();
+        parameters.m_expandEquality = true;
+        return iter;
+    }
+
+    public TupleIterator internal_evaluate(String queryText, boolean incrementally) throws JRDFStoreException {
+        if(isDisposed()) throw new DisposedException();
+
+        return incrementally ? internal_evaluateAgainstIDBs(queryText) : internal_evaluate(queryText);
+    }
+
+    public String getUnusedRules(Collection<DLClause> clauses, boolean toUpdate) {
+        if(isDisposed()) throw new DisposedException();
+
+        DLClause clause;
+        for(Iterator<DLClause> iter = clauses.iterator(); iter.hasNext(); ) {
+            if(materialisedRules.contains(clause = iter.next()))
+                iter.remove();
+            else if(toUpdate) materialisedRules.add(clause);
+        }
+
+        if(clauses.isEmpty()) return null;
+
+        return Program.toString(clauses);
+    }
+
+    public void outputMaterialisedRules() {
+        if(isDisposed()) throw new DisposedException();
+
+        System.out.println(DLClauseHelper.toString(materialisedRules));
+    }
+
+    public void outputAnswers(String query) {
+        if(isDisposed()) throw new DisposedException();
+
+        TupleIterator iter = null;
+        try {
+            iter = internal_evaluate(query);
+            System.out.println(query);
+            int arity = iter.getArity();
+            for(long multi = iter.open(); multi != 0; multi = iter.getNext()) {
+                for(int i = 0; i < arity; ++i)
+                    System.out.print(RDFoxTripleManager.getQuotedTerm(iter.getResource(i)) + "\t");
+                System.out.println();
+            }
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        } finally {
+            if(iter != null) iter.dispose();
+        }
+    }
+
+    public void outputInstance4UnaryPredicate(String iri) {
+        if(isDisposed()) throw new DisposedException();
+
+        outputAnswers("select ?x where { ?x "
+                              + "<http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <"
+                              + iri
+                              + "> .}");
+    }
+
+    public void outputSubjects(String p, String o) {
+        if(isDisposed()) throw new DisposedException();
+
+        outputAnswers("select x where { ?x <" + p + "> <" + o + "> . }");
+    }
+
+    public void outputObjects(String s, String p) {
+        if(isDisposed()) throw new DisposedException();
+
+        outputAnswers("select ?x where { <" + s + "> <" + p + "> ?x . }");
+    }
+
+    public void outputIDBFacts() {
+        if(isDisposed()) throw new DisposedException();
+
+        TupleIterator iter = null;
+        try {
+            iter = internal_evaluateAgainstIDBs("select distict ?x ?y ?z where { ?x ?y ?z }");
+            for(long multi = iter.open(); multi != 0; multi = iter.getNext()) {
+                for(int i = 0; i < 3; ++i)
+                    System.out.print(RDFoxTripleManager.getQuotedTerm(iter.getResource(i)) + "\t");
+                System.out.println();
+            }
+        } catch(JRDFStoreException e) {
+            // TODO Auto-generated catch block
+            e.printStackTrace();
+        } finally {
+            if(iter != null) iter.dispose();
+        }
+
+    }
+
+    public void outputType4Individual(String iri) {
+        if(isDisposed()) throw new DisposedException();
+
+        outputAnswers("select ?z where { <" + iri + "> " + Namespace.RDF_TYPE_QUOTED + " ?z }");
+    }
+
+    public int getSameAsNumber() {
+        if(isDisposed()) throw new DisposedException();
+
+        TupleIterator iter = null;
+        int counter = 0;
+        try {
+            iter = internal_evaluate("select ?x ?y where {?x " + Namespace.EQUALITY_QUOTED + " ?y . }");
+            for(long multi = iter.open(); multi != 0; multi = iter.getNext())
+                if(iter.getResourceID(0) != iter.getResourceID(1))
+                    ++counter;
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        } finally {
+            if(iter != null) iter.dispose();
+        }
+        return counter;
+    }
+
+    public UFS<String> getEqualityGroups(boolean reuse) {
+        if(isDisposed()) throw new DisposedException();
+
+        if(reuse && equalityGroups != null) return equalityGroups;
+
+        equalityGroups = new UFS<String>();
+
+        TupleIterator answers = null;
+        try {
+            Timer t = new Timer();
+            answers = internal_evaluate("select ?x ?z  where {?x " + Namespace.EQUALITY_QUOTED + "?z . }");
+            for(long multi = answers.open(); multi != 0; multi = answers.getNext()) {
+                if(answers.getResourceID(0) != answers.getResourceID(1))
+                    equalityGroups.merge(answers.getResource(0).m_lexicalForm, answers.getResource(1).m_lexicalForm);
+            }
+            Utility.logInfo("@Time to group individuals by equality: " + t.duration());
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        } finally {
+            if(answers != null) answers.dispose();
+        }
+
+        return equalityGroups;
+    }
+
+    public void clearRulesAndIDBFacts(Collection<int[]> collection) {
+        if(isDisposed()) throw new DisposedException();
+
+//              performDeletion(collection);
+        collection.clear();
+        try {
+            store.clearRulesAndMakeFactsExplicit();
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        }
+    }
+
+    protected void outputClassAssertions(String filename) {
+        TupleIterator allTuples = null;
+        boolean redirect = false;
+        try {
+            allTuples =
+                    getDataStore().compileQuery("SELECT ?X ?Z WHERE { ?X <" + Namespace.RDF_TYPE + "> ?Z }", prefixes, parameters);
+            redirect = Utility.redirectCurrentOut(filename);
+            for(long multi = allTuples.open(); multi != 0; multi = allTuples.getNext())
+                System.out.println(RDFoxTripleManager.getQuotedTerm(allTuples.getResource(0)) + " " + RDFoxTripleManager
+                        .getQuotedTerm(allTuples.getResource(1)));
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        } finally {
+            if(redirect) Utility.closeCurrentOut();
+            if(allTuples != null) allTuples.dispose();
+        }
+    }
+
+    @SuppressWarnings("unused")
+    private void performDeletion(Collection<int[]> collection) {
+        Utility.logInfo("Remove all rules, idb facts and added staff...");
+        Timer timer = new Timer();
+        TupleIterator iter = null;
+        try {
+            UpdateType ut = UpdateType.ScheduleForDeletion;
+            for(int[] t : collection)
+                store.addTriplesByResourceIDs(t, ut);
+
+            try {
+                iter = internal_evaluateAgainstIDBs("select ?x ?y ?z where { ?x ?y ?z . }");
+                for(long multi = iter.open(); multi != 0; multi = iter.getNext()) {
+                    int[] triple = new int[3];
+                    for(int i = 0; i < 3; ++i)
+                        triple[i] = iter.getResourceID(i);
+                    store.addTriplesByResourceIDs(triple, ut);
+                }
+            } finally {
+                if(iter != null) iter.dispose();
+                iter = null;
+            }
+            store.applyReasoning(true);
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        }
+        Utility.logInfo("Time for deletion: " + timer.duration());
+    }
+
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/DLPredicateComparator.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/DLPredicateComparator.java
new file mode 100644
index 0000000..05e399e
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/DLPredicateComparator.java
@@ -0,0 +1,24 @@
+package uk.ac.ox.cs.pagoda.reasoner.light;
+
+import uk.ac.ox.cs.pagoda.multistage.Normalisation;
+import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+
+import java.util.Comparator;
+
+public class DLPredicateComparator implements Comparator<String> {
+
+        @Override
+        public int compare(String arg0, String arg1) {
+                int ret = type(arg0) - type(arg1);
+                if (ret != 0) return ret;
+                
+                return arg0.compareTo(arg1); 
+        }
+
+        private int type(String p) {
+                if (p.contains(OverApproxExist.negativeSuffix)) return 1; 
+                if (p.contains(Normalisation.auxiliaryConceptPrefix)) return 2; 
+                else return 0; 
+        }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/KarmaQuery.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/KarmaQuery.java
new file mode 100644
index 0000000..03d2b67
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/KarmaQuery.java
@@ -0,0 +1,95 @@
+package uk.ac.ox.cs.pagoda.reasoner.light;
+
+import java.io.FileNotFoundException;
+import java.io.IOException;
+import java.util.LinkedList;
+import java.util.Map.Entry;
+
+import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.karma2.exception.IllegalInputQueryException;
+import org.semanticweb.karma2.model.ConjunctiveQuery;
+import org.semanticweb.karma2.model.cqparser.ConjunctiveQueryParser;
+import uk.ac.ox.cs.pagoda.MyPrefixes;
+import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
+import uk.ac.ox.cs.pagoda.hermit.RuleHelper;
+import uk.ac.ox.cs.pagoda.util.Utility;
+
+public class KarmaQuery {
+        
+        StringBuffer queryBuffer; 
+
+        public KarmaQuery(String queryText) {
+                LinkedList<String> answerVariables = new LinkedList<String>(); 
+                DLClause clause = DLClauseHelper.getQuery(queryText, answerVariables);
+                String clauseText = RuleHelper.getText(clause); 
+//              clauseText = RuleHelper.abbreviateIRI(clauseText).replace(":-", "<-");
+                clauseText = clauseText.replace(":-", "<-");
+                queryBuffer = new StringBuffer();
+                
+                clauseText = expandIRI4Arguments(clauseText); 
+                
+                for (Entry<String, String> entry : MyPrefixes.PAGOdAPrefixes.getPrefixIRIsByPrefixName().entrySet()) 
+                        if (clauseText.contains(entry.getKey())) {
+                                if (queryBuffer.length() > 0) queryBuffer.append(',').append(Utility.LINE_SEPARATOR);
+                                queryBuffer.append("prefix ").append(entry.getKey()).append(" <").append(entry.getValue()).append(">"); 
+                        }
+                if (queryBuffer.length() > 0) queryBuffer.append(Utility.LINE_SEPARATOR); 
+                
+                queryBuffer.append("p(");
+                boolean first = true; 
+                for (String var: answerVariables) { 
+                        if (first) first = false; 
+                        else queryBuffer.append(","); 
+                                
+                        queryBuffer.append("?").append(var); 
+                }
+                queryBuffer.append(")").append(clauseText.substring(0, clauseText.length() - 1));
+        }
+        
+        private String expandIRI4Arguments(String clauseText) {
+                int leftIndex = clauseText.indexOf('('), rightIndex = clauseText.indexOf(')', leftIndex + 1);
+                String argsText, newArgsText; 
+                while (leftIndex != -1) {
+                        argsText = clauseText.substring(leftIndex + 1, rightIndex);
+                        newArgsText = MyPrefixes.PAGOdAPrefixes.expandText(argsText); 
+                        clauseText = clauseText.replace(argsText, newArgsText); 
+                        
+                        rightIndex += newArgsText.length() - argsText.length();
+                        leftIndex = clauseText.indexOf('(', rightIndex + 1); 
+                        rightIndex = clauseText.indexOf(')', leftIndex + 1); 
+                }
+                
+                return clauseText; 
+        }
+
+        public ConjunctiveQuery getConjunctiveQuery() {
+                ConjunctiveQuery cq = null;
+                try {
+                        cq = new ConjunctiveQueryParser(toString()).parse();
+                } catch (FileNotFoundException e) {
+                        // TODO Auto-generated catch block
+                        e.printStackTrace();
+                } catch (IllegalInputQueryException e) {
+                        // TODO Auto-generated catch block
+                        e.printStackTrace();
+                } catch (IOException e) {
+                        // TODO Auto-generated catch block
+                        e.printStackTrace();
+                } catch (Exception e) {
+                        Utility.logDebug("The query cannot be properly handled by KARMA."); 
+                        return null; 
+                }
+                return cq; 
+        }
+        
+        @Override
+        public String toString() {
+                return queryBuffer.toString(); 
+        }
+
+        static String sample = "prefix P0: <http://swat.cse.lehigh.edu/onto/univ-bench.owl#>, " +
+                        "prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>, " +
+                        "prefix owl: <http://www.w3.org/2002/07/owl#>" +
+                        "q(?0) <- owl:Thing(?0), P0:Person(?0)";
+        
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/KarmaQueryEngine.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/KarmaQueryEngine.java
new file mode 100644
index 0000000..98f0c35
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/KarmaQueryEngine.java
@@ -0,0 +1,109 @@
+package uk.ac.ox.cs.pagoda.reasoner.light;
+
+import org.semanticweb.karma2.MyKarma;
+import org.semanticweb.karma2.clausifier.OntologyProcesser;
+import org.semanticweb.karma2.exception.IllegalInputOntologyException;
+import org.semanticweb.karma2.model.ConjunctiveQuery;
+import org.semanticweb.owlapi.model.OWLOntology;
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.store.DataStore;
+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.util.ConjunctiveQueryHelper;
+import uk.ac.ox.cs.pagoda.util.Utility;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
+
+import java.io.File;
+import java.io.FileNotFoundException;
+import java.nio.file.Paths;
+import java.util.Set;
+
+public class KarmaQueryEngine extends RDFoxQueryEngine {
+
+    String karmaDataFile = null, karmaRuleFile = null;
+    private MyKarma reasoner = null;
+
+    public KarmaQueryEngine(String name) {
+        super(name);
+
+//              int Base = 1 << 6; 
+//              int index = (new Random().nextInt() % Base + Base) % Base;
+//              karmaDataFile = "karma_data" + index + ".ttl"; 
+//              karmaRuleFile = "karma_rule" + index + ".dlog";
+        karmaDataFile = Paths.get(Utility.getGlobalTempDirAbsolutePath(), "karma_data.ttl").toString();
+        karmaRuleFile = Paths.get(Utility.getGlobalTempDirAbsolutePath(), "karma_rule.dlog").toString();
+
+        reasoner = new MyKarma();
+    }
+
+    public MyKarma getReasoner() {
+        if(isDisposed()) throw new DisposedException();
+        return reasoner;
+    }
+
+    public void processOntology(OWLOntology elhoOntology) {
+        if(isDisposed()) throw new DisposedException();
+        try {
+            OntologyProcesser.transformOntology(elhoOntology, new File(karmaDataFile), new File(karmaRuleFile));
+        } catch(IllegalInputOntologyException e) {
+            e.printStackTrace();
+        }
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+        reasoner.dispose();
+    }
+
+    @Override
+    public AnswerTuples evaluate(String queryText) {
+        if(isDisposed()) throw new DisposedException();
+        return evaluate(queryText, ConjunctiveQueryHelper.getAnswerVariables(queryText)[0], null);
+    }
+
+    @Override
+    public AnswerTuples evaluate(String queryText, String[] answerVars) {
+        if(isDisposed()) throw new DisposedException();
+        return evaluate(queryText, answerVars, null);
+    }
+
+    public AnswerTuples evaluate(String queryText, AnswerTuples soundAnswerTuples) {
+        if(isDisposed()) throw new DisposedException();
+        return evaluate(queryText, ConjunctiveQueryHelper.getAnswerVariables(queryText)[0], soundAnswerTuples);
+    }
+
+    public AnswerTuples evaluate(String queryText, String[] answerVars, AnswerTuples soundAnswerTuples) {
+        if(isDisposed()) throw new DisposedException();
+        KarmaQuery karmaQuery = new KarmaQuery(queryText.replace("_:", "?"));
+        reasoner.setConcurrence(false);
+        ConjunctiveQuery cq = karmaQuery.getConjunctiveQuery();
+        if(cq == null) return null;
+        Set<AnswerTuple> answers = reasoner.answerCQ(cq, soundAnswerTuples, !queryText.contains("_:"));
+        return new AnswerTuplesImp(answerVars, answers);
+    }
+
+    @Override
+    public DataStore getDataStore() {
+        if(isDisposed()) throw new DisposedException();
+        return reasoner.getStore();
+    }
+
+    public void initialiseKarma() {
+        if(isDisposed()) throw new DisposedException();
+        try {
+            reasoner.initializeData(new File(karmaDataFile));
+            reasoner.materialise(new File(karmaRuleFile));
+
+            File tmp;
+            if(karmaDataFile != null && ((tmp = new File(karmaDataFile)).exists())) tmp.delete();
+            if(karmaRuleFile != null && ((tmp = new File(karmaRuleFile)).exists())) tmp.delete();
+        } catch(FileNotFoundException e) {
+            e.printStackTrace();
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        }
+    }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxAnswerTuples.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxAnswerTuples.java
new file mode 100644
index 0000000..f823232
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxAnswerTuples.java
@@ -0,0 +1,117 @@
+package uk.ac.ox.cs.pagoda.reasoner.light;
+
+import org.semanticweb.HermiT.model.Constant;
+import org.semanticweb.HermiT.model.Individual;
+import org.semanticweb.HermiT.model.Term;
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.model.GroundTerm;
+import uk.ac.ox.cs.JRDFox.store.TupleIterator;
+import uk.ac.ox.cs.pagoda.query.AnswerTuple;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.util.Utility;
+import uk.ac.ox.cs.pagoda.util.disposable.DisposedException;
+
+public class RDFoxAnswerTuples extends AnswerTuples {
+
+        long multi; 
+        TupleIterator m_iter; 
+        String[] m_answerVars; 
+        
+        public RDFoxAnswerTuples(String[] answerVars, TupleIterator iter) {
+                m_answerVars = answerVars;
+                m_iter = iter; 
+                reset(); 
+        }
+
+        public static Term getHermitTerm(GroundTerm t) {
+                if(t instanceof uk.ac.ox.cs.JRDFox.model.Individual) {
+                        uk.ac.ox.cs.JRDFox.model.Individual individual = (uk.ac.ox.cs.JRDFox.model.Individual) t;
+                        return Individual.create(individual.getIRI());
+                }
+                else {
+                        uk.ac.ox.cs.JRDFox.model.Literal literal = ((uk.ac.ox.cs.JRDFox.model.Literal) t);
+                        return Constant.create(literal.getLexicalForm(), literal.getDatatype().getIRI());
+                }
+        }
+
+        @Override
+        public boolean isValid() {
+                if(isDisposed()) throw new DisposedException();
+
+                return multi != 0;
+        }
+
+        @Override
+        public int getArity() {
+                if(isDisposed()) throw new DisposedException();
+
+                try {
+                        return m_iter.getArity();
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                        return -1;
+                }
+        }
+
+        @Override
+        public void moveNext() {
+                if(isDisposed()) throw new DisposedException();
+
+                try {
+                        multi = m_iter.getNext();
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                }
+        }
+
+        @Override
+        public void dispose() {
+                super.dispose();
+                m_iter.dispose();
+        }
+        
+        @Override
+        public AnswerTuple getTuple() {
+                if(isDisposed()) throw new DisposedException();
+
+                return new AnswerTuple(m_iter, m_answerVars.length); 
+        }
+
+        @Override
+        public void reset() {
+                if(isDisposed()) throw new DisposedException();
+
+                try {
+                        multi = m_iter.open();
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                }               
+        }
+
+        @Override
+        public boolean contains(AnswerTuple t) {
+                if(isDisposed()) throw new DisposedException();
+
+                Utility.logError("Unsupported operation in RDFoxAnswerTuples"); 
+                return false;
+        }
+
+        @Override
+        public void remove() {
+                if(isDisposed()) throw new DisposedException();
+
+                Utility.logError("Unsupported operation in RDFoxAnswerTuples"); 
+        }
+
+        @Override
+        public String[] getAnswerVariables() {
+                if(isDisposed()) throw new DisposedException();
+
+                return m_answerVars;
+        }
+
+        protected void finalize() {
+                m_iter.dispose();
+        }
+        
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxQueryEngine.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxQueryEngine.java
new file mode 100644
index 0000000..f19f253
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxQueryEngine.java
@@ -0,0 +1,139 @@
+package uk.ac.ox.cs.pagoda.reasoner.light;
+
+import org.semanticweb.owlapi.model.OWLOntology;
+import org.semanticweb.owlapi.model.OWLOntologyCreationException;
+import org.semanticweb.owlapi.model.parameters.Imports;
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.Prefixes;
+import uk.ac.ox.cs.JRDFox.store.DataStore;
+import uk.ac.ox.cs.JRDFox.store.DataStore.StoreType;
+import uk.ac.ox.cs.pagoda.MyPrefixes;
+import uk.ac.ox.cs.pagoda.query.AnswerTuples;
+import uk.ac.ox.cs.pagoda.reasoner.QueryEngine;
+import uk.ac.ox.cs.pagoda.reasoner.QueryReasoner;
+import uk.ac.ox.cs.pagoda.tracking.AnswerTuplesWriter;
+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;
+
+import java.io.File;
+import java.util.Collection;
+
+public abstract class RDFoxQueryEngine extends QueryEngine {
+
+    public static final int matNoOfThreads = Runtime.getRuntime().availableProcessors() * 2;
+    protected String name;
+    protected Prefixes prefixes = MyPrefixes.PAGOdAPrefixes.getRDFoxPrefixes();
+
+    public RDFoxQueryEngine(String name) {
+        this.name = name;
+    }
+
+    public static DataStore createDataStore() {
+        DataStore instance = null;
+        try {
+//                      instance = new DataStore("par-head-n");
+            instance = new DataStore(StoreType.NarrowParallelHead);
+            instance.setNumberOfThreads(matNoOfThreads);
+            instance.initialize();
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        }
+        return instance;
+    }
+
+    public String getName() {
+        if(isDisposed()) throw new DisposedException();
+        return name;
+    }
+
+    public abstract DataStore getDataStore();
+
+    public void importRDFData(String fileName, String importedFile) {
+        if(isDisposed()) throw new DisposedException();
+        if(importedFile == null || importedFile.isEmpty()) return;
+        Timer t = new Timer();
+        DataStore store = getDataStore();
+        try {
+            long oldTripleCount = store.getTriplesCount(), tripleCount;
+            for(String file : importedFile.split(QueryReasoner.ImportDataFileSeparator)) {
+                store.importTurtleFile(new File(file), prefixes);
+            }
+            tripleCount = store.getTriplesCount();
+            Utility.logDebug(name + " store after importing " + fileName + ": " + tripleCount + " (" + (tripleCount - oldTripleCount) + " new)");
+            store.clearRulesAndMakeFactsExplicit();
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        }
+        Utility.logDebug(name + " store finished importing " + fileName + " in " + t.duration() + " seconds.");
+    }
+
+    public void importDataFromABoxOf(OWLOntology ontology) {
+        if(isDisposed()) throw new DisposedException();
+        DataStore store = getDataStore();
+        try {
+            long prevTriplesCount = store.getTriplesCount();
+            store.importOntology(ontology.getOWLOntologyManager().createOntology(ontology.getABoxAxioms(Imports.INCLUDED)));
+            long loadedTriples = store.getTriplesCount() - prevTriplesCount;
+            Utility.logDebug(name + ": loaded " + loadedTriples + " triples from " + ontology.getABoxAxioms(Imports.INCLUDED)
+                                                                                            .size() + " ABox axioms");
+        } catch(JRDFStoreException | OWLOntologyCreationException e) {
+            e.printStackTrace();
+            System.exit(1);
+        }
+
+    }
+
+    public void materialise(String programName, String programText) {
+        if(isDisposed()) throw new DisposedException();
+        if(programText == null) return;
+        Timer t = new Timer();
+        DataStore store = getDataStore();
+        try {
+            long oldTripleCount = store.getTriplesCount(), tripleCount;
+//                      store.addRules(new String[] {programText});
+            store.importRules(programText);
+            store.applyReasoning();
+            tripleCount = store.getTriplesCount();
+            Utility.logDebug(name + " store after materialising " + programName + ": " + tripleCount + " (" + (tripleCount - oldTripleCount) + " new)");
+            store.clearRulesAndMakeFactsExplicit();
+        } catch(JRDFStoreException e) {
+            e.printStackTrace();
+        }
+        Utility.logDebug(name + " store finished the materialisation of " + programName + " in " + t.duration() + " seconds.");
+    }
+
+    @Override
+    public void evaluate(Collection<String> queryTexts, String answerFile) {
+        if(isDisposed()) throw new DisposedException();
+        if(queryTexts == null)
+            return;
+
+        int queryID = 0;
+        AnswerTuplesWriter answerWriter = new AnswerTuplesWriter(answerFile);
+        AnswerTuples answerTuples;
+        Timer t = new Timer();
+        try {
+            for(String query : queryTexts) {
+                t.reset();
+                answerTuples = null;
+                try {
+                    answerTuples = evaluate(query);
+                    Utility.logDebug("time to answer Query " + ++queryID + ": " + t.duration());
+                    answerWriter.write(answerTuples.getAnswerVariables(), answerTuples);
+                } finally {
+                    if(answerTuples != null) answerTuples.dispose();
+                }
+            }
+        } finally {
+            answerWriter.close();
+        }
+
+        Utility.logDebug("done computing query answers by RDFox.");
+    }
+
+    @Override
+    public void dispose() {
+        super.dispose();
+    }
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxTripleManager.java b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxTripleManager.java
new file mode 100644
index 0000000..62885be
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/reasoner/light/RDFoxTripleManager.java
@@ -0,0 +1,269 @@
+package uk.ac.ox.cs.pagoda.reasoner.light;
+
+import net.sf.ehcache.Cache;
+import net.sf.ehcache.CacheManager;
+import net.sf.ehcache.Element;
+import org.semanticweb.HermiT.model.*;
+import uk.ac.ox.cs.JRDFox.JRDFStoreException;
+import uk.ac.ox.cs.JRDFox.model.Datatype;
+import uk.ac.ox.cs.JRDFox.model.GroundTerm;
+import uk.ac.ox.cs.JRDFox.store.DataStore;
+import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType;
+import uk.ac.ox.cs.JRDFox.store.Dictionary;
+import uk.ac.ox.cs.JRDFox.store.Resource;
+import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.Map;
+
+public class RDFoxTripleManager {
+
+        private final Cache termsCache;
+        private static final int TERMS_CACHE_SIZE = 10000;
+        private static final int CACHE_TTL_DEFAULT = 0;
+        private static final int CACHE_TTI_DEFAULT = 0;
+        private static final boolean CACHE_ETERNAL = true;
+        private static final boolean CACHE_USE_DISK = false;
+
+        UpdateType m_incrementally;
+//      boolean m_incrementally; 
+
+        DataStore m_store;
+        Dictionary m_dict; 
+//      Set<Atom> triplesByTerm = new HashSet<Atom>();
+        
+        public RDFoxTripleManager(DataStore store, boolean incrementally) {
+                m_store = store;
+//              m_incrementally = incrementally;
+
+                CacheManager cacheManager = CacheManager.getInstance();
+                String cacheName = "RDFoxTripleManager_" + store.hashCode();
+                if(! cacheManager.cacheExists(cacheName)) {
+                        termsCache = new Cache(cacheName,
+                                                                   TERMS_CACHE_SIZE, CACHE_USE_DISK, CACHE_ETERNAL,
+                                                                   CACHE_TTL_DEFAULT, CACHE_TTI_DEFAULT);
+                        cacheManager.addCache(termsCache);
+                }
+                else
+                        termsCache = cacheManager.getCache(cacheName);
+
+                if (incrementally)
+                        m_incrementally = UpdateType.ScheduleForAddition;
+                else 
+                        m_incrementally = UpdateType.Add; 
+                
+                try {
+                        m_dict = store.getDictionary();
+                        resourceID = m_dict.resolveResources(
+                                        new String[] {Namespace.RDF_TYPE,  Namespace.EQUALITY, Namespace.INEQUALITY},
+                                        new int[] {Datatype.IRI_REFERENCE.value(), Datatype.IRI_REFERENCE.value(), Datatype.IRI_REFERENCE.value()} 
+                                        ); 
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                }
+        }
+        
+        public boolean isRdfTypeID(int id) {
+                return id == resourceID[0]; 
+        }
+        
+        public void addTripleByID(int[] tuple) {
+//              System.out.println(getRawTerm(tuple[0]) + " " + getRawTerm(tuple[1]) + " " + getRawTerm(tuple[2]) + " ."); 
+                try {
+//                      Resource[] rsc = new Resource[3]; 
+//                      m_dict.getResources(tuple, 0, 3, rsc);
+//                      
+//                      GroundTerm[] terms = new GroundTerm[3]; 
+//                      for (int i = 0; i < 3; ++i)
+//                              terms[i] = uk.ac.ox.cs.JRDFox.model.Individual.create(rsc[i].m_lexicalForm); 
+//                      m_store.addTriples(terms, m_incrementally);
+                        
+                        m_store.addTriplesByResourceIDs(tuple, m_incrementally);
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                }
+        }
+        
+        public void addTripleByTerm(Atom atom) {
+                try {
+                        m_store.addTriples(getRDFoxTriple(atom), m_incrementally);
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                } 
+        }
+
+    public void removeTripleByTermIncrementally(Atom atom) {
+        try {
+            m_store.addTriples(getRDFoxTriple(atom), UpdateType.ScheduleForDeletion);
+        } catch (JRDFStoreException e) {
+            e.printStackTrace();
+        }
+    }
+        
+        public static GroundTerm[] getRDFoxTriple(Atom instance) {
+                if (instance.getArity() == 1) 
+                        return new GroundTerm[] {
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((Individual) instance.getArgument(0)).getIRI()), 
+                                        uk.ac.ox.cs.JRDFox.model.Individual.RDF_TYPE, 
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((AtomicConcept) instance.getDLPredicate()).getIRI()) };
+                else if (instance.getDLPredicate() instanceof Equality || instance.getDLPredicate() instanceof AnnotatedEquality) 
+                        return new GroundTerm[] {
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((Individual) instance.getArgument(0)).getIRI()), 
+                                        uk.ac.ox.cs.JRDFox.model.Individual.SAME_AS, 
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((Individual) instance.getArgument(1)).getIRI()) };
+                else if (instance.getDLPredicate() instanceof Inequality) 
+                        return new GroundTerm[] {
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((Individual) instance.getArgument(0)).getIRI()), 
+                                        uk.ac.ox.cs.JRDFox.model.Individual.DIFFERENT_FROM, 
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((Individual) instance.getArgument(1)).getIRI()) }; 
+                else 
+                        return new GroundTerm[] {
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((Individual) instance.getArgument(0)).getIRI()), 
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((AtomicRole) instance.getDLPredicate()).getIRI()), 
+                                        uk.ac.ox.cs.JRDFox.model.Individual.create(((Individual) instance.getArgument(1)).getIRI()) };
+        }
+        
+        int[] resourceID; // rdf:type, owl:sameAs, owl:differentFrom 
+
+        public int[] getInstance(Atom atom, Map<Variable, Integer> assignment) {
+                DLPredicate p = atom.getDLPredicate(); 
+                if (p instanceof Equality || p instanceof AnnotatedEquality) 
+                        return new int[] {
+                                        getResourceID(atom.getArgument(0), assignment),
+                                        resourceID[1],
+                                        getResourceID(atom.getArgument(1), assignment)
+                        }; 
+                else if (p instanceof Inequality) 
+                        return new int[] {
+                                        getResourceID(atom.getArgument(0), assignment), 
+                                        resourceID[2], 
+                                        getResourceID(atom.getArgument(1), assignment)
+                        }; 
+                else if (atom.getArity() == 1) 
+                        return new int[] {
+                                        getResourceID(atom.getArgument(0), assignment), 
+                                        resourceID[0], 
+                                        getResourceID(p)
+                        }; 
+                else 
+                        return new int[] {
+                                        getResourceID(atom.getArgument(0), assignment), 
+                                        getResourceID(p), 
+                                        getResourceID(atom.getArgument(1), assignment)
+                        }; 
+        }
+        
+        public String getRawTerm(int id) {
+                Resource[] res = new Resource[1]; 
+                try {
+                        m_dict.getResources(new int[] {id}, 0, 1, res);
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                }
+                return getQuotedTerm(res[0]); 
+        }
+
+        Map<String, Integer> predicateCache = new HashMap<String, Integer>(); 
+        
+        public int getResourceID(DLPredicate p) {
+                Integer id; 
+                String name = p instanceof AtomicConcept ? ((AtomicConcept) p).getIRI() : ((AtomicRole) p).getIRI();
+                if ((id = predicateCache.get(name)) != null) return id;
+                try {
+                        predicateCache.put(name, id = resolveResource(name, Datatype.IRI_REFERENCE.value()));
+                        
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                } 
+                return id;
+        }
+        
+        public int getResourceID(String name) {
+                Integer id = null; 
+                try {
+                        id =  resolveResource(name, Datatype.IRI_REFERENCE.value()); 
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                }
+                return id; 
+        }
+        
+        private int resolveResource(String name, int type) throws JRDFStoreException {
+                String[] lexicalForms = new String[] {name}; 
+                int[] types = new int[] {type};
+                return m_dict.resolveResources(lexicalForms, types)[0]; 
+        }
+        
+//      Map<Term, Integer> termCache = new HashMap<Term, Integer>();
+//      Queue<Term> termQueue = new LinkedList<Term>();
+
+        private int getResourceID(Term arg, Map<Variable, Integer> assignment) {
+                if (arg instanceof Variable) return assignment.get(arg);
+                int id = -1;
+                if(termsCache.isKeyInCache(arg))
+                        return ((int) termsCache.get(arg).getObjectValue());
+
+//              if (arg instanceof Individual) {
+                        try {
+                                if (arg instanceof Individual)
+                                        termsCache.put(new Element(arg, id = resolveResource(((Individual) arg).getIRI(), Datatype.IRI_REFERENCE.value())));
+                                else if (arg instanceof Constant)
+                                        termsCache.put(new Element(arg, id = resolveResource(((Constant) arg).getLexicalForm(), getDatatypeID(((Constant) arg).getDatatypeURI()))));
+                                
+                        } catch (JRDFStoreException e) {
+                                e.printStackTrace();
+                                System.exit(1);
+                        } 
+//              }
+                        
+                return id;
+        }
+        
+        private static int getDatatypeID(String uri) {
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#string")) return Datatype.XSD_STRING.value(); 
+                if (uri.equals("http://www.w3.org/1999/02/22-rdf-syntax-ns#PlainLiteral")) return Datatype.RDF_PLAIN_LITERAL.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#integer")) return Datatype.XSD_INTEGER.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#float")) return Datatype.XSD_FLOAT.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#double")) return Datatype.XSD_DOUBLE.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#boolean")) return Datatype.XSD_BOOLEAN.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#dateTime")) return Datatype.XSD_DATE_TIME.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#time")) return Datatype.XSD_TIME.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#date")) return Datatype.XSD_DATE.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#gYearMonth")) return Datatype.XSD_G_YEAR_MONTH.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#gYear")) return Datatype.XSD_G_YEAR.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#gMonthDay")) return Datatype.XSD_G_MONTH_DAY.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#gDay")) return Datatype.XSD_G_DAY.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#gMonth")) return Datatype.XSD_G_MONTH.value(); 
+                if (uri.equals("http://www.w3.org/2001/XMLSchema#duration")) return Datatype.XSD_DURATION.value(); 
+                
+                return -1;
+        }
+
+        public int[] getResourceIDs(Collection<uk.ac.ox.cs.JRDFox.model.Individual> individuals) {
+                String[] str = new String[individuals.size()]; 
+                int[] types = new int[individuals.size()]; 
+                int index = 0; 
+                for (uk.ac.ox.cs.JRDFox.model.Individual individual : individuals) {
+                        types[index] = Datatype.IRI_REFERENCE.value(); 
+                        str[index++] = individual.getIRI(); 
+                }
+                        
+                try {
+                        return m_dict.resolveResources(str, types);
+                } catch (JRDFStoreException e) {
+                        e.printStackTrace();
+                        return null; 
+                } 
+        }
+        
+        public static String getQuotedTerm(Resource r) {
+                if (r.m_datatype.equals(Datatype.IRI_REFERENCE))
+                        return OWLHelper.addAngles(r.m_lexicalForm); 
+                if (r.m_datatype.equals(Datatype.XSD_STRING) || r.m_datatype.equals(Datatype.RDF_PLAIN_LITERAL))
+                        return "\"" + r.m_lexicalForm + "\"";
+                else 
+                        return "\"" + r.m_lexicalForm + "\"^^<" + r.m_datatype.getIRI() + ">"; 
+        }
+}