diff --git a/CHANGES.md b/CHANGES.md
index 23381b111691d934bcf813865db3477d076137b5..c8dd41a37eb34d33d7de4ebf132f6e72e54445e8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,14 +1,16 @@
 # Change List
 
+## 2024-03-02 
+Support for reconstructing proofs from file in SC-TPTP format. Support and inclusion of Goeland as a tactic. Doc in the manual.
+
 ## 2024-03-02
 Addition of a tactic that proves a sequent by applying a generic theorem on facts provided by the user. It can be used via `by Apply(thm).on(fact1, fact2,...)`. Replaces cases where using `Tautology` was overkill.
+
 ## 2024-02-05
 The "draft()" option can now be used at the start of a file to skip checking proofs of theorem outside this file during development.
 
-
 ## 2024-01-02
-The "of" keyword can now be used to instantiate quantified variables in facts whose right hand side is a single universaly quantified formula. This can be combined freely with instantiation of ffree schematic symbols. Manual and tests update.
-
+The "of" keyword can now be used to instantiate quantified variables in facts whose right hand side is a single universaly quantified formula. This can be combined freely with instantiation of free schematic symbols. Manual and tests update.
 
 ## 2023-12-31
 Expanded the Substitution rules to allow substitution under quantifiers when a statement of the form $\forall x. f(x) = g(x)$ is given.
diff --git a/build.sbt b/build.sbt
index 8178b55994a3812d5655501a33bf6e6d8884a385..1e58411042d0ddb5eb6f8e4141d1a9149fb0e0c5 100644
--- a/build.sbt
+++ b/build.sbt
@@ -55,6 +55,7 @@ def githubProject(repo: String, commitHash: String) = RootProject(uri(s"$repo#$c
 lazy val scallion = githubProject("https://github.com/sankalpgambhir/scallion.git", "6434e21bd08872cf547c8f0efb67c963bfdf4190")
 
 lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8670a5fa8ea2dd5649a00424710274a5d18")
+lazy val customTstpParser = githubProject("https://github.com/SimonGuilloud/scala-tptp-parser.git", "eae9c1b7a9546f74779d77ff50fa6e8a1654cfa0")
 
 scallion/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
 silex/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
@@ -92,7 +93,8 @@ lazy val utils = Project(
   .dependsOn(kernel)
   .dependsOn(silex)
   .dependsOn(scallion % "compile->compile")
-  .settings(libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4")
+  .dependsOn(customTstpParser)
+  //.settings(libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4")
 
 ThisBuild / assemblyMergeStrategy := {
   case PathList("module-info.class") => MergeStrategy.discard
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 74465308c6ad2e9142ed75d100bc04b37058124e..c942aff6549e5dad4a610134951fcc7893771fbd 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -1,4 +1,6 @@
 import lisa.automation.Substitution.{ApplyRules as Substitute}
+import lisa.automation.Tableau
+import lisa.automation.atp.Goeland
 
 object Example extends lisa.Main {
 
@@ -54,6 +56,14 @@ object Example extends lisa.Main {
     )
   }
 
+  val buveurs = Theorem(exists(x, P(x) ==> forall(y, P(y)))) {
+    have(thesis) by Tableau
+  }
+
+  val buveurs2 = Theorem(exists(x, P(x) ==> forall(y, P(y)))) {
+    have(thesis) by Goeland("goeland/Example.buveurs2_sol")
+  }
+
   /*
 
   import lisa.mathematics.settheory.SetTheory.*
diff --git a/lisa-examples/src/main/scala/Lattices.scala b/lisa-examples/src/main/scala/Lattices.scala
index c4e7fba56716e09e5da62a8d722557cf381a0d82..be45953c81ab0854ccd1d19324b68657663230bb 100644
--- a/lisa-examples/src/main/scala/Lattices.scala
+++ b/lisa-examples/src/main/scala/Lattices.scala
@@ -1,7 +1,5 @@
 object Lattices extends lisa.Main {
 
-
-
   val x = variable
   val P = predicate[1]
   val f = function[1]
@@ -11,11 +9,6 @@ object Lattices extends lisa.Main {
   ) {
     sorry
   }
-  
-
-
-
-
 
   // We introduce the signature of lattices
   val <= = ConstantPredicateLabel.infix("<=", 2)
@@ -49,7 +42,6 @@ object Lattices extends lisa.Main {
     have(thesis) by Tautology.from(lub of (z := (x u y)), reflexivity of (x := (x u y)))
   }
 
-
   val meetUpperBound = Theorem(((x n y) <= x) /\ ((x n y) <= y)) {
     sorry
   }
@@ -58,7 +50,6 @@ object Lattices extends lisa.Main {
     have(thesis) by Tautology.from(s1, s1 of (x := y, y := x), antisymmetry of (x := x u y, y := y u x))
   }
 
-
   val meetCommutative = Theorem((x n y) === (y n x)) {
     sorry
   }
@@ -97,7 +88,6 @@ object Lattices extends lisa.Main {
 
                 // 2. right is a meet. In that case, glb gives us the decomposition
                 case (_, n(a: Term, b: Term)) =>
-
                   val s1 = solve(left <= a)
                   val s2 = solve(left <= b)
                   if s1.isValid & s2.isValid then have(left <= right) by Tautology.from(glb of (x := a, y := b, z := left), have(s1), have(s2))
@@ -131,7 +121,7 @@ object Lattices extends lisa.Main {
                 // 4. left is a meet, right is a variable or unknown term.
                 case (n(a: Term, b: Term), _) =>
                   val result = LazyList(a, b)
-                    .map { e =>  (e, solve(e <= right)) }
+                    .map { e => (e, solve(e <= right)) }
                     .find { _._2.isValid }
                     .map { case (e, step) =>
                       have(left <= right) by Tautology.from(
@@ -180,7 +170,6 @@ object Lattices extends lisa.Main {
     }
   }
 
-
   // uncomment when the tactic is implemented
 
   /*
@@ -205,6 +194,6 @@ object Lattices extends lisa.Main {
   val semiDistributivity = Theorem((x u (y n z)) <= ((x u y) n (x u z))) {
     have(thesis) by Whitman.solve
   }
-  */
-  
-}
\ No newline at end of file
+   */
+
+}
diff --git a/lisa-examples/src/main/scala/Test.scala b/lisa-examples/src/main/scala/Test.scala
deleted file mode 100644
index 026a3761a4610362f2a41b69b7a4c45ea5a536db..0000000000000000000000000000000000000000
--- a/lisa-examples/src/main/scala/Test.scala
+++ /dev/null
@@ -1,57 +0,0 @@
-
-object Test extends lisa.Main {
-
-  val u = variable
-  val v = variable
-  val w = variable
-  val x = variable
-  val y = variable
-  val z = variable
-  val a = variable
-  val c = variable
-  val d = variable
-
-  val f = function[1]
-  val g = function[1]
-  val h = function[2]
-
-  val E = predicate[2]
-  val P = predicate[2]
-
-  val assump1 = ∀(u, ∀(v, ∀(w, E(u, v) ==> (E(v, w) ==> E(u, w)))))
-  val assump2 = ∀(x, ∀(y, E(x, y) ==> (E(f(x), f(y)))))
-  val assump3 = ∀(z, E(f(g(z)), g(f(z))))
-
-  val goal = E(f(f(g(a))), g(f(f(a))))
-
-
-  val thm = Theorem((assump1, assump2, assump3) |- goal) {
-    have(thesis) by Tableau
-  }
-
-  val thm1 = Theorem(∀(x, E(x, x)) |- ∀(x, E(f(x), f(x)))) {
-    val s1 = assume(∀(x, E(x, x)))
-    have(thesis) by RightForall(s1 of f(x))
-  }
-
-  val thm2 = Theorem(∀(y, ∀(x, E(x, y))) |- ∀(y, ∀(x, E(f(x), h(x, y))))) {
-    val s1 = assume(∀(y, ∀(x, E(x, y))))
-    println((s1 of (h(x, y), f(x))).result)
-    have(∀(x, E(f(x), h(x, y)))) by RightForall(s1 of (h(x, y), f(x)))
-    thenHave(thesis) by RightForall
-  }
-
-  val thm3 = Theorem(∀(y, ∀(x, E(x, y))) |- E(f(x), y) /\ E(x, h(x, y))) {
-    val s1 = assume(∀(y, ∀(x, E(x, y))))
-    val s2 = have(∀(x, E(x, y))) by Restate.from(s1 of y)
-    have(thesis) by Tautology.from(s2 of f(x), s2 of (x, y := h(x, y)))
-
-  }
-
-  val ax = Axiom(∀(x, ∀(y, P(x, y))))
-  val thm4 = Theorem(c === d) {
-    have(thesis) by Restate.from(ax of (c, d, P := ===))
-    showCurrentProof()
-  }
-
-}
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
index c5a356512ec70f332ca6c1bb8445e61fa455a55a..610ffe8a67f8a5a5341578f2a098a50a3501c813 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -36,7 +36,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
    * @param arity The arity of the function symbol. Must be greater than 1.
    */
   sealed case class SchematicFunctionLabel(id: Identifier, arity: Int) extends SchematicTermLabel {
-    require(arity >= 1 && arity < MaxArity)
+    require(arity >= 1 && arity < MaxArity, "Trying to define SchemaFunctionLabel with arity " + arity + " for symbol " + id.name + "_" + id.no)
   }
 
   /**
diff --git a/lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala b/lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala
new file mode 100644
index 0000000000000000000000000000000000000000..568110cd0a5c214913515185cfce390b5e223be9
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala
@@ -0,0 +1,119 @@
+package lisa.automation.atp
+import lisa.utils.tptp.*
+import ProofParser.*
+import KernelParser.*
+
+import lisa.prooflib.ProofTacticLib.*
+import lisa.fol.FOL as F
+import lisa.prooflib.Library
+import lisa.utils.K
+
+import java.io.*
+import sys.process._
+import scala.io.Source
+import scala.util.{Try, Success, Failure}
+import lisa.prooflib.OutputManager
+
+/**
+  * Goéland is an automated theorem prover. This tactic calls the Goéland prover to solve the current sequent.
+  * Goéland is only available on Linux yet, but proofs generated by Goéland should be kept in the library for future use.
+  * To ensure that proofs are published and can be replayed in any system, proofs from an ATPcan only be generated in draft mode.
+  * When in non-draft mode, the proof file should be given as an argument to the tactic (the exact file is provided by Lisa upon run without draft mode).
+  */
+object Goeland extends ProofTactic with ProofSequentTactic {
+  private var i : Int = 0
+  
+  val goelandExec = "../bin/goeland_linux_release"
+
+  class OsNotSupportedException(msg: String) extends Exception(msg)
+  
+  val foldername = "goeland/"
+
+  /**
+    * Fetch a proof of a sequent that was previously proven by Goéland.
+    * The file must be in SC-TPTP format.
+    */
+  def apply(using lib: Library, proof: lib.Proof)(file:String)(bot: F.Sequent): proof.ProofTacticJudgement = {
+    val outputname = proof.owningTheorem.fullName+"_sol"
+    try {
+      val scproof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+      proof.ValidProofTactic(bot, scproof.steps, Seq())
+    } catch {
+      case e: FileNotFoundException => 
+        throw FileNotFoundException("The file "+foldername+outputname+".p was not found. To produce a proof, use `by Goeland`. ")
+      case e => throw e
+    }
+  }
+
+
+  /**
+    * Solve a sequent using the Goéland automated theorem prover.
+    * At the moment, this option is only available on Linux system.
+    * The proof is generated and saved in a file in the `Goeland` folder.
+    */
+  def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
+
+
+    solve(Seq(), bot, proof.owningTheorem.fullName, lib.isDraft) match {
+      case Success(value) => proof.ValidProofTactic(bot, value.steps, Seq())
+      case Failure(e) => e match
+        case e: FileNotFoundException  => throw new Exception("For compatibility reasons, external provers can't be called in non-draft mode" +
+          " unless all proofs have already been generated and be available in static files. You can enable draft mode by adding `draft()` at the top of your working file.")
+        case e: OsNotSupportedException => throw e
+        case e => 
+          throw e
+    }
+  }
+
+  inline def solve(axioms: Seq[F.Sequent], sequent: F.Sequent, source: String, generateProofs : Boolean): Try[K.SCProof] = 
+    solveK(axioms.map(_.underlying), sequent.underlying, source, generateProofs)
+
+
+  /**
+    * Solve a sequent using the Goéland automated theorem prover, and return the kernel proof.
+    * At the moment, this option is only available on Linux systems.
+    */
+  def solveK(using line: sourcecode.Line, file: sourcecode.File)(axioms: Seq[K.Sequent], sequent: K.Sequent, source:String, generateProofs : Boolean): Try[K.SCProof] = {
+    val filename = source
+    val outputname = source+"_sol"
+    val directory = File(foldername)
+    if (directory != null) && !directory.exists() then directory.mkdirs()
+
+    val freevars = (sequent.left.flatMap(_.freeVariables) ++ sequent.right.flatMap(_.freeVariables) ).toSet.map(x => x -> K.Term(K.VariableLabel(K.Identifier("X"+x.id.name, x.id.no)), Seq())).toMap
+
+    val backMap = freevars.map{
+      case (x: K.VariableLabel, K.Term(xx: K.VariableLabel, _)) => xx -> K.LambdaTermTerm(Seq(), K.Term(x, Seq()))
+      case _ => throw new Exception("This should not happen")
+    }
+    val r = problemToFile(foldername, filename, "question"+i, axioms, sequent, source)
+    i += 1
+
+    if generateProofs then
+      val OS = System.getProperty("os.name")
+      if OS.contains("nix") || OS.contains("nux") || OS.contains("aix") then
+        val ret = s"chmod u+x \"$goelandExec\"".!
+        val cmd = (s"$goelandExec -otptp -wlogs -no_id -quoted_pred -proof_file=$foldername$outputname $foldername$filename.p")
+        val res = try {
+          cmd.!!
+        } catch {
+          case e: Exception => 
+            throw e
+        }
+        val proof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+        Success(proof)
+      else if OS.contains("win") then
+        Failure(OsNotSupportedException("The Goeland automated theorem prover is not yet supported on Windows."))
+      else 
+        Failure(OsNotSupportedException("The Goeland automated theorem prover is only supported on Linux for now."))
+    else 
+      if File(foldername+outputname+".p").exists() then
+        val proof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+        println(OutputManager.WARNING(s"WARNING: in ${file.value}:$line, For compatibility reasons, replace `by Goeland` with `by Goeland(\"$foldername$outputname\")`."))
+        Success(proof)
+        
+      else Failure(Exception("For compatibility reasons, external provers can't be called in non-draft mode. You can enable draft mode by adding `draft()` at the top of your working file."))
+    
+
+  }
+
+}
\ No newline at end of file
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/Library.scala b/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
index 8927c413332f74a69fa0b54c41ddcc0d2d264802..37460714fec21b08effac3a1ae1309af11d85fb1 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
@@ -40,6 +40,7 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro
   def draft(using file: sourcecode.File, om: OutputManager)(): Unit =
     if last.nonEmpty then om.output(OutputManager.WARNING("Warning: draft option should be used before the first definition or theorem."))
     else _draft = Some(file)
+  def isDraft = _draft.nonEmpty
 
   val knownDefs: scala.collection.mutable.Map[F.ConstantLabel[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty
 
diff --git a/lisa-utils/src/main/scala/lisa/utils/tptp/Example.scala b/lisa-utils/src/main/scala/lisa/utils/tptp/Example.scala
index 952b8b73c599f87739f259bdb2261bd9164b799b..4c834ae9545d72c241b3bfc5f3d957c9397be5d9 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tptp/Example.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tptp/Example.scala
@@ -1,11 +1,13 @@
 package lisa.utils.tptp
 
 import lisa.utils.parsing.FOLParser.*
-import lisa.utils.tptp.KernelParser.annotatedFormulaToKernel
+import lisa.utils.tptp.KernelParser.annotatedStatementToKernel
 import lisa.utils.tptp.KernelParser.parseToKernel
 import lisa.utils.tptp.KernelParser.problemToSequent
 import lisa.utils.tptp.ProblemGatherer.getPRPproblems
 
+import KernelParser.{mapAtom, mapTerm, mapVariable}
+
 object Example {
 
   val prettyFormula = lisa.utils.parsing.FOLParser.printFormula
@@ -27,11 +29,11 @@ object Example {
     )
 
     println("\n---Individual Fetched Formulas---")
-    axioms.foreach(a => println(prettyFormula(parseToKernel(a))))
-    println(prettyFormula(parseToKernel(conjecture)))
+    axioms.foreach(a => println(prettyFormula(parseToKernel(a)(using mapAtom, mapTerm, mapVariable))))
+    println(prettyFormula(parseToKernel(conjecture)(using mapAtom, mapTerm, mapVariable)))
 
     println("\n---Annotated Formulas---")
-    anStatements.map(annotatedFormulaToKernel).foreach(printAnnotatedFormula)
+    anStatements.map(annotatedStatementToKernel(_)(using mapAtom, mapTerm, mapVariable)).foreach(f => printAnnotatedStatement(f))
 
     println("\n---Problems---")
 
@@ -55,16 +57,20 @@ object Example {
   }
 
   // Utility
-  def printAnnotatedFormula(a: AnnotatedFormula): Unit = {
-    if (a.role == "axiom") println("Given " + a.name + ": " + prettyFormula(a.formula))
-    else if (a.role == "conjecture") println("Prove " + a.name + ": " + prettyFormula(a.formula))
-    else println(a.role + " " + a.name + ": " + prettyFormula(a.formula))
+  def printAnnotatedStatement(a: AnnotatedStatement): Unit = {
+    val prettyStatement = a match {
+      case f: AnnotatedFormula => prettyFormula(f.formula)
+      case s: AnnotatedSequent => prettySequent(s.sequent)
+    }
+    if (a.role == "axiom") println("Given " + a.name + ": " + prettyStatement)
+    else if (a.role == "conjecture") println("Prove " + a.name + ": " + prettyStatement)
+    else println(a.role + " " + a.name + ": " + prettyStatement)
   }
 
   def printProblem(p: Problem): Unit = {
     println("Problem: " + p.name + " (" + p.domain + ") ---")
     println("Status: " + p.status)
     println("SPC: " + p.spc.mkString(", "))
-    p.formulas.foreach(printAnnotatedFormula)
+    p.formulas.foreach(printAnnotatedStatement)
   }
 }
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 18202949f2e08f7745a6c7a5175e48d2eda20051..1911e4791d819f5f80202d3bafb575a1df995964 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala
@@ -4,8 +4,7 @@ import leo.datastructures.TPTP
 import leo.datastructures.TPTP.CNF
 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 lisa.utils.K
 import lisa.utils.KernelHelpers.*
 import lisa.utils.KernelHelpers.given_Conversion_Identifier_String
 import lisa.utils.KernelHelpers.given_Conversion_String_Identifier
@@ -24,19 +23,25 @@ object KernelParser {
    * @param formula A formula in the tptp language
    * @return the corresponding LISA formula
    */
-  def parseToKernel(formula: String): K.Formula = convertToKernel(Parser.fof(formula))
+  def parseToKernel(formula: String)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): K.Formula = convertToKernel(
+    Parser.fof(formula)
+  )
 
   /**
    * @param formula a tptp formula in leo parser
    * @return the same formula in LISA
    */
-  def convertToKernel(formula: FOF.Formula): K.Formula = {
+  def convertToKernel(formula: FOF.Formula)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): K.Formula = {
     formula match {
-      case FOF.AtomicFormula(f, args) => K.AtomicFormula(K.ConstantAtomicLabel(f, args.size), args map convertTermToKernel)
+      case FOF.AtomicFormula(f, args) =>
+        if f == "$true" then K.top()
+        else if f == "$false" then K.bot()
+        else K.AtomicFormula(mapAtom(f, args.size), args map convertTermToKernel)
+      // else throw new Exception("Unknown atomic formula kind: " + kind +" in " + f)
       case FOF.QuantifiedFormula(quantifier, variableList, body) =>
         quantifier match {
-          case FOF.! => variableList.foldRight(convertToKernel(body))((s, f) => K.Forall(K.VariableLabel(s), f))
-          case FOF.? => variableList.foldRight(convertToKernel(body))((s, f) => K.Exists(K.VariableLabel(s), f))
+          case FOF.! => variableList.foldRight(convertToKernel(body))((s, f) => K.Forall(mapVariable(s), f))
+          case FOF.? => variableList.foldRight(convertToKernel(body))((s, f) => K.Exists(mapVariable(s), f))
         }
       case FOF.UnaryFormula(connective, body) =>
         connective match {
@@ -58,13 +63,17 @@ object KernelParser {
     }
   }
 
-  def convertToKernel(formula: CNF.Formula): K.Formula = {
+  def convertToKernel(sequent: FOF.Sequent)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): K.Sequent = {
+    K.Sequent(sequent.lhs.map(convertToKernel).toSet, sequent.rhs.map(convertToKernel).toSet)
+  }
+
+  def convertToKernel(formula: CNF.Formula)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): K.Formula = {
 
     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) => K.AtomicFormula(mapAtom(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
+        case CNF.NegativeAtomic(formula) => !K.AtomicFormula(mapAtom(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
         case CNF.Equality(left, right) => K.equality(convertTermToKernel(left), convertTermToKernel(right))
         case CNF.Inequality(left, right) => !K.equality(convertTermToKernel(left), convertTermToKernel(right))
       }
@@ -75,9 +84,9 @@ object KernelParser {
    * @param term a tptp term in leo parser
    * @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))
+  def convertTermToKernel(term: CNF.Term)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): K.Term = term match {
+    case CNF.AtomicTerm(f, args) => K.Term(mapTerm(f, args.size), args map convertTermToKernel)
+    case CNF.Variable(name) => K.VariableTerm(mapVariable(name))
     case CNF.DistinctObject(name) => ???
   }
 
@@ -85,26 +94,37 @@ object KernelParser {
    * @param term a tptp term in leo parser
    * @return the same term in LISA
    */
-  def convertTermToKernel(term: FOF.Term): K.Term = term match {
+  def convertTermToKernel(term: FOF.Term)(using mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): 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(mapTerm(f, args.size), args map convertTermToKernel)
+    case FOF.Variable(name) => K.VariableTerm(mapVariable(name))
     case FOF.DistinctObject(name) => ???
     case FOF.NumberTerm(value) => ???
+
   }
 
   /**
-   * @param formula an annotated tptp formula
+   * @param formula an annotated tptp statement
    * @return the corresponding LISA formula augmented with name and role.
    */
-  def annotatedFormulaToKernel(formula: String): AnnotatedFormula = {
+  def annotatedStatementToKernel(formula: String)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): AnnotatedStatement = {
     val i = Parser.annotatedFOF(formula)
-    i.formula match {
-      case FOF.Logical(formula) => AnnotatedFormula(i.role, i.name, convertToKernel(formula))
-    }
+    i match
+      case TPTP.FOFAnnotated(name, role, formula, annotations) =>
+        formula match {
+          case FOF.Logical(formula) => AnnotatedFormula(role, name, convertToKernel(formula), annotations)
+          case FOF.Sequent(antecedent, succedent) =>
+            AnnotatedSequent(role, name, K.Sequent(antecedent.map(convertToKernel).toSet, succedent.map(convertToKernel).toSet), annotations)
+        }
+
   }
 
-  private def problemToKernel(problemFile: File, md: ProblemMetadata): Problem = {
+  private def problemToKernel(problemFile: File, md: ProblemMetadata)(using
+      mapAtom: (String, Int) => K.AtomicLabel,
+      mapTerm: (String, Int) => K.TermLabel,
+      mapVariable: String => K.VariableLabel
+  ): Problem = {
     val file = io.Source.fromFile(problemFile)
     val pattern = "SPC\\s*:\\s*[A-z]{3}(_[A-z]{3})*".r
     val g = file.getLines()
@@ -115,11 +135,13 @@ object KernelParser {
     val sq = i.formulas map {
       case TPTP.FOFAnnotated(name, role, formula, annotations) =>
         formula match {
-          case FOF.Logical(formula) => AnnotatedFormula(role, name, convertToKernel(formula))
+          case FOF.Logical(formula) => AnnotatedFormula(role, name, convertToKernel(formula), annotations)
+          case FOF.Sequent(antecedent, succedent) =>
+            AnnotatedSequent(role, name, K.Sequent(antecedent.map(convertToKernel).toSet, succedent.map(convertToKernel).toSet), annotations)
         }
       case TPTP.CNFAnnotated(name, role, formula, annotations) =>
         formula match {
-          case CNF.Logical(formula) => AnnotatedFormula(role, name, convertToKernel(formula))
+          case CNF.Logical(formula) => AnnotatedFormula(role, name, convertToKernel(formula), annotations)
         }
       case _ => throw FileNotAcceptedException("Only FOF formulas are supported", problemFile.getPath)
     }
@@ -130,7 +152,7 @@ object KernelParser {
    * @param problemFile a file containning a tptp problem
    * @return a Problem object containing the data of the tptp problem in LISA representation
    */
-  def problemToKernel(problemFile: File): Problem = {
+  def problemToKernel(problemFile: File)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Problem = {
     problemToKernel(problemFile, getProblemInfos(problemFile))
   }
 
@@ -138,7 +160,7 @@ object KernelParser {
    * @param problemFile a path to a file containing a tptp problem
    * @return a Problem object containing the data of the tptp problem in LISA representation
    */
-  def problemToKernel(problemFile: String): Problem = {
+  def problemToKernel(problemFile: String)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Problem = {
     problemToKernel(File(problemFile))
   }
 
@@ -149,16 +171,27 @@ 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): LK.Sequent = {
-    if (problem.spc.contains("CNF")) problem.formulas.map(_.formula) |- ()
+  def problemToSequent(problem: Problem): K.Sequent = {
+    if (problem.spc.contains("CNF")) problem.formulas.map(_.asInstanceOf[AnnotatedFormula].formula) |- ()
     else
-      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
+      problem.formulas.foldLeft[K.Sequent](() |- ())((s, f) =>
+        if (f.role == "axiom") s +<< f.asInstanceOf[AnnotatedFormula].formula
+        else if (f.role == "conjecture" && s.right.isEmpty) s +>> f.asInstanceOf[AnnotatedFormula].formula
         else throw Exception("Can only agglomerate axioms and one conjecture into a sequents")
       )
   }
 
+  def sanitize(s: String) =
+    val pieces = s.split("_")
+    val lead = pieces.init
+    val last = pieces.last
+    if last.nonEmpty && last.forall(_.isDigit) && last.head != '0' then lead.mkString("$u") + "_" + last
+    else pieces.mkString("$u")
+
+  val mapAtom: ((String, Int) => K.AtomicLabel) = (f, n) => K.ConstantAtomicLabel(sanitize(f), n)
+  val mapTerm: ((String, Int) => K.TermLabel) = (f, n) => K.ConstantFunctionLabel(sanitize(f), n)
+  val mapVariable: (String => K.VariableLabel) = f => K.VariableLabel(sanitize(f))
+
   /**
    * Given a folder containing folders containing problem (typical organisation of TPTP library) and a list of spc,
    * return the same arrangement of problems in LISA syntax, filtered so that only problems with at least one
@@ -193,7 +226,7 @@ object KernelParser {
 
     val r = probfiles.foldRight(List.empty[Problem])((p, current) => {
       val md = getProblemInfos(p)
-      if (md.spc.exists(spc.contains)) problemToKernel(p, md) :: current
+      if (md.spc.exists(spc.contains)) problemToKernel(p, md)(using mapAtom, mapTerm, mapVariable) :: current
       else current
     })
     r
diff --git a/lisa-utils/src/main/scala/lisa/utils/tptp/ProofParser.scala b/lisa-utils/src/main/scala/lisa/utils/tptp/ProofParser.scala
new file mode 100644
index 0000000000000000000000000000000000000000..162313ebb655281176f3dc5fdd5f80220ec916b9
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/tptp/ProofParser.scala
@@ -0,0 +1,506 @@
+package lisa.utils.tptp
+
+import leo.datastructures.TPTP.AnnotatedFormula
+import leo.datastructures.TPTP.FOF
+import leo.datastructures.TPTP.FOFAnnotated
+import leo.modules.input.{TPTPParser => Parser}
+import lisa.utils.K
+
+import java.io.File
+
+import Parser.TPTPParseException
+import KernelParser.*
+import K.{given}
+
+object ProofParser {
+  val TPTPversion = "TPTP v8.0.0"
+  val rand = scala.util.Random()
+
+  given mapAtom: ((String, Int) => K.AtomicLabel) = (f, n) =>
+    val kind = f.head
+    val id = f.tail
+    if kind == 's' then
+      if n == 0 then K.VariableFormulaLabel(sanitize(id))
+      else K.SchematicPredicateLabel(sanitize(id), n)
+    else if kind == 'c' then K.ConstantAtomicLabel(sanitize(id), n)
+    else throw new Exception(s"Unknown kind of atomic label: $f")
+  given mapTerm: ((String, Int) => K.TermLabel) = (f, n) =>
+    val kind = f.head
+    val id = f.tail
+    if kind == 's' then K.SchematicFunctionLabel(sanitize(id), n)
+    else if kind == 'c' then K.ConstantFunctionLabel(sanitize(id), n)
+    else if n == 0 then K.VariableLabel(sanitize(f))
+    else K.SchematicFunctionLabel(sanitize(f), n)
+  given mapVariable: (String => K.VariableLabel) = f =>
+    if f.head == 'X' then K.VariableLabel(f.tail)
+    else K.VariableLabel(f)
+
+  def problemToFile(fileDirectory: String, fileName: String, name: String, axioms: Seq[K.Sequent], conjecture: K.Sequent, source: String): File = {
+    // case class Problem(file: String, domain: String, name: String, status: String, spc: Seq[String], formulas: Seq[AnnotatedStatement])
+    val number = rand.nextInt(1000)
+    val file = new File(fileDirectory + fileName + ".p")
+    // val fileName = originFile.split("/").last
+    val header =
+      s"""%--------------------------------------------------------------------------
+% File     : $fileName : $TPTPversion.
+% Domain   : None
+% Problem  : ${name}
+% Version  : None
+% English  :
+
+% Refs     : https://github.com/epfl-lara/lisa
+%          : lisa.utils.tptp.ProofParser
+% Source   : [Lisa, $source]
+% Names    : 
+
+% Status   : Unknown
+% Rating   : ?
+% Syntax   : ?
+% SPC      : FOF_UNK_RFO_SEQ
+
+% Comments : This problem, was printed from a statement in a proof of a theorem by the Lisa theorem prover for submission to proof-producing ATPs.
+%--------------------------------------------------------------------------
+"""
+    val writer = new java.io.PrintWriter(file)
+    writer.write(header)
+    var counter = 0
+    def nextc = { counter += 1; counter }
+    axioms.foreach(s => writer.write(sequentToFOFAnnotated(s, "a" + nextc, "axiom").pretty + "\n"))
+    writer.write(sequentToFOFAnnotated(conjecture, "c" + nextc, "conjecture").pretty + "\n\n")
+    writer.close()
+    file
+  }
+
+  def sequentToFOFAnnotated(sequent: K.Sequent, name: String, role: String): FOFAnnotated = {
+    val annotations = None
+    val formula = K.sequentToFormula(sequent)
+    FOFAnnotated(name, role, formulaToFOFStatement(formula), annotations)
+  }
+
+  def isLowerWord(s: String): Boolean = s.head.isLower && s.tail.forall(_.isLetterOrDigit)
+  inline def quoted(s: String): String = if isLowerWord(s) then s else s"'$s'"
+
+  def termToFOFTerm(term: K.Term): FOF.Term = {
+    val K.Term(label, args) = term
+    label match
+      case K.ConstantFunctionLabel(id, arity) =>
+        FOF.AtomicTerm(quoted("c" + id), args.map(termToFOFTerm))
+      case K.SchematicFunctionLabel(id, arity) =>
+        FOF.AtomicTerm(quoted("s" + id), args.map(termToFOFTerm))
+      case K.VariableLabel(id) => FOF.Variable("X" + id)
+  }
+  def formulaToFOFFormula(formula: K.Formula): FOF.Formula = {
+    formula match
+      case K.AtomicFormula(label, args) =>
+        label match
+          case K.equality => FOF.Equality(termToFOFTerm(args(0)), termToFOFTerm(args(1)))
+          case K.top => FOF.AtomicFormula("$true", Seq())
+          case K.bot => FOF.AtomicFormula("$false", Seq())
+          case K.ConstantAtomicLabel(id, arity) => FOF.AtomicFormula(quoted("c" + id), args.map(termToFOFTerm))
+          case K.SchematicPredicateLabel(id, arity) => FOF.AtomicFormula(quoted("s" + id), args.map(termToFOFTerm))
+          case K.VariableFormulaLabel(id) => FOF.AtomicFormula(quoted("s" + id), Seq())
+      case K.ConnectorFormula(label, args) =>
+        label match
+          case K.Neg => FOF.UnaryFormula(FOF.~, formulaToFOFFormula(args.head))
+          case K.Implies => FOF.BinaryFormula(FOF.Impl, formulaToFOFFormula(args(0)), formulaToFOFFormula(args(1)))
+          case K.Iff => FOF.BinaryFormula(FOF.<=>, formulaToFOFFormula(args(0)), formulaToFOFFormula(args(1)))
+          case K.And =>
+            if args.size == 0 then FOF.AtomicFormula("$true", Seq())
+            else if args.size == 1 then formulaToFOFFormula(args(0))
+            else FOF.BinaryFormula(FOF.&, formulaToFOFFormula(args(0)), formulaToFOFFormula(args(1)))
+          case K.Or =>
+            if args.size == 0 then FOF.AtomicFormula("$false", Seq())
+            else if args.size == 1 then formulaToFOFFormula(args(0))
+            else FOF.BinaryFormula(FOF.|, formulaToFOFFormula(args(0)), formulaToFOFFormula(args(1)))
+          case scl: K.SchematicConnectorLabel => throw new Exception(s"Schematic connectors are unsupported")
+      case K.BinderFormula(label, bound, inner) =>
+        label match
+          case K.Forall => FOF.QuantifiedFormula(FOF.!, Seq("X" + bound.id), formulaToFOFFormula(inner))
+          case K.Exists => FOF.QuantifiedFormula(FOF.?, Seq("X" + bound.id), formulaToFOFFormula(inner))
+          case K.ExistsOne => ???
+  }
+
+  def formulaToFOFStatement(formula: K.Formula): FOF.Statement = {
+    FOF.Logical(formulaToFOFFormula(formula))
+  }
+
+  def reconstructProof(file: File)(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): K.SCProof = {
+    val problem = Parser.problem(io.Source.fromFile(file))
+    val nameMap = scala.collection.mutable.Map[String, (Int, FOF.Sequent)]()
+    var prems = List[K.Sequent]()
+    var steps = List[K.SCProofStep]()
+    var numberSteps = 0
+    problem.formulas.foreach {
+      case fa: FOFAnnotated =>
+        if fa.role == "conjecture" then ()
+        else
+          val fofsequent = fa.formula match {
+            case FOF.Logical(formula) => FOF.Sequent(Seq(), Seq(formula))
+            case s: FOF.Sequent => s
+          }
+          if fa.role == "axiom" then
+            val sequent = K.Sequent(fofsequent.lhs.map(convertToKernel).toSet, fofsequent.rhs.map(convertToKernel).toSet)
+            nameMap(fa.name) = (-prems.size - 1, fofsequent)
+            prems = sequent :: prems
+          else
+            annotatedStatementToProofStep(fa, e => nameMap(e)._1, e => nameMap(e)._2) match {
+              case Some((step, name)) =>
+                nameMap(name) = (numberSteps, fofsequent)
+                numberSteps += 1
+                steps = step :: steps
+              case None => throw new Exception(s"Proof step could not be reconstructed from ${fa.pretty}")
+            }
+      case _ => throw new Exception("Only FOF statements are supported")
+    }
+    K.SCProof(steps.reverse.toIndexedSeq, prems.reverse.toIndexedSeq)
+  }
+
+  def annotatedStatementToProofStep(ann: FOFAnnotated, numbermap: String => Int, sequentmap: String => FOF.Sequent)(using
+      mapAtom: (String, Int) => K.AtomicLabel,
+      mapTerm: (String, Int) => K.TermLabel,
+      mapVariable: String => K.VariableLabel
+  ): Option[(K.SCProofStep, String)] = {
+    given (String => Int) = numbermap
+    given (String => FOF.Sequent) = sequentmap
+    val r = ann match {
+      case Inference.Hypothesis(step, name) => Some((step, name))
+      case Inference.Cut(step, name) => Some((step, name))
+      case Inference.LeftHypothesis(step, name) =>
+        Some((step, name))
+      case Inference.LeftNNot(step, name) => Some((step, name))
+      case Inference.LeftAnd(step, name) => Some((step, name))
+      case Inference.LeftNOr(step, name) => Some((step, name))
+      case Inference.LeftNImp(step, name) => Some((step, name))
+      case Inference.LeftNAnd(step, name) => Some((step, name))
+      case Inference.LeftOr(step, name) => Some((step, name))
+      case Inference.LeftImp1(step, name) => Some((step, name))
+      case Inference.LeftImp2(step, name) => Some((step, name))
+      case Inference.LeftNAll(step, name) => Some((step, name))
+      case Inference.LeftEx(step, name) => Some((step, name))
+      case Inference.LeftAll(step, name) => Some((step, name))
+      case Inference.LeftNEx(step, name) => Some((step, name))
+      case Inference.RightNot(step, name) => Some((step, name))
+      case _ => None
+    }
+    r
+  }
+
+  object Inference {
+    import leo.datastructures.TPTP.{Annotations, GeneralTerm, MetaFunctionData, NumberData, Integer, FOF, GeneralFormulaData, FOTData}
+    import K.apply
+
+    object Number {
+      def unapply(ann_seq: GeneralTerm): Option[BigInt] =
+        ann_seq match {
+          case GeneralTerm(List(NumberData(Integer(n))), None) => Some(n)
+          case _ => None
+        }
+    }
+    object Term {
+      def unapply(ann_seq: GeneralTerm)(using mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[K.Term] =
+        ann_seq match {
+          case GeneralTerm(List(GeneralFormulaData(FOTData(term))), None) => Some(convertTermToKernel(term))
+          case _ => None
+        }
+    }
+    object String {
+      def unapply(ann_seq: GeneralTerm): Option[String] =
+        ann_seq match {
+          case GeneralTerm(List(MetaFunctionData(string, List())), None) => Some(string)
+          case _ => None
+        }
+    }
+    object StrOrNum {
+      def unapply(ann_seq: GeneralTerm): Option[String] =
+        ann_seq match {
+          case String(s) => Some(s)
+          case Number(n) => Some(n.toString)
+          case _ => None
+        }
+    }
+    def unapply(ann_seq: Annotations): Option[(String, Seq[GeneralTerm], Seq[String])] =
+      ann_seq match {
+        case Some(
+              (
+                GeneralTerm(
+                  List(
+                    MetaFunctionData(
+                      "inference",
+                      List(
+                        GeneralTerm(List(MetaFunctionData(stepName, List())), None), // stepnames
+                        GeneralTerm(List(MetaFunctionData("param", parameters)), None), // params
+                        GeneralTerm(List(), Some(numberTerms))
+                      ) // numbers
+                    )
+                  ),
+                  None
+                ),
+                None
+              )
+            ) =>
+          Some(
+            (
+              stepName,
+              parameters,
+              numberTerms.map {
+                case StrOrNum(n) => n.toString
+                case String(n) => n
+                case _ => throw new Exception(s"Expected a list of number as last parameter of inference, but got $numberTerms")
+              }
+            )
+          )
+        case _ => None
+      }
+
+    object Hypothesis {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("hyp", Seq(StrOrNum(n), StrOrNum(m)), Seq())) =>
+            if (sequent.lhs(n.toInt) == sequent.rhs(m.toInt)) then
+              val left = sequent.lhs.map(convertToKernel)
+              val right = sequent.rhs.map(convertToKernel)
+              Some((K.RestateTrue(K.Sequent(left.toSet, right.toSet)), name))
+            else None
+          case _ => None
+        }
+    } // List(GeneralTerm(List(),Some(List(GeneralTerm(List(NumberData(Integer(6))),None), GeneralTerm(List(NumberData(Integer(5))),None)))))
+
+    object Cut {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("cut", Seq(StrOrNum(n), StrOrNum(m)), Seq(t1, t2))) =>
+            val formula1 = sequentmap(t1).rhs(n.toInt)
+            val formula2 = sequentmap(t2).lhs(m.toInt)
+            if (formula1 == formula2) then Some((K.Cut(convertToKernel(sequent), numbermap(t1), numbermap(t2), convertToKernel(formula1)), name))
+            else throw new Exception(s"Cut inference with different formulas given in the premises")
+          case _ =>
+            None
+        }
+
+    }
+
+    object LeftHypothesis {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftHyp", Seq(StrOrNum(n), StrOrNum(m)), Seq())) =>
+            val left = sequent.lhs.map(convertToKernel)
+            val right = sequent.rhs.map(convertToKernel)
+            val formula = left(n.toInt)
+            if (formula == K.Neg(left(m.toInt)) || K.Neg(formula) == left(m.toInt)) then Some((K.RestateTrue(K.Sequent(left.toSet, right.toSet)), name))
+            else None
+          case _ =>
+            None
+        }
+    }
+    object LeftNNot {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftNotNot", Seq(StrOrNum(n)), Seq(t1))) =>
+            Some((K.Weakening(convertToKernel(sequent), numbermap(t1)), name))
+          case _ => None
+        }
+    }
+    object LeftAnd {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftAnd", Seq(StrOrNum(n)), Seq(t1))) =>
+            Some((K.Weakening(convertToKernel(sequent), numbermap(t1)), name))
+          case _ => None
+        }
+    }
+    object LeftNOr {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftNotOr", Seq(StrOrNum(n)), Seq(t1))) =>
+            Some((K.Weakening(convertToKernel(sequent), numbermap(t1)), name))
+          case _ => None
+        }
+    }
+    object LeftNImp {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftNotImp", Seq(StrOrNum(n)), Seq(t1))) =>
+            Some((K.Weakening(convertToKernel(sequent), numbermap(t1)), name))
+          case _ => None
+        }
+    }
+
+    object LeftNAnd {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftNotAnd", Seq(StrOrNum(n)), Seq(t1, t2))) =>
+            val f = sequent.lhs(n.toInt)
+            val (a, b) = convertToKernel(f) match {
+              case K.ConnectorFormula(K.Neg, Seq(K.ConnectorFormula(K.And, Seq(x, y)))) => (x, y)
+              case _ => throw new Exception(s"Expected a negated conjunction, but got $f")
+            }
+            Some((K.LeftOr(convertToKernel(sequent), Seq(numbermap(t1), numbermap(t2)), Seq(K.Neg(a), K.Neg(b))), name))
+          case _ => None
+        }
+    }
+
+    object LeftOr {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftOr", Seq(StrOrNum(n)), Seq(t1, t2))) =>
+            val f = sequent.lhs(n.toInt)
+            val (a, b) = convertToKernel(f) match {
+              case K.ConnectorFormula(K.Or, Seq(x, y)) => (x, y)
+              case _ => throw new Exception(s"Expected a disjunction, but got $f")
+            }
+            Some((K.LeftOr(convertToKernel(sequent), Seq(numbermap(t1), numbermap(t2)), Seq(a, b))), name)
+          case _ => None
+        }
+    }
+
+    object LeftImp1 {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftImp1", Seq(StrOrNum(n)), Seq(t1, t2))) =>
+            val f = sequent.lhs(n.toInt)
+            val (a, b) = convertToKernel(f) match {
+              case K.ConnectorFormula(K.Implies, Seq(x, y)) => (x, y)
+              case _ => throw new Exception(s"Expected an implication, but got $f")
+            }
+            Some((K.LeftImplies(convertToKernel(sequent), numbermap(t1), numbermap(t2), a, b), name))
+          case _ => None
+        }
+    }
+
+    object LeftImp2 {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftImp2", Seq(StrOrNum(n)), Seq(t1, t2))) =>
+            val f = sequent.lhs(n.toInt)
+            val (a, b) = convertToKernel(f) match {
+              case K.ConnectorFormula(K.Implies, Seq(x, y)) => (x, y)
+              case _ => throw new Exception(s"Expected an implication, but got $f")
+            }
+            Some((K.LeftOr(convertToKernel(sequent), Seq(numbermap(t1), numbermap(t2)), Seq(K.Neg(a), b)), name))
+          case _ => None
+        }
+    }
+
+    object LeftNAll {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftNotForall", Seq(StrOrNum(n), Term(xl)), Seq(t1))) => // x has to be a GeneralTerm representinf a variable, i.e. $fot(x)
+            val f = sequent.lhs(n.toInt)
+            val x = xl match
+              case K.Term(x: K.VariableLabel, Seq()) => x
+              case _ => throw new Exception(s"Expected a variable, but got $xl")
+            val (y: K.VariableLabel, phi: K.Formula) = convertToKernel(f) match {
+              case K.ConnectorFormula(K.Neg, Seq(K.BinderFormula(K.Forall, x, phi))) => (x, phi)
+              case _ => throw new Exception(s"Expected a universal quantification, but got $f")
+            }
+            if x == y then Some((K.LeftExists(convertToKernel(sequent), numbermap(t1), phi, x), name))
+            else Some((K.LeftExists(convertToKernel(sequent), numbermap(t1), K.substituteVariablesInFormula(K.ConnectorFormula(K.Neg, Seq(phi)), Map(y -> xl), Seq()), x), name))
+          case _ => None
+        }
+    }
+
+    object LeftEx {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftEx", Seq(StrOrNum(n), Term(xl)), Seq(t1))) => // x has to be a GeneralTerm representinf a variable, i.e. $fot(x)
+            val f = sequent.lhs(n.toInt)
+            val x = xl match
+              case K.Term(x: K.VariableLabel, Seq()) => x
+              case _ => throw new Exception(s"Expected a variable, but got $xl")
+            val (y: K.VariableLabel, phi: K.Formula) = convertToKernel(f) match {
+              case K.BinderFormula(K.Exists, x, phi) => (x, phi)
+              case _ => throw new Exception(s"Expected an existential quantification, but got $f")
+            }
+            if x == y then Some((K.LeftExists(convertToKernel(sequent), numbermap(t1), phi, x), name))
+            else Some((K.LeftExists(convertToKernel(sequent), numbermap(t1), K.substituteVariablesInFormula(phi, Map(y -> xl), Seq()), x), name))
+          case _ => None
+        }
+    }
+
+    object LeftAll {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftForall", Seq(StrOrNum(n), Term(t)), Seq(t1))) =>
+            val f = sequent.lhs(n.toInt)
+            val (x, phi) = convertToKernel(f) match {
+              case K.BinderFormula(K.Forall, x, phi) => (x, phi)
+              case _ => throw new Exception(s"Expected a universal quantification, but got $f")
+            }
+            Some((K.LeftForall(convertToKernel(sequent), numbermap(t1), phi, x, t), name))
+          case _ => None
+        }
+    }
+
+    object LeftNEx {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("leftNotEx", Seq(StrOrNum(n), Term(t)), Seq(t1))) =>
+            val f = sequent.lhs(n.toInt)
+            val (x, phi) = convertToKernel(f) match {
+              case K.ConnectorFormula(K.Neg, Seq(K.BinderFormula(K.Exists, x, phi))) => (x, phi)
+              case _ => throw new Exception(s"Expected a negated existential quantification, but got $f")
+            }
+            Some((K.LeftForall(convertToKernel(sequent), numbermap(t1), K.ConnectorFormula(K.Neg, Seq(phi)), x, t), name))
+          case _ => None
+        }
+    }
+
+    object RightNot {
+      def unapply(ann_seq: FOFAnnotated)(using
+          numbermap: String => Int,
+          sequentmap: String => FOF.Sequent
+      )(using mapAtom: (String, Int) => K.AtomicLabel, mapTerm: (String, Int) => K.TermLabel, mapVariable: String => K.VariableLabel): Option[(K.SCProofStep, String)] =
+        ann_seq match {
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("rightNot", Seq(StrOrNum(n)), Seq(t1))) =>
+            Some((K.Weakening(convertToKernel(sequent), numbermap(t1)), name))
+          case _ => None
+        }
+    }
+
+  }
+}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tptp/package.scala b/lisa-utils/src/main/scala/lisa/utils/tptp/package.scala
index a299e9e0ee893ac3bb66de6047b8895bff700ce2..56192deefd9fb9107901d64f7e1304aa8671de1a 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tptp/package.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tptp/package.scala
@@ -1,9 +1,28 @@
 package lisa.utils.tptp
 
-import lisa.kernel.fol.FOL as K
+import leo.datastructures.TPTP
+import lisa.utils.K
 
-case class AnnotatedFormula(role: String, name: String, formula: K.Formula)
+sealed trait AnnotatedStatement {
+  def role: String
+  def name: String
+  def annotations: TPTP.Annotations
 
-case class Problem(file: String, domain: String, name: String, status: String, spc: Seq[String], formulas: Seq[AnnotatedFormula])
+  def toFormula: AnnotatedFormula = this match {
+    case f: AnnotatedFormula => f
+    case s: AnnotatedSequent => AnnotatedFormula(role, name, K.sequentToFormula(s.sequent), annotations)
+  }
+
+  def toSequent: AnnotatedSequent = this match {
+    case f: AnnotatedFormula => AnnotatedSequent(role, name, K.Sequent(Set(), Set(f.formula)), annotations)
+    case s: AnnotatedSequent => s
+  }
+}
+
+case class AnnotatedFormula(role: String, name: String, formula: K.Formula, annotations: TPTP.Annotations) extends AnnotatedStatement
+
+case class AnnotatedSequent(role: String, name: String, sequent: K.Sequent, annotations: TPTP.Annotations) extends AnnotatedStatement
+
+case class Problem(file: String, domain: String, name: String, status: String, spc: Seq[String], formulas: Seq[AnnotatedStatement])
 
 case class FileNotAcceptedException(msg: String, file: String) extends Exception(msg + " File: " + file)
diff --git a/refman/biblio.bib b/refman/biblio.bib
new file mode 100644
index 0000000000000000000000000000000000000000..9fc6726bdfd59d3f7ecb5c144c5fff447c5b47d7
--- /dev/null
+++ b/refman/biblio.bib
@@ -0,0 +1,27 @@
+
+
+@inproceedings{DBLP:conf/cade/CaillerRDRB22,
+  author       = {Julie Cailler and
+                  Johann Rosain and
+                  David Delahaye and
+                  Simon Robillard and
+                  Hinde{-}Lilia Bouziane},
+  editor       = {Jasmin Blanchette and
+                  Laura Kov{\'{a}}cs and
+                  Dirk Pattinson},
+  title        = {Go{\'{e}}land: {A} Concurrent Tableau-Based Theorem Prover (System
+                  Description)},
+  booktitle    = {Automated Reasoning - 11th International Joint Conference, {IJCAR}
+                  2022, Haifa, Israel, August 8-10, 2022, Proceedings},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {13385},
+  pages        = {359--368},
+  publisher    = {Springer},
+  year         = {2022},
+  url          = {https://doi.org/10.1007/978-3-031-10769-6\_22},
+  doi          = {10.1007/978-3-031-10769-6\_22},
+  timestamp    = {Mon, 24 Oct 2022 16:36:35 +0200},
+  biburl       = {https://dblp.org/rec/conf/cade/CaillerRDRB22.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
diff --git a/refman/lisa.pdf b/refman/lisa.pdf
index cd1bb87ae8e25ca998ff5ee7995f293a13ab3729..8855ed46532f486aef780ff64bb619ca8f1a58e5 100644
Binary files a/refman/lisa.pdf and b/refman/lisa.pdf differ
diff --git a/refman/lisa.tex b/refman/lisa.tex
index d78e27da4fd9770e26c436726c8c42238a34fc2d..4e6ae055134bf0090ce2e90f40a885107d000a71 100644
--- a/refman/lisa.tex
+++ b/refman/lisa.tex
@@ -49,7 +49,9 @@
 
 \input{prooflib.tex}
 
-\input{theory.tex}
+\input{tactics.tex}
+
+\input{theory.tex} 
 
 \input{theorytopics.tex}
 
diff --git a/refman/tactics.tex b/refman/tactics.tex
new file mode 100644
index 0000000000000000000000000000000000000000..d3c92691744ae5590d8e1518f379be04c8247ae7
--- /dev/null
+++ b/refman/tactics.tex
@@ -0,0 +1,20 @@
+\chapter{Tactics: Specifications and Use}
+\label{chapt:tactics}
+
+\subsection*{Goeland}
+Goeland\cite{DBLP:conf/cade/CaillerRDRB22} is an Automated Theorem prover for first order logic. The Goeland tactic exports a statement in SC-TPTP format, and call Goeland to prove it. Goeland produce a proof file in the SC-TPTP format, from which Lisa rebuilds a kernel proof.
+\paragraph*{Usage}.
+\newline\begin{lstlisting}[language=lisa, frame=single]
+  val gothm = Theorem (() |- ∃(x, ∀(y, Q(x) ==> Q(y)))) {
+    have(thesis) by Goeland
+  }
+
+  //or
+
+  val gothm = Theorem (() |- ∃(x, ∀(y, Q(x) ==> Q(y)))) {
+    have(thesis) by Goeland("goeland/Test.gothm_sol")
+  }
+\end{lstlisting}
+Goeland can only be used from linux systems, and the proof files produced by Goeland should be published along the Lisa library. Calling Goeland without arguments is only available in draft mode. It will produce a proof file for the theorem (if it succeeds). When the draft mode is disabled, for publication, Lisa will provide a file name that should be happended to the tactic. This ensures that the proof can be replayed in any system using the Lisa library.
+
+Goeland is a complete solver for first order logic, but equality is not yet supported. It is a faster alternative to the Tableau tactic.
\ No newline at end of file