diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 452f786..944ac89 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -587,6 +587,11 @@ mod tests
 	#[test]
 	fn format_combination_boolean_and_lower()
 	{
+		// Boolean + not
+		assert_eq!(format(not(true_())), "not true");
+		assert_eq!(format(not(false_())), "not false");
+
+		// Boolean + quantified formula
 		assert_eq!(format(exists(vec![variable_declaration("X")], true_())), "exists X true");
 		assert_eq!(format(exists(vec![variable_declaration("X")], false_())), "exists X false");
 		assert_eq!(format(
@@ -608,19 +613,19 @@ mod tests
 				variable_declaration("Z")], false_())),
 			"forall X, Y, Z false");
 
-		assert_eq!(format(not(true_())), "not true");
-		assert_eq!(format(not(false_())), "not false");
-
+		// Boolean + and
 		assert_eq!(format(and(vec![true_()])), "true");
 		assert_eq!(format(and(vec![true_(), true_(), true_()])), "true and true and true");
 		assert_eq!(format(and(vec![false_()])), "false");
 		assert_eq!(format(and(vec![false_(), false_(), false_()])), "false and false and false");
 
+		// Boolean + or
 		assert_eq!(format(or(vec![true_()])), "true");
 		assert_eq!(format(or(vec![true_(), true_(), true_()])), "true or true or true");
 		assert_eq!(format(or(vec![false_()])), "false");
 		assert_eq!(format(or(vec![false_(), false_(), false_()])), "false or false or false");
 
+		// Boolean + implies
 		assert_eq!(format(
 			implies(ImplicationDirection::LeftToRight, true_(), true_())),
 			"true -> true");
@@ -634,6 +639,7 @@ mod tests
 			implies(ImplicationDirection::RightToLeft, false_(), false_())),
 			"false <- false");
 
+		// Boolean + if and only if
 		assert_eq!(format(if_and_only_if(vec![true_()])), "true");
 		assert_eq!(format(
 			if_and_only_if(vec![true_(), true_(), true_()])),
@@ -652,6 +658,7 @@ mod tests
 		let term_3 = || exponentiate(constant("a"), exponentiate(constant("b"), constant("c")));
 		let term_4 = || negative(function("f", vec![integer(5), add(variable("X"), integer(3))]));
 
+		// Compare + not
 		assert_eq!(format(not(greater(term_1(), term_2()))), "not (a + b) * c > |d - e|");
 		assert_eq!(format(not(less(term_1(), term_2()))), "not (a + b) * c < |d - e|");
 		assert_eq!(format(not(less_or_equal(term_1(), term_2()))), "not (a + b) * c <= |d - e|");
@@ -659,6 +666,7 @@ mod tests
 		assert_eq!(format(not(equal(term_1(), term_2()))), "not (a + b) * c = |d - e|");
 		assert_eq!(format(not(not_equal(term_1(), term_2()))), "not (a + b) * c != |d - e|");
 
+		// Compare + quantified formula
 		assert_eq!(format(
 			exists(vec![variable_declaration("X")], greater(term_1(), term_2()))),
 			"exists X (a + b) * c > |d - e|");
@@ -696,6 +704,7 @@ mod tests
 			for_all(vec![variable_declaration("X")], not_equal(term_1(), term_2()))),
 			"forall X (a + b) * c != |d - e|");
 
+		// Compare + and
 		assert_eq!(format(
 			and(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
 				greater(term_2(), term_4())])),
@@ -721,6 +730,7 @@ mod tests
 				not_equal(term_2(), term_4())])),
 			"(a + b) * c != |d - e| and a ** b ** c != -f(5, X + 3) and |d - e| != -f(5, X + 3)");
 
+		// Compare + or
 		assert_eq!(format(
 			or(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
 				greater(term_2(), term_4())])),
@@ -746,6 +756,7 @@ mod tests
 				not_equal(term_2(), term_4())])),
 			"(a + b) * c != |d - e| or a ** b ** c != -f(5, X + 3) or |d - e| != -f(5, X + 3)");
 
+		// Compare + implies
 		assert_eq!(format(
 			implies(ImplicationDirection::LeftToRight, greater(term_1(), term_2()),
 				greater(term_3(), term_4()))),
@@ -795,6 +806,7 @@ mod tests
 				not_equal(term_3(), term_4()))),
 			"a ** b ** c != -f(5, X + 3) <- (a + b) * c != |d - e|");
 
+		// Compare + if and only if
 		assert_eq!(format(
 			if_and_only_if(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
 				greater(term_2(), term_4())])),
@@ -894,18 +906,6 @@ mod tests
 			"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)");
@@ -952,18 +952,6 @@ mod tests
 			"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)");
@@ -1078,18 +1066,6 @@ mod tests
 			"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![])]))),
@@ -1138,31 +1114,679 @@ mod tests
 	}
 
 	#[test]
-	fn format_combination_quantifiers_and_lower()
+	fn format_combination_quantified_formula_and_lower()
 	{
+		// Quantified formula + quantified formula
 		assert_eq!(format(
 			exists(vec![variable_declaration("X"), variable_declaration("Y"),
-				variable_declaration("Z")], exists(vec![variable_declaration("A"),
-					variable_declaration("B"), variable_declaration("C")],
-					predicate("p", vec![])))),
+				variable_declaration("Z")],
+				exists(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![])))),
 			"exists X, Y, Z exists A, B, C p");
 		assert_eq!(format(
 			exists(vec![variable_declaration("X"), variable_declaration("Y"),
-				variable_declaration("Z")], for_all(vec![variable_declaration("A"),
+				variable_declaration("Z")],
+				and(vec![exists(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![]))]))),
+			"exists X, Y, Z exists A, B, C p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![exists(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![]))]))),
+			"exists X, Y, Z exists A, B, C p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![exists(vec![variable_declaration("A"),
 					variable_declaration("B"), variable_declaration("C")],
-					predicate("p", vec![])))),
+					predicate("p", vec![]))]))),
+			"exists X, Y, Z exists A, B, C p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				for_all(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![])))),
+			"exists X, Y, Z forall A, B, C p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![]))]))),
+			"exists X, Y, Z forall A, B, C p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![]))]))),
+			"exists X, Y, Z forall A, B, C p");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![for_all(vec![variable_declaration("A"),
+					variable_declaration("B"), variable_declaration("C")],
+					predicate("p", vec![]))]))),
 			"exists X, Y, Z forall A, B, C p");
 		assert_eq!(format(
 			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
-				variable_declaration("Z")], exists(vec![variable_declaration("A"),
-					variable_declaration("B"), variable_declaration("C")],
-					predicate("p", vec![])))),
+				variable_declaration("Z")],
+				exists(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![])))),
 			"forall X, Y, Z exists A, B, C p");
 		assert_eq!(format(
 			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
-				variable_declaration("Z")], for_all(vec![variable_declaration("A"),
-					variable_declaration("B"), variable_declaration("C")],
-					predicate("p", vec![])))),
+				variable_declaration("Z")],
+				and(vec![exists(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![]))]))),
+			"forall X, Y, Z exists A, B, C p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![exists(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![]))]))),
+			"forall X, Y, Z exists A, B, C p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![exists(vec![variable_declaration("A"),
+					variable_declaration("B"), variable_declaration("C")], predicate("p", vec![]))]))),
+			"forall X, Y, Z exists A, B, C p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				for_all(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![])))),
 			"forall X, Y, Z forall A, B, C p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![]))]))),
+			"forall X, Y, Z forall A, B, C p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B"),
+					variable_declaration("C")], predicate("p", vec![]))]))),
+			"forall X, Y, Z forall A, B, C p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![for_all(vec![variable_declaration("A"),
+					variable_declaration("B"), variable_declaration("C")],
+					predicate("p", vec![]))]))),
+			"forall X, Y, Z forall A, B, C p");
+
+		// Quantified formula + and
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
+			"exists X, Y, Z (p and q and r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"exists X, Y, Z (p and q and r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"exists X, Y, Z (p and q and r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"exists X, Y, Z (p and q and r)");
+		assert_eq!(format(
+			and(vec![
+				exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])),
+				exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])),
+			"exists X, Y p and exists A, B q and exists C, D r");
+		assert_eq!(format(
+			and(vec![
+				and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				and(vec![exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"exists X, Y p and exists A, B q and exists C, D r");
+		assert_eq!(format(
+			and(vec![
+				or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				or(vec![exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"exists X, Y p and exists A, B q and exists C, D r");
+		assert_eq!(format(
+			and(vec![
+				if_and_only_if(vec![exists(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![exists(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]),
+				if_and_only_if(vec![exists(vec![variable_declaration("C"),
+					variable_declaration("D")], predicate("r", vec![]))])])),
+			"exists X, Y p and exists A, B q and exists C, D r");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
+			"forall X, Y, Z (p and q and r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"forall X, Y, Z (p and q and r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"forall X, Y, Z (p and q and r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"forall X, Y, Z (p and q and r)");
+		assert_eq!(format(
+			and(vec![
+				for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])),
+				for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])),
+			"forall X, Y p and forall A, B q and forall C, D r");
+		assert_eq!(format(
+			and(vec![
+				and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				and(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"forall X, Y p and forall A, B q and forall C, D r");
+		assert_eq!(format(
+			and(vec![
+				or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				or(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"forall X, Y p and forall A, B q and forall C, D r");
+		assert_eq!(format(
+			and(vec![
+				if_and_only_if(vec![for_all(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![for_all(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]),
+				if_and_only_if(vec![for_all(vec![variable_declaration("C"),
+					variable_declaration("D")], predicate("r", vec![]))])])),
+			"forall X, Y p and forall A, B q and forall C, D r");
+
+		// Quantified formula + or
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
+			"exists X, Y, Z (p or q or r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"exists X, Y, Z (p or q or r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"exists X, Y, Z (p or q or r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"exists X, Y, Z (p or q or r)");
+		assert_eq!(format(
+			or(vec![
+				exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])),
+				exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])),
+			"exists X, Y p or exists A, B q or exists C, D r");
+		assert_eq!(format(
+			or(vec![
+				and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				and(vec![exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"exists X, Y p or exists A, B q or exists C, D r");
+		assert_eq!(format(
+			or(vec![
+				or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				or(vec![exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"exists X, Y p or exists A, B q or exists C, D r");
+		assert_eq!(format(
+			or(vec![
+				if_and_only_if(vec![exists(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![exists(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]),
+				if_and_only_if(vec![exists(vec![variable_declaration("C"),
+					variable_declaration("D")], predicate("r", vec![]))])])),
+			"exists X, Y p or exists A, B q or exists C, D r");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
+			"forall X, Y, Z (p or q or r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"forall X, Y, Z (p or q or r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"forall X, Y, Z (p or q or r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"forall X, Y, Z (p or q or r)");
+		assert_eq!(format(
+			or(vec![
+				for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])),
+				for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])),
+			"forall X, Y p or forall A, B q or forall C, D r");
+		assert_eq!(format(
+			or(vec![
+				and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				and(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"forall X, Y p or forall A, B q or forall C, D r");
+		assert_eq!(format(
+			or(vec![
+				or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				or(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"forall X, Y p or forall A, B q or forall C, D r");
+		assert_eq!(format(
+			or(vec![
+				if_and_only_if(vec![for_all(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![for_all(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]),
+				if_and_only_if(vec![for_all(vec![variable_declaration("C"),
+					variable_declaration("D")], predicate("r", vec![]))])])),
+			"forall X, Y p or forall A, B q or forall C, D r");
+
+		// Quantified formula + implies
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+					predicate("q", vec![])))),
+			"exists X, Y, Z (p -> q)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+					predicate("q", vec![]))]))),
+			"exists X, Y, Z (p -> q)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+					predicate("q", vec![]))]))),
+			"exists X, Y, Z (p -> q)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![implies(ImplicationDirection::LeftToRight,
+					predicate("p", vec![]), predicate("q", vec![]))]))),
+			"exists X, Y, Z (p -> q)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+					predicate("q", vec![])))),
+			"exists X, Y, Z (q <- p)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+					predicate("q", vec![]))]))),
+			"exists X, Y, Z (q <- p)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+					predicate("q", vec![]))]))),
+			"exists X, Y, Z (q <- p)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![implies(ImplicationDirection::RightToLeft,
+					predicate("p", vec![]), predicate("q", vec![]))]))),
+			"exists X, Y, Z (q <- p)");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])))),
+			"exists X, Y p -> exists A, B q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]))),
+			"exists X, Y p -> exists A, B q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]))),
+			"exists X, Y p -> exists A, B q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				if_and_only_if(vec![exists(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![exists(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]))),
+			"exists X, Y p -> exists A, B q");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])))),
+			"exists A, B q <- exists X, Y p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]))),
+			"exists A, B q <- exists X, Y p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]))),
+			"exists A, B q <- exists X, Y p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				if_and_only_if(vec![exists(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![exists(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]))),
+			"exists A, B q <- exists X, Y p");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+					predicate("q", vec![])))),
+			"forall X, Y, Z (p -> q)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+					predicate("q", vec![]))]))),
+			"forall X, Y, Z (p -> q)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
+					predicate("q", vec![]))]))),
+			"forall X, Y, Z (p -> q)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![implies(ImplicationDirection::LeftToRight,
+					predicate("p", vec![]), predicate("q", vec![]))]))),
+			"forall X, Y, Z (p -> q)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+					predicate("q", vec![])))),
+			"forall X, Y, Z (q <- p)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+					predicate("q", vec![]))]))),
+			"forall X, Y, Z (q <- p)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
+					predicate("q", vec![]))]))),
+			"forall X, Y, Z (q <- p)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![implies(ImplicationDirection::RightToLeft,
+					predicate("p", vec![]), predicate("q", vec![]))]))),
+			"forall X, Y, Z (q <- p)");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])))),
+			"forall X, Y p -> forall A, B q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]))),
+			"forall X, Y p -> forall A, B q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]))),
+			"forall X, Y p -> forall A, B q");
+		assert_eq!(format(
+			implies(ImplicationDirection::LeftToRight,
+				if_and_only_if(vec![for_all(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![for_all(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]))),
+			"forall X, Y p -> forall A, B q");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])))),
+			"forall A, B q <- forall X, Y p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]))),
+			"forall A, B q <- forall X, Y p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]))),
+			"forall A, B q <- forall X, Y p");
+		assert_eq!(format(
+			implies(ImplicationDirection::RightToLeft,
+				if_and_only_if(vec![for_all(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![for_all(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]))),
+			"forall A, B q <- forall X, Y p");
+
+		// Quantified formula + if and only if
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])]))),
+			"exists X, Y, Z (p <-> q <-> r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"exists X, Y, Z (p <-> q <-> r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"exists X, Y, Z (p <-> q <-> r)");
+		assert_eq!(format(
+			exists(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![if_and_only_if(vec![predicate("p", vec![]),
+					predicate("q", vec![]), predicate("r", vec![])])]))),
+			"exists X, Y, Z (p <-> q <-> r)");
+		assert_eq!(format(
+			if_and_only_if(vec![
+				exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])),
+				exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])),
+			"exists X, Y p <-> exists A, B q <-> exists C, D r");
+		assert_eq!(format(
+			if_and_only_if(vec![
+				and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				and(vec![exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"exists X, Y p <-> exists A, B q <-> exists C, D r");
+		assert_eq!(format(
+			if_and_only_if(vec![
+				or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				or(vec![exists(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"exists X, Y p <-> exists A, B q <-> exists C, D r");
+		assert_eq!(format(
+			if_and_only_if(vec![
+				if_and_only_if(vec![exists(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![exists(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]),
+				if_and_only_if(vec![exists(vec![variable_declaration("C"),
+					variable_declaration("D")], predicate("r", vec![]))])])),
+			"exists X, Y p <-> exists A, B q <-> exists C, D r");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])]))),
+			"forall X, Y, Z (p <-> q <-> r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				and(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"forall X, Y, Z (p <-> q <-> r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				or(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
+					predicate("r", vec![])])]))),
+			"forall X, Y, Z (p <-> q <-> r)");
+		assert_eq!(format(
+			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
+				variable_declaration("Z")],
+				if_and_only_if(vec![if_and_only_if(vec![predicate("p", vec![]),
+					predicate("q", vec![]), predicate("r", vec![])])]))),
+			"forall X, Y, Z (p <-> q <-> r)");
+		assert_eq!(format(
+			if_and_only_if(vec![
+				for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![])),
+				for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![])),
+				for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])),
+			"forall X, Y p <-> forall A, B q <-> forall C, D r");
+		assert_eq!(format(
+			if_and_only_if(vec![
+				and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				and(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"forall X, Y p <-> forall A, B q <-> forall C, D r");
+		assert_eq!(format(
+			if_and_only_if(vec![
+				or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")],
+					predicate("p", vec![]))]),
+				or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")],
+					predicate("q", vec![]))]),
+				or(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")],
+					predicate("r", vec![]))])])),
+			"forall X, Y p <-> forall A, B q <-> forall C, D r");
+		assert_eq!(format(
+			if_and_only_if(vec![
+				if_and_only_if(vec![for_all(vec![variable_declaration("X"),
+					variable_declaration("Y")], predicate("p", vec![]))]),
+				if_and_only_if(vec![for_all(vec![variable_declaration("A"),
+					variable_declaration("B")], predicate("q", vec![]))]),
+				if_and_only_if(vec![for_all(vec![variable_declaration("C"),
+					variable_declaration("D")], predicate("r", vec![]))])])),
+			"forall X, Y p <-> forall A, B q <-> forall C, D r");
 	}
 }