diff --git a/.gitignore b/.gitignore
index b05d0969a..90ddd1034 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,7 +2,7 @@
 .idea
 .metals
 .vscode
-project/metals.sbt
+*/metals.sbt
 
 # build-related
 .bsp
@@ -22,3 +22,9 @@ cache
 
 # emacs backup files
 *~
+
+# data extracted
+data_extract
+
+# TPTP data
+lisa-utils/src/main/resources
diff --git a/build.sbt b/build.sbt
index 8178b5599..9a25d67a1 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,4 +1,4 @@
-ThisBuild / version      := "0.6"
+ThisBuild / version := "0.6"
 ThisBuild / homepage := Some(url("https://github.com/epfl-lara/lisa"))
 ThisBuild / startYear := Some(2021)
 ThisBuild / organization := "ch.epfl.lara"
@@ -7,24 +7,20 @@ ThisBuild / organizationHomepage := Some(url("https://lara.epfl.ch"))
 ThisBuild / licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html"))
 ThisBuild / versionScheme := Some("semver-spec")
 ThisBuild / scalacOptions ++= Seq(
-      "-feature",
-      "-deprecation",
-      "-unchecked",
-    )
+  "-feature",
+  "-deprecation",
+  "-unchecked"
+)
 ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8")
 ThisBuild / semanticdbEnabled := true
 ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
 ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
 
-
-
-
 val commonSettings = Seq(
   crossScalaVersions := Seq("2.12.13", "2.13.4", "3.0.1", "3.2.0"),
   run / fork := true
 )
 
-
 val scala2 = "2.13.8"
 val scala3 = "3.3.1"
 
@@ -35,14 +31,15 @@ val commonSettings2 = commonSettings ++ Seq(
 val commonSettings3 = commonSettings ++ Seq(
   scalaVersion := scala3,
   scalacOptions ++= Seq(
-    "-language:implicitConversions",
+    "-language:implicitConversions"
 
     // "-source:future", re-enable when liancheng/scalafix-organize-imports#221 is fixed
 
   ),
   libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test",
   libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.3.0",
-  //libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
+  libraryDependencies += "com.lihaoyi" %% "ujson" % "3.1.0",
+  // libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
   libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13),
   Test / parallelExecution := false
 )
@@ -56,13 +53,13 @@ lazy val scallion = githubProject("https://github.com/sankalpgambhir/scallion.gi
 
 lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8670a5fa8ea2dd5649a00424710274a5d18")
 
-scallion/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
-silex/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
+scallion / scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
+silex / scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
 
 lazy val root = Project(
-    id = "lisa",
-    base = file(".")
-  )
+  id = "lisa",
+  base = file(".")
+)
   .settings(commonSettings3)
   .dependsOn(kernel, withTests(utils), withTests(sets)) // Everything but `examples`
   .aggregate(utils) // To run tests on all modules
@@ -87,7 +84,6 @@ lazy val utils = Project(
   id = "lisa-utils",
   base = file("lisa-utils")
 )
-
   .settings(commonSettings3)
   .dependsOn(kernel)
   .dependsOn(silex)
@@ -104,7 +100,6 @@ ThisBuild / assemblyMergeStrategy := {
     oldStrategy(x)
 }
 
-
 lazy val examples = Project(
   id = "lisa-examples",
   base = file("lisa-examples")
diff --git a/lisa-examples/src/main/scala/Kernel2Code.scala b/lisa-examples/src/main/scala/Kernel2Code.scala
new file mode 100644
index 000000000..e3f4690ac
--- /dev/null
+++ b/lisa-examples/src/main/scala/Kernel2Code.scala
@@ -0,0 +1,328 @@
+import lisa.automation.Tableau
+import lisa.utils.ProofsConverter.*
+import lisa.utils.parsing.ProofPrinter._
+import lisa.utils.FOLPrinter.*
+import lisa.utils.ProofsShrink.*
+
+object Kernel2Code extends lisa.Main {
+
+  val x = variable
+  val y = variable
+  val f = function[1]
+  val Q = predicate[1]
+  val R = predicate[1]
+  val S = predicate[2]
+
+  val x_1 = variable
+  val x_2 = variable
+  val y_1 = variable
+  val MaRvIn_1 = formulaVariable
+
+  // A standard theorem about reordering quantifiers. Does the converse hold?
+  val thm1 = Theorem(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) {
+    have(S(x, y) |- S(x, y)) by Restate
+    thenHave(∀(y, S(x, y)) |- S(x, y)) by LeftForall
+    thenHave(∀(y, S(x, y)) |- ∃(x, S(x, y))) by RightExists
+    thenHave(∃(x, ∀(y, S(x, y))) |- ∃(x, S(x, y))) by LeftExists
+    thenHave(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) by RightForall
+  }
+
+  // println(generateStandaloneTheoremFileContent("thm1_raw", thm1.kernelProof.get))
+  // println(generateStandaloneTheoremFileContent("thm1_optimized", optimizeProofIteratively(thm1.kernelProof.get)))
+
+  val thm1_raw = Theorem(
+    ∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
+  ) {
+    val s_0 = have(S(x, y) ⊢ S(x, y)) subproof {
+      val s_0_0 = have(S(x, y) ⊢ S(x, y)) by Restate
+    }
+    val s_1 = have(∀(y, S(x, y)) ⊢ S(x, y)) subproof {
+      val s_1_0 = have(∀(y, S(x, y)) ⊢ S(x, y)) by LeftForall(s_0)
+    }
+    val s_2 = have(∀(y, S(x, y)) ⊢ ∃(x, S(x, y))) subproof {
+      val s_2_0 = have(∀(y, S(x, y)) ⊢ ∃(x, S(x, y))) by RightExists(s_1)
+    }
+    val s_3 = have(∃(x, ∀(y, S(x, y))) ⊢ ∃(x, S(x, y))) subproof {
+      val s_3_0 = have(∃(x, ∀(y, S(x, y))) ⊢ ∃(x, S(x, y))) by LeftExists(s_2)
+    }
+    val s_4 = have(∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))) subproof {
+      val s_4_0 = have(∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))) by RightForall(s_3)
+    }
+  }
+
+  val thm1_optimized = Theorem(
+    ∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
+  ) {
+    val s_0 = have(S(x, y) ⊢ S(x, y)) by Restate
+    val s_1 = thenHave(∀(y, S(x, y)) ⊢ S(x, y)) by LeftForall
+    val s_2 = thenHave(∀(y, S(x, y)) ⊢ ∃(x, S(x, y))) by RightExists
+    val s_3 = thenHave(∃(x, ∀(y, S(x, y))) ⊢ ∃(x, S(x, y))) by LeftExists
+    val s_4 = thenHave(∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))) by RightForall
+  }
+
+  // A standard and important property of ∀: It distributes over conjunction. This is useful to justify prenex normal form.
+  val thm2 = Theorem((∀(x, Q(x)) /\ ∀(x, R(x))) <=> ∀(x, Q(x) /\ R(x))) {
+
+    // Here we prove the two directions of <=> separately and then combine them.
+    val forward = have((∀(x, Q(x)), ∀(x, R(x))) |- ∀(x, Q(x) /\ R(x))) subproof {
+      have((Q(x), R(x)) |- Q(x) /\ R(x)) by Restate
+      thenHave((∀(x, Q(x)), R(x)) |- Q(x) /\ R(x)) by LeftForall
+      thenHave((∀(x, Q(x)), ∀(x, R(x))) |- Q(x) /\ R(x)) by LeftForall
+      thenHave(thesis) by RightForall
+    }
+
+    // The second direction
+    val backward = have(∀(x, Q(x) /\ R(x)) |- ∀(x, Q(x)) /\ ∀(x, R(x))) subproof {
+      assume(∀(x, Q(x) /\ R(x)))
+      val assump = have(Q(x) /\ R(x)) by InstantiateForall
+      have(Q(x)) by Weakening(assump)
+      val conj1 = thenHave(∀(x, Q(x))) by RightForall
+      have(R(x)) by Weakening(assump)
+      val conj2 = thenHave(∀(x, R(x))) by RightForall
+      have(thesis) by Tautology.from(conj1, conj2)
+    }
+
+    have(thesis) by Tautology.from(forward, backward)
+  }
+
+  // println(generateStandaloneTheoremFileContent("thm2_raw", thm2.kernelProof.get))
+  // println(generateStandaloneTheoremFileContent("thm2_optimized", optimizeProofIteratively(thm2.kernelProof.get)))
+
+  val thm2_raw = Theorem(
+    ((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))
+  ) {
+    val s_0 = have((∀(x, R(x)), ∀(x, Q(x))) ⊢ ∀(x, (Q(x) ∧ R(x)))) subproof {
+      val s_0_0 = have((R(x), Q(x)) ⊢ (Q(x) ∧ R(x))) subproof {
+        val s_0_0_0 = have((R(x), Q(x)) ⊢ (Q(x) ∧ R(x))) by Restate
+      }
+      val s_0_1 = have((R(x), ∀(x, Q(x))) ⊢ (Q(x) ∧ R(x))) subproof {
+        val s_0_1_0 = have((R(x), ∀(x, Q(x))) ⊢ (Q(x) ∧ R(x))) by LeftForall(s_0_0)
+      }
+      val s_0_2 = have((∀(x, R(x)), ∀(x, Q(x))) ⊢ (Q(x) ∧ R(x))) subproof {
+        val s_0_2_0 = have((∀(x, R(x)), ∀(x, Q(x))) ⊢ (Q(x) ∧ R(x))) by LeftForall(s_0_1)
+      }
+      val s_0_3 = have((∀(x, R(x)), ∀(x, Q(x))) ⊢ ∀(x, (Q(x) ∧ R(x)))) subproof {
+        val s_0_3_0 = have((∀(x, R(x)), ∀(x, Q(x))) ⊢ ∀(x, (Q(x) ∧ R(x)))) by RightForall(s_0_2)
+      }
+      val s_0_4 = thenHave((∀(x, R(x)), ∀(x, Q(x))) ⊢ ∀(x, (Q(x) ∧ R(x)))) by Restate
+    }
+    val s_1 = have(∀(x, (Q(x) ∧ R(x))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) subproof {
+      val s_1_0 = have(∀(x, (Q(x) ∧ R(x))) ⊢ ∀(x, (Q(x) ∧ R(x)))) subproof {
+        val s_1_0_0 = have(∀(x, (Q(x) ∧ R(x))) ⊢ ∀(x, (Q(x) ∧ R(x)))) by Hypothesis
+      }
+      val s_1_1 = have(∀(x, (Q(x) ∧ R(x))) ⊢ (Q(x) ∧ R(x))) subproof {
+        val s_1_1_0 = have((∀(x, (Q(x) ∧ R(x))), (Q(x) ∧ R(x))) ⊢ (Q(x) ∧ R(x))) subproof {
+          val s_1_1_0_0 = have((∀(x, (Q(x) ∧ R(x))), (Q(x) ∧ R(x))) ⊢ (Q(x) ∧ R(x))) by Restate
+        }
+        val s_1_1_1 = have(∀(x, (Q(x) ∧ R(x))) ⊢ (Q(x) ∧ R(x))) subproof {
+          val s_1_1_1_0 = have(∀(x, (Q(x) ∧ R(x))) ⊢ (Q(x) ∧ R(x))) by LeftForall(s_1_1_0)
+        }
+      }
+      val s_1_2 = have(∀(x, (Q(x) ∧ R(x))) ⊢ Q(x)) subproof {
+        val s_1_2_0 = have(∀(x, (Q(x) ∧ R(x))) ⊢ Q(x)) by Weakening(s_1_1)
+      }
+      val s_1_3 = have(∀(x, (Q(x) ∧ R(x))) ⊢ ∀(x, Q(x))) subproof {
+        val s_1_3_0 = have(∀(x, (Q(x) ∧ R(x))) ⊢ ∀(x, Q(x))) by RightForall(s_1_2)
+      }
+      val s_1_4 = have(∀(x, (Q(x) ∧ R(x))) ⊢ R(x)) subproof {
+        val s_1_4_0 = have(∀(x, (Q(x) ∧ R(x))) ⊢ R(x)) by Weakening(s_1_1)
+      }
+      val s_1_5 = have(∀(x, (Q(x) ∧ R(x))) ⊢ ∀(x, R(x))) subproof {
+        val s_1_5_0 = have(∀(x, (Q(x) ∧ R(x))) ⊢ ∀(x, R(x))) by RightForall(s_1_4)
+      }
+      val s_1_6 = have(∀(x, (Q(x) ∧ R(x))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) subproof {
+        val s_1_6_0 = have((∀(x, (Q(x) ∧ R(x))) ==> ∀(x, Q(x)))) by Restate.from(s_1_3)
+        val s_1_6_1 = have((∀(x, (Q(x) ∧ R(x))) ==> ∀(x, R(x)))) by Restate.from(s_1_5)
+        val s_1_6_2 = have((∀(x, (Q(x) ∧ R(x))), (∀(x, (Q(x) ∧ R(x))) ==> ∀(x, Q(x))), (∀(x, (Q(x) ∧ R(x))) ==> ∀(x, R(x)))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) subproof {
+          val s_1_6_2_0 = have(⊤) by Restate
+          val s_1_6_2_1 = thenHave((∀(x, (Q(x) ∧ R(x))), (∀(x, (Q(x) ∧ R(x))) ==> ∀(x, Q(x))), (∀(x, (Q(x) ∧ R(x))) ==> ∀(x, R(x)))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) by Restate
+        }
+        val s_1_6_3 = have((∀(x, (Q(x) ∧ R(x))), (∀(x, (Q(x) ∧ R(x))) ==> ∀(x, R(x)))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) by Cut(s_1_6_0, s_1_6_2)
+        val s_1_6_4 = have(∀(x, (Q(x) ∧ R(x))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) by Cut(s_1_6_1, s_1_6_3)
+      }
+      val s_1_7 = thenHave(∀(x, (Q(x) ∧ R(x))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) by Restate
+    }
+    val s_2 = have(((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))) subproof {
+      val s_2_0 = have(((∀(x, R(x)) ∧ ∀(x, Q(x))) ==> ∀(x, (Q(x) ∧ R(x))))) by Restate.from(s_0)
+      val s_2_1 = have((∀(x, (Q(x) ∧ R(x))) ==> (∀(x, Q(x)) ∧ ∀(x, R(x))))) by Restate.from(s_1)
+      val s_2_2 = have((((∀(x, R(x)) ∧ ∀(x, Q(x))) ==> ∀(x, (Q(x) ∧ R(x)))), (∀(x, (Q(x) ∧ R(x))) ==> (∀(x, Q(x)) ∧ ∀(x, R(x))))) ⊢ ((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))) subproof {
+        val s_2_2_0 = have(⊤) by Restate
+        val s_2_2_1 =
+          thenHave((((∀(x, R(x)) ∧ ∀(x, Q(x))) ==> ∀(x, (Q(x) ∧ R(x)))), (∀(x, (Q(x) ∧ R(x))) ==> (∀(x, Q(x)) ∧ ∀(x, R(x))))) ⊢ ((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))) by Restate
+      }
+      val s_2_3 = have((∀(x, (Q(x) ∧ R(x))) ==> (∀(x, Q(x)) ∧ ∀(x, R(x)))) ⊢ ((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))) by Cut(s_2_0, s_2_2)
+      val s_2_4 = have(((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))) by Cut(s_2_1, s_2_3)
+    }
+  }
+
+  val thm2_optimized = Theorem(
+    ((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))
+  ) {
+    val s_0 = have((R(x), Q(x)) ⊢ (Q(x) ∧ R(x))) by Restate
+    val s_1 = thenHave((R(x), ∀(x, Q(x))) ⊢ (Q(x) ∧ R(x))) by LeftForall
+    val s_2 = thenHave((∀(x, R(x)), ∀(x, Q(x))) ⊢ (Q(x) ∧ R(x))) by LeftForall
+    val s_3 = thenHave((∀(x, R(x)), ∀(x, Q(x))) ⊢ ∀(x, (Q(x) ∧ R(x)))) by RightForall
+    val s_4 = have((∀(x, (Q(x) ∧ R(x))), (Q(x) ∧ R(x))) ⊢ (Q(x) ∧ R(x))) by Restate
+    val s_5 = thenHave(∀(x, (Q(x) ∧ R(x))) ⊢ (Q(x) ∧ R(x))) by LeftForall
+    val s_6 = thenHave(∀(x, (Q(x) ∧ R(x))) ⊢ Q(x)) by Weakening
+    val s_7 = thenHave(∀(x, (Q(x) ∧ R(x))) ⊢ ∀(x, Q(x))) by RightForall
+    val s_8 = have(∀(x, (Q(x) ∧ R(x))) ⊢ R(x)) by Weakening(s_5)
+    val s_9 = thenHave(∀(x, (Q(x) ∧ R(x))) ⊢ ∀(x, R(x))) by RightForall
+    val s_10 = have((∀(x, (Q(x) ∧ R(x))) ==> ∀(x, Q(x)))) by Restate.from(s_7)
+    val s_11 = have((∀(x, (Q(x) ∧ R(x))) ==> ∀(x, R(x)))) by Restate.from(s_9)
+    val s_12 = have(⊤) by Restate
+    val s_13 = thenHave((∀(x, (Q(x) ∧ R(x))), (∀(x, (Q(x) ∧ R(x))) ==> ∀(x, Q(x))), (∀(x, (Q(x) ∧ R(x))) ==> ∀(x, R(x)))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) by Restate
+    val s_14 = have((∀(x, (Q(x) ∧ R(x))), (∀(x, (Q(x) ∧ R(x))) ==> ∀(x, R(x)))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) by Cut(s_10, s_13)
+    val s_15 = have(∀(x, (Q(x) ∧ R(x))) ⊢ (∀(x, Q(x)) ∧ ∀(x, R(x)))) by Cut(s_11, s_14)
+    val s_16 = have(((∀(x, R(x)) ∧ ∀(x, Q(x))) ==> ∀(x, (Q(x) ∧ R(x))))) by Restate.from(s_3)
+    val s_17 = have((∀(x, (Q(x) ∧ R(x))) ==> (∀(x, Q(x)) ∧ ∀(x, R(x))))) by Restate.from(s_15)
+    val s_18 =
+      have((((∀(x, R(x)) ∧ ∀(x, Q(x))) ==> ∀(x, (Q(x) ∧ R(x)))), (∀(x, (Q(x) ∧ R(x))) ==> (∀(x, Q(x)) ∧ ∀(x, R(x))))) ⊢ ((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))) by Restate.from(s_12)
+    val s_19 = have((∀(x, (Q(x) ∧ R(x))) ==> (∀(x, Q(x)) ∧ ∀(x, R(x)))) ⊢ ((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))) by Cut(s_16, s_18)
+    val s_20 = have(((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))) by Cut(s_17, s_19)
+  }
+
+  // This theorem requires instantiating the assumption twice, once with x and once with f(x), and then combine the two.
+  // Since x is free is the sequent step1, then step 1 is true with anything substituted for x.
+  // We can do such substitution with the "of" keyword.
+  // Specifically, `step1 of (x := f(x))` proves the formula P(f(x)) ==> P(f(f(x)))
+  val thm3 = Theorem(∀(x, Q(x) ==> Q(f(x))) |- Q(x) ==> Q(f(f(x)))) {
+    assume(∀(x, Q(x) ==> Q(f(x))))
+    val step1 = have(Q(x) ==> Q(f(x))) by InstantiateForall
+    have(thesis) by Tautology.from(step1, step1 of (x := f(x)))
+  }
+
+  // println(generateStandaloneTheoremFileContent("thm3_raw", thm3.kernelProof.get))
+  // println(generateStandaloneTheoremFileContent("thm3_optimized", optimizeProofIteratively(thm3.kernelProof.get)))
+
+  val thm3_raw = Theorem(
+    ∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))
+  ) {
+    val s_0 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ ∀(x, (Q(x) ==> Q(f(x))))) subproof {
+      val s_0_0 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ ∀(x, (Q(x) ==> Q(f(x))))) by Hypothesis
+    }
+    val s_1 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) subproof {
+      val s_1_0 = have((∀(x, (Q(x) ==> Q(f(x)))), (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) subproof {
+        val s_1_0_0 = have((∀(x, (Q(x) ==> Q(f(x)))), (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) by Restate
+      }
+      val s_1_1 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) subproof {
+        val s_1_1_0 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) by LeftForall(s_1_0)
+      }
+    }
+    val s_2 = have(∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ⊢ (Q(f(x)) ==> Q(f(f(x))))) subproof {
+      val s_2_0 = have(∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ⊢ (Q(f(x)) ==> Q(f(f(x))))) by InstFunSchema(Map(x -> f(x)))(s_1)
+      val s_2_1 = have(∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ⊢ (Q(f(x)) ==> Q(f(f(x))))) by InstFunSchema(Map(x -> f(x)))(s_1)
+    }
+    val s_3 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))) subproof {
+      val s_3_0 = have((∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x))))) by Restate.from(s_1)
+      val s_3_1 = have((∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) by Restate.from(s_2)
+      val s_3_2 = have((∀(x, (Q(x) ==> Q(f(x)))), (∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) subproof {
+        val s_3_2_0 = have(
+          Q(f(x)) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊤ ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(⊤))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+        ) by Restate
+        val s_3_2_1 = thenHave(
+          Q(f(x)) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+        ) by RightSubstIff.withParametersSimple(
+          List(((Q(f(x))), (⊤))),
+          lambda(
+            Seq(MaRvIn_1),
+            ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ MaRvIn_1 ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(MaRvIn_1))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+          )
+        )
+        val s_3_2_2 = have(
+          ¬(Q(f(x))) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊥ ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(⊥))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+        ) by Restate
+        val s_3_2_3 = thenHave(
+          ¬(Q(f(x))) ⊢ ¬(
+            (¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x)))))
+          )
+        ) by RightSubstIff.withParametersSimple(
+          List(((Q(f(x))), (⊥))),
+          lambda(
+            Seq(MaRvIn_1),
+            ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ MaRvIn_1 ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(MaRvIn_1))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+          )
+        )
+        val s_3_2_4 = thenHave(
+          () ⊢ (Q(f(x)), ¬(
+            (¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x)))))
+          ))
+        ) by Restate
+        val s_3_2_5 = have(
+          ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+        ) by Cut(s_3_2_4, s_3_2_1)
+        val s_3_2_6 = thenHave(
+          ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+        ) by Restate
+        val s_3_2_7 =
+          thenHave((∀(x, (Q(x) ==> Q(f(x)))), (∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) by Restate
+      }
+      val s_3_3 = have((∀(x, (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) by Cut(s_3_0, s_3_2)
+      val s_3_4 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))) by Cut(s_3_1, s_3_3)
+    }
+  }
+
+  val thm3_optimized = Theorem(
+    ∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))
+  ) {
+    val s_0 = have((∀(x, (Q(x) ==> Q(f(x)))), (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) by Restate
+    val s_1 = thenHave(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) by LeftForall
+    val s_2 = thenHave(∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ⊢ (Q(f(x)) ==> Q(f(f(x))))) by InstFunSchema(Map(x -> f(x)))
+    val s_3 = have((∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x))))) by Restate.from(s_1)
+    val s_4 = have((∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) by Restate.from(s_2)
+    val s_5 = have(
+      Q(f(x)) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊤ ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(⊤))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+    ) by Restate
+    val s_6 = thenHave(
+      Q(f(x)) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+    ) by Restate
+    val s_7 = have(
+      ¬(Q(f(x))) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊥ ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(⊥))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+    ) by Restate
+    val s_8 = thenHave(
+      () ⊢ (Q(f(x)), ¬(
+        (¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x)))))
+      ))
+    ) by Restate
+    val s_9 = have(
+      ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+    ) by Cut(s_8, s_6)
+    val s_10 = thenHave((∀(x, (Q(x) ==> Q(f(x)))), (∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) by Restate
+    val s_11 = have((∀(x, (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) by Cut(s_3, s_10)
+    val s_12 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))) by Cut(s_4, s_11)
+  }
+
+  val thm1bis = Theorem(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) {
+    have(thesis) by Tableau
+  }
+
+  // println(generateStandaloneTheoremFileContent("thm1bis_raw", thm1bis.kernelProof.get))
+  // println(generateStandaloneTheoremFileContent("thm1bis_optimized", optimizeProofIteratively(thm1bis.kernelProof.get)))
+
+  val thm1bis_raw = Theorem(
+    ∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
+  ) {
+    val s_0 = have(∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))) subproof {
+      val s_0_0 = have((S(x, y_1), ¬(S(x, y_1))) ⊢ ()) by Restate
+      val s_0_1 = thenHave((S(x, y_1), ∀(x_2, ¬(S(x_2, y_1)))) ⊢ ()) by LeftForall
+      val s_0_2 = thenHave((∀(x_2, ¬(S(x_2, y_1))), ∀(y, S(x, y))) ⊢ ()) by LeftForall
+      val s_0_3 = thenHave((∀(x_2, ¬(S(x_2, y_1))), ∃(x, ∀(y, S(x, y)))) ⊢ ()) by LeftExists
+      val s_0_4 = thenHave((∃(x, ∀(y, S(x, y))), ∃(y_1, ∀(x_2, ¬(S(x_2, y_1))))) ⊢ ()) by LeftExists
+      val s_0_5 = thenHave((∃(x, ∀(y, S(x, y))) ∧ ∃(y_1, ∀(x_2, ¬(S(x_2, y_1))))) ⊢ ()) by Weakening
+      val s_0_6 = thenHave((∃(x, ∀(y, S(x, y))) ∧ ∃(y_1, ∀(x_2, ¬(S(x_2, y_1))))) ⊢ ()) by Weakening
+      val s_0_7 = thenHave(∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))) by Restate
+    }
+  }
+
+  val thm1bis_optimized = Theorem(
+    ∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
+  ) {
+    val s_0 = have((S(x, y_1), ¬(S(x, y_1))) ⊢ ()) by Restate
+    val s_1 = thenHave((S(x, y_1), ∀(x_2, ¬(S(x_2, y_1)))) ⊢ ()) by LeftForall
+    val s_2 = thenHave((∀(x_2, ¬(S(x_2, y_1))), ∀(y, S(x, y))) ⊢ ()) by LeftForall
+    val s_3 = thenHave((∀(x_2, ¬(S(x_2, y_1))), ∃(x, ∀(y, S(x, y)))) ⊢ ()) by LeftExists
+    val s_4 = thenHave((∃(x, ∀(y, S(x, y))), ∃(y_1, ∀(x_2, ¬(S(x_2, y_1))))) ⊢ ()) by LeftExists
+    val s_5 = thenHave(∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))) by Restate
+  }
+
+}
diff --git a/lisa-examples/src/main/scala/TPTPSolver.scala b/lisa-examples/src/main/scala/TPTPSolver.scala
new file mode 100644
index 000000000..3820def23
--- /dev/null
+++ b/lisa-examples/src/main/scala/TPTPSolver.scala
@@ -0,0 +1,135 @@
+import java.io.File
+import java.io.FileWriter
+
+import scala.concurrent.duration._
+
+import lisa.utils.ProofsConverter.*
+import lisa.utils.RunSolver.*
+import lisa.utils.tptp.*
+import lisa.utils.tptp.KernelParser.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.utils.ProofsShrink.optimizeProofIteratively
+
+// TODO: separate axioms and definitions from the main sequent and give names to hypotheses
+
+object TPTPSolver extends lisa.Main {
+  sealed trait ProofType
+  case object BySolver extends ProofType
+  case object Kernel extends ProofType
+  case object KernelOptimized extends ProofType
+
+  class ProblemSolverResults(val problem: Problem, val solverName: String, val solverStatus: String, val proofCode: String, val proofType: ProofType)
+
+  val spc = Seq("PRP", "FOF") // type of problems we want to extract and solve
+
+  // We limit the execution time to solve each problem
+  val timeoutTableau = .1.second
+  val timeoutTautology = .1.second
+
+  val exportOnlySolvedProblems = true
+  val exportOptimizedProofs = true
+  val exportBySolverProofs = true
+
+  val jsonResultsPath: String = null
+  if (jsonResultsPath == null) throw new Exception("Please specify a path for the JSON results file")
+  val TPTPProblemPath: String = null
+  if (TPTPProblemPath == null) throw new Exception("Please specify a path for the TPTP problems")
+
+  val d = new File(TPTPProblemPath)
+  val libraries = d.listFiles.filter(_.isDirectory)
+  val probfiles = libraries.flatMap(_.listFiles).filter(_.isFile)
+
+  // val d = new File(TPTPProblemPath + "SYN/")
+  // val probfiles = d.listFiles.filter(_.isFile)
+
+  var nbProblemsExtracted = 0
+  var nbProblemsSolved = Map("Tableau" -> 0, "Tautology" -> 0)
+  var nbInvalidProofs = Map("Tableau" -> 0, "Tautology" -> 0)
+  var results = Seq.empty[ProblemSolverResults]
+
+  for ((probfile, i) <- probfiles.zipWithIndex) {
+    // Progress bar
+    if ((i + 1) % 10 == 0 || i + 1 == probfiles.size) {
+      val pbarLength = 20
+      var pbarContent = "=" * (((i + 1) * pbarLength) / probfiles.size)
+      pbarContent += " " * (pbarLength - pbarContent.length)
+      print(s"[$pbarContent]")
+      print(s" -- ${i + 1}/${probfiles.size} processed files")
+      print(s" -- $nbProblemsExtracted extracted problems")
+      print(s" -- Tableau: ${nbProblemsSolved("Tableau")} solved + ${nbInvalidProofs("Tableau")} invalid")
+      println(s" -- Tautology: ${nbProblemsSolved("Tautology")} solved + ${nbInvalidProofs("Tautology")} invalid")
+    }
+
+    // Try to extract and solve the problem
+    try {
+      val md = getProblemInfos(probfile)
+      if (!(md.spc.contains("SAT"))) {
+        if (md.spc.exists(spc.contains)) {
+          val problem = problemToKernel(probfile, md)
+          val seq = problemToSequent(problem)
+          nbProblemsExtracted += 1
+
+          def exportResults(problem: Problem, solverName: String, solverResult: SolverResult): Unit =
+            val solverStatus = solverResult.getClass.getSimpleName.stripSuffix("$")
+            solverResult match
+              case Solved(proof) =>
+                nbProblemsSolved += (solverName -> (nbProblemsSolved(solverName) + 1))
+                results :+= new ProblemSolverResults(problem, solverName, solverStatus, generateStandaloneTheoremFileContent(problem.name, proof), Kernel)
+                if (exportOptimizedProofs)
+                  results :+= new ProblemSolverResults(problem, solverName, solverStatus, generateStandaloneTheoremFileContent(problem.name, optimizeProofIteratively(proof)), KernelOptimized)
+                if (exportBySolverProofs)
+                  val statementString = any2code(seq)
+                  val proofCode = s"have(thesis) by $solverName"
+                  val symbolDeclarations = generateSymbolDeclarationCode(Set(K.sequentToFormula(seq)), "private")
+                  results :+= new ProblemSolverResults(problem, solverName, solverStatus, generateStandaloneTheoremFileContent(problem.name, statementString, proofCode, symbolDeclarations), BySolver)
+              case InvalidProof(proof) =>
+                nbInvalidProofs += (solverName -> (nbInvalidProofs(solverName) + 1))
+                if (!exportOnlySolvedProblems)
+                  results :+= new ProblemSolverResults(problem, solverName, solverStatus, generateStandaloneTheoremFileContent(problem.name, proof), Kernel)
+              case _ =>
+                if (!exportOnlySolvedProblems)
+                  results :+= new ProblemSolverResults(problem, solverName, solverStatus, "", Kernel)
+
+          // Attempting proof by Tableau
+          val tableauResult = proveSequent(seq, timeoutTableau, Tableau.solve)
+          exportResults(problem, "Tableau", tableauResult)
+
+          // Attempting proof by Tautology
+          def tautologySolver(s: lisa.utils.K.Sequent): Option[SCProof] = Tautology.solveSequent(s) match
+            case Left(proof) => Some(proof)
+            case _ => None
+          val tautologyResult = proveSequent(seq, timeoutTautology, tautologySolver)
+          exportResults(problem, "Tautology", tautologyResult)
+        }
+        // } else println(s"Problem $probfile not extracted because of its type: ${md.spc.mkString(",")}")
+      }
+    } catch case e => println(s"Error while processing $probfile (index $i): $e")
+  }
+
+  // Write results to a JSON file
+  val jsonResultsFile = new File(jsonResultsPath)
+  if (!jsonResultsFile.getParentFile.exists())
+    jsonResultsFile.getParentFile.mkdirs()
+  val jsonWriter = new java.io.PrintWriter(jsonResultsPath)
+  ujson.writeTo(
+    results.map(r =>
+      ujson.Obj(
+        "problemName" -> r.problem.name,
+        "problemDomain" -> r.problem.domain,
+        "problemStatus" -> r.problem.status,
+        "problemSPC" -> r.problem.spc.mkString(","),
+        "problemSequent" -> any2code(problemToSequent(r.problem)),
+        "problemFile" -> r.problem.file,
+        "solver" -> r.solverName,
+        "solverStatus" -> r.solverStatus,
+        "proofType" -> r.proofType.getClass.getSimpleName.stripSuffix("$"),
+        "solverProofCode" -> r.proofCode
+      )
+    ),
+    jsonWriter,
+    indent = 2
+  )
+  jsonWriter.close()
+
+}
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index cb1ca1eeb..84800d36b 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -610,7 +610,8 @@ trait Common {
     def rename(newid: Identifier): ConstantPredicateLabel[N] = ConstantPredicateLabel(newid, arity)
     def freshRename(taken: Iterable[Identifier]): ConstantPredicateLabel[N] = rename(K.freshId(taken, id))
     override def toString(): String = id
-    def mkString(args: Seq[Term]): String = if (infix) (args(0).toStringSeparated() + " " + toString() + " " + args(1).toStringSeparated()) else toString() + "(" + args.mkString(", ") + ")"
+    def mkString(args: Seq[Term]): String =
+      if (infix) ("(" + args(0).toStringSeparated() + " " + toString() + " " + args(1).toStringSeparated() + ")") else toString() + "(" + args.mkString(", ") + ")"
     override def mkStringSeparated(args: Seq[Term]): String = if (infix) "(" + mkString(args) + ")" else mkString(args)
   }
   object ConstantPredicateLabel {
@@ -708,7 +709,11 @@ trait Common {
     def rename(newid: Identifier): ConstantConnectorLabel[N] = throw new Error("Can't rename a constant connector label")
     def freshRename(taken: Iterable[Identifier]): ConstantConnectorLabel[N] = rename(K.freshId(taken, id))
     override def toString(): String = id
-    def mkString(args: Seq[Formula]): String = if (args.length == 2) (args(0).toString() + " " + toString() + " " + args(1).toString()) else toString() + "(" + args.mkString(", ") + ")"
+    def mkString(args: Seq[Formula]): String = if (args.length == 1) {
+      underlyingLabel match
+        case K.Neg => toString() + "(" + args(0).toString() + ")"
+        case _ => args(0).toString()
+    } else "(" + args.mkString(" " + toString() + " ") + ")"
     override def mkStringSeparated(args: Seq[Formula]): String = if (args.length == 2) "(" + mkString(args) + ")" else mkString(args)
 
   }
diff --git a/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala b/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
index 576a279c3..a3f3bf98d 100644
--- a/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
@@ -84,7 +84,11 @@ object FOLHelpers {
     case cl: K.SchematicConnectorLabel => asFrontLabel(cl)
   def asFrontLabel[N <: Arity](cpl: K.ConstantAtomicLabel): ConstantAtomicLabelOfArity[N] = cpl.arity.asInstanceOf[N] match
     case n: 0 => ConstantFormula(cpl.id)
-    case n: N => ConstantPredicateLabel(cpl.id, cpl.arity.asInstanceOf)
+    case n: N =>
+      if (cpl.id == Identifier("="))
+        ConstantPredicateLabel.infix("===", cpl.arity.asInstanceOf)
+      else
+        ConstantPredicateLabel(cpl.id, cpl.arity.asInstanceOf)
   def asFrontLabel(sfl: K.SchematicFormulaLabel): SchematicAtomicLabel[?] | SchematicConnectorLabel[?] =
     sfl match
       case v: K.VariableFormulaLabel => asFrontLabel(v)
diff --git a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
index 1f13bf849..dc1aadaaa 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
@@ -168,9 +168,8 @@ trait Sequents extends Common with lisa.fol.Lambdas with Predef {
     infix def ++?(s1: Sequent): Sequent = this addAllIfNotExists s1
 
     override def toString =
-      (if left.size == 0 then "" else if left.size == 1 then left.head.toString else "( " + left.mkString(", ") + " )") +
-        " ⊢ " +
-        (if right.size == 0 then "" else if right.size == 1 then right.head.toString else "( " + right.mkString(", ") + " )")
+      (if (left.size == 0 && right.size <= 1) then "" else if left.size == 1 then left.head.toString + " ⊢ " else "(" + left.mkString(", ") + ") ⊢ ") +
+        (if right.size == 1 then right.head.toString else "(" + right.mkString(", ") + ")")
 
   }
 
diff --git a/lisa-utils/src/main/scala/lisa/utils/ProofsConverter.scala b/lisa-utils/src/main/scala/lisa/utils/ProofsConverter.scala
new file mode 100644
index 000000000..44edc0843
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/ProofsConverter.scala
@@ -0,0 +1,248 @@
+package lisa.utils
+
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.utils.K
+import lisa.utils.KernelHelpers.lambda
+import lisa.prooflib.ProofTacticLib.*
+import lisa.fol.FOL as F
+import lisa.fol.FOLHelpers.*
+
+object ProofsConverter {
+
+// TODO: remove unnecessary variables "val s_..." in generated proofs -> need to detect which steps are used later in other steps
+// TODO: generate more realistic variable names
+
+  private def indent(s: String, indent: Int = 2): String = s.split("\n").map(s => if s == "" then "" else " " * indent + s).mkString("\n")
+  private def unindent(s: String, indent: Int = 2): String = s.split("\n").map(_.stripPrefix(" " * indent)).mkString("\n")
+
+  /**
+   * Converts a Sequent, Formula or Term to a valid Scala/Lisa code
+   *
+   * @param f formula to convert
+   * @return Scala code representing the formula in string format
+   */
+  def any2code(a: K.Sequent | K.Formula | K.Term): String = (a match
+    case sq: K.Sequent => asFront(sq)
+    case form: K.Formula => asFront(form)
+    case term: K.Term => asFront(term)
+  ).toString.replace("⇒", "==>").replace("⇔", "<=>")
+
+  /**
+   * Converts a SCProof to a valid Scala/Lisa code using tactics.
+   *
+   * @param p proof to convert
+   * @return Scala code representing the proof in string format
+   */
+  private def scproof2code(p: K.SCProof): String = {
+    def scproof2codeAux(p: K.SCProof, varPrefix: String = "s", implicitPremises: Seq[String] = Seq.empty): String = {
+      def scproofstep2code(ps: SCProofStep, stepNum: Int, implicitPremises: Seq[String], varPrefix: String): String = {
+
+        def index2stepvar(i: Int): String =
+          if i < -implicitPremises.size then throw new Exception(s"step $i is not defined")
+          else if i < 0 then implicitPremises(-i - 1)
+          else s"${varPrefix}_$i"
+
+        ps match
+          case Sorry(_) => "sorry"
+          case sp @ SCSubproof(_, _) =>
+            indent(
+              s"val ${varPrefix}_$stepNum = have(${any2code(sp.bot)}) subproof {\n" +
+                scproof2codeAux(sp.sp, s"${varPrefix}_$stepNum", sp.premises.map(index2stepvar)) +
+                "\n}"
+            )
+          case _ =>
+            var tacticName = ps.getClass.getSimpleName
+            var opening = "("
+            var closing = ")"
+            ps match
+              case Restate(_, _) => opening = ".from("
+              case RestateTrue(_) => tacticName = "Restate"
+              case LeftSubstEq(_, _, equals, lambdaPhi) =>
+                tacticName = s"LeftSubstEq.withParametersSimple(List(${equals
+                    .map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
+                    .mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
+              case RightSubstEq(_, _, equals, lambdaPhi) =>
+                tacticName = s"RightSubstEq.withParametersSimple(List(${equals
+                    .map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
+                    .mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
+              case LeftSubstIff(_, _, equals, lambdaPhi) =>
+                tacticName = s"LeftSubstIff.withParametersSimple(List(${equals
+                    .map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
+                    .mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
+              case RightSubstIff(_, _, equals, lambdaPhi) =>
+                tacticName = s"RightSubstIff.withParametersSimple(List(${equals
+                    .map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
+                    .mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
+              case InstSchema(_, _, mCon, mPred, mTerm) =>
+                if mCon.isEmpty && mPred.isEmpty then
+                  tacticName = s"InstFunSchema(Map(${mTerm.toList
+                      .map((k, v) => s"${asFrontLabel(k)} -> ${any2code(v.body)}")
+                      .mkString(", ")}))"
+                else if mCon.isEmpty && mTerm.isEmpty then
+                  tacticName = s"InstPredSchema(Map(${mPred.toList
+                      .map((k, v) => s"${asFrontLabel(k)} -> ${any2code(v.body)}")
+                      .mkString(", ")}))"
+                else throw new Exception("InstSchema not implemented")
+              case _ => ()
+
+            indent(
+              s"val ${varPrefix}_$stepNum = " + (
+                if (ps.premises.size == 1 && ps.premises.head + 1 == stepNum && stepNum > 0)
+                then s"thenHave(${any2code(ps.bot)}) by $tacticName"
+                else
+                  s"have(${any2code(ps.bot)}) by $tacticName" + (
+                    if ps.premises.size == 0 then ""
+                    else s"$opening${ps.premises.map(index2stepvar).mkString(", ")}$closing"
+                  )
+              )
+            )
+      }
+
+      p.steps.zipWithIndex.map((ps, i) => scproofstep2code(ps, i, implicitPremises, varPrefix)).mkString("\n")
+    }
+    unindent(scproof2codeAux(p))
+  }
+
+  /**
+   * Extracts all formulas from a proof
+   *
+   * @param proof proof to extract formulas from
+   * @return set of formulas
+   */
+  def extractFormulasFromProof(proof: K.SCProof): Set[K.Formula] =
+    proof.steps.foldLeft(Set.empty[K.Formula])((prev, next) => {
+      prev ++ (next match
+        case sp @ SCSubproof(subproof, _) => extractFormulasFromProof(subproof)
+        case LeftSubstEq(_, _, _, lambdaPhi) => Seq(lambdaPhi._2, K.sequentToFormula(next.bot))
+        case RightSubstEq(_, _, _, lambdaPhi) => Seq(lambdaPhi._2, K.sequentToFormula(next.bot))
+        case LeftSubstIff(_, _, _, lambdaPhi) => Seq(lambdaPhi._2, K.sequentToFormula(next.bot))
+        case RightSubstIff(_, _, _, lambdaPhi) => Seq(lambdaPhi._2, K.sequentToFormula(next.bot))
+        case _ => Seq(K.sequentToFormula(next.bot))
+      )
+    })
+
+  /**
+   * Extracts all symbols: variables, functions, formula variables, predicates and connectors from a set of formulas
+   *
+   * @param formulas set of formulas to extract variables from
+   * @return tuple of sets of variables, functions, formula variables, predicates and connectors
+   */
+  def extractSymbols(
+      formulas: Set[K.Formula]
+  ): (Set[K.VariableLabel], Set[K.SchematicFunctionLabel], Set[K.VariableFormulaLabel], Set[K.SchematicPredicateLabel], Set[K.SchematicConnectorLabel]) =
+    def extractVariablesAux(
+        formula: K.Formula
+    ): (Set[K.VariableLabel], Set[K.SchematicFunctionLabel], Set[K.VariableFormulaLabel], Set[K.SchematicPredicateLabel], Set[K.SchematicConnectorLabel]) =
+      val variableSet = formula.schematicTermLabels.collect { case v: K.VariableLabel => v } ++ formula.freeVariables ++ formula.freeSchematicTermLabels.collect { case v: K.VariableLabel => v }
+      // val constantSet = formula.constantTermLabels.collect { case c: K.ConstantFunctionLabel if c.arity == 0 => c }
+      val functionSet = formula.schematicTermLabels.collect { case f: K.SchematicFunctionLabel => f } ++ formula.freeSchematicTermLabels.collect { case f: K.SchematicFunctionLabel => f }
+      // val constantFunctionSet = formula.constantTermLabels.collect { case c: K.ConstantFunctionLabel if c.arity > 0 => c }
+      val formulaVariableSet = formula.schematicAtomicLabels.collect { case v: K.VariableFormulaLabel => v } ++ formula.freeVariableFormulaLabels
+      val predicateSet = formula.schematicAtomicLabels.collect { case p: K.SchematicPredicateLabel => p }
+      // val constantPredicateSet = formula.constantAtomicLabels
+      val connectorSet = formula.schematicConnectorLabels.collect { case c: K.SchematicConnectorLabel => c }
+      (variableSet, functionSet, formulaVariableSet, predicateSet, connectorSet)
+
+    formulas.foldLeft((Set.empty[K.VariableLabel], Set.empty[K.SchematicFunctionLabel], Set.empty[K.VariableFormulaLabel], Set.empty[K.SchematicPredicateLabel], Set.empty[K.SchematicConnectorLabel]))(
+      (prev, next) => {
+        val (variableSet, functionSet, formulaVariableSet, predicateSet, connectorSet) = prev
+        val (variableSet_, functionSet_, formulaVariableSet_, predicateSet_, connectorSet_) = extractVariablesAux(next)
+        (
+          variableSet ++ variableSet_,
+          functionSet ++ functionSet_,
+          formulaVariableSet ++ formulaVariableSet_,
+          predicateSet ++ predicateSet_,
+          connectorSet ++ connectorSet_
+        )
+      }
+    )
+
+  /**
+   * Generates a valid Scala/Lisa code to declare variables, functions, formula variables, predicates and connectors
+   * used in a set of formulas
+   *
+   * @param formulas set of formulas to generate variables for
+   * @param accessibility accessibility of the variables (e.g. "private")
+   *
+   * @return Scala code representing the variables in string format
+   */
+  def generateSymbolDeclarationCode(formulas: Set[K.Formula], accessibility: String): String =
+    val (variableSet, functionSet, formulaVariableSet, predicateSet, connectorSet) = extractSymbols(formulas)
+    val access = if accessibility != "" then accessibility.strip() + " " else ""
+    (variableSet.map(v => access + s"val ${v.id} = variable").toList.sorted ++
+      functionSet.map(f => access + s"val ${f.id} = function[${f.arity}]").toList.sorted ++
+      formulaVariableSet.map(v => access + s"val ${v.id} = formulaVariable").toList.sorted ++
+      predicateSet.map(p => access + s"val ${p.id} = predicate[${p.arity}]").toList.sorted ++
+      connectorSet.map(c => access + s"val ${c.id} = connector[${c.arity}]").toList.sorted).mkString("\n")
+
+  /**
+   * Generates a valid Scala/Lisa code to declare variables, functions, formula variables, predicates and connectors
+   * used in a proof
+   *
+   * @param proof proof to generate variables for
+   * @param accessibility accessibility of the variables (e.g. "private")
+   *
+   * @return Scala code representing the variables in string format
+   */
+  def generateSymbolDeclarationCode(proof: K.SCProof, accessibility: String = "private"): String =
+    generateSymbolDeclarationCode(extractFormulasFromProof(proof), accessibility)
+
+  /**
+   * Generates a valid Scala/Lisa code of a theorem and its proof
+   *
+   * @param name name of the theorem
+   * @param proof proof of the theorem
+   *
+   * @return Scala code representing the theorem in string format
+   */
+  def generateTheoremCode(name: String, statementString: String, proofCode: String): String = {
+    // lowercase and underscore-separated version of the theorem name
+    val filteredName = "[A-Za-z0-9]+".r.findAllIn(name).mkString("_").toLowerCase
+    s"val $filteredName = Theorem(\n" +
+      indent(statementString) +
+      s"\n) {\n" +
+      indent(proofCode) +
+      s"\n}"
+  }
+
+  /**
+   * Generates a valid Scala/Lisa code of a theorem and its proof in a standalone file, including the necessary variables declarations.
+   * The theorem and its proof must be self-contained, i.e. no dependencies to other theorems, axioms, definitions, etc.
+   *
+   * @param name name of the theorem
+   * @param proofCode code of the proof of the theorem
+   *
+   * @return Scala code representing the theorem in string format
+   */
+  def generateStandaloneTheoremFileContent(name: String, statementString: String, proofCode: String, symbolDeclarations: String): String =
+    val camelName = "[A-Za-z0-9]+".r.findAllIn(name).map(_.capitalize).mkString
+    s"object $camelName extends lisa.Main {\n\n" +
+      indent(
+        symbolDeclarations +
+          "\n\n" +
+          generateTheoremCode(name, statementString, proofCode)
+      ) +
+      "\n}"
+
+  /**
+   * Generates a valid Scala/Lisa code of a theorem and its proof in a standalone file, including the necessary variables declarations.
+   * The theorem and its proof must be self-contained, i.e. no dependencies to other theorems, axioms, definitions, etc.
+   *
+   * @param name name of the theorem
+   * @param proof proof of the theorem
+   *
+   * @return Scala code representing the theorem in string format
+   */
+  def generateStandaloneTheoremFileContent(name: String, proof: K.SCProof): String =
+    generateStandaloneTheoremFileContent(name, any2code(proof.conclusion), scproof2code(proof), generateSymbolDeclarationCode(proof))
+
+  /**
+   * Parse and check that a generated theorem file is valid, i.e. that it compiles and the theorem is proven
+   * @param fileContent content of the generated file
+   * @return true if the file is valid, false otherwise
+   */
+  def checkGeneratedFileContent(fileContent: String): Boolean =
+    // TODO
+    false
+
+}
diff --git a/lisa-utils/src/main/scala/lisa/utils/RunSolver.scala b/lisa-utils/src/main/scala/lisa/utils/RunSolver.scala
new file mode 100644
index 000000000..b0fb2ec8b
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/RunSolver.scala
@@ -0,0 +1,115 @@
+package lisa.utils
+
+import scala.concurrent.duration._
+import scala.concurrent.ExecutionContext.Implicits.global
+import scala.concurrent._
+import java.util.concurrent.CancellationException
+
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.SCProofChecker.checkSCProof
+
+object RunSolver {
+  sealed trait SolverResult
+  case class Solved(proof: SCProof) extends SolverResult
+  case class InvalidProof(proof: SCProof) extends SolverResult
+  case object Unsolved extends SolverResult
+  case object Timeout extends SolverResult
+  case class SolverThrow(t: Throwable) extends SolverResult
+
+  def proveSequent(sequent: Sequent, timeout: Duration, solver: Sequent => Option[SCProof]): SolverResult = {
+    val (futureSolver, cancelSolver) = Future.interruptibly { solver(sequent) }
+    try
+      Await.result(futureSolver, timeout) match
+        case Some(proof) =>
+          if (checkSCProof(proof).isValid) Solved(proof)
+          else InvalidProof(proof)
+        case None => Unsolved
+    catch
+      case _: TimeoutException =>
+        cancelSolver()
+        Timeout
+      case t: Throwable =>
+        cancelSolver()
+        SolverThrow(t)
+  }
+
+  // Class to handle future cancellation
+  // Source: https://viktorklang.com/blog/Futures-in-Scala-protips-6.html
+  final class Interrupt extends (() => Boolean) {
+    // We need a state-machine to track the progress.
+    // It can have the following states:
+    // a null reference means execution has not started.
+    // a Thread reference means that the execution has started but is not done.
+    // a this reference means that it is already cancelled or is already too late.
+    private[this] final var state: AnyRef = null
+
+    /**
+     * This is the signal to cancel the execution of the logic.
+     * Returns whether the cancellation signal was successully issued or not.
+     */
+    override final def apply(): Boolean = this.synchronized {
+      state match {
+        case null =>
+          state = this
+          true
+        case _: this.type => false
+        case t: Thread =>
+          state = this
+          // def kill = t.interrupt() // ask nicely for interruption, but this requires cooperation from the thread (involves checking isInterrupted() regularly)
+          @annotation.nowarn
+          def kill = t.stop() // brutally kill the thread without asking, more portable but less "safe". I believe it's safe here because we don't share any resources with the thread.
+          kill
+          true
+      }
+    }
+
+    // Initializes right before execution of logic and
+    // allows to not run the logic at all if already cancelled.
+    private[this] final def enter(): Boolean =
+      this.synchronized {
+        state match {
+          case _: this.type => false
+          case null =>
+            state = Thread.currentThread
+            true
+        }
+      }
+
+    // Cleans up after the logic has executed
+    // Prevents cancellation to occur "too late"
+    private[this] final def exit(): Boolean =
+      this.synchronized {
+        state match {
+          case _: this.type => false
+          case t: Thread =>
+            state = this
+            true
+        }
+      }
+
+    /**
+     * Executes the suplied block of logic and returns the result.
+     * Throws CancellationException if the block was interrupted.
+     */
+    def interruptibly[T](block: => T): T =
+      if (enter()) {
+        try block
+        catch {
+          case ie: InterruptedException => throw new CancellationException()
+          case td: ThreadDeath => throw new CancellationException()
+          case t: Throwable => throw t
+        } finally {
+          if (!exit() && Thread.interrupted())
+            () // If we were interrupted and flag was not cleared
+        }
+      } else throw new CancellationException()
+  }
+
+  implicit class FutureInterrupt(val future: Future.type) extends AnyVal {
+    def interruptibly[T](block: => T)(implicit ec: ExecutionContext): (Future[T], () => Boolean) = {
+      val interrupt = new Interrupt()
+      (Future(interrupt.interruptibly(block))(ec), interrupt)
+    }
+  }
+}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala b/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala
index 18202949f..d366f4fed 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala
@@ -10,6 +10,7 @@ import lisa.utils.KernelHelpers.*
 import lisa.utils.KernelHelpers.given_Conversion_Identifier_String
 import lisa.utils.KernelHelpers.given_Conversion_String_Identifier
 import lisa.utils.tptp.*
+import lisa.kernel.fol.FOL.*
 
 import java.io.File
 import scala.util.matching.Regex
@@ -18,7 +19,7 @@ import Parser.TPTPParseException
 
 object KernelParser {
 
-  private case class ProblemMetadata(file: String, domain: String, problem: String, status: String, spc: Seq[String])
+  case class ProblemMetadata(file: String, domain: String, problem: String, status: String, spc: Seq[String])
 
   /**
    * @param formula A formula in the tptp language
@@ -26,13 +27,23 @@ object KernelParser {
    */
   def parseToKernel(formula: String): K.Formula = convertToKernel(Parser.fof(formula))
 
+  def cleanVarname(f: String): String =
+    val forbiddenChars = Identifier.forbiddenChars ++ Set('\\', '/', '\'', '"', '`', '.', ',', ';', ':', '!', '%', '^', '&', '*', '|', '-', '+', '=', '<', '>', '~', '@', '#')
+    // replace all the forbidden chars + whitespaces by '0'
+    f.map(c => if (forbiddenChars.contains(c) || c.isWhitespace) then '0' else c)
+
   /**
    * @param formula a tptp formula in leo parser
    * @return the same formula in LISA
    */
   def convertToKernel(formula: FOF.Formula): K.Formula = {
     formula match {
-      case FOF.AtomicFormula(f, args) => K.AtomicFormula(K.ConstantAtomicLabel(f, args.size), args map convertTermToKernel)
+      case FOF.AtomicFormula(f, args) =>
+        K.AtomicFormula(
+          if args.isEmpty then K.VariableFormulaLabel(cleanVarname(f))
+          else K.SchematicPredicateLabel(cleanVarname(f), args.size),
+          args map convertTermToKernel
+        )
       case FOF.QuantifiedFormula(quantifier, variableList, body) =>
         quantifier match {
           case FOF.! => variableList.foldRight(convertToKernel(body))((s, f) => K.Forall(K.VariableLabel(s), f))
@@ -59,12 +70,18 @@ object KernelParser {
   }
 
   def convertToKernel(formula: CNF.Formula): K.Formula = {
+    def atomicFormulaToKernel(formula: CNF.AtomicFormula): K.Formula =
+      K.AtomicFormula(
+        if formula.args.isEmpty then K.VariableFormulaLabel(cleanVarname(formula.f))
+        else K.SchematicPredicateLabel(cleanVarname(formula.f), formula.args.size),
+        formula.args.map(convertTermToKernel).toList
+      )
 
     K.ConnectorFormula(
       K.Or,
       formula.map {
-        case CNF.PositiveAtomic(formula) => K.AtomicFormula(K.ConstantAtomicLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
-        case CNF.NegativeAtomic(formula) => !K.AtomicFormula(K.ConstantAtomicLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
+        case CNF.PositiveAtomic(formula) => atomicFormulaToKernel(formula)
+        case CNF.NegativeAtomic(formula) => !atomicFormulaToKernel(formula)
         case CNF.Equality(left, right) => K.equality(convertTermToKernel(left), convertTermToKernel(right))
         case CNF.Inequality(left, right) => !K.equality(convertTermToKernel(left), convertTermToKernel(right))
       }
@@ -76,8 +93,13 @@ object KernelParser {
    * @return the same term in LISA
    */
   def convertTermToKernel(term: CNF.Term): K.Term = term match {
-    case CNF.AtomicTerm(f, args) => K.Term(K.ConstantFunctionLabel(f, args.size), args map convertTermToKernel)
-    case CNF.Variable(name) => K.VariableTerm(K.VariableLabel(name))
+    case CNF.AtomicTerm(f, args) =>
+      K.Term(
+        if args.isEmpty then K.VariableLabel(cleanVarname(f))
+        else K.SchematicFunctionLabel(cleanVarname(f), args.size),
+        args map convertTermToKernel
+      )
+    case CNF.Variable(name) => K.VariableTerm(K.VariableLabel(cleanVarname(name)))
     case CNF.DistinctObject(name) => ???
   }
 
@@ -87,8 +109,12 @@ object KernelParser {
    */
   def convertTermToKernel(term: FOF.Term): K.Term = term match {
     case FOF.AtomicTerm(f, args) =>
-      K.Term(K.ConstantFunctionLabel(f, args.size), args map convertTermToKernel)
-    case FOF.Variable(name) => K.VariableTerm(K.VariableLabel(name))
+      K.Term(
+        if args.isEmpty then K.VariableLabel(cleanVarname(f))
+        else K.SchematicFunctionLabel(cleanVarname(f), args.size),
+        args map convertTermToKernel
+      )
+    case FOF.Variable(name) => K.VariableTerm(K.VariableLabel(cleanVarname(name)))
     case FOF.DistinctObject(name) => ???
     case FOF.NumberTerm(value) => ???
   }
@@ -104,13 +130,8 @@ object KernelParser {
     }
   }
 
-  private def problemToKernel(problemFile: File, md: ProblemMetadata): Problem = {
+  def problemToKernel(problemFile: File, md: ProblemMetadata): Problem = {
     val file = io.Source.fromFile(problemFile)
-    val pattern = "SPC\\s*:\\s*[A-z]{3}(_[A-z]{3})*".r
-    val g = file.getLines()
-
-    def search(): String = pattern.findFirstIn(g.next()).getOrElse(search())
-
     val i = Parser.problem(file)
     val sq = i.formulas map {
       case TPTP.FOFAnnotated(name, role, formula, annotations) =>
@@ -153,7 +174,7 @@ object KernelParser {
     if (problem.spc.contains("CNF")) problem.formulas.map(_.formula) |- ()
     else
       problem.formulas.foldLeft[LK.Sequent](() |- ())((s, f) =>
-        if (f._1 == "axiom") s +<< f._3
+        if (Set("axiom", "hypothesis", "lemma").contains(f._1)) 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")
       )
@@ -174,11 +195,15 @@ object KernelParser {
       if (d.isDirectory) {
         if (d.listFiles().isEmpty) println("empty directory")
         d.listFiles.filter(_.isDirectory)
-
       } else throw new Exception("Specified path is not a directory.")
     } else throw new Exception("Specified path does not exist.")
 
-    probfiles.map(d => gatherFormulas(spc, d.getPath)).toSeq
+    probfiles.zipWithIndex
+      .map((d, i) => {
+        println("[ " + (i + 1) + " / " + probfiles.size + " ] Gathering formulas from " + d.getName())
+        gatherFormulas(spc, d.getPath)
+      })
+      .toSeq
   }
 
   def gatherFormulas(spc: Seq[String], path: String): Seq[Problem] = {
@@ -187,13 +212,22 @@ object KernelParser {
       if (d.isDirectory) {
         if (d.listFiles().isEmpty) println("empty directory")
         d.listFiles.filter(_.isFile)
-
       } else throw new Exception("Specified path is not a directory.")
     } else throw new Exception("Specified path does not exist.")
 
-    val r = probfiles.foldRight(List.empty[Problem])((p, current) => {
+    val r = probfiles.zipWithIndex.foldLeft(List.empty[Problem])((current, p_i) => {
+      val (p, i) = p_i
+
+      // Progress bar
+      if ((i + 1) % 100 == 0 || i + 1 == probfiles.size) {
+        val pbarLength = 30
+        var pbarContent = "=" * (((i + 1) * pbarLength) / probfiles.size)
+        pbarContent += " " * (pbarLength - pbarContent.length)
+        println("\t[" + pbarContent + "] (" + (i + 1) + " / " + probfiles.size + ") " + d.getName())
+      }
+
       val md = getProblemInfos(p)
-      if (md.spc.exists(spc.contains)) problemToKernel(p, md) :: current
+      if (md.spc.exists(spc.contains)) current :+ problemToKernel(p, md)
       else current
     })
     r
@@ -203,7 +237,7 @@ object KernelParser {
    * @param file a file containing a tptp problem
    * @return the metadata info (file name, domain, problem, status and spc) in the file
    */
-  private def getProblemInfos(file: File): ProblemMetadata = {
+  def getProblemInfos(file: File): ProblemMetadata = {
     val pattern = "((File)|(Domain)|(Problem)|(Status)|(SPC))\\s*:.*".r
     val s = io.Source.fromFile(file)
     val g = s.getLines()
diff --git a/lisa-utils/src/main/scala/lisa/utils/tptp/ProblemGatherer.scala b/lisa-utils/src/main/scala/lisa/utils/tptp/ProblemGatherer.scala
index b635c5a72..53c834697 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tptp/ProblemGatherer.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tptp/ProblemGatherer.scala
@@ -3,14 +3,22 @@ package lisa.utils.tptp
 import lisa.utils.tptp.KernelParser.*
 
 object ProblemGatherer {
+  // Path to the TPTP problems directory
+  val TPTPProblemPath: String = getClass.getResource("/TPTP/Problems/").getPath
 
   /**
-   * The tptp library needs to be included in main/resources. It can be found at http://www.tptp.org/
-   * @return sequence of tptp problems with the PRP (propositional) tag.
+   * @return sequence of tptp problems in the library lib with the tags in spc.
+   */
+  def getLibProblems(spc: Seq[String], lib: String): Seq[Problem] = gatherFormulas(spc, TPTPProblemPath + lib + "/")
+
+  /**
+   * This takes up to several minutes to run.
+   * @return sequence of all tptp problems with the tags in spc.
    */
-  def getPRPproblems: Seq[Problem] = {
-    val path = getClass.getResource("/TPTP/Problems/SYN/").getPath
-    gatherFormulas(Seq("PRP"), path)
-  }
+  def getAllProblems(spc: Seq[String]): Seq[Problem] = gatherAllTPTPFormulas(spc, TPTPProblemPath).flatten
 
+  /**
+   * @return sequence of tptp problems with the PRP (propositional) tag.
+   */
+  def getPRPproblems: Seq[Problem] = getLibProblems(Seq("PRP"), "SYN")
 }