diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 7cf24d6..282e31a 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -28,10 +28,18 @@ impl std::fmt::Display for crate::PredicateDeclaration
 	}
 }
 
+#[derive(Clone, Copy, Eq, PartialEq)]
+enum ChildPosition
+{
+	Any,
+	ImpliesAntecedent,
+}
+
 struct FormulaDisplay<'formula>
 {
 	formula: &'formula crate::Formula,
 	parent_formula: Option<&'formula crate::Formula>,
+	position: ChildPosition,
 }
 
 impl<'formula> FormulaDisplay<'formula>
@@ -84,16 +92,17 @@ impl<'formula> FormulaDisplay<'formula>
 				| Formula::And(_)
 				| Formula::Or(_)
 					=> true,
-				Formula::Implies(crate::Implies{direction: parent_direction,
-					antecedent: parent_antecedent, ..}) =>
+				Formula::Implies(crate::Implies{direction: parent_direction, ..}) =>
 					if direction == parent_direction
 					{
-						// Implications with the same direction nested on the antecedent side require
-						// parentheses because implication is considered right-associative
-						std::ptr::eq(self.formula, &**parent_antecedent)
+						// Implications with the same direction nested on the antecedent side
+						// require parentheses because implication is considered right-associative
+						self.position == ChildPosition::ImpliesAntecedent
 					}
 					else
 					{
+						// Nested implications with opposite direction always require parentheses
+						// because the order of formulas like p <- q -> r would be ambiguous
 						true
 					},
 				_ => false,
@@ -114,13 +123,14 @@ impl<'formula> FormulaDisplay<'formula>
 }
 
 fn display_formula<'formula>(formula: &'formula crate::Formula,
-	parent_formula: Option<&'formula crate::Formula>)
+	parent_formula: Option<&'formula crate::Formula>, position: ChildPosition)
 	-> FormulaDisplay<'formula>
 {
 	FormulaDisplay
 	{
 		formula,
 		parent_formula,
+		position,
 	}
 }
 
@@ -152,7 +162,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					separator = ", "
 				}
 
-				write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?;
+				write!(format, " {:?}",
+					display_formula(&exists.argument, Some(self.formula), ChildPosition::Any))?;
 			},
 			crate::Formula::ForAll(for_all) =>
 			{
@@ -169,25 +180,27 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					separator = ", "
 				}
 
-				write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?;
+				write!(format, " {:?}",
+					display_formula(&for_all.argument, Some(self.formula), ChildPosition::Any))?;
 			},
 			crate::Formula::Not(argument) => write!(format, "not {:?}",
-				display_formula(argument, Some(self.formula)))?,
+				display_formula(argument, Some(self.formula), ChildPosition::Any))?,
 			crate::Formula::And(arguments) =>
 			{
 				let mut separator = "";
 
 				assert!(!arguments.is_empty());
 
-				let parent_formula = match arguments.len()
+				let (parent_formula, position) = match arguments.len()
 				{
-					0 | 1 => self.parent_formula,
-					_ => Some(self.formula),
+					0 | 1 => (self.parent_formula, self.position),
+					_ => (Some(self.formula), ChildPosition::Any),
 				};
 
 				for argument in arguments
 				{
-					write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
+					write!(format, "{}{:?}", separator,
+						display_formula(argument, parent_formula, position))?;
 
 					separator = " and "
 				}
@@ -198,15 +211,16 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 				assert!(!arguments.is_empty());
 
-				let parent_formula = match arguments.len()
+				let (parent_formula, position) = match arguments.len()
 				{
-					0 | 1 => self.parent_formula,
-					_ => Some(self.formula),
+					0 | 1 => (self.parent_formula, self.position),
+					_ => (Some(self.formula), ChildPosition::Any),
 				};
 
 				for argument in arguments
 				{
-					write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
+					write!(format, "{}{:?}", separator,
+						display_formula(argument, parent_formula, position))?;
 
 					separator = " or "
 				}
@@ -215,12 +229,15 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			{
 				let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
 				{
-					write!(format, "{:?}", display_formula(antecedent, Some(self.formula)))
+					write!(format, "{:?}",
+						display_formula(antecedent, Some(self.formula),
+							ChildPosition::ImpliesAntecedent))
 				};
 
 				let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
 				{
-					write!(format, "{:?}", display_formula(implication, Some(self.formula)))
+					write!(format, "{:?}",
+						display_formula(implication, Some(self.formula), ChildPosition::Any))
 				};
 
 				match direction
@@ -245,15 +262,16 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 				assert!(!arguments.is_empty());
 
-				let parent_formula = match arguments.len()
+				let (parent_formula, position) = match arguments.len()
 				{
-					0 | 1 => self.parent_formula,
-					_ => Some(self.formula),
+					0 | 1 => (self.parent_formula, self.position),
+					_ => (Some(self.formula), ChildPosition::Any),
 				};
 
 				for argument in arguments
 				{
-					write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
+					write!(format, "{}{:?}", separator,
+						display_formula(argument, parent_formula, position))?;
 
 					separator = " <-> "
 				}
@@ -328,7 +346,7 @@ impl std::fmt::Debug for crate::Formula
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", display_formula(&self, None))
+		write!(format, "{:?}", display_formula(&self, None, ChildPosition::Any))
 	}
 }
 
@@ -336,7 +354,7 @@ impl std::fmt::Display for crate::Formula
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{}", display_formula(&self, None))
+		write!(format, "{}", display_formula(&self, None, ChildPosition::Any))
 	}
 }