diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index 6d4eb4ce0c8aafea649da06f3db79f9f740ded64..8e7eb102fbafd9be5faccbe6144d829251f1cd24 100644
--- a/src/main/scala/Example.scala
+++ b/src/main/scala/Example.scala
@@ -1,4 +1,7 @@
-import lisa.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
+import utilities.tptp.ProblemGatherer.*
+import utilities.tptp.KernelParser.*
+import utilities.tptp.*
 import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
@@ -6,8 +9,6 @@ import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SCProofChecker.*
 import lisa.kernel.proof.SequentCalculus.*
 import proven.tactics.SimplePropositionalSolver.solveSequent
-import tptp.KernelParser.*
-import tptp.ProblemGatherer.getPRPproblems
 
 /**
  * Discover some of the elements of LISA to get started.
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/src/main/scala/lisa/kernel/proof/Judgement.scala
index 6d3abfb7c77dee359cf154351cd7c42cbccc5c85..680d70b42f6d504076b1481848d6f308136d20c7 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -53,7 +53,7 @@ sealed abstract class RunningTheoryJudgement[J <: RunningTheory#Justification] {
   def get: J = this match {
     case ValidJustification(just) => just
     case InvalidJustification(message, error) =>
-      throw new InvalidJustificationException(message, error)
+      throw InvalidJustificationException(message, error)
   }
 }
 
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index a2f3b2b7df8bdaf254183f4adfd25361a490781d..3f630ed232c799316a9fc5cbbdeb0d52db91770e 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -1,8 +1,8 @@
 package lisa.settheory
 
-import lisa.KernelHelpers.{_, given}
 import lisa.kernel.fol.FOL._
 import lisa.kernel.proof.RunningTheory
+import utilities.KernelHelpers.{given, _}
 
 /**
  * Base trait for set theoretical axiom systems.
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index c2bedfa3143a22afd62d46b15b791fa8f9adfd1f..12fcff5c645b5fefcb3a824ff3f24b45a8ab645f 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -1,6 +1,6 @@
 package lisa.settheory
-import lisa.KernelHelpers.{_, given}
 import lisa.kernel.fol.FOL._
+import utilities.KernelHelpers.{given, _}
 
 /**
  * Axioms for the Tarski-Grothendieck theory (TG)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 7c7a7d222e46dc0bd0f1a9ebd96514f272d2ac44..da11ebd906918d378cff11dbb4bb936a886ec022 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -1,8 +1,8 @@
 package lisa.settheory
 
-import lisa.KernelHelpers.{_, given}
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
+import utilities.KernelHelpers.{given, _}
 
 /**
  * Axioms for the Zermelo theory (Z)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index e3648b7ee1a805ddaeb42e2881e6ea911bcbc42a..24271f812566fe17be9c4ccde566a66e13d7876e 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -1,7 +1,7 @@
 package lisa.settheory
 
-import lisa.KernelHelpers.{_, given}
 import lisa.kernel.fol.FOL._
+import utilities.KernelHelpers.{given, _}
 
 /**
  * Axioms for the Zermelo-Fraenkel theory (ZF)
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index b82f09ff37a5b29a9ef59a418ef9d42ad0fe82c2..4a8b0fb2473bf9d4ffae5e1b7be70fdaa0d1a64c 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -1,5 +1,5 @@
 package proven.DSetTheory
-import lisa.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
 import lisa.kernel.Printer
 import lisa.kernel.Printer.prettyFormula
 import lisa.kernel.Printer.prettySCProof
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index 52934b109d6b153840f66e921c5c79eeaad1592d..11aaa0221bd3d55e03ef5dda18291a7b44f7819a 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -1,10 +1,17 @@
 package proven
-import lisa.KernelHelpers.{_, given}
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SequentCalculus.*
+import utilities.KernelHelpers.{*, given}
+import lisa.kernel.Printer
+import proven.tactics.ProofTactics.*
+import proven.tactics.Destructors.*
+import lisa.settheory.AxiomaticSetTheory.*
+
+import scala.collection.immutable.SortedSet
+import lisa.kernel.proof.{SCProof, SCProofChecker}
 import lisa.settheory.AxiomaticSetTheory
 import lisa.settheory.AxiomaticSetTheory.*
 import proven.ElementsOfSetTheory.theory
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 36f53f3f6a5cfc00667e7b91abfec3b9223d0367..396c6caa0f91fc4e3ae91df79816ffacf07c92a7 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -1,7 +1,9 @@
 package proven.tactics
 
-import lisa.KernelHelpers.*
+import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.fol.FOL.*
+import utilities.KernelHelpers.*
+import proven.tactics.ProofTactics.hypothesis
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
 import proven.tactics.ProofTactics.hypothesis
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index 191e77a1a4ba440723959a1e51b0af10be7b2de8..bd90e0a72f69f6cdd721aada6a1a0443aad9f597 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -1,10 +1,11 @@
 package proven.tactics
 
-import lisa.KernelHelpers.{_, given}
 import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
+import utilities.KernelHelpers.{*, given}
+import lisa.kernel.Printer.*
 
 import scala.collection.immutable.Set
 
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
index 50d87de5df78fe040405d32ec84154d76cb71c41..87b85b602d7a0e93f151984deab8b61d8a314533 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
@@ -1,11 +1,12 @@
 package proven.tactics
 
-import lisa.KernelHelpers.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
 
 import scala.collection.mutable.Set as mSet
+import utilities.KernelHelpers.*
+import lisa.kernel.proof.SCProof
 
 /**
  * A simple but complete solver for propositional logic. Will not terminate for large problems
diff --git a/src/main/scala/lisa/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
similarity index 99%
rename from src/main/scala/lisa/KernelHelpers.scala
rename to src/main/scala/utilities/KernelHelpers.scala
index 90be4463658fa0d9a192c6bf5c94d00e48c92196..b55795ff9d53ab1d37fbbda6e7fd569ca1ad1e18 100644
--- a/src/main/scala/lisa/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -1,4 +1,4 @@
-package lisa
+package utilities
 
 /**
  * A helper file that provides various syntactic sugars for LISA.
@@ -9,8 +9,8 @@ package lisa
  */
 object KernelHelpers {
 
-  import lisa.kernel.proof.SequentCalculus.Sequent
   import lisa.kernel.fol.FOL.*
+  import lisa.kernel.proof.SequentCalculus.Sequent
 
   /* Prefix syntax */
 
diff --git a/src/main/scala/tptp/KernelParser.scala b/src/main/scala/utilities/tptp/KernelParser.scala
similarity index 94%
rename from src/main/scala/tptp/KernelParser.scala
rename to src/main/scala/utilities/tptp/KernelParser.scala
index 149453e368f7dd8b3011b8d631c7004c937d60b3..036242c53fb52a7e3a0a35113b468b71419f8f9e 100644
--- a/src/main/scala/tptp/KernelParser.scala
+++ b/src/main/scala/utilities/tptp/KernelParser.scala
@@ -1,12 +1,13 @@
-package tptp
+package utilities.tptp
 
 import leo.datastructures.TPTP
 import leo.datastructures.TPTP.CNF
 import leo.datastructures.TPTP.FOF
+import utilities.tptp.*
 import leo.modules.input.TPTPParser as Parser
-import lisa.KernelHelpers.*
 import lisa.kernel.fol.FOL as K
-import lisa.kernel.proof.SequentCalculus as SK
+import lisa.kernel.proof.SequentCalculus as LK
+import utilities.KernelHelpers.*
 
 import java.io.File
 import scala.util.matching.Regex
@@ -15,12 +16,6 @@ import Parser.TPTPParseException
 
 object KernelParser {
 
-  case class AnnotatedFormula(role: String, name: String, formula: K.Formula)
-
-  case class Problem(file: String, domain: String, name: String, status: String, spc: Seq[String], formulas: Seq[AnnotatedFormula])
-
-  case class FileNotAcceptedException(msg: String, file: String) extends Exception(msg + " File: " + file)
-
   private case class ProblemMetadata(file: String, domain: String, problem: String, status: String, spc: Seq[String])
 
   /**
@@ -152,10 +147,10 @@ object KernelParser {
    * @param problem a problem, containing a list of annotated formulas from a tptp file
    * @return a sequent with axioms of the problem on the left, and the conjecture on the right
    */
-  def problemToSequent(problem: Problem): SK.Sequent = {
+  def problemToSequent(problem: Problem): LK.Sequent = {
     if (problem.spc.contains("CNF")) problem.formulas.map(_.formula) |- ()
     else
-      problem.formulas.foldLeft[SK.Sequent](() |- ())((s, f) =>
+      problem.formulas.foldLeft[LK.Sequent](() |- ())((s, f) =>
         if (f._1 == "axiom") s +< f._3
         else if (f._1 == "conjecture" && s.right.isEmpty) s +> f._3
         else throw Exception("Can only agglomerate axioms and one conjecture into a sequents")
diff --git a/src/main/scala/tptp/ProblemGatherer.scala b/src/main/scala/utilities/tptp/ProblemGatherer.scala
similarity index 89%
rename from src/main/scala/tptp/ProblemGatherer.scala
rename to src/main/scala/utilities/tptp/ProblemGatherer.scala
index 41644e1419b1c3b3a9a76ebd1bd8f5db521e5ece..ae1df1fa1ff398746d32cced949d37362b5d2db9 100644
--- a/src/main/scala/tptp/ProblemGatherer.scala
+++ b/src/main/scala/utilities/tptp/ProblemGatherer.scala
@@ -1,6 +1,6 @@
-package tptp
+package utilities.tptp
 
-import tptp.KernelParser._
+import KernelParser._
 
 object ProblemGatherer {
 
diff --git a/src/main/scala/utilities/tptp/package.scala b/src/main/scala/utilities/tptp/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..538a2f41aa8e4e89c82905e1b0ce0d5e699ea66d
--- /dev/null
+++ b/src/main/scala/utilities/tptp/package.scala
@@ -0,0 +1,9 @@
+package utilities.tptp
+
+import lisa.kernel.fol.FOL as K
+
+case class AnnotatedFormula(role: String, name: String, formula: K.Formula)
+
+case class Problem(file: String, domain: String, name: String, status: String, spc: Seq[String], formulas: Seq[AnnotatedFormula])
+
+case class FileNotAcceptedException(msg: String, file: String) extends Exception(msg + " File: " + file)
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index f8ee2a8cce949bde472c35ccf6255b72bf3af0ca..518ce3f9d2897d668fccc041227fdeb00987b591 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -1,6 +1,6 @@
 package lisa.kernel
 
-import lisa.KernelHelpers.*
+import utilities.KernelHelpers.*
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL
 import lisa.kernel.fol.FOL.*
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
index 8f02688c47d5fd1ac6b438ca7dd967bc50d5f16f..615d58e1954d3db2f8611d49e83e011579860c07 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,6 +1,6 @@
 package lisa.kernel
 
-import lisa.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 9259274b6e5edeaf0fc0fd9f6b297d811c70824a..213336b64dc14311d269d0dd3d60fa38e85ae10d 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -1,7 +1,7 @@
 package lisa.kernel
 
 //import lisa.settheory.AxiomaticSetTheory.{emptySet, emptySetAxiom, pair, pairAxiom, useAxiom}
-import lisa.KernelHelpers.*
+import utilities.KernelHelpers.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index 07b5a3a0718138d44c59d7c990589cdb748d89d8..b132433709c7dcca2d70a11e90a23b361eb51a59 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,6 +1,6 @@
 package lisa.kernel
 
-import lisa.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index 98ade22df1a34052e455ad71246b4d26573dfec0..fde50ed0fa44ab306a93559c5912e1749389057f 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -1,10 +1,11 @@
 package proven
 
-import lisa.KernelHelpers.{_, given}
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.fol.FOL.*
+import utilities.KernelHelpers.{*, given}
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.settheory.AxiomaticSetTheory.*
 import proven.ElementsOfSetTheory.*
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 9731249f967d98ba67d54776dfbdb3990f48774b..05bd4c4ab2614490e20ac5444ac4619c760eb90d 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,6 +1,6 @@
 package proven
 
-import lisa.KernelHelpers.*
+import utilities.KernelHelpers.*
 import lisa.kernel.Printer
 import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
@@ -8,9 +8,9 @@ import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.PredicateLogic
 import lisa.kernel.proof.SCProofChecker
 import org.scalatest.funsuite.AnyFunSuite
+import utilities.tptp.ProblemGatherer.getPRPproblems
+import utilities.tptp.KernelParser.*
 import proven.tactics.SimplePropositionalSolver as SPS
-import tptp.KernelParser.*
-import tptp.ProblemGatherer.getPRPproblems
 
 class SimpleProverTests extends AnyFunSuite {
 
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index 8a5961861d983936260560f92ababa61b462ef2d..08d91983ff5457771008de72604cb0208888b9ba 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -1,7 +1,5 @@
 package test
 
-import lisa.KernelHelpers._
-import lisa.KernelHelpers.given_Conversion_Boolean_List_String_Option
 import lisa.kernel.Printer
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker._
@@ -9,6 +7,9 @@ import lisa.kernel.proof.SequentCalculus.Sequent
 import lisa.kernel.proof.SequentCalculus.isSameSequent
 import lisa.settheory.AxiomaticSetTheory
 import org.scalatest.funsuite.AnyFunSuite
+import lisa.kernel.proof.SCProof
+import utilities.KernelHelpers._
+import utilities.KernelHelpers.given_Conversion_Boolean_List_String_Option
 
 abstract class ProofCheckerSuite extends AnyFunSuite {
   import lisa.kernel.fol.FOL.*