diff --git a/build.sbt b/build.sbt
index 1699b485af425c1089b7cbb613b8e71738479de1..b82c7792f594c5cbc60812ba73f0cdcbbc828e9a 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,20 +1,80 @@
-name := "lisa"
-organization := "ch.epfl.lara"
-licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html"))
+inThisBuild(Def.settings(
+  organization := "ch.epfl.lara",
+  organizationName := "LARA",
+  organizationHomepage := Some(url("https://lara.epfl.ch")),
+  licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html")),
+  versionScheme := Some("semver-spec"),
+))
 
-version := "0.1"
+val scala2 = "2.13.8"
+val scala3 = "3.1.3"
 
-scalaVersion := "3.1.3"
+lazy val commonSettings2 = Seq(
+  scalaVersion := scala2,
+)
+lazy val commonSettings3 = Seq(
+  scalaVersion := scala3,
+  scalacOptions ++= Seq(
+    "-feature",
+    "-deprecation",
+    //"-source:future",
+    "-language:implicitConversions",
+    //"-old-syntax",
+    //"-no-indent",
+  ),
+  libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test",
+  Test / parallelExecution := false,
+  semanticdbEnabled := true,
+  semanticdbVersion := scalafixSemanticdb.revision,
+  scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0",
+)
+
+lazy val root = Project(
+  id = "lisa-core",
+  base = file("."),
+)
+  .settings(commonSettings3)
+  .settings(
+    version := "0.1",
+  )
+  .dependsOn(kernel, utils, theories, tptp) // Everything but `examples`
+
+lazy val kernel = Project(
+  id = "lisa-kernel",
+  base = file("lisa-kernel"),
+)
+  .settings(commonSettings2)
+  .settings(
+    crossScalaVersions := Seq(scala3)
+  )
 
-scalacOptions ++= Seq("-deprecation", "-feature")
-scalacOptions ++= Seq(
-  "-language:implicitConversions"
+lazy val utils = Project(
+  id = "lisa-utils",
+  base = file("lisa-utils"),
 )
+  .settings(commonSettings3)
+  .dependsOn(kernel)
 
-libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test"
-libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4"
-Test / parallelExecution := false
+lazy val theories = Project(
+  id = "lisa-theories",
+  base = file("lisa-theories"),
+)
+  .settings(commonSettings3)
+  .dependsOn(utils)
 
-ThisBuild / semanticdbEnabled := true
-ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
-ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
+lazy val tptp = Project(
+  id = "lisa-tptp",
+  base = file("lisa-tptp"),
+)
+  .settings(commonSettings3)
+  .settings(
+    libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4",
+  )
+  .dependsOn(utils)
+
+lazy val examples = Project(
+  id = "lisa-examples",
+  base = file("lisa-examples"),
+)
+  .settings(commonSettings3)
+  .dependsOn(root)
diff --git a/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
similarity index 95%
rename from src/main/scala/Example.scala
rename to lisa-examples/src/main/scala/Example.scala
index dae950af9c5743fb50b6dc47743d8c581e1388d4..228994a701211f0565665e14f601e1a75f963c38 100644
--- a/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -1,14 +1,14 @@
+import lisa.utils.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SCProofChecker.*
 import lisa.kernel.proof.SequentCalculus.*
-import proven.tactics.SimplePropositionalSolver.solveSequent
-import utilities.Helpers.{_, given}
-import utilities.Printer.*
-import utilities.tptp.KernelParser.*
-import utilities.tptp.ProblemGatherer.*
-import utilities.tptp.*
+import lisa.proven.tactics.SimplePropositionalSolver.solveSequent
+import lisa.utils.Helpers.{_, given}
+import lisa.tptp.KernelParser.*
+import lisa.tptp.ProblemGatherer.*
+import lisa.tptp.*
 
 /**
  * Discover some of the elements of LISA to get started.
@@ -26,7 +26,7 @@ object Example {
    * The last two lines don't need to be changed.
    */
   def proofExample(): Unit = {
-    object Ex extends proven.Main {
+    object Ex extends lisa.proven.Main {
       THEOREM("fixedPointDoubleApplication") of "" PROOF {
         steps(
           ???,
diff --git a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
similarity index 99%
rename from src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index 075e2054ef017276f873df05740826f7a0c65e13..def0f7fa2c336179391cb2fabf0bba49a24d59eb 100644
--- a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -230,12 +230,13 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
         case SimplePredicate(id, args) =>
           val lab = "pred_" + id.id + "_" + id.arity
           if (id == equality) {
-            if (codesOfTerm(args(0)) == codesOfTerm(args(1)))
+            if (codesOfTerm(args(0)) == codesOfTerm(args(1))) {
               phi.normalForm = Some(NLiteral(true))
               parent.normalForm = Some(NLiteral(false))
-            else
+            } else {
               phi.normalForm = Some(NormalPredicate(id, args, updateCodesSig((lab, (args map codesOfTerm).sorted))))
               parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
+            }
           } else {
             phi.normalForm = Some(NormalPredicate(id, args, updateCodesSig((lab, args map codesOfTerm))))
             parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
diff --git a/src/main/scala/lisa/kernel/fol/FOL.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FOL.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/FOL.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/FOL.scala
diff --git a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/fol/Substitutions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
similarity index 98%
rename from src/main/scala/lisa/kernel/fol/Substitutions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
index e89e60797782a2b7d5446f6e013b850879eaf178..0f2fe1f43a5653f38f8bb02e432a771e014b3515 100644
--- a/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -66,9 +66,10 @@ trait Substitutions extends FormulaDefinitions {
     t match {
       case VariableTerm(_) => t
       case FunctionTerm(label, args) =>
-        label match
+        label match {
           case label: SchematicFunctionLabel if label.arity == 0 => m.getOrElse(label, t)
           case label => FunctionTerm(label, args.map(instantiateNullaryFunctionSchemas(_, m)))
+        }
     }
   }
 
@@ -87,13 +88,13 @@ trait Substitutions extends FormulaDefinitions {
       case VariableTerm(_) => t
       case FunctionTerm(label, args) =>
         val newArgs = args.map(instantiateFunctionSchemas(_, m))
-        label match
+        label match {
           case label: ConstantFunctionLabel => FunctionTerm(label, newArgs)
           case label: SchematicFunctionLabel =>
             if (m.contains(label))
               m(label)(newArgs) // = instantiateNullaryFunctionSchemas(m(label).body, (m(label).vars zip newArgs).toMap)
             else FunctionTerm(label, newArgs)
-
+        }
     }
   }
 
@@ -160,9 +161,10 @@ trait Substitutions extends FormulaDefinitions {
     require(m.forall { case (symbol, LambdaTermFormula(arguments, body)) => arguments.length == symbol.arity })
     phi match {
       case PredicateFormula(label, args) =>
-        label match
+        label match {
           case label: SchematicPredicateLabel if m.contains(label) => m(label)(args)
           case label => phi
+        }
       case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiatePredicateSchemas(_, m)))
       case BinderFormula(label, bound, inner) =>
         val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet
diff --git a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/TermDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
similarity index 100%
rename from src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/Judgement.scala
similarity index 94%
rename from src/main/scala/lisa/kernel/proof/Judgement.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/Judgement.scala
index e6fdb2f0e5c18ce53a53876e06233e5a2e45e832..71374b9d8118c603d81aa8829f893690f5464eae 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -7,7 +7,7 @@ import lisa.kernel.proof.RunningTheory
  * Typically, see [[SCProofChecker.checkSingleSCStep]] and [[SCProofChecker.checkSCProof]].
  */
 sealed abstract class SCProofCheckerJudgement {
-  import SCProofCheckerJudgement.*
+  import SCProofCheckerJudgement._
   val proof: SCProof
 
   /**
@@ -40,7 +40,7 @@ object SCProofCheckerJudgement {
  * The judgement (or verdict) of a running theory.
  */
 sealed abstract class RunningTheoryJudgement[+J <: RunningTheory#Justification] {
-  import RunningTheoryJudgement.*
+  import RunningTheoryJudgement._
 
   /**
    * Whether this judgement is positive -- the justification could be imported into the running theory;
@@ -48,8 +48,8 @@ sealed abstract class RunningTheoryJudgement[+J <: RunningTheory#Justification]
    * @return An instance of either [[ValidJustification]] or [[InvalidJustification]]
    */
   def isValid: Boolean = this match {
-    case _: ValidJustification[?] => true
-    case _: InvalidJustification[?] => false
+    case _: ValidJustification[_] => true
+    case _: InvalidJustification[_] => false
   }
   def get: J = this match {
     case ValidJustification(just) => just
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
similarity index 94%
rename from src/main/scala/lisa/kernel/proof/RunningTheory.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index ec979c1b856bed5bb4ead205ac5aeef9b1a44f38..0a94eaeb5b52fb487bcb7d8ae2da0fc68102d21e 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -1,13 +1,13 @@
 package lisa.kernel.proof
 
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.RunningTheoryJudgement.*
-import lisa.kernel.proof.SCProofChecker.*
-import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.fol.FOL._
+import lisa.kernel.proof.RunningTheoryJudgement._
+import lisa.kernel.proof.SCProofChecker._
+import lisa.kernel.proof.SequentCalculus._
 
 import scala.collection.immutable.Set
-import scala.collection.mutable.Map as mMap
-import scala.collection.mutable.Set as mSet
+import scala.collection.mutable.{Map => mMap}
+import scala.collection.mutable.{Set => mSet}
 
 /**
  * This class describes the theory, i.e. the context and language, in which theorems are proven.
@@ -72,9 +72,10 @@ class RunningTheory {
    * Check if a label is a symbol of the theory
    */
 
-  def isSymbol(label: ConstantLabel): Boolean = label match
+  def isSymbol(label: ConstantLabel): Boolean = label match {
     case c: ConstantFunctionLabel => funDefinitions.contains(c)
     case c: ConstantPredicateLabel => predDefinitions.contains(c)
+  }
 
   def isAvailable(label: ConstantLabel): Boolean = !knownSymbols.contains(label.id)
 
@@ -94,7 +95,7 @@ class RunningTheory {
 
   private def proofToTheorem(name: String, proof: SCProof, justifications: Seq[Justification]): RunningTheoryJudgement[this.Theorem] =
     if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
-      if (belongsToTheory(proof.conclusion))
+      if (belongsToTheory(proof.conclusion)) {
         val r = SCProofChecker.checkSCProof(proof)
         r match {
           case SCProofCheckerJudgement.SCValidProof(_) =>
@@ -104,6 +105,7 @@ class RunningTheory {
           case r @ SCProofCheckerJudgement.SCInvalidProof(_, _, message) =>
             InvalidJustification("The given proof is incorrect: " + message, Some(r))
         }
+      }
       else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None)
     else InvalidJustification("Not all imports of the proof are correctly justified.", None)
 
@@ -120,12 +122,12 @@ class RunningTheory {
     val LambdaTermFormula(vars, body) = expression
     if (belongsToTheory(body))
       if (isAvailable(label))
-        if (body.freeVariables.isEmpty && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty)
+        if (body.freeVariables.isEmpty && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty) {
           val newDef = PredicateDefinition(label, expression)
           predDefinitions.update(label, Some(newDef))
           knownSymbols.update(label.id, label)
           RunningTheoryJudgement.ValidJustification(newDef)
-        else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
+        } else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
       else InvalidJustification("The specified symbol id is already part of the theory and can't be redefined.", None)
     else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None)
   }
@@ -156,7 +158,7 @@ class RunningTheory {
     if (belongsToTheory(body))
       if (isAvailable(label))
         if (body.freeVariables.subsetOf(Set(out)) && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty)
-          if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
+          if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j))))) {
             val r = SCProofChecker.checkSCProof(proof)
             r match {
               case SCProofCheckerJudgement.SCValidProof(_) =>
@@ -173,7 +175,7 @@ class RunningTheory {
                 }
               case r @ SCProofCheckerJudgement.SCInvalidProof(_, path, message) => InvalidJustification("The given proof is incorrect: " + message, Some(r))
             }
-          else InvalidJustification("Not all imports of the proof are correctly justified.", None)
+          } else InvalidJustification("Not all imports of the proof are correctly justified.", None)
         else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
       else InvalidJustification("The specified symbol id is already part of the theory and can't be redefined.", None)
     else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None)
@@ -277,9 +279,10 @@ class RunningTheory {
   def addSymbol(s: ConstantLabel): Unit = {
     if (isAvailable(s)) {
       knownSymbols.update(s.id, s)
-      s match
+      s match {
         case c: ConstantFunctionLabel => funDefinitions.update(c, None)
         case c: ConstantPredicateLabel => predDefinitions.update(c, None)
+      }
     } else {}
   }
 
@@ -327,5 +330,5 @@ object RunningTheory {
   /**
    * An empty theory suitable to reason about first order logic.
    */
-  def PredicateLogic: RunningTheory = RunningTheory()
+  def PredicateLogic: RunningTheory = new RunningTheory()
 }
diff --git a/src/main/scala/lisa/kernel/proof/SCProof.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala
similarity index 99%
rename from src/main/scala/lisa/kernel/proof/SCProof.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala
index 244c795e40b3d054de9021ddfabfbec1bd34f7c1..0892ef5d274a3587c375b33d9ab84dcb5d2920f5 100644
--- a/src/main/scala/lisa/kernel/proof/SCProof.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala
@@ -38,11 +38,11 @@ case class SCProof(steps: IndexedSeq[SCProofStep], imports: IndexedSeq[Sequent]
     if (i >= 0)
       if (i >= steps.length) throw new IndexOutOfBoundsException(s"index $i is out of bounds of the steps Seq")
       else steps(i).bot
-    else
+    else {
       val i2 = -(i + 1)
       if (i2 >= imports.length) throw new IndexOutOfBoundsException(s"index $i is out of bounds of the imports Seq")
       else imports(i2)
-
+    }
   }
 
   /**
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
similarity index 94%
rename from src/main/scala/lisa/kernel/proof/SCProofChecker.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 1ae79196707b059f70495a60d36ca7831c4e60ad..34cf960d8279e34170ec60f7690d5080b5d33aca 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -1,9 +1,8 @@
 package lisa.kernel.proof
 
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProofCheckerJudgement.*
-import lisa.kernel.proof.SequentCalculus.*
-import utilities.Printer
+import lisa.kernel.fol.FOL._
+import lisa.kernel.proof.SCProofCheckerJudgement._
+import lisa.kernel.proof.SequentCalculus._
 
 object SCProofChecker {
 
@@ -73,28 +72,28 @@ object SCProofChecker {
            *  Γ, φ∧ψ |- Δ               Γ, φ∧ψ |- Δ
            */
           case LeftAnd(b, t1, phi, psi) =>
-            if (isSameSet(ref(t1).right, b.right))
+            if (isSameSet(ref(t1).right, b.right)) {
               val phiAndPsi = ConnectorFormula(And, Seq(phi, psi))
               if (
                 isSameSet(b.left + phi, ref(t1).left + phiAndPsi) ||
-                isSameSet(b.left + psi, ref(t1).left + phiAndPsi) ||
-                isSameSet(b.left + phi + psi, ref(t1).left + phiAndPsi)
+                  isSameSet(b.left + psi, ref(t1).left + phiAndPsi) ||
+                  isSameSet(b.left + phi + psi, ref(t1).left + phiAndPsi)
               )
                 SCValidProof(SCProof(step))
               else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
-            else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion must be the same.")
+            } else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion must be the same.")
           /*
            *  Γ, φ |- Δ    Σ, ψ |- Π
            * ------------------------
            *    Γ, Σ, φ∨ψ |- Δ, Π
            */
           case LeftOr(b, t, disjuncts) =>
-            if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)))
+            if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _))) {
               val phiOrPsi = ConnectorFormula(Or, disjuncts)
               if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).reduce(_ union _) + phiOrPsi))
                 SCValidProof(SCProof(step))
               else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
-            else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+            } else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
           /*
            *  Γ |- φ, Δ    Σ, ψ |- Π
            * ------------------------
@@ -119,8 +118,8 @@ object SCProofChecker {
             if (isSameSet(ref(t1).right, b.right))
               if (
                 isSameSet(b.left + phiImpPsi, ref(t1).left + phiIffPsi) ||
-                isSameSet(b.left + psiImpPhi, ref(t1).left + phiIffPsi) ||
-                isSameSet(b.left + phiImpPsi + psiImpPhi, ref(t1).left + phiIffPsi)
+                  isSameSet(b.left + psiImpPhi, ref(t1).left + phiIffPsi) ||
+                  isSameSet(b.left + phiImpPsi + psiImpPhi, ref(t1).left + phiIffPsi)
               )
                 SCValidProof(SCProof(step))
               else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
@@ -202,8 +201,8 @@ object SCProofChecker {
             if (isSameSet(ref(t1).left, b.left))
               if (
                 isSameSet(b.right + phi, ref(t1).right + phiOrPsi) ||
-                isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
-                isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi)
+                  isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
+                  isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi)
               )
                 SCValidProof(SCProof(step))
               else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
@@ -349,7 +348,7 @@ object SCProofChecker {
             if (isSameSet(b.right, ref(t1).right))
               if (
                 isSameSet(b.left + phi_t_for_f, ref(t1).left ++ sEqT_es + phi_s_for_f) ||
-                isSameSet(b.left + phi_s_for_f, ref(t1).left ++ sEqT_es + phi_t_for_f)
+                  isSameSet(b.left + phi_s_for_f, ref(t1).left ++ sEqT_es + phi_t_for_f)
               )
                 SCValidProof(SCProof(step))
               else
@@ -367,13 +366,13 @@ object SCProofChecker {
            */
           case RightSubstEq(b, t1, equals, lambdaPhi) =>
             val sEqT_es = equals map { case (s, t) => PredicateFormula(equality, Seq(s, t)) }
-            if (isSameSet(ref(t1).left ++ sEqT_es, b.left))
+            if (isSameSet(ref(t1).left ++ sEqT_es, b.left)) {
               val (s_es, t_es) = equals.unzip
               val phi_s_for_f = lambdaPhi(s_es)
               val phi_t_for_f = lambdaPhi(t_es)
               if (
                 isSameSet(b.right + phi_s_for_f, ref(t1).right + phi_t_for_f) ||
-                isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f)
+                  isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f)
               )
                 SCValidProof(SCProof(step))
               else
@@ -382,7 +381,7 @@ object SCProofChecker {
                   Nil,
                   s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ(s_) φ(t_), but it isn't the case."
                 )
-            else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
+            } else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
           /*
            *    Γ, φ(ψ_) |- Δ
            * ---------------------
@@ -464,7 +463,7 @@ object SCProofChecker {
 
           case SCSubproof(sp, premises, _) =>
             if (premises.size == sp.imports.size) {
-              val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)))
+              val invalid = premises.zipWithIndex.find { case (no, p) => !isSameSequent(ref(no), sp.imports(p)) }
               if (invalid.isEmpty) {
                 checkSCProof(sp)
               } else
@@ -489,12 +488,12 @@ object SCProofChecker {
    */
   def checkSCProof(proof: SCProof): SCProofCheckerJudgement = {
     val possibleError = proof.steps.view.zipWithIndex
-      .map((step, no) =>
+      .map { case (step, no) =>
         checkSingleSCStep(no, step, (i: Int) => proof.getSequent(i), Some(proof.imports.size)) match {
           case SCInvalidProof(_, path, message) => SCInvalidProof(proof, no +: path, message)
           case SCValidProof(_) => SCValidProof(proof)
         }
-      )
+      }
       .find(j => !j.isValid)
     if (possibleError.isEmpty) SCValidProof(proof)
     else possibleError.get
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
similarity index 99%
rename from src/main/scala/lisa/kernel/proof/SequentCalculus.scala
rename to lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index b0209090413502d526e246b059ecba55299f0a1a..15d677b98d8f62a67d696fa03f0ea7d9e861ee3b 100644
--- a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -1,6 +1,6 @@
 package lisa.kernel.proof
 
-import lisa.kernel.fol.FOL.*
+import lisa.kernel.fol.FOL._
 
 import scala.collection.immutable.Set
 
diff --git a/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala b/lisa-theories/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
similarity index 100%
rename from src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
rename to lisa-theories/src/main/scala/lisa/settheory/AxiomaticSetTheory.scala
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
similarity index 97%
rename from src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
rename to lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 8ecbc1f4827e61d04ed46cf0895f7371cf525e71..531076bd52012a2710b36498e0bef0fddd47c2eb 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -2,7 +2,7 @@ package lisa.settheory
 
 import lisa.kernel.fol.FOL._
 import lisa.kernel.proof.RunningTheory
-import utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
 
 /**
  * Base trait for set theoretical axiom systems.
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
similarity index 95%
rename from src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
rename to lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index ec50a16138395644ec1df0238f7c2e7d453fb7b0..72e9bbb4f3d187154ba3e075dff0da932d4d2003 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -1,7 +1,7 @@
 package lisa.settheory
 
 import lisa.kernel.fol.FOL._
-import utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
 
 /**
  * Axioms for the Tarski-Grothendieck theory (TG)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
similarity index 97%
rename from src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
rename to lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 4d1dcbadaefeeca8f5c180b9c4407ec90482faa5..f38aa7b1edd8ee07cd64b0cbb1ce565097bbe8d8 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -2,7 +2,7 @@ package lisa.settheory
 
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
-import utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
 
 /**
  * Axioms for the Zermelo theory (Z)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
similarity index 95%
rename from src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
rename to lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index 4cea73f78a46d2459f81978108cf326cee6d2238..fd0d2b677775f9d5f1963d45ff7d0a53cb3455a0 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -1,7 +1,7 @@
 package lisa.settheory
 
 import lisa.kernel.fol.FOL._
-import utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
 
 /**
  * Axioms for the Zermelo-Fraenkel theory (ZF)
diff --git a/src/main/scala/utilities/tptp/KernelParser.scala b/lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
similarity index 99%
rename from src/main/scala/utilities/tptp/KernelParser.scala
rename to lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
index 215e85d79f370b762bea599561a3a5354b5f9378..df98eeaca2551db85baa408ab1090c01ebb435c3 100644
--- a/src/main/scala/utilities/tptp/KernelParser.scala
+++ b/lisa-tptp/src/main/scala/lisa/tptp/KernelParser.scala
@@ -1,4 +1,4 @@
-package utilities.tptp
+package lisa.tptp
 
 import leo.datastructures.TPTP
 import leo.datastructures.TPTP.CNF
@@ -6,8 +6,8 @@ import leo.datastructures.TPTP.FOF
 import leo.modules.input.TPTPParser as Parser
 import lisa.kernel.fol.FOL as K
 import lisa.kernel.proof.SequentCalculus as LK
-import utilities.Helpers.*
-import utilities.tptp.*
+import lisa.utils.Helpers.*
+import lisa.tptp.*
 
 import java.io.File
 import scala.util.matching.Regex
diff --git a/src/main/scala/utilities/tptp/ProblemGatherer.scala b/lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
similarity index 87%
rename from src/main/scala/utilities/tptp/ProblemGatherer.scala
rename to lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
index ae1df1fa1ff398746d32cced949d37362b5d2db9..8c1278c86bc7e542f5deae796c93496b0b3cdb80 100644
--- a/src/main/scala/utilities/tptp/ProblemGatherer.scala
+++ b/lisa-tptp/src/main/scala/lisa/tptp/ProblemGatherer.scala
@@ -1,6 +1,6 @@
-package utilities.tptp
+package lisa.tptp
 
-import KernelParser._
+import lisa.tptp.KernelParser._
 
 object ProblemGatherer {
 
diff --git a/src/main/scala/utilities/tptp/package.scala b/lisa-tptp/src/main/scala/lisa/tptp/package.scala
similarity index 93%
rename from src/main/scala/utilities/tptp/package.scala
rename to lisa-tptp/src/main/scala/lisa/tptp/package.scala
index 538a2f41aa8e4e89c82905e1b0ce0d5e699ea66d..b59b6938b76333e2fae943ee8ea3e90ac32d07af 100644
--- a/src/main/scala/utilities/tptp/package.scala
+++ b/lisa-tptp/src/main/scala/lisa/tptp/package.scala
@@ -1,4 +1,4 @@
-package utilities.tptp
+package lisa.tptp
 
 import lisa.kernel.fol.FOL as K
 
diff --git a/src/main/scala/utilities/Helpers.scala b/lisa-utils/src/main/scala/lisa/utils/Helpers.scala
similarity index 71%
rename from src/main/scala/utilities/Helpers.scala
rename to lisa-utils/src/main/scala/lisa/utils/Helpers.scala
index a69647319951f6352dc7753a67506d3820927ff2..0b8f82418ff53b04f2149b45bd6164cb84be7b89 100644
--- a/src/main/scala/utilities/Helpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Helpers.scala
@@ -1,4 +1,4 @@
-package utilities
+package lisa.utils
 
 /**
  * A helper file that provides various syntactic sugars for LISA's FOL and proofs.
@@ -7,4 +7,4 @@ package utilities
  * import utilities.Helpers.*
  * </pre>
  */
-object Helpers extends TheoriesHelpers {}
+object Helpers extends TheoriesHelpers
diff --git a/src/main/scala/utilities/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
similarity index 99%
rename from src/main/scala/utilities/KernelHelpers.scala
rename to lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 5dd3793c8aad2a2ddc5529540fa3b699c67ecbfd..6b378f9f7327d4b24b99803111ffaa2620077bb1 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -1,4 +1,4 @@
-package utilities
+package lisa.utils
 
 import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheoryJudgement
diff --git a/src/main/scala/utilities/Library.scala b/lisa-utils/src/main/scala/lisa/utils/Library.scala
similarity index 99%
rename from src/main/scala/utilities/Library.scala
rename to lisa-utils/src/main/scala/lisa/utils/Library.scala
index 18a5fdad92df9753423c714187269c094af5420b..c882e6800f9bbf122c60bdb98faa93e0e1414c07 100644
--- a/src/main/scala/utilities/Library.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Library.scala
@@ -1,4 +1,4 @@
-package utilities
+package lisa.utils
 
 import lisa.kernel.proof.RunningTheory
 
@@ -13,7 +13,7 @@ abstract class Library(val theory: RunningTheory) {
   export lisa.kernel.proof.SequentCalculus.*
   export lisa.kernel.proof.SCProof as Proof
   export theory.{Justification, Theorem, Definition, Axiom, PredicateDefinition, FunctionDefinition}
-  export Helpers.{*, given}
+  export lisa.utils.Helpers.{*, given}
   import lisa.kernel.proof.RunningTheoryJudgement as Judgement
 
   /**
diff --git a/src/main/scala/utilities/Printer.scala b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
similarity index 99%
rename from src/main/scala/utilities/Printer.scala
rename to lisa-utils/src/main/scala/lisa/utils/Printer.scala
index c65ae1e72a57e134b280ded4e9efb0455dc84610..c19f126692a699e4a15b9b2250f2acf8f61f2ec5 100644
--- a/src/main/scala/utilities/Printer.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
@@ -1,4 +1,4 @@
-package utilities
+package lisa.utils
 
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
similarity index 99%
rename from src/main/scala/utilities/TheoriesHelpers.scala
rename to lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
index 6c487530e98569f48f4cf4c028af0050909d7e1e..265bfd7fe2e50e92a44b56f87147a53dd0330689 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
@@ -1,10 +1,10 @@
-package utilities
+package lisa.utils
 
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.*
-import utilities.Printer
+import lisa.utils.Printer
 
 /**
  * A helper file that provides various syntactic sugars for LISA's FOL and proofs. Best imported through utilities.Helpers
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
similarity index 99%
rename from src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
rename to lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index c499619ec8712709280d0e31206fcc5ca0dbb748..fe309785dad9ba3a4e59264c12e4aaa1f2e8672c 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -1,10 +1,10 @@
 package lisa.kernel
 
-import utilities.Printer
+import lisa.utils.Printer
 import lisa.kernel.fol.FOL
 import lisa.kernel.fol.FOL.*
 import org.scalatest.funsuite.AnyFunSuite
-import utilities.Helpers.*
+import lisa.utils.Helpers.*
 
 import scala.collection.MapView
 import scala.collection.mutable.ArrayBuffer
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
similarity index 98%
rename from src/test/scala/lisa/kernel/FolTests.scala
rename to lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
index 42e6caed9f3a9dd861be9db59162238fee6484d7..f4b12ded9e2cf23dbecc2e63386450d66a737779 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,6 +1,6 @@
 package lisa.kernel
 
-import utilities.Printer
+import lisa.utils.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.*
@@ -8,7 +8,7 @@ import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SequentCalculus.*
 import org.scalatest.funsuite.AnyFunSuite
-import utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
 
 import scala.collection.immutable.SortedSet
 import scala.util.Random
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
similarity index 92%
rename from src/test/scala/lisa/kernel/IncorrectProofsTests.scala
rename to lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 3d7aa18bf839e0e322f083663d889198d303b746..786e63add0d36d6b10cd5b3fc4a7ac8876ab0600 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -1,11 +1,10 @@
 package lisa.kernel
 
-//import lisa.settheory.AxiomaticSetTheory.{emptySet, emptySetAxiom, pair, pairAxiom, useAxiom}
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
-import test.ProofCheckerSuite
-import utilities.Helpers.*
+import lisa.test.ProofCheckerSuite
+import lisa.utils.Helpers.*
 
 import scala.collection.immutable.SortedSet
 import scala.language.implicitConversions
@@ -23,9 +22,6 @@ class IncorrectProofsTests extends ProofCheckerSuite {
     val g = PredicateFormula(gl, Seq.empty)
     val h = PredicateFormula(hl, Seq.empty)
 
-    val emptySetAxiom = lisa.settheory.AxiomaticSetTheory.emptySetAxiom
-    val pairAxiom = lisa.settheory.AxiomaticSetTheory.pairAxiom
-
     val incorrectProofs: Seq[SCProof] = List(
       SCProof(
         Hypothesis(emptySeq +< (x === x) +> (x === x), x === x),
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
similarity index 97%
rename from src/test/scala/lisa/kernel/ProofTests.scala
rename to lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
index d5704b084af2fccf9bf8fd0f39e8a7d009cab378..85f9210f4f8e4a1fb1436790c133e3ccb0dccd1d 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,6 +1,6 @@
 package lisa.kernel
 
-import utilities.Printer
+import lisa.utils.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.*
@@ -8,7 +8,7 @@ import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SequentCalculus.*
 import org.scalatest.funsuite.AnyFunSuite
-import utilities.Helpers.{_, given}
+import lisa.utils.Helpers.{_, given}
 
 import scala.util.Random
 
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
similarity index 90%
rename from src/test/scala/test/ProofCheckerSuite.scala
rename to lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
index caaee39fda0749d07d6b38c21e122b36cdd2c422..dcb4fa26edfa53b7cc7fcdd2065487f9f258fe61 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
@@ -1,14 +1,12 @@
-package test
+package lisa.test
 
-import utilities.Printer
+import lisa.utils.Printer
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker._
 import lisa.kernel.proof.SequentCalculus.Sequent
 import lisa.kernel.proof.SequentCalculus.isSameSequent
-import lisa.settheory.AxiomaticSetTheory
 import org.scalatest.funsuite.AnyFunSuite
-import utilities.Helpers._
-import utilities.Helpers.given_Conversion_Boolean_List_String_Option
+import lisa.utils.Helpers.{_, given}
 
 abstract class ProofCheckerSuite extends AnyFunSuite {
   import lisa.kernel.fol.FOL.*
@@ -37,7 +35,6 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
   protected val (sl, tl, ul, vl) = (VariableLabel("s"), VariableLabel("t"), VariableLabel("u"), VariableLabel("v"))
   protected val (s, t, u, v) = (VariableTerm(sl), VariableTerm(tl), VariableTerm(ul), VariableTerm(vl))
 
-  val axioms = AxiomaticSetTheory.axioms
   def checkProof(proof: SCProof): Unit = {
     val judgement = checkSCProof(proof)
     println(Printer.prettySCProof(judgement))
diff --git a/src/test/scala/lisa/kernel/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
similarity index 98%
rename from src/test/scala/lisa/kernel/PrinterTest.scala
rename to lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index 67e91f29c1ca1820f2804de870b44f3359ca0dce..e2675436263d65a009fc3595281effb770cedce1 100644
--- a/src/test/scala/lisa/kernel/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -1,6 +1,6 @@
-package lisa.kernel
+package lisa.utils
 
-import utilities.Printer._
+import lisa.utils.Printer._
 import lisa.kernel.fol.FOL._
 import org.scalatest.funsuite.AnyFunSuite
 
diff --git a/src/main/scala/proven/Main.scala b/src/main/scala/lisa/proven/Main.scala
similarity index 89%
rename from src/main/scala/proven/Main.scala
rename to src/main/scala/lisa/proven/Main.scala
index 7ee72a6ebb51b86c9ec723186368706616c726e3..e69a7102df8c926c334659937f63d76a2305b515 100644
--- a/src/main/scala/proven/Main.scala
+++ b/src/main/scala/lisa/proven/Main.scala
@@ -1,10 +1,10 @@
-package proven
+package lisa.proven
 
 /**
  * The parent trait of all theory files containing mathematical development
  */
 trait Main {
-  export proven.SetTheoryLibrary.{*, given}
+  export lisa.proven.SetTheoryLibrary.{*, given}
 
   private val realOutput: String => Unit = println
   private var outString: List[String] = List()
diff --git a/src/main/scala/proven/SetTheoryLibrary.scala b/src/main/scala/lisa/proven/SetTheoryLibrary.scala
similarity index 69%
rename from src/main/scala/proven/SetTheoryLibrary.scala
rename to src/main/scala/lisa/proven/SetTheoryLibrary.scala
index fd9e5250a1a2bd6ec7ac28ebf4cfd584c46ed590..8045393e04a6df2fef2908d137d31c81a01f8868 100644
--- a/src/main/scala/proven/SetTheoryLibrary.scala
+++ b/src/main/scala/lisa/proven/SetTheoryLibrary.scala
@@ -1,9 +1,9 @@
-package proven
+package lisa.proven
 
 /**
  * Specific implementation of [[utilities.Library]] for Set Theory, with a RunningTheory that is supposed to be used by the standard library.
  */
-object SetTheoryLibrary extends utilities.Library(lisa.settheory.AxiomaticSetTheory.runningSetTheory) {
+object SetTheoryLibrary extends lisa.utils.Library(lisa.settheory.AxiomaticSetTheory.runningSetTheory) {
   val AxiomaticSetTheory: lisa.settheory.AxiomaticSetTheory.type = lisa.settheory.AxiomaticSetTheory
   export AxiomaticSetTheory.*
 
diff --git a/src/main/scala/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala
similarity index 99%
rename from src/main/scala/proven/mathematics/Mapping.scala
rename to src/main/scala/lisa/proven/mathematics/Mapping.scala
index ec6873404f8d4e4b94a4fcc86e7d43956338be57..7267e0c7add9ce057eb8b98795a68f11441bfd05 100644
--- a/src/main/scala/proven/mathematics/Mapping.scala
+++ b/src/main/scala/lisa/proven/mathematics/Mapping.scala
@@ -1,7 +1,7 @@
-package proven.mathematics
+package lisa.proven.mathematics
 
-import proven.tactics.Destructors.*
-import proven.tactics.ProofTactics.*
+import lisa.proven.tactics.Destructors.*
+import lisa.proven.tactics.ProofTactics.*
 
 import SetTheory.*
 
@@ -9,7 +9,7 @@ import SetTheory.*
  * This file contains theorem related to the replacement schema, i.e. how to "map" a set through a functional symbol.
  * Leads to the definition of the cartesian product.
  */
-object Mapping extends proven.Main {
+object Mapping extends lisa.proven.Main {
 
   THEOREM("functionalMapping") of
     "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF {
diff --git a/src/main/scala/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
similarity index 99%
rename from src/main/scala/proven/mathematics/SetTheory.scala
rename to src/main/scala/lisa/proven/mathematics/SetTheory.scala
index add21cfebf996abea27b41f6b3730d6e347d7cfd..22822eb716ee39a060abd33cc3a0992ff657d4d4 100644
--- a/src/main/scala/proven/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
@@ -1,12 +1,12 @@
-package proven.mathematics
+package lisa.proven.mathematics
 
-import proven.tactics.Destructors.*
-import proven.tactics.ProofTactics.*
+import lisa.proven.tactics.Destructors.*
+import lisa.proven.tactics.ProofTactics.*
 
 /**
  * An embryo of mathematical development, containing a few example theorems and the definition of the ordered pair.
  */
-object SetTheory extends proven.Main {
+object SetTheory extends lisa.proven.Main {
 
   THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF {
     val y = SchematicFunctionLabel("y", 0)
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/lisa/proven/tactics/Destructors.scala
similarity index 92%
rename from src/main/scala/proven/tactics/Destructors.scala
rename to src/main/scala/lisa/proven/tactics/Destructors.scala
index 39f2c6cd06d1dec8647e96ae3a19c5726ae52963..f7b978dd03aa4791385229e1dad97d794fcd9e4a 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/lisa/proven/tactics/Destructors.scala
@@ -1,11 +1,11 @@
-package proven.tactics
+package lisa.proven.tactics
 
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.SequentCalculus.*
-import proven.tactics.ProofTactics.hypothesis
-import utilities.Helpers.*
+import lisa.proven.tactics.ProofTactics.hypothesis
+import lisa.utils.Helpers.*
 
 object Destructors {
   def destructRightOr(p: SCProof, a: Formula, b: Formula): SCProof = {
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/lisa/proven/tactics/ProofTactics.scala
similarity index 98%
rename from src/main/scala/proven/tactics/ProofTactics.scala
rename to src/main/scala/lisa/proven/tactics/ProofTactics.scala
index dde13d44e93ce53c4f5b5c94f1e047a7a432b3c0..3567982a354292dbc5265718db827708d4643aaf 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/lisa/proven/tactics/ProofTactics.scala
@@ -1,10 +1,10 @@
-package proven.tactics
+package lisa.proven.tactics
 
+import lisa.utils.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
-import utilities.Helpers.{_, given}
-import utilities.Printer.*
+import lisa.utils.Helpers.{_, given}
 
 import scala.collection.immutable.Set
 
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
similarity index 99%
rename from src/main/scala/proven/tactics/SimplePropositionalSolver.scala
rename to src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
index 69e75d73ac08756a9c2c05181bdcd0a4d780fdb4..a38c006e9abf19de0f1be951ddf13d713644cd68 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
@@ -1,9 +1,9 @@
-package proven.tactics
+package lisa.proven.tactics
 
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
-import utilities.Helpers.*
+import lisa.utils.Helpers.*
 
 import scala.collection.mutable.Set as mSet
 
diff --git a/src/test/scala/lisa/proven/InitialProofsTests.scala b/src/test/scala/lisa/proven/InitialProofsTests.scala
index 331a3f44b312ca7015be8ce472d05ff4660f7c6d..c9873cdc3330c6955052aa3b39503440ffcde208 100644
--- a/src/test/scala/lisa/proven/InitialProofsTests.scala
+++ b/src/test/scala/lisa/proven/InitialProofsTests.scala
@@ -1,18 +1,18 @@
 package lisa.proven
 
-import utilities.Printer
-import test.ProofCheckerSuite
+import lisa.utils.Printer
+import lisa.test.ProofCheckerSuite
 
 class InitialProofsTests extends ProofCheckerSuite {
-  import proven.SetTheoryLibrary.*
+  import lisa.proven.SetTheoryLibrary.*
 
   test("File SetTheory initialize well") {
-    proven.mathematics.SetTheory
+    lisa.proven.mathematics.SetTheory
     succeed
   }
 
   test("File Mapping initialize well") {
-    proven.mathematics.Mapping
+    lisa.proven.mathematics.Mapping
     succeed
   }
 
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 8598562aa8dd742ca7fee37d2314905d9f47c1ba..57599edf48f06045f226e1dac631bb36f33eabc2 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,16 +1,16 @@
 package lisa.proven
 
-import utilities.Printer
-import utilities.Printer.*
+import lisa.utils.Printer
+import lisa.utils.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.PredicateLogic
 import lisa.kernel.proof.SCProofChecker
 import org.scalatest.funsuite.AnyFunSuite
-import proven.tactics.SimplePropositionalSolver as SPS
-import utilities.Helpers.*
-import utilities.tptp.KernelParser.*
-import utilities.tptp.ProblemGatherer.getPRPproblems
+import lisa.proven.tactics.SimplePropositionalSolver as SPS
+import lisa.utils.Helpers.*
+import lisa.tptp.KernelParser.*
+import lisa.tptp.ProblemGatherer.getPRPproblems
 
 class SimpleProverTests extends AnyFunSuite {