Add new fresh data factory

This will help write more significant test.

14 files changed, 455 insertions, 376 deletions

diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
index ca54054..3467d3c 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -39,7 +39,7 @@ import implicits.JavaCollections._
 
 import uk.ac.ox.cs.rsacomb.converter._
 import uk.ac.ox.cs.rsacomb.suffix._
-import uk.ac.ox.cs.rsacomb.util.RSA
+import uk.ac.ox.cs.rsacomb.util.{DataFactory, RSA}
 
 /** Canonical model generator
   *
@@ -92,7 +92,7 @@ class CanonicalModel(val ontology: RSAOntology) {
   val (facts, rules): (List[TupleTableAtom], List[Rule]) = {
     // Compute rules from ontology axioms
     val (facts, rules) = {
-      val term = RSAUtil.genFreshVariable()
+      val term = Variable.create("X")
       val unsafe = ontology.unsafe
       ontology.axioms
         .map(a =>
@@ -216,13 +216,13 @@ class CanonicalModel(val ontology: RSAOntology) {
         unsafe: List[OWLObjectPropertyExpression],
         skolem: SkolemStrategy,
         suffix: RSASuffix
-    ): Result =
+    )(implicit fresh: DataFactory): Result =
       axiom match {
 
         case a: OWLSubClassOfAxiom if a.isT5 => {
           val role = axiom.objectPropertyExpressionsInSignature(0)
           if (unsafe contains role)
-            super.convert(a, term, unsafe, new Standard(a), Forward)
+            super.convert(a, term, unsafe, new Standard(a), Forward)(fresh)
           else {
             val (f1, r1) = rules1(a)
             (f1, r1 ::: rules2(a) ::: rules3(a))
@@ -231,12 +231,12 @@ class CanonicalModel(val ontology: RSAOntology) {
 
         case a: OWLSubObjectPropertyOfAxiom => {
           val (facts, rules) = List(Empty, Forward, Backward)
-            .map(super.convert(a, term, unsafe, NoSkolem, _))
+            .map(super.convert(a, term, unsafe, NoSkolem, _)(fresh))
             .unzip
           (facts.flatten, rules.flatten)
         }
 
-        case a => super.convert(a, term, unsafe, skolem, suffix)
+        case a => super.convert(a, term, unsafe, skolem, suffix)(fresh)
 
       }
   }
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
index 4c63e17..a1fd20f 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
@@ -28,7 +28,7 @@ import sparql.ConjunctiveQuery
 
 import uk.ac.ox.cs.rsacomb.ontology.Ontology
 import uk.ac.ox.cs.rsacomb.converter.Normalizer
-import uk.ac.ox.cs.rsacomb.approximation.Lowerbound
+import uk.ac.ox.cs.rsacomb.approximation.{Upperbound, Lowerbound}
 
 case class RSAOption[+T](opt: T) {
   def get[T]: T = opt.asInstanceOf[T]
@@ -133,7 +133,7 @@ object RSAComb extends App {
   ).normalize(new Normalizer)
 
   /* Approximate the ontology to RSA */
-  val toRSA = new Lowerbound
+  val toRSA = new Upperbound
   val rsa = ontology approximate toRSA
 
   if (config contains 'query) {
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
index 30e1305..869dd88 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -81,30 +81,6 @@ import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
 import uk.ac.ox.cs.rsacomb.util.Logger
 import uk.ac.ox.cs.rsacomb.ontology.Ontology
 
-object RSAUtil {
-
-  // implicit def axiomsToOntology(axioms: Seq[OWLAxiom]) = {
-  //   val manager = OWLManager.createOWLOntologyManager()
-  //   manager.createOntology(axioms.asJava)
-  // }
-
-  /** Manager instance to interface with OWLAPI */
-  val manager = OWLManager.createOWLOntologyManager()
-  val factory = manager.getOWLDataFactory()
-
-  /** Simple fresh variable/class generator */
-  private var counter = -1;
-  def genFreshVariable(): Variable = {
-    counter += 1
-    Variable.create(f"I$counter%05d")
-  }
-  def getFreshOWLClass(): OWLClass = {
-    counter += 1
-    factory.getOWLClass(s"X$counter")
-  }
-
-}
-
 object RSAOntology {
 
   import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Lowerbound.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Lowerbound.scala
index 290cbaf..88732d5 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Lowerbound.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Lowerbound.scala
@@ -13,8 +13,8 @@ import scalax.collection.GraphPredef._, scalax.collection.GraphEdge._
 import scalax.collection.GraphTraversal._
 
 import uk.ac.ox.cs.rsacomb.RSAOntology
-import uk.ac.ox.cs.rsacomb.RSAUtil
 import uk.ac.ox.cs.rsacomb.ontology.Ontology
+import uk.ac.ox.cs.rsacomb.util.DataFactory
 
 object Lowerbound {
 
@@ -38,7 +38,8 @@ object Lowerbound {
   *
   * @see [[uk.ac.ox.cs.rsacomb.converter.Normalizer]]
   */
-class Lowerbound extends Approximation[RSAOntology] {
+class Lowerbound(implicit fresh: DataFactory)
+    extends Approximation[RSAOntology] {
 
   /** Simplify conversion between Java and Scala collections */
   import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
@@ -122,12 +123,10 @@ class Lowerbound extends Approximation[RSAOntology] {
         val sup = a.getSuperClass.getNNF
         sup match {
           case sup: OWLObjectUnionOf => {
-            val body = sub.asConjunctSet.map((atom) =>
-              (atom, RSAUtil.getFreshOWLClass())
-            )
-            val head = sup.asDisjunctSet.map((atom) =>
-              (atom, RSAUtil.getFreshOWLClass())
-            )
+            val body =
+              sub.asConjunctSet.map((atom) => (atom, fresh.getOWLClass))
+            val head =
+              sup.asDisjunctSet.map((atom) => (atom, fresh.getOWLClass))
 
             val r1 =
               Lowerbound.factory.getOWLSubClassOfAxiom(
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Upperbound.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Upperbound.scala
index ad924aa..1ae7941 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Upperbound.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Upperbound.scala
@@ -13,8 +13,8 @@ import scalax.collection.GraphPredef._, scalax.collection.GraphEdge._
 import scalax.collection.GraphTraversal._
 
 import uk.ac.ox.cs.rsacomb.RSAOntology
-import uk.ac.ox.cs.rsacomb.RSAUtil
 import uk.ac.ox.cs.rsacomb.ontology.Ontology
+import uk.ac.ox.cs.rsacomb.util.DataFactory
 
 object Upperbound {
 
@@ -38,7 +38,8 @@ object Upperbound {
   *
   * @see [[uk.ac.ox.cs.rsacomb.converter.Normalizer]]
   */
-class Upperbound extends Approximation[RSAOntology] {
+class Upperbound(implicit fresh: DataFactory)
+    extends Approximation[RSAOntology] {
 
   /** Simplify conversion between Java and Scala collections */
   import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
@@ -138,15 +139,17 @@ class Upperbound extends Approximation[RSAOntology] {
       import uk.ac.ox.cs.rsacomb.implicits.RSAAxiom._
       axiom.toTriple match {
         case Some((subclass, role, filler)) => {
-          val skolem = Upperbound.factory.getOWLNamedIndividual(s"i_${axiom.toString.hashCode}")
-          val fresh = RSAUtil.getFreshOWLClass()
+          val skolem = Upperbound.factory.getOWLNamedIndividual(
+            s"i_${axiom.toString.hashCode}"
+          )
+          val cls = fresh.getOWLClass
           List(
             Upperbound.factory.getOWLSubClassOfAxiom(
               subclass,
-              Upperbound.factory.getOWLObjectSomeValuesFrom(role, fresh)
+              Upperbound.factory.getOWLObjectSomeValuesFrom(role, cls)
             ),
             Upperbound.factory.getOWLSubClassOfAxiom(
-              fresh,
+              cls,
               Upperbound.factory.getOWLObjectOneOf(skolem)
             ),
             Upperbound.factory.getOWLClassAssertionAxiom(filler, skolem)
@@ -169,5 +172,5 @@ class Upperbound extends Approximation[RSAOntology] {
   // val edges2 = Seq('I ~> 'M, 'I ~> 'L, 'L ~> 'N, 'M ~> 'N)
   // val edges3 = Seq('P ~> 'O)
   // val graph = Graph.from(edges = edges1 ++ edges2 ++ edges3)
-  
+
 }
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala
index b5da3cc..c24f99d 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala
@@ -19,9 +19,8 @@ package uk.ac.ox.cs.rsacomb.converter
 import org.semanticweb.owlapi.apibinding.OWLManager
 import org.semanticweb.owlapi.model._
 
-import uk.ac.ox.cs.rsacomb.util.Logger
+import uk.ac.ox.cs.rsacomb.util.{Logger, DataFactory}
 import uk.ac.ox.cs.rsacomb.RSAOntology
-import uk.ac.ox.cs.rsacomb.RSAUtil
 
 object Normalizer {
 
@@ -45,7 +44,9 @@ class Normalizer() {
 
   /** Normalizes a [[OWLLogicalAxiom]]
     */
-  def normalize(axiom: OWLLogicalAxiom): Seq[OWLLogicalAxiom] =
+  def normalize(
+      axiom: OWLLogicalAxiom
+  )(implicit fresh: DataFactory): Seq[OWLLogicalAxiom] =
     axiom match {
       case a: OWLSubClassOfAxiom => {
         val sub = a.getSubClass.getNNF
@@ -56,11 +57,11 @@ class Normalizer() {
             *   C c D -> { C c X, X c D }
             */
           case _ if !sub.isOWLClass && !sup.isOWLClass => {
-            val cls = RSAUtil.getFreshOWLClass()
+            val cls = fresh.getOWLClass
             Seq(
               factory.getOWLSubClassOfAxiom(sub, cls),
               factory.getOWLSubClassOfAxiom(cls, sup)
-            ).flatMap(normalize)
+            ).flatMap(normalize(_)(fresh))
           }
           /** Conjunction on the lhs
             *
@@ -77,7 +78,7 @@ class Normalizer() {
                   if (conj.isOWLClass)
                     (acc1 :+ conj, acc2)
                   else {
-                    val cls = RSAUtil.getFreshOWLClass()
+                    val cls = fresh.getOWLClass
                     (
                       acc1 :+ cls,
                       acc2 :+ factory.getOWLSubClassOfAxiom(conj, cls)
@@ -89,9 +90,11 @@ class Normalizer() {
                 factory.getOWLObjectIntersectionOf(acc1: _*),
                 sup
               ))
-                .flatMap(normalize)
+                .flatMap(normalize(_)(fresh))
             } else {
-              normalize(factory.getOWLSubClassOfAxiom(factory.getOWLThing, sup))
+              normalize(
+                factory.getOWLSubClassOfAxiom(factory.getOWLThing, sup)
+              )(fresh)
             }
           }
           /** Conjunction on the rhs
@@ -103,9 +106,11 @@ class Normalizer() {
             if (conjuncts.length > 0) {
               conjuncts
                 .map(cls => factory.getOWLSubClassOfAxiom(sub, cls))
-                .flatMap(normalize)
+                .flatMap(normalize(_)(fresh))
             } else {
-              normalize(factory.getOWLSubClassOfAxiom(sub, factory.getOWLThing))
+              normalize(
+                factory.getOWLSubClassOfAxiom(sub, factory.getOWLThing)
+              )(fresh)
             }
           }
           /** Disjunction on the lhs
@@ -117,11 +122,11 @@ class Normalizer() {
             if (disjuncts.length > 0) {
               disjuncts
                 .map(cls => factory.getOWLSubClassOfAxiom(cls, sup))
-                .flatMap(normalize)
+                .flatMap(normalize(_)(fresh))
             } else {
               normalize(
                 factory.getOWLSubClassOfAxiom(factory.getOWLNothing, sup)
-              )
+              )(fresh)
             }
           }
           /** Disjunction on the rhs
@@ -137,9 +142,10 @@ class Normalizer() {
             if (disjuncts.length > 0) {
               val acc = (Seq[OWLClassExpression](), Seq[OWLLogicalAxiom]())
               val (acc1, acc2) = disjuncts.foldLeft(acc)(
-                { case ((acc1, acc2), disj: OWLClass) => (acc1 :+ disj, acc2)
+                {
+                  case ((acc1, acc2), disj: OWLClass) => (acc1 :+ disj, acc2)
                   case ((acc1, acc2), disj) => {
-                    val cls = RSAUtil.getFreshOWLClass()
+                    val cls = fresh.getOWLClass
                     (
                       acc1 :+ cls,
                       acc2 :+ factory.getOWLSubClassOfAxiom(cls, disj)
@@ -150,9 +156,11 @@ class Normalizer() {
               (acc2 :+ factory.getOWLSubClassOfAxiom(
                 sub,
                 factory.getOWLObjectUnionOf(acc1: _*)
-              )).flatMap(normalize)
+              )).flatMap(normalize(_)(fresh))
             } else {
-              normalize(factory.getOWLSubClassOfAxiom(sub, factory.getOWLNothing))
+              normalize(
+                factory.getOWLSubClassOfAxiom(sub, factory.getOWLNothing)
+              )(fresh)
             }
           }
           /** Complex class expression on existential restriction on the lhs
@@ -161,14 +169,14 @@ class Normalizer() {
             */
           case (sub: OWLObjectSomeValuesFrom, _)
               if !sub.getFiller.isOWLClass => {
-            val cls = RSAUtil.getFreshOWLClass()
+            val cls = fresh.getOWLClass
             Seq(
               factory.getOWLSubClassOfAxiom(sub.getFiller, cls),
               factory.getOWLSubClassOfAxiom(
                 factory.getOWLObjectSomeValuesFrom(sub.getProperty, cls),
                 sup
               )
-            ).flatMap(normalize)
+            ).flatMap(normalize(_)(fresh))
           }
           /** Complex class expression on existential restriction on the rhs
             *
@@ -176,14 +184,14 @@ class Normalizer() {
             */
           case (_, sup: OWLObjectSomeValuesFrom)
               if !sup.getFiller.isOWLClass => {
-            val cls = RSAUtil.getFreshOWLClass()
+            val cls = fresh.getOWLClass
             Seq(
               factory.getOWLSubClassOfAxiom(cls, sup.getFiller),
               factory.getOWLSubClassOfAxiom(
                 sub,
                 factory.getOWLObjectSomeValuesFrom(sup.getProperty, cls)
               )
-            ).flatMap(normalize)
+            ).flatMap(normalize(_)(fresh))
           }
           /** Object universal quantification on the lhs
             *
@@ -197,7 +205,7 @@ class Normalizer() {
           case (sub: OWLObjectAllValuesFrom, _) => {
             val role = sub.getProperty
             val filler = sub.getFiller
-            val (c, d) = (RSAUtil.getFreshOWLClass, RSAUtil.getFreshOWLClass)
+            val (c, d) = (fresh.getOWLClass, fresh.getOWLClass)
             Seq(
               factory.getOWLSubClassOfAxiom(
                 factory.getOWLThing,
@@ -208,12 +216,13 @@ class Normalizer() {
                 factory.getOWLNothing
               ),
               factory.getOWLSubClassOfAxiom(
-                c, factory.getOWLObjectSomeValuesFrom(role, d)
+                c,
+                factory.getOWLObjectSomeValuesFrom(role, d)
               )
             )
           }
           /** Object/Data universal quantification on the lhs */
-          case (sub: OWLDataAllValuesFrom, _)   => notSupported(a)
+          case (sub: OWLDataAllValuesFrom, _) => notSupported(a)
           /** Object universal quantification on the rhs
             *
             *   C c forall R . D -> exists R- . C c D
@@ -228,7 +237,7 @@ class Normalizer() {
                   ),
                 sup.getFiller
               )
-            )
+            )(fresh)
           /** Object universal quantification on the rhs not supported */
           case (_, sup: OWLDataAllValuesFrom) => notSupported(a)
           /** Exact object/data cardinality restriction on the lhs/rhs
@@ -238,19 +247,19 @@ class Normalizer() {
           case (sub: OWLObjectExactCardinality, _) =>
             normalize(
               factory.getOWLSubClassOfAxiom(sub.asIntersectionOfMinMax, sup)
-            )
+            )(fresh)
           case (sub: OWLDataExactCardinality, _) =>
             normalize(
               factory.getOWLSubClassOfAxiom(sub.asIntersectionOfMinMax, sup)
-            )
+            )(fresh)
           case (_, sup: OWLObjectExactCardinality) =>
             normalize(
               factory.getOWLSubClassOfAxiom(sub, sup.asIntersectionOfMinMax)
-            )
+            )(fresh)
           case (_, sup: OWLDataExactCardinality) =>
             normalize(
               factory.getOWLSubClassOfAxiom(sub, sup.asIntersectionOfMinMax)
-            )
+            )(fresh)
           /** Min object/data cardinality restriction on the lhs/rhs
             *
             *   >= 0 R . C -> top
@@ -263,7 +272,7 @@ class Normalizer() {
               case 0 =>
                 normalize(
                   factory.getOWLSubClassOfAxiom(factory.getOWLThing, sup)
-                )
+                )(fresh)
               case 1 =>
                 normalize(
                   factory.getOWLSubClassOfAxiom(
@@ -273,7 +282,7 @@ class Normalizer() {
                     ),
                     sup
                   )
-                )
+                )(fresh)
               case _ => notSupported(a)
             }
           case (sub: OWLDataMinCardinality, _) =>
@@ -281,7 +290,7 @@ class Normalizer() {
               case 0 =>
                 normalize(
                   factory.getOWLSubClassOfAxiom(factory.getOWLThing, sup)
-                )
+                )(fresh)
               case 1 =>
                 normalize(
                   factory.getOWLSubClassOfAxiom(
@@ -291,7 +300,7 @@ class Normalizer() {
                     ),
                     sup
                   )
-                )
+                )(fresh)
               case _ => notSupported(a)
             }
           case (_, sup: OWLObjectMinCardinality) =>
@@ -306,7 +315,7 @@ class Normalizer() {
                       sup.getFiller
                     )
                   )
-                )
+                )(fresh)
               case _ => notSupported(a)
             }
           case (_, sup: OWLDataMinCardinality) =>
@@ -321,7 +330,7 @@ class Normalizer() {
                       sup.getFiller
                     )
                   )
-                )
+                )(fresh)
               case _ => notSupported(a)
             }
           /** Max object/data cardinality restriction on the lhs not supported */
@@ -344,17 +353,17 @@ class Normalizer() {
                 ),
                 factory.getOWLNothing
               )
-            )
+            )(fresh)
           case (_, sup: OWLObjectMaxCardinality)
               if sup.getCardinality == 1 && !sup.getFiller.isOWLClass => {
-            val cls = RSAUtil.getFreshOWLClass()
+            val cls = fresh.getOWLClass
             Seq(
               factory.getOWLSubClassOfAxiom(cls, sup.getFiller),
               factory.getOWLSubClassOfAxiom(
                 sub,
                 factory.getOWLObjectMaxCardinality(1, sup.getProperty, cls)
               )
-            ).flatMap(normalize)
+            ).flatMap(normalize(_)(fresh))
           }
           case (_, sup: OWLObjectMaxCardinality) if sup.getCardinality >= 2 =>
             notSupported(a)
@@ -368,7 +377,7 @@ class Normalizer() {
                 ),
                 factory.getOWLNothing
               )
-            )
+            )(fresh)
           case (_, sup: OWLDataMaxCardinality) if sup.getCardinality >= 1 =>
             notSupported(a)
           /** HasValue expression on the lhs/rhs
@@ -384,7 +393,7 @@ class Normalizer() {
                 ),
                 sup
               )
-            )
+            )(fresh)
           case (sub: OWLDataHasValue, _) =>
             normalize(
               factory.getOWLSubClassOfAxiom(
@@ -394,7 +403,7 @@ class Normalizer() {
                 ),
                 sup
               )
-            )
+            )(fresh)
           case (_, sup: OWLObjectHasValue) =>
             normalize(
               factory.getOWLSubClassOfAxiom(
@@ -404,7 +413,7 @@ class Normalizer() {
                   factory.getOWLObjectOneOf(sup.getFiller)
                 )
               )
-            )
+            )(fresh)
           case (_, sup: OWLDataHasValue) =>
             normalize(
               factory.getOWLSubClassOfAxiom(
@@ -414,7 +423,7 @@ class Normalizer() {
                   factory.getOWLDataOneOf(sup.getFiller)
                 )
               )
-            )
+            )(fresh)
           /** Enumeration of individuals on the lhs
             *
             *   {a1, ... ,an} c D -> { D(a1), ..., D(an) }
@@ -433,7 +442,7 @@ class Normalizer() {
                   sup.getIndividuals.map(factory.getOWLObjectOneOf(_))
                 )
               )
-            )
+            )(fresh)
           /** Class complement on the lhs
             *
             *   ~C c D -> top c C u D
@@ -444,7 +453,7 @@ class Normalizer() {
                 factory.getOWLThing,
                 factory.getOWLObjectUnionOf(sub.getComplementNNF, sup)
               )
-            )
+            )(fresh)
           /** Class complement on the rhs
             *
             *   C c ~D -> C n D c bot
@@ -455,7 +464,7 @@ class Normalizer() {
                 factory.getOWLObjectIntersectionOf(sup.getComplementNNF, sub),
                 factory.getOWLNothing
               )
-            )
+            )(fresh)
           /** Self-restriction over an object property */
           case (sub: OWLObjectHasSelf, _) => notSupported(a)
           case (_, sup: OWLObjectHasSelf) => notSupported(a)
@@ -466,32 +475,34 @@ class Normalizer() {
       }
 
       case a: OWLEquivalentClassesAxiom => {
-        a.getAxiomWithoutAnnotations.asOWLSubClassOfAxioms.flatMap(normalize)
+        a.getAxiomWithoutAnnotations.asOWLSubClassOfAxioms.flatMap(
+          normalize(_)(fresh)
+        )
       }
 
       case a: OWLEquivalentObjectPropertiesAxiom => {
         a.getAxiomWithoutAnnotations.asSubObjectPropertyOfAxioms.flatMap(
-          normalize
+          normalize(_)(fresh)
         )
       }
 
       case a: OWLEquivalentDataPropertiesAxiom => {
         a.getAxiomWithoutAnnotations.asSubDataPropertyOfAxioms.flatMap(
-          normalize
+          normalize(_)(fresh)
         )
       }
 
       case a: OWLObjectPropertyDomainAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLObjectPropertyRangeAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLDataPropertyDomainAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLDataPropertyRangeAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLDisjointClassesAxiom =>
         a.asPairwiseAxioms.map((a) => {
@@ -504,20 +515,22 @@ class Normalizer() {
 
       case a: OWLInverseObjectPropertiesAxiom =>
         a.getAxiomWithoutAnnotations.asSubObjectPropertyOfAxioms.flatMap(
-          normalize
+          normalize(_)(fresh)
         )
 
       case a: OWLFunctionalObjectPropertyAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLFunctionalDataPropertyAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLInverseFunctionalObjectPropertyAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLSymmetricObjectPropertyAxiom =>
-        a.getAxiomWithoutAnnotations.asSubPropertyAxioms.flatMap(normalize)
+        a.getAxiomWithoutAnnotations.asSubPropertyAxioms.flatMap(
+          normalize(_)(fresh)
+        )
 
       case a: OWLDifferentIndividualsAxiom =>
         a.asPairwiseAxioms.map((a) => {
@@ -529,42 +542,44 @@ class Normalizer() {
         })
 
       case a: OWLIrreflexiveObjectPropertyAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLSameIndividualAxiom =>
-        a.getAxiomWithoutAnnotations.asOWLSubClassOfAxioms.flatMap(normalize)
+        a.getAxiomWithoutAnnotations.asOWLSubClassOfAxioms.flatMap(
+          normalize(_)(fresh)
+        )
 
       case a: OWLDisjointUnionAxiom =>
         Seq(a.getOWLDisjointClassesAxiom, a.getOWLEquivalentClassesAxiom)
-          .flatMap(normalize)
+          .flatMap(normalize(_)(fresh))
 
       /** Complex class assertion
         *
         * C(a) -> { X(a), X c C }
         */
       case a: OWLClassAssertionAxiom if !a.getClassExpression.isOWLClass => {
-        val cls = RSAUtil.getFreshOWLClass()
+        val cls = fresh.getOWLClass
         Seq(
           factory.getOWLClassAssertionAxiom(cls, a.getIndividual),
           factory.getOWLSubClassOfAxiom(cls, a.getClassExpression)
-        ).flatMap(normalize)
+        ).flatMap(normalize(_)(fresh))
       }
 
       case a: OWLNegativeObjectPropertyAssertionAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLNegativeDataPropertyAssertionAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLTransitiveObjectPropertyAxiom => {
         val role = a.getProperty
         normalize(
-          factory.getOWLSubPropertyChainOfAxiom( List(role, role), role)
-        )
+          factory.getOWLSubPropertyChainOfAxiom(List(role, role), role)
+        )(fresh)
       }
 
       case a: OWLReflexiveObjectPropertyAxiom =>
-        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)(fresh)
 
       case a: OWLAsymmetricObjectPropertyAxiom => notSupported(a)
 
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
index 03c1246..266c158 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
@@ -27,10 +27,9 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
   TupleTableAtom
 }
 import tech.oxfordsemantic.jrdfox.logic.expression.{Term, IRI, FunctionCall}
-import uk.ac.ox.cs.rsacomb.RSAUtil
 import uk.ac.ox.cs.rsacomb.RSAOntology
 import uk.ac.ox.cs.rsacomb.suffix.{Empty, Inverse, RSASuffix}
-import uk.ac.ox.cs.rsacomb.util.{RSA, RDFoxUtil}
+import uk.ac.ox.cs.rsacomb.util.{DataFactory, RSA, RDFoxUtil}
 
 /** Horn-ALCHOIQ to RDFox axiom converter.
   *
@@ -129,16 +128,16 @@ trait RDFoxConverter {
       unsafe: List[OWLObjectPropertyExpression],
       skolem: SkolemStrategy,
       suffix: RSASuffix
-  ): Result =
+  )(implicit fresh: DataFactory): Result =
     axiom match {
 
       case a: OWLSubClassOfAxiom => {
         val subcls = a.getSubClass
         val supcls = a.getSuperClass
         val (sub, _) =
-          convert(subcls, term, unsafe, NoSkolem, suffix)
+          convert(subcls, term, unsafe, NoSkolem, suffix)(fresh)
         val (sup, ext) =
-          convert(supcls, term, unsafe, skolem, suffix)
+          convert(supcls, term, unsafe, skolem, suffix)(fresh)
         val rule = Rule.create(sup, ext ::: sub)
         ResultR(List(rule))
       }
@@ -148,7 +147,7 @@ trait RDFoxConverter {
       case a: OWLEquivalentClassesAxiom => {
         val (atoms, rules) = a.asPairwiseAxioms
           .flatMap(_.asOWLSubClassOfAxioms)
-          .map(a => convert(a, term, unsafe, skolem dup a, suffix))
+          .map(a => convert(a, term, unsafe, skolem dup a, suffix)(fresh))
           .unzip
         (atoms.flatten, rules.flatten)
       }
@@ -156,61 +155,64 @@ trait RDFoxConverter {
       case a: OWLEquivalentObjectPropertiesAxiom => {
         val (atoms, rules) = a.asPairwiseAxioms
           .flatMap(_.asSubObjectPropertyOfAxioms)
-          .map(a => convert(a, term, unsafe, skolem dup a, suffix))
+          .map(a => convert(a, term, unsafe, skolem dup a, suffix)(fresh))
           .unzip
         (atoms.flatten, rules.flatten)
       }
 
       case a: OWLSubObjectPropertyOfAxiom => {
-        val term1 = RSAUtil.genFreshVariable()
-        val body = convert(a.getSubProperty, term, term1, suffix)
-        val head = convert(a.getSuperProperty, term, term1, suffix)
+        val term1 = fresh.getVariable
+        val body = convert(a.getSubProperty, term, term1, suffix)(fresh)
+        val head = convert(a.getSuperProperty, term, term1, suffix)(fresh)
         ResultR(List(Rule.create(head, body)))
       }
 
       case a: OWLSubDataPropertyOfAxiom => {
-        val term1 = RSAUtil.genFreshVariable()
-        val body = convert(a.getSubProperty, term, term1, suffix)
-        val head = convert(a.getSuperProperty, term, term1, suffix)
+        val term1 = fresh.getVariable
+        val body = convert(a.getSubProperty, term, term1, suffix)(fresh)
+        val head = convert(a.getSuperProperty, term, term1, suffix)(fresh)
         ResultR(List(Rule.create(head, body)))
       }
 
       case a: OWLObjectPropertyDomainAxiom =>
-        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)
+        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)(fresh)
 
       case a: OWLObjectPropertyRangeAxiom => {
-        val term1 = RSAUtil.genFreshVariable()
-        val (res, ext) = convert(a.getRange, term, unsafe, skolem, suffix)
-        val prop = convert(a.getProperty, term1, term, suffix)
+        val term1 = fresh.getVariable
+        val (res, ext) =
+          convert(a.getRange, term, unsafe, skolem, suffix)(fresh)
+        val prop = convert(a.getProperty, term1, term, suffix)(fresh)
         ResultR(List(Rule.create(res, prop :: ext)))
       }
 
       case a: OWLDataPropertyDomainAxiom =>
-        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)
+        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)(fresh)
 
       case a: OWLDisjointClassesAxiom => {
         val body = a.getOperandsAsList.asScala.toSeq
-          .flatMap((cls) => convert(cls, term, unsafe, NoSkolem, suffix)._1)
+          .flatMap((cls) =>
+            convert(cls, term, unsafe, NoSkolem, suffix)(fresh)._1
+          )
         val bottom = TupleTableAtom.rdf(term, IRI.RDF_TYPE, IRI.NOTHING)
         ResultR(List(Rule.create(bottom, body: _*)))
       }
 
       case a: OWLInverseObjectPropertiesAxiom => {
         val (atoms, rules) = a.asSubObjectPropertyOfAxioms
-          .map(a => convert(a, term, unsafe, skolem dup a, suffix))
+          .map(a => convert(a, term, unsafe, skolem dup a, suffix)(fresh))
           .unzip
         (atoms.flatten, rules.flatten)
       }
 
       case a: OWLFunctionalObjectPropertyAxiom =>
-        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)
+        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)(fresh)
 
       case a: OWLInverseFunctionalObjectPropertyAxiom =>
-        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)
+        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)(fresh)
 
       case a: OWLSymmetricObjectPropertyAxiom => {
         val (atoms, rules) = a.asSubPropertyAxioms
-          .map(a => convert(a, term, unsafe, skolem dup a, suffix))
+          .map(a => convert(a, term, unsafe, skolem dup a, suffix)(fresh))
           .unzip
         (atoms.flatten, rules.flatten)
       }
@@ -221,7 +223,7 @@ trait RDFoxConverter {
           case i: OWLNamedIndividual => {
             val cls = a.getClassExpression
             val (res, _) =
-              convert(cls, i.getIRI, unsafe, NoSkolem, suffix)
+              convert(cls, i.getIRI, unsafe, NoSkolem, suffix)(fresh)
             ResultF(res)
           }
           case _ => Result()
@@ -234,7 +236,7 @@ trait RDFoxConverter {
         else {
           val subj = a.getSubject.asOWLNamedIndividual.getIRI
           val obj = a.getObject.asOWLNamedIndividual.getIRI
-          val prop = convert(a.getProperty, subj, obj, suffix)
+          val prop = convert(a.getProperty, subj, obj, suffix)(fresh)
           ResultF(List(prop))
         }
 
@@ -248,29 +250,29 @@ trait RDFoxConverter {
         else {
           val subj = a.getSubject.asOWLNamedIndividual.getIRI
           val obj = a.getObject
-          val prop = convert(a.getProperty, subj, obj, suffix)
+          val prop = convert(a.getProperty, subj, obj, suffix)(fresh)
           ResultF(List(prop))
         }
 
       case a: OWLSubPropertyChainOfAxiom => {
-        val (term1, body) = a.getPropertyChain.foldLeft((term, List[TupleTableAtom]())){
-          case ((term, atoms), prop) => {
-            val term1 = RSAUtil.genFreshVariable()
-            val atom = convert(prop, term, term1, suffix)
-            (term1, atoms :+ atom)
+        val (term1, body) =
+          a.getPropertyChain.foldLeft((term, List[TupleTableAtom]())) {
+            case ((term, atoms), prop) => {
+              val term1 = fresh.getVariable
+              val atom = convert(prop, term, term1, suffix)(fresh)
+              (term1, atoms :+ atom)
+            }
           }
-        }
-        val head = convert(a.getSuperProperty, term, term1, suffix)
-        ResultR(List(Rule.create(head, body)))
+        val head = convert(a.getSuperProperty, term, term1, suffix)(fresh)
+        val rule = Rule.create(head, body)
+        println(rule)
+        ResultR(List(rule))
       }
 
       /** Catch-all case for all unhandled axiom types. */
       case a => unsupported(axiom)
     }
 
-  protected def toBeNormalised(axiom: OWLLogicalAxiom): Result =
-    throw new RuntimeException(s"Axiom '$axiom' should be normalised!")
-
   protected def unsupported(axiom: OWLLogicalAxiom): Result =
     throw new RuntimeException(s"Axiom '$axiom' is not supported (yet?)")
 
@@ -299,7 +301,7 @@ trait RDFoxConverter {
       unsafe: List[OWLObjectPropertyExpression],
       skolem: SkolemStrategy,
       suffix: RSASuffix
-  ): Shards =
+  )(implicit fresh: DataFactory): Shards =
     expr match {
 
       /** Simple class name.
@@ -318,7 +320,7 @@ trait RDFoxConverter {
         */
       case e: OWLObjectIntersectionOf => {
         val (res, ext) = e.asConjunctSet
-          .map(convert(_, term, unsafe, skolem, suffix))
+          .map(convert(_, term, unsafe, skolem, suffix)(fresh))
           .unzip
         (res.flatten, ext.flatten)
       }
@@ -352,14 +354,14 @@ trait RDFoxConverter {
       case e: OWLObjectSomeValuesFrom => {
         val cls = e.getFiller()
         val role = e.getProperty()
-        val varX = RSAUtil.genFreshVariable
+        val varX = fresh.getVariable
         val (bind, term1) = skolem match {
           case NoSkolem    => (None, varX)
           case c: Constant => (None, c.iri)
           case s: Standard => (Some(RDFoxUtil.skolem(s.name, term, varX)), varX)
         }
-        val (res, ext) = convert(cls, term1, unsafe, skolem, suffix)
-        val prop = convert(role, term, term1, suffix)
+        val (res, ext) = convert(cls, term1, unsafe, skolem, suffix)(fresh)
+        val prop = convert(role, term, term1, suffix)(fresh)
         (prop :: res, ext ++ bind)
       }
 
@@ -379,13 +381,13 @@ trait RDFoxConverter {
         // Computes the result of rule skolemization. Depending on the used
         // technique it might involve the introduction of additional atoms,
         // and/or fresh constants and variables.
-        val varX = RSAUtil.genFreshVariable
+        val varX = fresh.getVariable
         val (bind, term1) = skolem match {
           case NoSkolem    => (None, varX)
           case c: Constant => (None, c.iri)
           case s: Standard => (Some(RDFoxUtil.skolem(s.name, term, varX)), varX)
         }
-        val prop = convert(role, term, term1, suffix)
+        val prop = convert(role, term, term1, suffix)(fresh)
         (List(prop), bind.toList)
       }
 
@@ -404,11 +406,12 @@ trait RDFoxConverter {
             s"Class expression '$e' has cardinality restriction != 1."
           )
         val vars @ (y :: z :: _) =
-          Seq(RSAUtil.genFreshVariable(), RSAUtil.genFreshVariable())
+          Seq(fresh.getVariable, fresh.getVariable)
         val cls = e.getFiller
         val role = e.getProperty
-        val (res, ext) = vars.map(convert(cls, _, unsafe, skolem, suffix)).unzip
-        val props = vars.map(convert(role, term, _, suffix))
+        val (res, ext) =
+          vars.map(convert(cls, _, unsafe, skolem, suffix)(fresh)).unzip
+        val props = vars.map(convert(role, term, _, suffix)(fresh))
         val eq = TupleTableAtom.rdf(y, IRI.SAME_AS, z)
         (List(eq), res.flatten ++ props)
       }
@@ -431,7 +434,7 @@ trait RDFoxConverter {
         val filler = e.getFiller
         val property = e.getProperty
         val expr = factory.getOWLObjectSomeValuesFrom(property, filler)
-        convert(expr, term, unsafe, skolem, suffix)
+        convert(expr, term, unsafe, skolem, suffix)(fresh)
       }
 
       /** Minimum cardinality restriction class
@@ -452,7 +455,7 @@ trait RDFoxConverter {
         val filler = e.getFiller
         val property = e.getProperty
         val expr = factory.getOWLDataSomeValuesFrom(property, filler)
-        convert(expr, term, unsafe, skolem, suffix)
+        convert(expr, term, unsafe, skolem, suffix)(fresh)
       }
 
       //case (_, sup: OWLObjectExactCardinality) => {
@@ -475,7 +478,7 @@ trait RDFoxConverter {
           case i: OWLNamedIndividual     => i.getIRI
           case i: OWLAnonymousIndividual => i.getID
         }
-        (List(convert(e.getProperty, term, term1, suffix)), List())
+        (List(convert(e.getProperty, term, term1, suffix)(fresh)), List())
       }
 
       /** Existential quantification with singleton literal filler
@@ -484,7 +487,7 @@ trait RDFoxConverter {
         * [[http://www.w3.org/TR/owl2-syntax/#Literal_Value_Restriction]]
         */
       case e: OWLDataHasValue =>
-        (List(convert(e.getProperty, term, e.getFiller, suffix)), List())
+        (List(convert(e.getProperty, term, e.getFiller, suffix)(fresh)), List())
 
       case e: OWLObjectUnionOf => {
         (List(), List())
@@ -503,7 +506,7 @@ trait RDFoxConverter {
       term1: Term,
       term2: Term,
       suffix: RSASuffix
-  ): TupleTableAtom =
+  )(implicit fresh: DataFactory): TupleTableAtom =
     expr match {
 
       /** Simple named role/object property.
@@ -524,7 +527,7 @@ trait RDFoxConverter {
         */
       case e: OWLObjectInverseOf =>
         //convert(e.getInverse, term1, term2, suffix + Inverse)
-        convert(e.getInverse, term2, term1, suffix)
+        convert(e.getInverse, term2, term1, suffix)(fresh)
 
       /** The infamous impossible case.
         *
@@ -543,7 +546,7 @@ trait RDFoxConverter {
       term1: Term,
       term2: Term,
       suffix: RSASuffix
-  ): TupleTableAtom =
+  )(implicit fresh: DataFactory): TupleTableAtom =
     expr match {
 
       /** Simple named role/data property
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
index 09bfa1e..795e039 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
@@ -25,10 +25,9 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
 }
 import tech.oxfordsemantic.jrdfox.logic.expression.{IRI}
 
-import uk.ac.ox.cs.rsacomb.RSAUtil
 import uk.ac.ox.cs.rsacomb.RSAOntology
 import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Nth}
-import uk.ac.ox.cs.rsacomb.util.RDFoxUtil
+import uk.ac.ox.cs.rsacomb.util.{DataFactory, RDFoxUtil}
 
 /* Is this the best way to determine if an atom is an RDF triple?
  * Note that we can't use `getNumberOfArguments()` because is not
@@ -91,11 +90,13 @@ object RSAAtom {
         TupleTableAtom.create(ttname, atom.getArguments())
       }
 
-    lazy val reified: (Option[TupleTableAtom], List[TupleTableAtom]) =
+    def reified(implicit
+        fresh: DataFactory
+    ): (Option[TupleTableAtom], List[TupleTableAtom]) =
       if (isRDF) {
         (None, List(atom))
       } else {
-        val varS = RSAUtil.genFreshVariable()
+        val varS = fresh.getVariable
         val skolem = RDFoxUtil.skolem(name, (args :+ varS): _*)
         val atom = TupleTableAtom.rdf(varS, IRI.RDF_TYPE, name)
         val atoms = args.zipWithIndex
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/ontology/Ontology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/ontology/Ontology.scala
index ba44605..1f44ce1 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/ontology/Ontology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/ontology/Ontology.scala
@@ -35,9 +35,7 @@ import tech.oxfordsemantic.jrdfox.logic.expression.{Resource, Term, Variable}
 import uk.ac.ox.cs.rsacomb.approximation.Approximation
 import uk.ac.ox.cs.rsacomb.converter._
 import uk.ac.ox.cs.rsacomb.suffix._
-import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
-
-import uk.ac.ox.cs.rsacomb.RSAUtil
+import uk.ac.ox.cs.rsacomb.util.{DataFactory, RDFoxUtil, RSA}
 
 object Ontology {
 
@@ -95,12 +93,13 @@ object Ontology {
           unsafe: List[OWLObjectPropertyExpression],
           skolem: SkolemStrategy,
           suffix: RSASuffix
-      ): Shards =
+      )(implicit fresh: DataFactory): Shards =
         (expr, skolem) match {
 
           case (e: OWLObjectSomeValuesFrom, c: Constant) => {
             nodemap.update(c.iri.getIRI, c.axiom)
-            val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
+            val (res, ext) =
+              super.convert(e, term, unsafe, skolem, suffix)(fresh)
             if (unsafe contains e.getProperty)
               (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext)
             else
@@ -109,19 +108,20 @@ object Ontology {
 
           case (e: OWLDataSomeValuesFrom, c: Constant) => {
             nodemap.update(c.iri.getIRI, c.axiom)
-            val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
+            val (res, ext) =
+              super.convert(e, term, unsafe, skolem, suffix)(fresh)
             if (unsafe contains e.getProperty)
               (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext)
             else
               (RSA.PE(term, c.iri) :: res, ext)
           }
 
-          case _ => super.convert(expr, term, unsafe, skolem, suffix)
+          case _ => super.convert(expr, term, unsafe, skolem, suffix)(fresh)
         }
     }
 
     /* Ontology convertion into LP rules */
-    val term = RSAUtil.genFreshVariable()
+    val term = Variable.create("X")
     val result = axioms.map(a =>
       RSAConverter.convert(a, term, unsafe, new Constant(a), Empty)
     )
@@ -216,8 +216,6 @@ class Ontology(val axioms: List[OWLLogicalAxiom], val datafiles: List[File]) {
   /** Simplify conversion between Java and Scala collections */
   import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
 
-  println(s"Axioms: ${axioms.length}")
-
   /** OWLOntology based on input axioms
     *
     * This is mainly used to instantiate a new reasoner to be used in
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/package.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/package.scala
new file mode 100644
index 0000000..53fa095
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/package.scala
@@ -0,0 +1,21 @@
+/*
+ * Copyright 2020, 2021 KRR Oxford
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+package uk.ac.ox.cs
+package object rsacomb {
+
+  implicit val seed: util.DataFactory = util.DataFactory(0)
+}
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/util/DataFactory.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/util/DataFactory.scala
new file mode 100644
index 0000000..848c6b5
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/util/DataFactory.scala
@@ -0,0 +1,29 @@
+package uk.ac.ox.cs.rsacomb.util
+
+import org.semanticweb.owlapi.apibinding.OWLManager
+import org.semanticweb.owlapi.model.OWLClass
+import tech.oxfordsemantic.jrdfox.logic.expression.Variable
+
+/** Simple fresh variable/class generator */
+object DataFactory {
+
+  /** Manager instance to interface with OWLAPI */
+  private val manager = OWLManager.createOWLOntologyManager()
+  private val factory = manager.getOWLDataFactory()
+
+  def apply(counter: Integer = -1): DataFactory = new DataFactory(counter)
+}
+
+class DataFactory(private var counter: Integer) {
+
+  private def getNext(): Integer = {
+    counter += 1
+    counter
+  }
+
+  def getVariable(): Variable =
+    Variable.create(f"I${this.getNext()}%05d")
+
+  def getOWLClass(): OWLClass =
+    DataFactory.factory.getOWLClass(s"X${this.getNext()}")
+}
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala
index abfe1ee..8d363e9 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala
@@ -31,6 +31,8 @@ import tech.oxfordsemantic.jrdfox.logic.expression.Variable
 import scala.collection.JavaConverters._
 
 import uk.ac.ox.cs.rsacomb.RSAOntology
+import uk.ac.ox.cs.rsacomb.approximation.Lowerbound
+import uk.ac.ox.cs.rsacomb.ontology.Ontology
 import uk.ac.ox.cs.rsacomb.converter.{SkolemStrategy, NoSkolem}
 import uk.ac.ox.cs.rsacomb.suffix.Empty
 import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
@@ -44,7 +46,7 @@ object Ontology1_CanonicalModelSpec {
     IRI.create("http://example.com/rsa_example.owl#" + str)
 
   val ontology_path: File = new File("examples/example1.ttl")
-  val ontology = RSAOntology(ontology_path)
+  val ontology = Ontology(ontology_path, List()).approximate(new Lowerbound)
   val program = ontology.canonicalModel
   val converter = program.CanonicalModelConverter
 
@@ -109,7 +111,7 @@ class Ontology1_CanonicalModelSpec
 
   renderer.render(AsubClassOfD) should "be converted into a single Rule" in {
     val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
+    val unsafe = ontology.unsafe
     val (facts, rules) =
       converter.convert(AsubClassOfD, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
@@ -119,7 +121,7 @@ class Ontology1_CanonicalModelSpec
   // Role R //
 
   renderer.render(roleR) should "be safe" in {
-    ontology.unsafeRoles should not contain roleR
+    ontology.unsafe should not contain roleR
   }
 
   it should "have 3 elements in its conflict set" in {
@@ -143,7 +145,7 @@ class Ontology1_CanonicalModelSpec
   // Role S //
 
   renderer.render(roleS) should "be safe" in {
-    ontology.unsafeRoles should not contain roleS
+    ontology.unsafe should not contain roleS
   }
 
   it should "have 3 elements in its conflict set" in {
@@ -169,14 +171,14 @@ class Ontology1_CanonicalModelSpec
   // S⁻
 
   renderer.render(roleS_inv) should "be unsafe" in {
-    ontology.unsafeRoles should contain(roleS_inv)
+    ontology.unsafe should contain(roleS_inv)
   }
 
   renderer.render(
     AsomeValuesFromSiC
   ) should "produce 1 rule" ignore {
     val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
+    val unsafe = ontology.unsafe
     val (facts, rules) =
       converter.convert(AsomeValuesFromSiC, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
@@ -200,7 +202,7 @@ class Ontology1_CanonicalModelSpec
     // Rule 2 provides 0 rules
     // Rule 3 provides 48 rule (split in 2)
     val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
+    val unsafe = ontology.unsafe
     val (facts, rules) =
       converter.convert(DsomeValuesFromRB, term, unsafe, NoSkolem, Empty)
     facts should have length 48
@@ -225,7 +227,7 @@ class Ontology1_CanonicalModelSpec
     // Rule 3 provides 32 rule (split in 2)
     // Then (1*2 + 32) + (0) + (32*2) = 98
     val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
+    val unsafe = ontology.unsafe
     val (facts, rules) =
       converter.convert(BsomeValuesFromSD, term, unsafe, NoSkolem, Empty)
     facts should have length 32
@@ -236,7 +238,7 @@ class Ontology1_CanonicalModelSpec
     SsubPropertyOfT
   ) should "produce 3 rules" in {
     val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
+    val unsafe = ontology.unsafe
     val (facts, rules) =
       converter.convert(SsubPropertyOfT, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
@@ -245,167 +247,167 @@ class Ontology1_CanonicalModelSpec
 
 }
 
-object Ontology2_CanonicalModelSpec {
-
-  /* Renderer to display OWL Axioms with DL syntax*/
-  val renderer = new DLSyntaxObjectRenderer()
-
-  def base(str: String): IRI =
-    IRI.create("http://example.com/rsa_example.owl#" + str)
-
-  val ontology_path: File = new File("examples/example2.owl")
-  val ontology = RSAOntology(ontology_path)
-  val program = ontology.canonicalModel
-  val converter = program.CanonicalModelConverter
-
-  val roleR = new OWLObjectPropertyImpl(base("R"))
-  val roleS = new OWLObjectPropertyImpl(base("S"))
-  val roleT = new OWLObjectPropertyImpl(base("T"))
-  val roleP = new OWLObjectPropertyImpl(base("P"))
-  val roleR_inv = roleR.getInverseProperty()
-  val roleS_inv = roleS.getInverseProperty()
-  val roleT_inv = roleT.getInverseProperty()
-  val roleP_inv = roleP.getInverseProperty()
-
-  val AsomeValuesFromRB = new OWLSubClassOfAxiomImpl(
-    new OWLClassImpl(base("A")),
-    new OWLObjectSomeValuesFromImpl(
-      roleR,
-      new OWLClassImpl(base("B"))
-    ),
-    Seq().asJava
-  )
-
-  val BsomeValuesFromSC = new OWLSubClassOfAxiomImpl(
-    new OWLClassImpl(base("B")),
-    new OWLObjectSomeValuesFromImpl(
-      roleS,
-      new OWLClassImpl(base("C"))
-    ),
-    Seq().asJava
-  )
-
-  val CsomeValuesFromTD = new OWLSubClassOfAxiomImpl(
-    new OWLClassImpl(base("C")),
-    new OWLObjectSomeValuesFromImpl(
-      roleT,
-      new OWLClassImpl(base("D"))
-    ),
-    Seq().asJava
-  )
-
-  val DsomeValuesFromPA = new OWLSubClassOfAxiomImpl(
-    new OWLClassImpl(base("D")),
-    new OWLObjectSomeValuesFromImpl(
-      roleP,
-      new OWLClassImpl(base("A"))
-    ),
-    Seq().asJava
-  )
-
-}
-
-class Ontology2_CanonicalModelSpec
-    extends AnyFlatSpec
-    with Matchers
-    with LoneElement {
-
-  import Ontology2_CanonicalModelSpec._
-
-  "The program generated from Example #1" should "not be empty" in {
-    program.rules should not be empty
-  }
-
-  // Role R //
-
-  renderer.render(roleR) should "be unsafe" in {
-    ontology.unsafeRoles should contain(roleR)
-  }
-
-  it should "have only its inverse in its conflict set" in {
-    ontology.confl(roleR).loneElement shouldBe roleR_inv
-  }
-
-  // Role S //
-
-  renderer.render(roleS) should "be unsafe" in {
-    ontology.unsafeRoles should contain(roleS)
-  }
-
-  it should "have only its inverse in its conflict set" in {
-    ontology.confl(roleS).loneElement shouldBe roleS_inv
-  }
-
-  // Role T //
-
-  renderer.render(roleT) should "be unsafe" in {
-    ontology.unsafeRoles should contain(roleT)
-  }
-
-  it should "have only its inverse in its conflict set" in {
-    ontology.confl(roleT).loneElement shouldBe roleT_inv
-  }
-
-  // Role P //
-
-  renderer.render(roleP) should "be unsafe" in {
-    ontology.unsafeRoles should contain(roleP)
-  }
-
-  it should "have only its inverse in its conflict set" in {
-    ontology.confl(roleP).loneElement shouldBe roleP_inv
-  }
-
-  // A ⊑ ∃ R.B
-
-  renderer.render(
-    AsomeValuesFromRB
-  ) should "produce 1 rule" in {
-    val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
-    val (facts, rules) =
-      converter.convert(AsomeValuesFromRB, term, unsafe, NoSkolem, Empty)
-    facts shouldBe empty
-    rules should have length 1
-  }
-
-  // B ⊑ ∃ S.C
-
-  renderer.render(
-    BsomeValuesFromSC
-  ) should "produce 1 rule" in {
-    val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
-    val (facts, rules) =
-      converter.convert(BsomeValuesFromSC, term, unsafe, NoSkolem, Empty)
-    facts shouldBe empty
-    rules should have length 1
-  }
-
-  // C ⊑ ∃ T.D
-
-  renderer.render(
-    CsomeValuesFromTD
-  ) should "produce 1 rule" in {
-    val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
-    val (facts, rules) =
-      converter.convert(CsomeValuesFromTD, term, unsafe, NoSkolem, Empty)
-    facts shouldBe empty
-    rules should have length 1
-  }
-
-  // D ⊑ ∃ P.A
-
-  renderer.render(
-    DsomeValuesFromPA
-  ) should "produce 1 rule" in {
-    val term = Variable.create("X")
-    val unsafe = ontology.unsafeRoles
-    val (facts, rules) =
-      converter.convert(DsomeValuesFromPA, term, unsafe, NoSkolem, Empty)
-    facts shouldBe empty
-    rules should have length 1
-  }
-
-}
+// object Ontology2_CanonicalModelSpec {
+
+//   /* Renderer to display OWL Axioms with DL syntax*/
+//   val renderer = new DLSyntaxObjectRenderer()
+
+//   def base(str: String): IRI =
+//     IRI.create("http://example.com/rsa_example.owl#" + str)
+
+//   val ontology_path: File = new File("examples/example2.owl")
+//   val ontology = Ontology(ontology_path, List()).approximate(new Lowerbound)
+//   val program = ontology.canonicalModel
+//   val converter = program.CanonicalModelConverter
+
+//   val roleR = new OWLObjectPropertyImpl(base("R"))
+//   val roleS = new OWLObjectPropertyImpl(base("S"))
+//   val roleT = new OWLObjectPropertyImpl(base("T"))
+//   val roleP = new OWLObjectPropertyImpl(base("P"))
+//   val roleR_inv = roleR.getInverseProperty()
+//   val roleS_inv = roleS.getInverseProperty()
+//   val roleT_inv = roleT.getInverseProperty()
+//   val roleP_inv = roleP.getInverseProperty()
+
+//   val AsomeValuesFromRB = new OWLSubClassOfAxiomImpl(
+//     new OWLClassImpl(base("A")),
+//     new OWLObjectSomeValuesFromImpl(
+//       roleR,
+//       new OWLClassImpl(base("B"))
+//     ),
+//     Seq().asJava
+//   )
+
+//   val BsomeValuesFromSC = new OWLSubClassOfAxiomImpl(
+//     new OWLClassImpl(base("B")),
+//     new OWLObjectSomeValuesFromImpl(
+//       roleS,
+//       new OWLClassImpl(base("C"))
+//     ),
+//     Seq().asJava
+//   )
+
+//   val CsomeValuesFromTD = new OWLSubClassOfAxiomImpl(
+//     new OWLClassImpl(base("C")),
+//     new OWLObjectSomeValuesFromImpl(
+//       roleT,
+//       new OWLClassImpl(base("D"))
+//     ),
+//     Seq().asJava
+//   )
+
+//   val DsomeValuesFromPA = new OWLSubClassOfAxiomImpl(
+//     new OWLClassImpl(base("D")),
+//     new OWLObjectSomeValuesFromImpl(
+//       roleP,
+//       new OWLClassImpl(base("A"))
+//     ),
+//     Seq().asJava
+//   )
+
+// }
+
+// class Ontology2_CanonicalModelSpec
+//     extends AnyFlatSpec
+//     with Matchers
+//     with LoneElement {
+
+//   import Ontology2_CanonicalModelSpec._
+
+//   "The program generated from Example #1" should "not be empty" in {
+//     program.rules should not be empty
+//   }
+
+//   // Role R //
+
+//   renderer.render(roleR) should "be unsafe" in {
+//     ontology.unsafe should contain(roleR)
+//   }
+
+//   it should "have only its inverse in its conflict set" in {
+//     ontology.confl(roleR).loneElement shouldBe roleR_inv
+//   }
+
+//   // Role S //
+
+//   renderer.render(roleS) should "be unsafe" in {
+//     ontology.unsafe should contain(roleS)
+//   }
+
+//   it should "have only its inverse in its conflict set" in {
+//     ontology.confl(roleS).loneElement shouldBe roleS_inv
+//   }
+
+//   // Role T //
+
+//   renderer.render(roleT) should "be unsafe" in {
+//     ontology.unsafe should contain(roleT)
+//   }
+
+//   it should "have only its inverse in its conflict set" in {
+//     ontology.confl(roleT).loneElement shouldBe roleT_inv
+//   }
+
+//   // Role P //
+
+//   renderer.render(roleP) should "be unsafe" in {
+//     ontology.unsafe should contain(roleP)
+//   }
+
+//   it should "have only its inverse in its conflict set" in {
+//     ontology.confl(roleP).loneElement shouldBe roleP_inv
+//   }
+
+//   // A ⊑ ∃ R.B
+
+//   renderer.render(
+//     AsomeValuesFromRB
+//   ) should "produce 1 rule" in {
+//     val term = Variable.create("X")
+//     val unsafe = ontology.unsafe
+//     val (facts, rules) =
+//       converter.convert(AsomeValuesFromRB, term, unsafe, NoSkolem, Empty)
+//     facts shouldBe empty
+//     rules should have length 1
+//   }
+
+//   // B ⊑ ∃ S.C
+
+//   renderer.render(
+//     BsomeValuesFromSC
+//   ) should "produce 1 rule" in {
+//     val term = Variable.create("X")
+//     val unsafe = ontology.unsafe
+//     val (facts, rules) =
+//       converter.convert(BsomeValuesFromSC, term, unsafe, NoSkolem, Empty)
+//     facts shouldBe empty
+//     rules should have length 1
+//   }
+
+//   // C ⊑ ∃ T.D
+
+//   renderer.render(
+//     CsomeValuesFromTD
+//   ) should "produce 1 rule" in {
+//     val term = Variable.create("X")
+//     val unsafe = ontology.unsafe
+//     val (facts, rules) =
+//       converter.convert(CsomeValuesFromTD, term, unsafe, NoSkolem, Empty)
+//     facts shouldBe empty
+//     rules should have length 1
+//   }
+
+//   // D ⊑ ∃ P.A
+
+//   renderer.render(
+//     DsomeValuesFromPA
+//   ) should "produce 1 rule" in {
+//     val term = Variable.create("X")
+//     val unsafe = ontology.unsafe
+//     val (facts, rules) =
+//       converter.convert(DsomeValuesFromPA, term, unsafe, NoSkolem, Empty)
+//     facts shouldBe empty
+//     rules should have length 1
+//   }
+
+// }
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/SuiteAll.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/SuiteAll.scala
index 1df0757..9653546 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/SuiteAll.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/SuiteAll.scala
@@ -32,7 +32,7 @@ import uk.ac.ox.cs.rsacomb.sparql.{
 class SuiteAll
     extends Suites(
       new Ontology1_CanonicalModelSpec,
-      new Ontology2_CanonicalModelSpec,
+      //new Ontology2_CanonicalModelSpec,
       new NaiveFilteringProgramSpec,
       new OWLAxiomSpec,
       new OWLClassSpec,
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/converter/NormalizerSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/converter/NormalizerSpec.scala
index 7285df2..5047e12 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/converter/NormalizerSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/converter/NormalizerSpec.scala
@@ -27,6 +27,7 @@ import tech.oxfordsemantic.jrdfox.logic.expression.{Variable, IRI}
 import uk.ac.ox.cs.rsacomb.converter.RDFoxConverter
 import uk.ac.ox.cs.rsacomb.suffix.{Empty, Forward, Backward, Inverse}
 import uk.ac.ox.cs.rsacomb.converter.{Normalizer, SkolemStrategy, NoSkolem}
+import uk.ac.ox.cs.rsacomb.util.DataFactory
 
 object NormalizerSpec {
   val manager = OWLManager.createOWLOntologyManager()
@@ -89,27 +90,58 @@ class NormalizerSpec extends AnyFlatSpec with Matchers with LoneElement {
       ).flatMap(normalizer.normalize)
   }
 
-  "Disjunction on the rhs" should "be shifted" in {
-    def cls(n: Int) = factory.getOWLClass(s"_:class$n")
-    val axiom1 =
-      factory.getOWLSubClassOfAxiom(
-        factory.getOWLObjectIntersectionOf(cls(1), cls(2), cls(3)),
-        factory.getOWLObjectUnionOf(cls(4), cls(5))
-      )
-    val axiom2 =
-      factory.getOWLSubClassOfAxiom(
-        cls(1),
-        factory.getOWLObjectUnionOf(cls(2), cls(3), cls(4))
-      )
-    val axiom3 =
-      factory.getOWLSubClassOfAxiom(
-        factory.getOWLObjectIntersectionOf(cls(1), cls(2), cls(3)),
-        factory.getOWLObjectUnionOf(cls(4))
-      )
-    normalizer.normalize(axiom1) should have length 5
-    normalizer.normalize(axiom2) should have length 5
-    normalizer.normalize(axiom3) should have length 4
+  "A c \\exists R . D" should "be normalised to { A c \\exists R . C, C c D } if D is not a concept name" in {
+    val seed = 42
+    val test = normalizer.normalize(
+      factory
+        .getOWLSubClassOfAxiom(
+          factory.getOWLClass("A"),
+          factory.getOWLObjectSomeValuesFrom(
+            factory.getOWLObjectProperty("R"),
+            factory.getOWLObjectIntersectionOf(
+              factory.getOWLClass("D1"),
+              factory.getOWLClass("D2")
+            )
+          )
+        )
+    )(DataFactory(seed))
+    val cls = DataFactory(seed).getOWLClass
+    val result = List(
+      factory
+        .getOWLSubClassOfAxiom(
+          factory.getOWLClass("A"),
+          factory.getOWLObjectSomeValuesFrom(
+            factory.getOWLObjectProperty("R"),
+            cls
+          )
+        ),
+      factory.getOWLSubClassOfAxiom(cls, factory.getOWLClass("D1")),
+      factory.getOWLSubClassOfAxiom(cls, factory.getOWLClass("D2"))
+    )
+    test should contain theSameElementsAs result
   }
+
+  // "Disjunction on the rhs" should "be shifted" in {
+  //   def cls(n: Int) = factory.getOWLClass(s"_:class$n")
+  //   val axiom1 =
+  //     factory.getOWLSubClassOfAxiom(
+  //       factory.getOWLObjectIntersectionOf(cls(1), cls(2), cls(3)),
+  //       factory.getOWLObjectUnionOf(cls(4), cls(5))
+  //     )
+  //   val axiom2 =
+  //     factory.getOWLSubClassOfAxiom(
+  //       cls(1),
+  //       factory.getOWLObjectUnionOf(cls(2), cls(3), cls(4))
+  //     )
+  //   val axiom3 =
+  //     factory.getOWLSubClassOfAxiom(
+  //       factory.getOWLObjectIntersectionOf(cls(1), cls(2), cls(3)),
+  //       factory.getOWLObjectUnionOf(cls(4))
+  //     )
+  //   normalizer.normalize(axiom1) should have length 5
+  //   normalizer.normalize(axiom2) should have length 5
+  //   normalizer.normalize(axiom3) should have length 4
+  // }
   //"A class name" should "be converted into a single atom" in {
   //  val cls = factory.getOWLClass(iriString0)
   //  val atom = TupleTableAtom.rdf(term0, IRI.RDF_TYPE, IRI.create(iriString0))