diff --git a/src/format_tptp.rs b/src/format_tptp.rs
index 8e39ce9..03556c0 100644
--- a/src/format_tptp.rs
+++ b/src/format_tptp.rs
@@ -4,6 +4,27 @@ pub trait DisplayTPTP<'a, DisplayType>
 	fn display_tptp(&'a self) -> DisplayType;
 }
 
+fn is_arithmetic_term(term: &foliage::Term) -> bool
+{
+	match term
+	{
+		foliage::Term::Infimum => false,
+		foliage::Term::Supremum => false,
+		foliage::Term::Integer(_) => true,
+		foliage::Term::Symbolic(_) => false,
+		foliage::Term::String(_) => false,
+		foliage::Term::Variable(ref declaration) => match declaration.domain
+		{
+			foliage::Domain::Program => false,
+			foliage::Domain::Integer => true,
+		},
+		foliage::Term::Add(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right),
+		foliage::Term::Subtract(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right),
+		foliage::Term::Multiply(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right),
+		foliage::Term::Negative(ref argument) => is_arithmetic_term(argument),
+	}
+}
+
 struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration);
 struct TermDisplay<'a>(&'a foliage::Term);
 struct FormulaDisplay<'a>(&'a foliage::Formula);
@@ -106,6 +127,52 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
+		#[derive(Eq, PartialEq)]
+		enum Notation
+		{
+			Prefix,
+			Infix,
+		}
+
+		let mut display_comparison = |notation, operator_identifier: &str, left, right| -> Result<(), std::fmt::Error>
+		{
+			if notation == Notation::Prefix
+			{
+				write!(format, "{}(", operator_identifier)?;
+			}
+
+			if is_arithmetic_term(left) && !is_arithmetic_term(right)
+			{
+				write!(format, "f__integer__({})", left.display_tptp())?;
+			}
+			else
+			{
+				write!(format, "{}", left.display_tptp())?;
+			}
+
+			match notation
+			{
+				Notation::Prefix => write!(format, ", ")?,
+				Notation::Infix => write!(format, " {} ", operator_identifier)?,
+			}
+
+			if is_arithmetic_term(right) && !is_arithmetic_term(left)
+			{
+				write!(format, "f__integer__({})", right.display_tptp())?;
+			}
+			else
+			{
+				write!(format, "{}", right.display_tptp())?;
+			}
+
+			if notation == Notation::Prefix
+			{
+				write!(format, ")")?;
+			}
+
+			Ok(())
+		};
+
 		match self.0
 		{
 			foliage::Formula::Exists(ref exists) =>
@@ -167,12 +234,12 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
 			},
 			foliage::Formula::Implies(ref left, ref right) => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()),
 			foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", left.display_tptp(), right.display_tptp()),
-			foliage::Formula::Less(ref left, ref right) => write!(format, "$less({:?}, {:?})", left.display_tptp(), right.display_tptp()),
-			foliage::Formula::LessOrEqual(ref left, ref right) => write!(format, "$lesseq({:?}, {:?})", left.display_tptp(), right.display_tptp()),
-			foliage::Formula::Greater(ref left, ref right) => write!(format, "$greater({:?}, {:?})", left.display_tptp(), right.display_tptp()),
-			foliage::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "$greatereq({:?}, {:?})", left.display_tptp(), right.display_tptp()),
-			foliage::Formula::Equal(ref left, ref right) => write!(format, "({:?} = {:?})", left.display_tptp(), right.display_tptp()),
-			foliage::Formula::NotEqual(ref left, ref right) => write!(format, "({:?} ~= {:?})", left.display_tptp(), right.display_tptp()),
+			foliage::Formula::Less(ref left, ref right) => display_comparison(Notation::Prefix, "$less", left, right),
+			foliage::Formula::LessOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$lesseq", left, right),
+			foliage::Formula::Greater(ref left, ref right) => display_comparison(Notation::Prefix, "$greater", left, right),
+			foliage::Formula::GreaterOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$greatereq", left, right),
+			foliage::Formula::Equal(ref left, ref right) => display_comparison(Notation::Infix, "=", left, right),
+			foliage::Formula::NotEqual(ref left, ref right) => display_comparison(Notation::Infix, "~=", left, right),
 			foliage::Formula::Boolean(value) =>
 				match value
 				{