diff --git a/src/formatting/fol/tptp.rs b/src/formatting/fol/tptp.rs
index e6f472a7..bbb7518d 100644
--- a/src/formatting/fol/tptp.rs
+++ b/src/formatting/fol/tptp.rs
@@ -46,8 +46,8 @@ impl Display for Format<'_, IntegerTerm> {
 
                 Ok(())
             }
-            IntegerTerm::Variable(v) => write!(f, "{v}$i"),
-            IntegerTerm::FunctionConstant(c) => write!(f, "{c}$i"),
+            IntegerTerm::Variable(v) => write!(f, "{v}_i"),
+            IntegerTerm::FunctionConstant(c) => write!(f, "{c}_i"),
             IntegerTerm::UnaryOperation { op, arg } => {
                 let op = Format(op);
                 let arg = Format(arg.as_ref());
@@ -67,8 +67,8 @@ impl Display for Format<'_, SymbolicTerm> {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
         match self.0 {
             SymbolicTerm::Symbol(s) => write!(f, "{s}"),
-            SymbolicTerm::FunctionConstant(c) => write!(f, "{c}$s"),
-            SymbolicTerm::Variable(v) => write!(f, "{v}$s"),
+            SymbolicTerm::FunctionConstant(c) => write!(f, "{c}_s"),
+            SymbolicTerm::Variable(v) => write!(f, "{v}_s"),
         }
     }
 }
@@ -78,8 +78,8 @@ impl Display for Format<'_, GeneralTerm> {
         match self.0 {
             GeneralTerm::Infimum => write!(f, "c__infimum__"),
             GeneralTerm::Supremum => write!(f, "c__supremum__"),
-            GeneralTerm::FunctionConstant(c) => write!(f, "{c}$g"),
-            GeneralTerm::Variable(v) => write!(f, "{v}"),
+            GeneralTerm::FunctionConstant(c) => write!(f, "{c}_g"),
+            GeneralTerm::Variable(v) => write!(f, "{v}_g"),
             GeneralTerm::IntegerTerm(t) => write!(f, "f__integer__({})", Format(t)),
             GeneralTerm::SymbolicTerm(t) => write!(f, "f__symbolic__({})", Format(t)),
         }
@@ -206,9 +206,9 @@ impl Display for Format<'_, FunctionConstant> {
         let sort = &self.0.sort;
 
         match sort {
-            Sort::General => write!(f, "{name}$g"),
-            Sort::Integer => write!(f, "{name}$i"),
-            Sort::Symbol => write!(f, "{name}$s"),
+            Sort::General => write!(f, "{name}_g"),
+            Sort::Integer => write!(f, "{name}_i"),
+            Sort::Symbol => write!(f, "{name}_s"),
         }
     }
 }
@@ -219,9 +219,9 @@ impl Display for Format<'_, Variable> {
         let sort = &self.0.sort;
 
         match sort {
-            Sort::General => write!(f, "{name}"),
-            Sort::Integer => write!(f, "{name}$i"),
-            Sort::Symbol => write!(f, "{name}$s"),
+            Sort::General => write!(f, "{name}_g"),
+            Sort::Integer => write!(f, "{name}_i"),
+            Sort::Symbol => write!(f, "{name}_s"),
         }
     }
 }
@@ -337,7 +337,7 @@ mod tests {
         );
         assert_eq!(
             Format(&IntegerTerm::Variable("A".into())).to_string(),
-            "A$i"
+            "A_i"
         );
         assert_eq!(
             Format(&IntegerTerm::BinaryOperation {
@@ -355,7 +355,7 @@ mod tests {
                 rhs: IntegerTerm::Variable("N".into()).into(),
             })
             .to_string(),
-            "$sum(10, N$i)"
+            "$sum(10, N_i)"
         );
         assert_eq!(
             Format(&IntegerTerm::BinaryOperation {
@@ -368,7 +368,7 @@ mod tests {
                 .into(),
             })
             .to_string(),
-            "$difference($uminus(195), $uminus(N$i))"
+            "$difference($uminus(195), $uminus(N_i))"
         );
     }
 
@@ -377,7 +377,7 @@ mod tests {
         assert_eq!(Format(&SymbolicTerm::Symbol("p".into())).to_string(), "p");
         assert_eq!(
             Format(&SymbolicTerm::Variable("X".into())).to_string(),
-            "X$s"
+            "X_s"
         )
     }
 
@@ -387,7 +387,7 @@ mod tests {
         assert_eq!(Format(&GeneralTerm::Supremum).to_string(), "c__supremum__");
         assert_eq!(
             Format(&GeneralTerm::Variable("N1".into())).to_string(),
-            "N1"
+            "N1_g"
         );
         assert_eq!(
             Format(&GeneralTerm::SymbolicTerm(SymbolicTerm::Symbol("p".into()))).to_string(),
@@ -414,7 +414,7 @@ mod tests {
                 ]
             })
             .to_string(),
-            "prime(f__integer__($sum(N1$i, 3)), f__integer__(5))"
+            "prime(f__integer__($sum(N1_i, 3)), f__integer__(5))"
         )
     }
 
@@ -511,7 +511,7 @@ mod tests {
                 ]
             })
             .to_string(),
-            "$less(1, 2) & p__less__(f__integer__(2), X)"
+            "$less(1, 2) & p__less__(f__integer__(2), X_g)"
         );
         assert_eq!(
             Format(&Comparison {
@@ -522,7 +522,7 @@ mod tests {
                 },]
             })
             .to_string(),
-            "$less(1, N$i)"
+            "$less(1, N_i)"
         );
         assert_eq!(
             Format(&Comparison {
@@ -534,7 +534,7 @@ mod tests {
             })
             .to_string(),
             // "f__symbolic__(a) = f__symbolic__(B$s)"
-            "a = B$s"
+            "a = B_s"
         );
         assert_eq!(
             Format(&Comparison {
@@ -545,7 +545,7 @@ mod tests {
                 },]
             })
             .to_string(),
-            "p__less__(f__symbolic__(a), f__symbolic__(B$s))"
+            "p__less__(f__symbolic__(a), f__symbolic__(B_s))"
         );
     }
 
@@ -566,7 +566,7 @@ mod tests {
                 ]
             })
             .to_string(),
-            "![X1$i: $int, N2: general]"
+            "![X1_i: $int, N2_g: general]"
         );
         assert_eq!(
             Format(&Quantification {
@@ -577,7 +577,7 @@ mod tests {
                 },]
             })
             .to_string(),
-            "?[X1$s: symbol]"
+            "?[X1_s: symbol]"
         );
     }
 
@@ -648,7 +648,51 @@ mod tests {
                 .into()
             })
             .to_string(),
-            "![X$i: $int, Y1: general]: (p & q)"
+            "![X_i: $int, Y1_g: general]: (p & q)"
+        );
+        assert_eq!(
+            Format(&Formula::QuantifiedFormula {
+                quantification: Quantification {
+                    quantifier: Quantifier::Forall,
+                    variables: vec![
+                        Variable {
+                            name: "X_i".into(),
+                            sort: Sort::Symbol,
+                        },
+                        Variable {
+                            name: "X".into(),
+                            sort: Sort::Integer,
+                        },
+                        Variable {
+                            name: "Y1".into(),
+                            sort: Sort::General,
+                        },
+                    ]
+                },
+                formula: Formula::BinaryFormula {
+                    connective: BinaryConnective::Conjunction,
+                    lhs: Formula::BinaryFormula {
+                        connective: BinaryConnective::Conjunction,
+                        lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
+                            predicate_symbol: "p".into(),
+                            terms: vec![GeneralTerm::IntegerTerm(IntegerTerm::Variable("X".to_string()))],
+                        }))
+                        .into(),
+                        rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
+                            predicate_symbol: "q".into(),
+                            terms: vec![GeneralTerm::Variable("Y1".to_string())],
+                        }))
+                        .into(),
+                    }.into(),
+                    rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
+                        predicate_symbol: "t".into(),
+                        terms: vec![GeneralTerm::SymbolicTerm(SymbolicTerm::Variable("X_i".into()))],
+                    }))
+                    .into(),
+                }.into()
+            })
+            .to_string(),
+            "![X_i_s: symbol, X_i: $int, Y1_g: general]: (p(f__integer__(X_i)) & q(Y1_g) & t(f__symbolic__(X_i_s)))"
         );
     }
 }