diff --git a/bin/sctptpUtils.jar b/bin/sctptpUtils.jar
index 043aba6cc..fa64beb36 100755
Binary files a/bin/sctptpUtils.jar and b/bin/sctptpUtils.jar differ
diff --git a/lisa-sets/src/main/scala/lisa/Tests.scala b/lisa-sets/src/main/scala/lisa/Tests.scala
index fbce7797e..ac4c77cb4 100644
--- a/lisa-sets/src/main/scala/lisa/Tests.scala
+++ b/lisa-sets/src/main/scala/lisa/Tests.scala
@@ -35,25 +35,36 @@ object Tests extends lisa.Main {
   def _div(x: Expr[Ind], y: Expr[Ind]): Expr[Ind] = div(x)(y)
   def _mult(x: Expr[Ind], y: Expr[Ind]): Expr[Ind] = mult(x)(y)
 
+
+
+
+
+
+
   val divide_mult_shift = Theorem(
-    (
-      ∀(x, x / t1 === x),
+    ( ∀(x, x / t1 === x),
       ∀(x, ∀(y, x / y === t1 / (y / x))),
       ∀(x, ∀(y, (x / y) * y === x))
     ) |- ((t2 / t3) * (t3 / t2)) / t1 === t1
   ):
     have(thesis) by Egg
 
-  val saturation = Theorem((∀(x, x === f(f(f(x)))), ∀(x, ∀(y, x === f(f(x))))) |- ∅ === f(∅)):
+
+  val saturationEGG = Theorem((∀(x, x === f(f(f(x)))), ∀(x, ∀(y, x === f(f(x))))) |- a === f(a)):
     have(thesis) by Egg
 
-  val drinkers2 = Theorem(∃(x, ∀(y, d(x) ==> d(y)))):
+
+  val drinkersGO = Theorem(∃(x, ∀(y, d(x) ==> d(y)))):
     have(thesis) by Goeland
 
-  val example = Theorem((∀(x, P(x)) \/ ∀(y, Q(y))) ==> (P(∅) \/ Q(∅))):
+
+  val exampleP9 = Theorem((∀(x, P(x)) \/ ∀(y, Q(y))) ==> (P(a) \/ Q(a))):
     have(thesis) by Prover9
 
-  val example2 = Theorem(∃(x, ∀(y, d(x) ==> d(y)))):
+
+  val drinkersP9 = Theorem(∃(x, ∀(y, d(x) ==> d(y)))):
     have(thesis) by Prover9
 
+
+
 }
diff --git a/lisa-sets/src/main/scala/lisa/automation/atp/Prover9.scala b/lisa-sets/src/main/scala/lisa/automation/atp/Prover9.scala
index 5c4bd8615..0fe6fdc3a 100644
--- a/lisa-sets/src/main/scala/lisa/automation/atp/Prover9.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/atp/Prover9.scala
@@ -97,7 +97,11 @@ object Prover9 extends ProofTactic with ProofSequentTactic {
         val cmd = (s"java -jar $sctptpExec p9 --input $foldername$filename.p --output $foldername$outputname.p")
         val res =
           try {
-            cmd.!!
+            val stdoutStream = new ByteArrayOutputStream
+            val stderrStream = new ByteArrayOutputStream
+            val stdoutWriter = new PrintWriter(stdoutStream)
+            val stderrWriter = new PrintWriter(stderrStream)
+            val exitValue = cmd.!(ProcessLogger(stdoutWriter.println, stderrWriter.println))
           } catch {
             case e: Exception =>
               throw e
diff --git a/lisa-sets/src/main/scala/lisa/tptp/ProofParser.scala b/lisa-sets/src/main/scala/lisa/tptp/ProofParser.scala
index 13da2cd69..b37b61d42 100644
--- a/lisa-sets/src/main/scala/lisa/tptp/ProofParser.scala
+++ b/lisa-sets/src/main/scala/lisa/tptp/ProofParser.scala
@@ -936,7 +936,7 @@ object ProofParser {
     object RightSubstFun {
       def unapply(ann_seq: FOFAnnotated)(using defctx: DefContext, numbermap: String => Int, sequentmap: String => FOF.Sequent)(using maps: MapTriplet): Option[(K.SCProofStep, String)] =
         ann_seq match {
-          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("rightSubstFun", Seq(_, StrOrNum(n), StrOrNum(_), String(xl), Prop(fl)), Seq(t1)), origin) =>
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("rightSubstFun", Seq(_, StrOrNum(n), StrOrNum(_), Prop(fl), String(xl)), Seq(t1)), origin) =>
             val f = convertToKernel(sequent.lhs(n.toInt))
             def extractForall(f: K.Expression): (List[K.Variable], K.Expression, K.Expression) = f match
               case K.Forall(x, phi) => val (xs, psi, psi1) = extractForall(phi); (x :: xs, psi, psi1)
@@ -954,7 +954,7 @@ object ProofParser {
     object RightSubstPred {
       def unapply(ann_seq: FOFAnnotated)(using defctx: DefContext, numbermap: String => Int, sequentmap: String => FOF.Sequent)(using maps: MapTriplet): Option[(K.SCProofStep, String)] =
         ann_seq match {
-          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("rightSubstPred", Seq(_, StrOrNum(n), StrOrNum(_), String(xl), Prop(fl)), Seq(t1)), origin) =>
+          case FOFAnnotated(name, role, sequent: FOF.Sequent, Inference("rightSubstPred", Seq(_, StrOrNum(n), StrOrNum(_), Prop(fl), String(xl)), Seq(t1)), origin) =>
             val f = convertToKernel(sequent.lhs(n.toInt))
             def extractForall(f: K.Expression): (List[K.Variable], K.Expression, K.Expression) = f match
               case K.Forall(x, phi) => val (xs, psi, psi1) = extractForall(phi); (x :: xs, psi, psi1)