diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 805a745..00163ad 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -364,14 +364,32 @@ mod tests
 	use crate::*;
 	use crate::format::terms::tests::*;
 
-	fn assert_all<F>(input: F, output: &str)
-	where
-		F: Fn(Box<Fn(Box<Formula>) -> Box<Formula>>) -> Box<Formula>,
+	// Tests all neutral intermediates (such as 1-ary conjunction)
+	macro_rules! assert
 	{
-		assert_eq!(format(input(Box::new(|f| f))), output);
-		assert_eq!(format(input(Box::new(|f| and(vec![f])))), output);
-		assert_eq!(format(input(Box::new(|f| or(vec![f])))), output);
-		assert_eq!(format(input(Box::new(|f| if_and_only_if(vec![f])))), output);
+		($formula:expr, $output:expr) =>
+		{
+			assert_eq!(format($formula), $output);
+		};
+	}
+
+	// Tests all neutral intermediates (such as 1-ary conjunction)
+	macro_rules! assert_all
+	{
+		($intermediate:ident, $formula:expr, $output:expr) =>
+		{
+			let $intermediate = |f| f;
+			assert!($formula, $output);
+
+			let $intermediate = |f| and(vec![f]);
+			assert!($formula, $output);
+
+			let $intermediate = |f| or(vec![f]);
+			assert!($formula, $output);
+
+			let $intermediate = |f| if_and_only_if(vec![f]);
+			assert!($formula, $output);
+		};
 	}
 
 	fn format(formula: Box<ast::Formula>) -> String
@@ -914,115 +932,34 @@ mod tests
 	fn format_combination_not_and_lower()
 	{
 		// Not + not
-		assert_eq!(format(not(not(p()))), "not not p");
+		assert!(not(not(p())), "not not p");
 
 		// Not + quantified formulas
-		assert_eq!(format(not(exists(xyz(), p()))), "not exists X, Y, Z p");
-		assert_eq!(format(not(exists(xyz(), and(vec![p()])))), "not exists X, Y, Z p");
-		assert_eq!(format(not(exists(xyz(), or(vec![p()])))), "not exists X, Y, Z p");
-		assert_eq!(format(not(exists(xyz(), if_and_only_if(vec![p()])))), "not exists X, Y, Z p");
-		assert_eq!(format(exists(xyz(), not(p()))), "exists X, Y, Z not p");
-		assert_eq!(format(exists(xyz(), and(vec![not(p())]))), "exists X, Y, Z not p");
-		assert_eq!(format(exists(xyz(), or(vec![not(p())]))), "exists X, Y, Z not p");
-		assert_eq!(format(exists(xyz(), if_and_only_if(vec![not(p())]))), "exists X, Y, Z not p");
-		assert_eq!(format(not(for_all(xyz(), p()))), "not forall X, Y, Z p");
-		assert_eq!(format(not(for_all(xyz(), and(vec![p()])))), "not forall X, Y, Z p");
-		assert_eq!(format(not(for_all(xyz(), or(vec![p()])))), "not forall X, Y, Z p");
-		assert_eq!(format(not(for_all(xyz(), if_and_only_if(vec![p()])))), "not forall X, Y, Z p");
-		assert_eq!(format(for_all(xyz(), not(p()))), "forall X, Y, Z not p");
-		assert_eq!(format(for_all(xyz(), and(vec![not(p())]))), "forall X, Y, Z not p");
-		assert_eq!(format(for_all(xyz(), or(vec![not(p())]))), "forall X, Y, Z not p");
-		assert_eq!(format(for_all(xyz(), if_and_only_if(vec![not(p())]))), "forall X, Y, Z not p");
+		assert_all!(i, not(exists(xyz(), i(p()))), "not exists X, Y, Z p");
+		assert_all!(i, not(for_all(xyz(), i(p()))), "not forall X, Y, Z p");
+		assert_all!(i, for_all(xyz(), i(not(p()))), "forall X, Y, Z not p");
 
 		// Not + and
-		assert_eq!(format(not(and(pqr()))), "not (p and q and r)");
-		assert_eq!(format(not(and(vec![and(pqr())]))), "not (p and q and r)");
-		assert_eq!(format(not(or(vec![and(pqr())]))), "not (p and q and r)");
-		assert_eq!(format(not(if_and_only_if(vec![and(pqr())]))), "not (p and q and r)");
-		assert_eq!(format(and(vec![not(p())])), "not p");
-		assert_eq!(format(and(vec![not(and(vec![p()]))])), "not p");
-		assert_eq!(format(and(vec![not(or(vec![p()]))])), "not p");
-		assert_eq!(format(and(vec![not(if_and_only_if(vec![p()]))])), "not p");
-		assert_eq!(format(and(vec![not(p()), not(q()), not(r())])), "not p and not q and not r");
-		assert_eq!(format(
-			and(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])),
-			"not p and not q and not r");
-		assert_eq!(format(
-			and(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])),
-			"not p and not q and not r");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]),
-				if_and_only_if(vec![not(r())])])),
+		assert_all!(i, and(vec![not(i(p()))]), "not p");
+		assert_all!(i, not(i(and(pqr()))), "not (p and q and r)");
+		assert_all!(i, and(vec![i(not(p())), i(not(q())), i(not(r()))]),
 			"not p and not q and not r");
 
 		// Not + or
-		assert_eq!(format(not(or(pqr()))), "not (p or q or r)");
-		assert_eq!(format(not(and(vec![or(pqr())]))), "not (p or q or r)");
-		assert_eq!(format(not(or(vec![or(pqr())]))), "not (p or q or r)");
-		assert_eq!(format(not(if_and_only_if(vec![or(pqr())]))), "not (p or q or r)");
-		assert_eq!(format(or(vec![not(p())])), "not p");
-		assert_eq!(format(or(vec![not(and(vec![p()]))])), "not p");
-		assert_eq!(format(or(vec![not(or(vec![p()]))])), "not p");
-		assert_eq!(format(or(vec![not(if_and_only_if(vec![p()]))])), "not p");
-		assert_eq!(format(or(vec![not(p()), not(q()), not(r())])), "not p or not q or not r");
-		assert_eq!(format(
-			or(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])),
-			"not p or not q or not r");
-		assert_eq!(format(
-			or(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])),
-			"not p or not q or not r");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]),
-				if_and_only_if(vec![not(r())])])),
-			"not p or not q or not r");
+		assert_all!(i, or(vec![i(not(p()))]), "not p");
+		assert_all!(i, not(i(or(pqr()))), "not (p or q or r)");
+		assert_all!(i, or(vec![i(not(p())), i(not(q())), i(not(r()))]), "not p or not q or not r");
 
 		// Not + implies
-		assert_eq!(format(not(implies_right(p(), q()))), "not (p -> q)");
-		assert_eq!(format(not(and(vec![implies_right(p(), q())]))), "not (p -> q)");
-		assert_eq!(format(not(or(vec![implies_right(p(), q())]))), "not (p -> q)");
-		assert_eq!(format(not(if_and_only_if(vec![implies_right(p(), q())]))), "not (p -> q)");
-		assert_eq!(format(not(implies_left(p(), q()))), "not (q <- p)");
-		assert_eq!(format(not(and(vec![implies_left(p(), q())]))), "not (q <- p)");
-		assert_eq!(format(not(or(vec![implies_left(p(), q())]))), "not (q <- p)");
-		assert_eq!(format(not(if_and_only_if(vec![implies_left(p(), q())]))), "not (q <- p)");
-		assert_eq!(format(implies_right(not(p()), not(q()))), "not p -> not q");
-		assert_eq!(format(
-			implies_right(and(vec![not(p())]), and(vec![not(q())]))),
-			"not p -> not q");
-		assert_eq!(format(implies_right(or(vec![not(p())]), or(vec![not(q())]))), "not p -> not q");
-		assert_eq!(format(
-			implies_right(if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]))),
-			"not p -> not q");
-		assert_eq!(format(implies_left(not(p()), not(q()))), "not q <- not p");
-		assert_eq!(format(
-			implies_left(and(vec![not(p())]), and(vec![not(q())]))),
-			"not q <- not p");
-		assert_eq!(format(implies_left(or(vec![not(p())]), or(vec![not(q())]))), "not q <- not p");
-		assert_eq!(format(
-			implies_left(if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]))),
-			"not q <- not p");
+		assert_all!(i, not(i(implies_right(p(), q()))), "not (p -> q)");
+		assert_all!(i, not(i(implies_left(p(), q()))), "not (q <- p)");
+		assert_all!(i, implies_right(i(not(p())), i(not(q()))), "not p -> not q");
+		assert_all!(i, implies_left(i(not(p())), i(not(q()))), "not q <- not p");
 
 		// Not + if and only if
-		assert_eq!(format(not(if_and_only_if(pqr()))), "not (p <-> q <-> r)");
-		assert_eq!(format(not(and(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)");
-		assert_eq!(format(not(or(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)");
-		assert_eq!(format(not(if_and_only_if(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)");
-		assert_eq!(format(if_and_only_if(vec![not(p())])), "not p");
-		assert_eq!(format(if_and_only_if(vec![not(and(vec![p()]))])),"not p");
-		assert_eq!(format(if_and_only_if(vec![not(or(vec![p()]))])), "not p");
-		assert_eq!(format(if_and_only_if(vec![not(if_and_only_if(vec![p()]))])), "not p");
-		assert_eq!(format(
-			if_and_only_if(vec![not(p()), not(q()), not(r())])),
-			"not p <-> not q <-> not r");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])),
-			"not p <-> not q <-> not r");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])),
-			"not p <-> not q <-> not r");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]),
-				if_and_only_if(vec![not(r())])])),
+		assert_all!(i, if_and_only_if(vec![i(not(p()))]), "not p");
+		assert_all!(i, not(i(if_and_only_if(pqr()))), "not (p <-> q <-> r)");
+		assert_all!(i, if_and_only_if(vec![i(not(p())), i(not(q())), i(not(r()))]),
 			"not p <-> not q <-> not r");
 	}
 
@@ -1375,18 +1312,7 @@ mod tests
 			and(vec![if_and_only_if(vec![or(vec![p()])]), if_and_only_if(vec![or(vec![q()])]),
 				if_and_only_if(vec![or(vec![r()])])])),
 			"p and q and r");
-		assert_eq!(format(
-			and(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])),
-			"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
-		assert_eq!(format(
-			and(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]), and(vec![or(p3q3r3())])])),
-			"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
-		assert_eq!(format(
-			and(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]), or(vec![or(p3q3r3())])])),
-			"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![or(p1q1r1())]), if_and_only_if(vec![or(p2q2r2())]),
-				if_and_only_if(vec![or(p3q3r3())])])),
+		assert_all!(i, and(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]),
 			"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
 
 		assert_eq!(format(or(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])), "p or q or r");