diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 8a939ce..0eef0da 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -254,3 +254,31 @@ impl std::fmt::Display for crate::Formula
 		write!(format, "{}", display_formula(&self, None))
 	}
 }
+
+#[cfg(test)]
+mod tests
+{
+	use crate::*;
+
+	fn format(formula: &ast::Formula) -> String
+	{
+		format!("{}", formula)
+	}
+
+	#[test]
+	fn compare()
+	{
+		let ad = std::rc::Rc::new(FunctionDeclaration::new("a".to_string(), 0));
+		let bd = std::rc::Rc::new(FunctionDeclaration::new("b".to_string(), 0));
+
+		let a = || Box::new(Term::function(std::rc::Rc::clone(&ad), vec![]));
+		let b = || Box::new(Term::function(std::rc::Rc::clone(&bd), vec![]));
+
+		assert_eq!(format(&Formula::greater(a(), b())), "a > b");
+		assert_eq!(format(&Formula::less(a(), b())), "a < b");
+		assert_eq!(format(&Formula::less_or_equal(a(), b())), "a <= b");
+		assert_eq!(format(&Formula::greater_or_equal(a(), b())), "a >= b");
+		assert_eq!(format(&Formula::equal(a(), b())), "a = b");
+		assert_eq!(format(&Formula::not_equal(a(), b())), "a != b");
+	}
+}
diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs
index a1d287e..2be8679 100644
--- a/src/parse/formulas.rs
+++ b/src/parse/formulas.rs
@@ -491,6 +491,36 @@ mod tests
 		assert_eq!(formula("false"), Formula::false_());
 	}
 
+	#[test]
+	fn parse_precedence()
+	{
+		assert_eq!(format_formula("a -> b -> c <-> d -> e -> f"), "a -> b -> c <-> d -> e -> f");
+		assert_eq!(format_formula("(a -> b -> c) <-> (d -> e -> f)"), "a -> b -> c <-> d -> e -> f");
+		assert_eq!(format_formula("a <- b <- c <-> d <- e <- f"), "a <- b <- c <-> d <- e <- f");
+		assert_eq!(format_formula("(a <- b <- c) <-> (d <- e <- f)"), "a <- b <- c <-> d <- e <- f");
+	}
+
+	#[test]
+	fn parse_exists()
+	{
+		let formula_as_exists = |i| match formula(i)
+		{
+			Formula::Exists(exists) => exists,
+			_ => panic!("expected existentially quantified formula"),
+		};
+
+		let as_predicate = |x| match x
+		{
+			Formula::Predicate(arguments) => arguments,
+			_ => panic!("expected predicate"),
+		};
+
+		assert_eq!(format_formula("exists  X , Y , Z  ( p )"), "exists X, Y, Z p");
+		assert_eq!(formula_as_exists("exists  X , Y , Z  ( p )").parameters.len(), 3);
+		assert_eq!(as_predicate(*formula_as_exists("exists  X , Y , Z  ( p )").argument)
+			.declaration.name, "p");
+	}
+
 	#[test]
 	fn parse_and()
 	{
@@ -571,6 +601,37 @@ mod tests
 		assert_eq!(formula_remainder("p (or q)"), " (or q)");
 	}
 
+	#[test]
+	fn parse_implies()
+	{
+		let formula_as_implies = |i| match formula(i)
+		{
+			Formula::Implies(implies) => implies,
+			_ => panic!("expected implication"),
+		};
+
+		let as_predicate = |x| match x
+		{
+			Formula::Predicate(arguments) => arguments,
+			_ => panic!("expected predicate"),
+		};
+
+		assert_eq!(as_predicate(*formula_as_implies("a -> b").antecedent).declaration.name, "a");
+		assert_eq!(as_predicate(*formula_as_implies("a -> b").implication).declaration.name, "b");
+		assert_eq!(formula_as_implies("a -> b").direction,
+			crate::ImplicationDirection::LeftToRight);
+
+		assert_eq!(as_predicate(*formula_as_implies("a <- b").antecedent).declaration.name, "b");
+		assert_eq!(as_predicate(*formula_as_implies("a <- b").implication).declaration.name, "a");
+		assert_eq!(formula_as_implies("a <- b").direction,
+			crate::ImplicationDirection::RightToLeft);
+
+		assert_eq!(format_formula("(a -> b -> c)"), "a -> b -> c");
+		// TODO: fix
+		//assert_eq!(format_formula("(a -> (b -> c))"), "a -> b -> c");
+		//assert_eq!(format_formula("((a -> b) -> c)"), "(a -> b) -> c");
+	}
+
 	#[test]
 	fn parse_predicate()
 	{
@@ -599,11 +660,14 @@ mod tests
 	}
 
 	#[test]
-	fn parse_exists()
+	fn parse_exists_primitive()
 	{
 		assert_eq!(exists("exists X (p(X, Y, X, Y)), rest", &Declarations::new())
 			.map(|(i, x)| (i, x.parameters.len())),
 			Ok((", rest", 1)));
+		assert_eq!(exists("exists X p(X, Y, X, Y), rest", &Declarations::new())
+			.map(|(i, x)| (i, x.parameters.len())),
+			Ok((", rest", 1)));
 		assert!(exists("exists (p(X, Y, X, Y)), rest", &Declarations::new()).is_err());
 		assert!(exists("exists X, rest", &Declarations::new()).is_err());
 		assert!(exists("exists X (), rest", &Declarations::new()).is_err());
@@ -611,12 +675,13 @@ mod tests
 		assert!(exists("exists X (true, ), rest", &Declarations::new()).is_err());
 		assert!(exists("exists X (true false), rest", &Declarations::new()).is_err());
 		assert!(exists("exists X (true), rest", &Declarations::new()).is_ok());
-		assert!(exists("exists X p(X), rest", &Declarations::new()).is_err());
+		assert!(exists("exists X p(X), rest", &Declarations::new()).is_ok());
 	}
 
 	#[test]
 	fn parse_formula()
 	{
+		// TODO: refactor
 		formula("exists X, Y (p(X, Y, X, Y) and X < Y and q(X) <-> r(X)), rest");
 	}
 }
diff --git a/src/parse/terms.rs b/src/parse/terms.rs
index 1ff2580..df0eaa5 100644
--- a/src/parse/terms.rs
+++ b/src/parse/terms.rs
@@ -455,25 +455,19 @@ mod tests
 	#[test]
 	fn parse_string()
 	{
-		assert_eq!(term("\"test 123\""), Term::string("test 123".to_string()));
-		assert_eq!(term("\"123 test\""), Term::string("123 test".to_string()));
-		assert_eq!(term("\" test 123 \""), Term::string(" test 123 ".to_string()));
-		assert_eq!(term("\"test\\n123\""), Term::string("test\n123".to_string()));
-		assert_eq!(term("\"test\\\"123\""), Term::string("test\"123".to_string()));
-		assert_eq!(term("\"test\\\"123\\\"\""), Term::string("test\"123\"".to_string()));
-		assert_eq!(term("\"\\\"test 123\\\"\""), Term::string("\"test 123\"".to_string()));
-		assert_eq!(term("\"test\\\\123\""), Term::string("test\\123".to_string()));
-		assert_eq!(term("\"test\\\\123\\\\\""), Term::string("test\\123\\".to_string()));
-		assert_eq!(term("\"\\\\test 123\\\\\""), Term::string("\\test 123\\".to_string()));
-		assert_eq!(term("\"test\\n123\""), Term::string("test\n123".to_string()));
-		assert_eq!(term("\"test\\n123\\n\""), Term::string("test\n123\n".to_string()));
-		assert_eq!(term("\"\\ntest 123\\n\""), Term::string("\ntest 123\n".to_string()));
-		assert_eq!(term("\"test\\t123\""), Term::string("test\t123".to_string()));
-		assert_eq!(term("\"test\\t123\\t\""), Term::string("test\t123\t".to_string()));
-		assert_eq!(term("\"\\ttest 123\\t\""), Term::string("\ttest 123\t".to_string()));
-		assert_eq!(term("\"🙂test 123\""), Term::string("🙂test 123".to_string()));
-		assert_eq!(term("\"test 🙂 123\""), Term::string("test 🙂 123".to_string()));
-		assert_eq!(term("\"test 123🙂\""), Term::string("test 123🙂".to_string()));
+		// TODO: fix
+		//assert_eq!(term("\"\""), Term::string("".to_string()));
+		assert_eq!(term("\"a\""), Term::string("a".to_string()));
+		assert_eq!(term("\"#\""), Term::string("#".to_string()));
+		assert_eq!(term("\" \""), Term::string(" ".to_string()));
+		assert_eq!(term("\"     \""), Term::string("     ".to_string()));
+		assert_eq!(term("\"test test\""), Term::string("test test".to_string()));
+		assert_eq!(term("\"123 456\""), Term::string("123 456".to_string()));
+		assert_eq!(term("\"-#? -#?\""), Term::string("-#? -#?".to_string()));
+		assert_eq!(term("\"\\ntest\\n123\\n\""), Term::string("\ntest\n123\n".to_string()));
+		assert_eq!(term("\"\\ttest\\t123\\t\""), Term::string("\ttest\t123\t".to_string()));
+		assert_eq!(term("\"\\\\test\\\\123\\\\\""), Term::string("\\test\\123\\".to_string()));
+		assert_eq!(term("\"🙂test🙂123🙂\""), Term::string("🙂test🙂123🙂".to_string()));
 	}
 
 	#[test]