diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
index b4d179bbc9af893694293238a7a394c5893e7985..2c39320d74edcc7350a39ee890863a13dc6fbece 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
@@ -137,7 +137,7 @@ object Parser {
     case class ConstantToken(id: String) extends FormulaToken(id)
 
     // Variables, schematic functions and predicates
-    case class SchematicToken(id: String) extends FormulaToken("?" + id)
+    case class SchematicToken(id: String) extends FormulaToken(schematicSymbol + id)
 
     case class ParenthesisToken(isOpen: Boolean) extends FormulaToken(if (isOpen) "(" else ")")
 
@@ -153,6 +153,8 @@ object Parser {
     // TODO: add positions ==> ranges to tokens
     type Position = Unit
 
+    private val schematicSymbol = "'"
+
     private val lexer = Lexer(
       elem('∀') |> { _ => ForallToken },
       word("∃!") |> { _ => ExistsOneToken },
@@ -172,8 +174,8 @@ object Parser {
       elem(';') |> SemicolonToken,
       elem('⊢') | word("|-") |> SequentToken,
       many1(whiteSpace) |> SpaceToken,
-      elem('?') ~ many1(elem(_.isLetter) | elem('_') | elem(_.isDigit) | elem('\'')) |> { cs =>
-        // drop the '?'
+      word(schematicSymbol) ~ many1(elem(_.isLetter) | elem('_') | elem(_.isDigit) | elem('\'')) |> { cs =>
+        // drop the '
         SchematicToken(cs.drop(1).mkString)
       },
       many1(elem(_.isLetter) | elem('_') | elem(_.isDigit)) |> { cs => ConstantToken(cs.mkString) }
diff --git a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
index f945193d6a70fe68cd936e7273607741fdf034cc..6717983e38b6e5978f53585295abdcddbeae4d7b 100644
--- a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
@@ -11,7 +11,7 @@ class ParserTest extends AnyFunSuite with TestUtils {
   }
 
   test("variable") {
-    assert(Parser.parseTerm("?x") == VariableTerm(x))
+    assert(Parser.parseTerm("'x") == VariableTerm(x))
   }
 
   test("constant function application") {
@@ -20,24 +20,24 @@ class ParserTest extends AnyFunSuite with TestUtils {
     assert(Parser.parseTerm("f(x, y)") == Term(f2, Seq(cx, cy)))
     assert(Parser.parseTerm("f(x, y, z)") == Term(f3, Seq(cx, cy, cz)))
 
-    assert(Parser.parseTerm("f(?x)") == Term(f1, Seq(x)))
-    assert(Parser.parseTerm("f(?x, ?y)") == Term(f2, Seq(x, y)))
-    assert(Parser.parseTerm("f(?x, ?y, ?z)") == Term(f3, Seq(x, y, z)))
+    assert(Parser.parseTerm("f('x)") == Term(f1, Seq(x)))
+    assert(Parser.parseTerm("f('x, 'y)") == Term(f2, Seq(x, y)))
+    assert(Parser.parseTerm("f('x, 'y, 'z)") == Term(f3, Seq(x, y, z)))
   }
 
   test("schematic function application") {
     // Parser.parseTerm("?f()") -- schematic functions of 0 arguments do not exist, those are variables
-    assert(Parser.parseTerm("?f(x)") == Term(sf1, Seq(cx)))
-    assert(Parser.parseTerm("?f(x, y)") == Term(sf2, Seq(cx, cy)))
-    assert(Parser.parseTerm("?f(x, y, z)") == Term(sf3, Seq(cx, cy, cz)))
+    assert(Parser.parseTerm("'f(x)") == Term(sf1, Seq(cx)))
+    assert(Parser.parseTerm("'f(x, y)") == Term(sf2, Seq(cx, cy)))
+    assert(Parser.parseTerm("'f(x, y, z)") == Term(sf3, Seq(cx, cy, cz)))
 
-    assert(Parser.parseTerm("?f(?x)") == Term(sf1, Seq(x)))
-    assert(Parser.parseTerm("?f(?x, ?y)") == Term(sf2, Seq(x, y)))
-    assert(Parser.parseTerm("?f(?x, ?y, ?z)") == Term(sf3, Seq(x, y, z)))
+    assert(Parser.parseTerm("'f('x)") == Term(sf1, Seq(x)))
+    assert(Parser.parseTerm("'f('x, 'y)") == Term(sf2, Seq(x, y)))
+    assert(Parser.parseTerm("'f('x, 'y, 'z)") == Term(sf3, Seq(x, y, z)))
   }
 
   test("nested function application") {
-    assert(Parser.parseTerm("?f(?f(?x), ?y)") == Term(sf2, Seq(Term(sf1, Seq(x)), y)))
+    assert(Parser.parseTerm("'f('f('x), 'y)") == Term(sf2, Seq(Term(sf1, Seq(x)), y)))
   }
 
   test("0-ary predicate") {
@@ -59,13 +59,13 @@ class ParserTest extends AnyFunSuite with TestUtils {
 
   test("predicate application") {
     assert(Parser.parseFormula("p(x, y, z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(cx, cy, cz)))
-    assert(Parser.parseFormula("p(?x, ?y, ?z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z)))
+    assert(Parser.parseFormula("p('x, 'y, 'z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z)))
   }
 
   test("equality") {
     assert(Parser.parseFormula("(x = x)") == PredicateFormula(equality, Seq(cx, cx)))
     assert(Parser.parseFormula("x = x") == PredicateFormula(equality, Seq(cx, cx)))
-    assert(Parser.parseFormula("a ∧ (?x = ?x)") == ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x)))))
+    assert(Parser.parseFormula("a ∧ ('x = 'x)") == ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x)))))
   }
 
   test("unicode connectors") {
@@ -122,13 +122,13 @@ class ParserTest extends AnyFunSuite with TestUtils {
   }
 
   test("quantifiers") {
-    assert(Parser.parseFormula("∀ ?x. (p)") == BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
-    assert(Parser.parseFormula("∃ ?x. (p)") == BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
-    assert(Parser.parseFormula("∃! ?x. (p)") == BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
+    assert(Parser.parseFormula("∀ 'x. (p)") == BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
+    assert(Parser.parseFormula("∃ 'x. (p)") == BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
+    assert(Parser.parseFormula("∃! 'x. (p)") == BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
 
-    assert(Parser.parseFormula("∀ ?x. p") == BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
-    assert(Parser.parseFormula("∃ ?x. p") == BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
-    assert(Parser.parseFormula("∃! ?x. p") == BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
+    assert(Parser.parseFormula("∀ 'x. p") == BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
+    assert(Parser.parseFormula("∃ 'x. p") == BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
+    assert(Parser.parseFormula("∃! 'x. p") == BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
   }
 
   test("nested quantifiers") {
@@ -138,7 +138,7 @@ class ParserTest extends AnyFunSuite with TestUtils {
   test("quantifier parentheses") {
     assert(Parser.parseFormula("∀x. b ∧ a") == BinderFormula(Forall, x, ConnectorFormula(And, Seq(b, a))))
     assert(
-      Parser.parseFormula("∀ ?x. p(?x) ∧ q(?x)") == BinderFormula(
+      Parser.parseFormula("∀ 'x. p('x) ∧ q('x)") == BinderFormula(
         Forall,
         x,
         ConnectorFormula(And, Seq(PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x)), PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))))
@@ -148,7 +148,7 @@ class ParserTest extends AnyFunSuite with TestUtils {
     assert(Parser.parseFormula("(∀x. b) ∧ a") == ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a)))
 
     assert(
-      Parser.parseFormula("(∀ ?x. p(?x)) ∧ q(?x)") == ConnectorFormula(
+      Parser.parseFormula("(∀ 'x. p('x)) ∧ q('x)") == ConnectorFormula(
         And,
         Seq(
           BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x))),
@@ -170,7 +170,7 @@ class ParserTest extends AnyFunSuite with TestUtils {
   }
 
   test("complex formulas") {
-    assert(Parser.parseFormula("∀x. ?x = ?x") == BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x))))
+    assert(Parser.parseFormula("∀x. 'x = 'x") == BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x))))
   }
 
   test("parser limitations") {
@@ -181,15 +181,15 @@ class ParserTest extends AnyFunSuite with TestUtils {
 
   test("sequent") {
     val forallEq = BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))
-    assert(Parser.parseSequent("∀x. ?x = ?x") == Sequent(Set(), Set(forallEq)))
-    assert(Parser.parseSequent("⊢ ∀x. ?x = ?x") == Sequent(Set(), Set(forallEq)))
-    assert(Parser.parseSequent("∀x. ?x = ?x ⊢ ∀x. ?x = ?x") == Sequent(Set(forallEq), Set(forallEq)))
+    assert(Parser.parseSequent("∀x. 'x = 'x") == Sequent(Set(), Set(forallEq)))
+    assert(Parser.parseSequent("⊢ ∀x. 'x = 'x") == Sequent(Set(), Set(forallEq)))
+    assert(Parser.parseSequent("∀x. 'x = 'x ⊢ ∀x. 'x = 'x") == Sequent(Set(forallEq), Set(forallEq)))
     val existsXEq = BinderFormula(Exists, x, PredicateFormula(equality, Seq(x, x)))
-    assert(Parser.parseSequent("∀x. ?x = ?x ⊢ ∃x. ?x = ?x") == Sequent(Set(forallEq), Set(existsXEq)))
+    assert(Parser.parseSequent("∀x. 'x = 'x ⊢ ∃x. 'x = 'x") == Sequent(Set(forallEq), Set(existsXEq)))
     val existsYEq = BinderFormula(Exists, y, PredicateFormula(equality, Seq(y, y)))
-    assert(Parser.parseSequent("∀x. ?x = ?x ⊢ ∃x. ?x = ?x; ∃y. ?y = ?y") == Sequent(Set(forallEq), Set(existsYEq, existsXEq)))
+    assert(Parser.parseSequent("∀x. 'x = 'x ⊢ ∃x. 'x = 'x; ∃y. 'y = 'y") == Sequent(Set(forallEq), Set(existsYEq, existsXEq)))
     assert(
-      Parser.parseSequent("p ; ∀x. ?x = ?x ⊢ ∃x. ?x = ?x; ∃y. ?y = ?y") ==
+      Parser.parseSequent("p ; ∀x. 'x = 'x ⊢ ∃x. 'x = 'x; ∃y. 'y = 'y") ==
         Sequent(Set(forallEq, PredicateFormula(ConstantPredicateLabel("p", 0), Seq())), Set(existsYEq, existsXEq))
     )
   }
@@ -197,23 +197,23 @@ class ParserTest extends AnyFunSuite with TestUtils {
   test("sequents from Mapping and SetTheory") {
     val va = VariableLabel("a")
     val leftAndRight = BinderFormula(ExistsOne, x, PredicateFormula(sPhi2, Seq(x, va)))
-    assert(Parser.parseSequent("∃!x. ?phi(?x, ?a) ⊢ ∃!x. ?phi(?x, ?a)") == Sequent(Set(leftAndRight), Set(leftAndRight)))
+    assert(Parser.parseSequent("∃!x. 'phi('x, 'a) ⊢ ∃!x. 'phi('x, 'a)") == Sequent(Set(leftAndRight), Set(leftAndRight)))
 
     assert(
-      Parser.parseSequent("∀x. (?x = ?x1) ↔ ?phi(?x) ⊢ (?z = ?f(?x1)) ⇒ (∃x. (?z = ?f(?x)) ∧ ?phi(?x))") == Sequent(
+      Parser.parseSequent("∀x. ('x = 'x1) ↔ 'phi('x) ⊢ ('z = 'f('x1)) ⇒ (∃x. ('z = 'f('x)) ∧ 'phi('x))") == Sequent(
         Set(BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(x === x1, sPhi1(x))))),
         Set((z === sf1(x1)) ==> exists(x, (z === sf1(x)) /\ sPhi1(x)))
       )
     )
     assert(
-      Parser.parseSequent("∃x1. ∀x. (?x = ?x1) ↔ ?phi(?x) ⊢ ∃z1. ∀z. (?z = ?z1) ↔ (∃x. (?z = ?f(?x)) ∧ ?phi(?x))") == (exists(x1, forall(x, (x === x1) <=> (sPhi1(x)))) |- exists(
+      Parser.parseSequent("∃x1. ∀x. ('x = 'x1) ↔ 'phi('x) ⊢ ∃z1. ∀z. ('z = 'z1) ↔ (∃x. ('z = 'f('x)) ∧ 'phi('x))") == (exists(x1, forall(x, (x === x1) <=> (sPhi1(x)))) |- exists(
         z1,
         forall(z, (z === z1) <=> exists(x, (z === sf1(x)) /\ sPhi1(x)))
       ))
     )
-    assert(Parser.parseSequent("⊢ (?x = ?x) ∨ (?x = ?y)") == (() |- (x === x) \/ (x === y)))
+    assert(Parser.parseSequent("⊢ ('x = 'x) ∨ ('x = 'y)") == (() |- (x === x) \/ (x === y)))
     assert(
-      Parser.parseSequent("(?x = ?x) ∨ (?x = ?y); (?x = ?x) ∨ (?x = ?y) ↔ (?x = ?x') ∨ (?x = ?y') ⊢ (?x = ?x') ∨ (?x = ?y')") == (Set(
+      Parser.parseSequent("('x = 'x) ∨ ('x = 'y); ('x = 'x) ∨ ('x = 'y) ↔ ('x = 'x') ∨ ('x = 'y') ⊢ ('x = 'x') ∨ ('x = 'y')") == (Set(
         (x === x) \/ (x === y),
         ((x === x) \/ (x === y)) <=> ((x === xPrime) \/ (x === yPrime))
       ) |- (x === xPrime) \/ (x === yPrime))
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index a15b86b89d0ece8d3eb5ae20a11db66165e9dd4e..5fd97a7f959e2d007a01a53cf13bdd51e0d500bb 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -26,17 +26,17 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(b)), ConnectorFormula(Neg, Seq(c))))))) == "¬a ∧ (¬b ∧ ¬c)")
     assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(Neg, Seq(b)))), ConnectorFormula(Neg, Seq(c))))) == "¬a ∧ ¬b ∧ ¬c")
 
-    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ ?x = ?x")
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ 'x = 'x")
 
-    assert(Parser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀ ?x. ?x = ?x")
-    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ (∀ ?x. ?x = ?x)")
-    assert(Parser.printFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀ ?x. b) ∧ a")
-    assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ ?x. b) ∧ a")
-    assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ ?x. b) ∨ a")
+    assert(Parser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀ 'x. 'x = 'x")
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ (∀ 'x. 'x = 'x)")
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀ 'x. b) ∧ a")
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ 'x. b) ∧ a")
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ 'x. b) ∨ a")
 
-    assert(Parser.printFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀ ?x. ∃ ?y. ∃! ?z. a")
+    assert(Parser.printFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀ 'x. ∃ 'y. ∃! 'z. a")
 
-    assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("f", 3), Seq(x, y, z))) == "f(?x, ?y, ?z)")
+    assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("f", 3), Seq(x, y, z))) == "f('x, 'y, 'z)")
   }
 
   test("constant") {
@@ -44,7 +44,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
   }
 
   test("variable") {
-    assert(Parser.printTerm(VariableTerm(x)) == "?x")
+    assert(Parser.printTerm(VariableTerm(x)) == "'x")
   }
 
   test("constant function application") {
@@ -52,23 +52,23 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     assert(Parser.printTerm(Term(f2, Seq(cx, cy))) == "f(x, y)")
     assert(Parser.printTerm(Term(f3, Seq(cx, cy, cz))) == "f(x, y, z)")
 
-    assert(Parser.printTerm(Term(f1, Seq(x))) == "f(?x)")
-    assert(Parser.printTerm(Term(f2, Seq(x, y))) == "f(?x, ?y)")
-    assert(Parser.printTerm(Term(f3, Seq(x, y, z))) == "f(?x, ?y, ?z)")
+    assert(Parser.printTerm(Term(f1, Seq(x))) == "f('x)")
+    assert(Parser.printTerm(Term(f2, Seq(x, y))) == "f('x, 'y)")
+    assert(Parser.printTerm(Term(f3, Seq(x, y, z))) == "f('x, 'y, 'z)")
   }
 
   test("schematic function application") {
-    assert(Parser.printTerm(Term(sf1, Seq(cx))) == "?f(x)")
-    assert(Parser.printTerm(Term(sf2, Seq(cx, cy))) == "?f(x, y)")
-    assert(Parser.printTerm(Term(sf3, Seq(cx, cy, cz))) == "?f(x, y, z)")
+    assert(Parser.printTerm(Term(sf1, Seq(cx))) == "'f(x)")
+    assert(Parser.printTerm(Term(sf2, Seq(cx, cy))) == "'f(x, y)")
+    assert(Parser.printTerm(Term(sf3, Seq(cx, cy, cz))) == "'f(x, y, z)")
 
-    assert(Parser.printTerm(Term(sf1, Seq(x))) == "?f(?x)")
-    assert(Parser.printTerm(Term(sf2, Seq(x, y))) == "?f(?x, ?y)")
-    assert(Parser.printTerm(Term(sf3, Seq(x, y, z))) == "?f(?x, ?y, ?z)")
+    assert(Parser.printTerm(Term(sf1, Seq(x))) == "'f('x)")
+    assert(Parser.printTerm(Term(sf2, Seq(x, y))) == "'f('x, 'y)")
+    assert(Parser.printTerm(Term(sf3, Seq(x, y, z))) == "'f('x, 'y, 'z)")
   }
 
   test("nested function application") {
-    assert(Parser.printTerm(Term(sf2, Seq(Term(sf1, Seq(x)), y))) == "?f(?f(?x), ?y)")
+    assert(Parser.printTerm(Term(sf2, Seq(Term(sf1, Seq(x)), y))) == "'f('f('x), 'y)")
   }
 
   test("0-ary predicate") {
@@ -77,12 +77,12 @@ class PrinterTest extends AnyFunSuite with TestUtils {
 
   test("predicate application") {
     assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("p", 3), Seq(cx, cy, cz))) == "p(x, y, z)")
-    assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z))) == "p(?x, ?y, ?z)")
+    assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z))) == "p('x, 'y, 'z)")
   }
 
   test("equality") {
     assert(Parser.printFormula(PredicateFormula(equality, Seq(cx, cx))) == "x = x")
-    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ ?x = ?x")
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ 'x = 'x")
   }
 
   test("unicode connectors") {
@@ -144,17 +144,17 @@ class PrinterTest extends AnyFunSuite with TestUtils {
   }
 
   test("quantifiers") {
-    assert(Parser.printFormula(BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∀ ?x. p")
-    assert(Parser.printFormula(BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∃ ?x. p")
-    assert(Parser.printFormula(BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∃! ?x. p")
+    assert(Parser.printFormula(BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∀ 'x. p")
+    assert(Parser.printFormula(BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∃ 'x. p")
+    assert(Parser.printFormula(BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∃! 'x. p")
   }
 
   test("nested quantifiers") {
-    assert(Parser.printFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀ ?x. ∃ ?y. ∃! ?z. a")
+    assert(Parser.printFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀ 'x. ∃ 'y. ∃! 'z. a")
   }
 
   test("quantifier parentheses") {
-    assert(Parser.printFormula(BinderFormula(Forall, x, ConnectorFormula(And, Seq(b, a)))) == "∀ ?x. b ∧ a")
+    assert(Parser.printFormula(BinderFormula(Forall, x, ConnectorFormula(And, Seq(b, a)))) == "∀ 'x. b ∧ a")
     assert(
       Parser.printFormula(
         BinderFormula(
@@ -162,10 +162,10 @@ class PrinterTest extends AnyFunSuite with TestUtils {
           x,
           ConnectorFormula(And, Seq(PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x)), PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))))
         )
-      ) == "∀ ?x. p(?x) ∧ q(?x)"
+      ) == "∀ 'x. p('x) ∧ q('x)"
     )
 
-    assert(Parser.printFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀ ?x. b) ∧ a")
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀ 'x. b) ∧ a")
 
     assert(
       Parser.printFormula(
@@ -176,11 +176,11 @@ class PrinterTest extends AnyFunSuite with TestUtils {
             PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))
           )
         )
-      ) == "(∀ ?x. p(?x)) ∧ q(?x)"
+      ) == "(∀ 'x. p('x)) ∧ q('x)"
     )
 
-    assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ ?x. b) ∨ a")
-    assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ ?x. b) ∧ a")
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ 'x. b) ∨ a")
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ 'x. b) ∧ a")
   }
 
   test("complex formulas with connectors") {
@@ -191,15 +191,15 @@ class PrinterTest extends AnyFunSuite with TestUtils {
   }
 
   test("complex formulas") {
-    assert(Parser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀ ?x. ?x = ?x")
+    assert(Parser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀ 'x. 'x = 'x")
   }
 
   test("sequent") {
     val forallEq = BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))
-    assert(Parser.printSequent(Sequent(Set(), Set(forallEq))) == "⊢ ∀ ?x. ?x = ?x")
-    assert(Parser.printSequent(Sequent(Set(forallEq), Set(forallEq))) == "∀ ?x. ?x = ?x ⊢ ∀ ?x. ?x = ?x")
+    assert(Parser.printSequent(Sequent(Set(), Set(forallEq))) == "⊢ ∀ 'x. 'x = 'x")
+    assert(Parser.printSequent(Sequent(Set(forallEq), Set(forallEq))) == "∀ 'x. 'x = 'x ⊢ ∀ 'x. 'x = 'x")
     val existsXEq = BinderFormula(Exists, x, PredicateFormula(equality, Seq(x, x)))
-    assert(Parser.printSequent(Sequent(Set(forallEq), Set(existsXEq))) == "∀ ?x. ?x = ?x ⊢ ∃ ?x. ?x = ?x")
+    assert(Parser.printSequent(Sequent(Set(forallEq), Set(existsXEq))) == "∀ 'x. 'x = 'x ⊢ ∃ 'x. 'x = 'x")
   }
 
   // warning: this test might be flaky because formula order is not fixed in sequents but fixed in the string representation
@@ -208,11 +208,11 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     val existsXEq = BinderFormula(Exists, x, PredicateFormula(equality, Seq(x, x)))
     val existsYEq = BinderFormula(Exists, y, PredicateFormula(equality, Seq(y, y)))
     assert(
-      Parser.printSequent(Sequent(Set(forallEq), Set(existsYEq, existsXEq))) == "∀ ?x. ?x = ?x ⊢ ∃ ?y. ?y = ?y; " +
-        "∃ ?x. ?x = ?x"
+      Parser.printSequent(Sequent(Set(forallEq), Set(existsYEq, existsXEq))) == "∀ 'x. 'x = 'x ⊢ ∃ 'y. 'y = 'y; " +
+        "∃ 'x. 'x = 'x"
     )
     assert(
-      Parser.printSequent(Sequent(Set(forallEq, PredicateFormula(ConstantPredicateLabel("p", 0), Seq())), Set(existsYEq, existsXEq))) == "∀ ?x. ?x = ?x; p ⊢ ∃ ?y. ?y = ?y; ∃ ?x. ?x = ?x"
+      Parser.printSequent(Sequent(Set(forallEq, PredicateFormula(ConstantPredicateLabel("p", 0), Seq())), Set(existsYEq, existsXEq))) == "∀ 'x. 'x = 'x; p ⊢ ∃ 'y. 'y = 'y; ∃ 'x. 'x = 'x"
     )
   }
 
@@ -220,7 +220,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
   test("sequents from Mapping and SetTheory") {
     val va = VariableLabel("a")
     val leftAndRight = BinderFormula(ExistsOne, x, PredicateFormula(sPhi2, Seq(x, va)))
-    assert(Parser.printSequent(Sequent(Set(leftAndRight), Set(leftAndRight))) == "∃! ?x. ?phi(?x, ?a) ⊢ ∃! ?x. ?phi(?x, ?a)")
+    assert(Parser.printSequent(Sequent(Set(leftAndRight), Set(leftAndRight))) == "∃! 'x. 'phi('x, 'a) ⊢ ∃! 'x. 'phi('x, 'a)")
 
     assert(
       Parser.printSequent(
@@ -228,7 +228,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
           Set(BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(x === x1, sPhi1(x))))),
           Set((z === sf1(x1)) ==> exists(x, (z === sf1(x)) /\ sPhi1(x)))
         )
-      ) == "∀ ?x. ?x = ?x1 ⇔ ?phi(?x) ⊢ ?z = ?f(?x1) ⇒ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
+      ) == "∀ 'x. 'x = 'x1 ⇔ 'phi('x) ⊢ 'z = 'f('x1) ⇒ (∃ 'x. 'z = 'f('x) ∧ 'phi('x))"
     )
     assert(
       Parser.printSequent(
@@ -236,16 +236,16 @@ class PrinterTest extends AnyFunSuite with TestUtils {
           z1,
           forall(z, (z === z1) <=> exists(x, (z === sf1(x)) /\ sPhi1(x)))
         )
-      ) == "∃ ?x1. ∀ ?x. ?x = ?x1 ⇔ ?phi(?x) ⊢ ∃ ?z1. ∀ ?z. ?z = ?z1 ⇔ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
+      ) == "∃ 'x1. ∀ 'x. 'x = 'x1 ⇔ 'phi('x) ⊢ ∃ 'z1. ∀ 'z. 'z = 'z1 ⇔ (∃ 'x. 'z = 'f('x) ∧ 'phi('x))"
     )
-    assert(Parser.printSequent((() |- (x === x) \/ (x === y))) == "⊢ ?x = ?x ∨ ?x = ?y")
+    assert(Parser.printSequent((() |- (x === x) \/ (x === y))) == "⊢ 'x = 'x ∨ 'x = 'y")
     assert(
       Parser.printSequent(
         Set(
           (x === x) \/ (x === y),
           ((x === x) \/ (x === y)) <=> ((x === xPrime) \/ (x === yPrime))
         ) |- (x === xPrime) \/ (x === yPrime)
-      ) == "?x = ?x ∨ ?x = ?y; ?x = ?x ∨ ?x = ?y ⇔ ?x = ?x' ∨ ?x = ?y' ⊢ ?x = ?x' ∨ ?x = ?y'"
+      ) == "'x = 'x ∨ 'x = 'y; 'x = 'x ∨ 'x = 'y ⇔ 'x = 'x' ∨ 'x = 'y' ⊢ 'x = 'x' ∨ 'x = 'y'"
     )
   }
 }