diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index c8f1210..452f786 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -16,7 +16,8 @@ fn requires_parentheses<'formula>(formula: &'formula crate::Formula,
 		| Formula::ForAll(_)
 			=> false,
 		Formula::And(formulas)
-		| Formula::Or(formulas) if formulas.len() <= 1
+		| Formula::Or(formulas)
+		| Formula::IfAndOnlyIf(formulas) if formulas.len() <= 1
 			=> false,
 		Formula::And(_) => match *parent_formula
 		{
@@ -238,11 +239,19 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			{
 				let mut separator = "";
 
+				assert!(!arguments.is_empty());
+
+				let parent_formula = match arguments.len()
+				{
+					0 | 1 => self.parent_formula,
+					_ => Some(self.formula),
+				};
+
 				for argument in arguments
 				{
-					write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
+					write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
 
-					separator = " <-> ";
+					separator = " <-> "
 				}
 			},
 			crate::Formula::Compare(
@@ -815,39 +824,317 @@ mod tests
 	#[test]
 	fn format_combination_not_and_lower()
 	{
+		// Not + not
 		assert_eq!(format(not(not(predicate("p", vec![])))), "not not p");
 
+		// Not + quantified formulas
 		assert_eq!(format(
 			not(exists(vec![variable_declaration("X"), variable_declaration("Y"),
 				variable_declaration("Z")], predicate("p", vec![])))),
 			"not exists X, Y, Z p");
+		assert_eq!(format(
+			not(exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], and(vec![predicate("p", vec![])])))),
+			"not exists X, Y, Z p");
+		assert_eq!(format(
+			not(exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], or(vec![predicate("p", vec![])])))),
+			"not exists X, Y, Z p");
+		assert_eq!(format(
+			not(exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], if_and_only_if(vec![predicate("p", vec![])])))),
+			"not exists X, Y, Z p");
 		assert_eq!(format(
 			exists(vec![variable_declaration("X"), variable_declaration("Y"),
 				variable_declaration("Z")], not(predicate("p", vec![])))),
 			"exists X, Y, Z not p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], and(vec![not(predicate("p", vec![]))]))),
+			"exists X, Y, Z not p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], or(vec![not(predicate("p", vec![]))]))),
+			"exists X, Y, Z not p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], if_and_only_if(vec![not(predicate("p", vec![]))]))),
+			"exists X, Y, Z not p");
 		assert_eq!(format(
 			not(for_all(vec![variable_declaration("X"), variable_declaration("Y"),
 				variable_declaration("Z")], predicate("p", vec![])))),
 			"not forall X, Y, Z p");
+		assert_eq!(format(
+			not(for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], and(vec![predicate("p", vec![])])))),
+			"not forall X, Y, Z p");
+		assert_eq!(format(
+			not(for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], or(vec![predicate("p", vec![])])))),
+			"not forall X, Y, Z p");
+		assert_eq!(format(
+			not(for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], if_and_only_if(vec![predicate("p", vec![])])))),
+			"not forall X, Y, Z p");
 		assert_eq!(format(
 			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
 				variable_declaration("Z")], not(predicate("p", vec![])))),
 			"forall X, Y, Z not p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], and(vec![not(predicate("p", vec![]))]))),
+			"forall X, Y, Z not p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], or(vec![not(predicate("p", vec![]))]))),
+			"forall X, Y, Z not p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")], if_and_only_if(vec![not(predicate("p", vec![]))]))),
+			"forall X, Y, Z not p");
 
+		// Not + and
 		assert_eq!(format(
 			not(and(vec![predicate("p", vec![])]))),
 			"not p");
+		assert_eq!(format(
+			not(and(vec![and(vec![predicate("p", vec![])])]))),
+			"not p");
+		assert_eq!(format(
+			not(or(vec![and(vec![predicate("p", vec![])])]))),
+			"not p");
+		assert_eq!(format(
+			not(if_and_only_if(vec![and(vec![predicate("p", vec![])])]))),
+			"not p");
 		assert_eq!(format(
 			not(and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
 			"not (p and q and r)");
-
 		assert_eq!(format(
-			or(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
-			"p or q or r");
-
+			not(and(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])])]))),
+			"not (p and q and r)");
 		assert_eq!(format(
-			and(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
-			"p and (q or r)");
+			not(or(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])])]))),
+			"not (p and q and r)");
+		assert_eq!(format(
+			not(if_and_only_if(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])])]))),
+			"not (p and q and r)");
+		assert_eq!(format(
+			and(vec![not(predicate("p", vec![]))])),
+			"not p");
+		assert_eq!(format(
+			and(vec![not(and(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			and(vec![not(or(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			and(vec![not(if_and_only_if(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			and(vec![not(predicate("p", vec![])), not(predicate("q", vec![])),
+				not(predicate("r", vec![]))])),
+			"not p and not q and not r");
+		assert_eq!(format(
+			and(vec![and(vec![not(predicate("p", vec![]))]),
+				and(vec![not(predicate("q", vec![]))]), and(vec![not(predicate("r", vec![]))])])),
+			"not p and not q and not r");
+		assert_eq!(format(
+			and(vec![or(vec![not(predicate("p", vec![]))]),
+				or(vec![not(predicate("q", vec![]))]), or(vec![not(predicate("r", vec![]))])])),
+			"not p and not q and not r");
+		assert_eq!(format(
+			and(vec![if_and_only_if(vec![not(predicate("p", vec![]))]),
+				if_and_only_if(vec![not(predicate("q", vec![]))]),
+				if_and_only_if(vec![not(predicate("r", vec![]))])])),
+			"not p and not q and not r");
+
+		// Not + or
+		assert_eq!(format(
+			not(or(vec![predicate("p", vec![])]))),
+			"not p");
+		assert_eq!(format(
+			not(and(vec![or(vec![predicate("p", vec![])])]))),
+			"not p");
+		assert_eq!(format(
+			not(or(vec![or(vec![predicate("p", vec![])])]))),
+			"not p");
+		assert_eq!(format(
+			not(if_and_only_if(vec![or(vec![predicate("p", vec![])])]))),
+			"not p");
+		assert_eq!(format(
+			not(or(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
+			"not (p or q or r)");
+		assert_eq!(format(
+			not(and(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])])]))),
+			"not (p or q or r)");
+		assert_eq!(format(
+			not(or(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])])]))),
+			"not (p or q or r)");
+		assert_eq!(format(
+			not(if_and_only_if(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])])]))),
+			"not (p or q or r)");
+		assert_eq!(format(
+			or(vec![not(predicate("p", vec![]))])),
+			"not p");
+		assert_eq!(format(
+			or(vec![not(and(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			or(vec![not(or(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			or(vec![not(if_and_only_if(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			or(vec![not(predicate("p", vec![])), not(predicate("q", vec![])),
+				not(predicate("r", vec![]))])),
+			"not p or not q or not r");
+		assert_eq!(format(
+			or(vec![and(vec![not(predicate("p", vec![]))]),
+				and(vec![not(predicate("q", vec![]))]), and(vec![not(predicate("r", vec![]))])])),
+			"not p or not q or not r");
+		assert_eq!(format(
+			or(vec![or(vec![not(predicate("p", vec![]))]),
+				or(vec![not(predicate("q", vec![]))]), or(vec![not(predicate("r", vec![]))])])),
+			"not p or not q or not r");
+		assert_eq!(format(
+			or(vec![if_and_only_if(vec![not(predicate("p", vec![]))]),
+				if_and_only_if(vec![not(predicate("q", vec![]))]),
+				if_and_only_if(vec![not(predicate("r", vec![]))])])),
+			"not p or not q or not r");
+
+		// Not + implies
+		assert_eq!(format(
+			not(implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+				predicate("q", vec![])))),
+			"not (p -> q)");
+		assert_eq!(format(
+			not(and(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+				predicate("q", vec![]))]))),
+			"not (p -> q)");
+		assert_eq!(format(
+			not(or(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+				predicate("q", vec![]))]))),
+			"not (p -> q)");
+		assert_eq!(format(
+			not(if_and_only_if(vec![implies(ImplicationDirection::LeftToRight,
+				predicate("p", vec![]), predicate("q", vec![]))]))),
+			"not (p -> q)");
+		assert_eq!(format(
+			not(implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+				predicate("q", vec![])))),
+			"not (q <- p)");
+		assert_eq!(format(
+			not(and(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+				predicate("q", vec![]))]))),
+			"not (q <- p)");
+		assert_eq!(format(
+			not(or(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+				predicate("q", vec![]))]))),
+			"not (q <- p)");
+		assert_eq!(format(
+			not(if_and_only_if(vec![implies(ImplicationDirection::RightToLeft,
+				predicate("p", vec![]), predicate("q", vec![]))]))),
+			"not (q <- p)");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight, not(predicate("p", vec![])),
+				not(predicate("q", vec![])))),
+			"not p -> not q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight, and(vec![not(predicate("p", vec![]))]),
+				and(vec![not(predicate("q", vec![]))]))),
+			"not p -> not q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight, or(vec![not(predicate("p", vec![]))]),
+				or(vec![not(predicate("q", vec![]))]))),
+			"not p -> not q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				if_and_only_if(vec![not(predicate("p", vec![]))]),
+				if_and_only_if(vec![not(predicate("q", vec![]))]))),
+			"not p -> not q");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft, not(predicate("p", vec![])),
+				not(predicate("q", vec![])))),
+			"not q <- not p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft, and(vec![not(predicate("p", vec![]))]),
+				and(vec![not(predicate("q", vec![]))]))),
+			"not q <- not p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft, or(vec![not(predicate("p", vec![]))]),
+				or(vec![not(predicate("q", vec![]))]))),
+			"not q <- not p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				if_and_only_if(vec![not(predicate("p", vec![]))]),
+				if_and_only_if(vec![not(predicate("q", vec![]))]))),
+			"not q <- not p");
+
+		// Not + if and only if
+		assert_eq!(format(
+			not(if_and_only_if(vec![predicate("p", vec![])]))),
+			"not p");
+		assert_eq!(format(
+			not(and(vec![if_and_only_if(vec![predicate("p", vec![])])]))),
+			"not p");
+		assert_eq!(format(
+			not(or(vec![if_and_only_if(vec![predicate("p", vec![])])]))),
+			"not p");
+		assert_eq!(format(
+			not(if_and_only_if(vec![if_and_only_if(vec![predicate("p", vec![])])]))),
+			"not p");
+		assert_eq!(format(
+			not(if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])]))),
+			"not (p <-> q <-> r)");
+		assert_eq!(format(
+			not(and(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])])]))),
+			"not (p <-> q <-> r)");
+		assert_eq!(format(
+			not(or(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+				predicate("r", vec![])])]))),
+			"not (p <-> q <-> r)");
+		assert_eq!(format(
+			not(if_and_only_if(vec![if_and_only_if(vec![predicate("p", vec![]),
+				predicate("q", vec![]), predicate("r", vec![])])]))),
+			"not (p <-> q <-> r)");
+		assert_eq!(format(
+			if_and_only_if(vec![not(predicate("p", vec![]))])),
+			"not p");
+		assert_eq!(format(
+			if_and_only_if(vec![not(and(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			if_and_only_if(vec![not(or(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			if_and_only_if(vec![not(if_and_only_if(vec![predicate("p", vec![])]))])),
+			"not p");
+		assert_eq!(format(
+			if_and_only_if(vec![not(predicate("p", vec![])), not(predicate("q", vec![])),
+				not(predicate("r", vec![]))])),
+			"not p <-> not q <-> not r");
+		assert_eq!(format(
+			if_and_only_if(vec![and(vec![not(predicate("p", vec![]))]),
+				and(vec![not(predicate("q", vec![]))]), and(vec![not(predicate("r", vec![]))])])),
+			"not p <-> not q <-> not r");
+		assert_eq!(format(
+			if_and_only_if(vec![or(vec![not(predicate("p", vec![]))]),
+				or(vec![not(predicate("q", vec![]))]), or(vec![not(predicate("r", vec![]))])])),
+			"not p <-> not q <-> not r");
+		assert_eq!(format(
+			if_and_only_if(vec![if_and_only_if(vec![not(predicate("p", vec![]))]),
+				if_and_only_if(vec![not(predicate("q", vec![]))]),
+				if_and_only_if(vec![not(predicate("r", vec![]))])])),
+			"not p <-> not q <-> not r");
 	}
 
 	#[test]