diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp
index 3223179..8a41a24 100644
--- a/src/anthem/Translation.cpp
+++ b/src/anthem/Translation.cpp
@@ -79,6 +79,13 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 
 	auto completedFormulas = complete(std::move(scopedFormulas));
 
+	// TODO: rethink simplification steps
+	if (context.simplify)
+		for (auto &completedFormula : completedFormulas)
+			simplify(completedFormula);
+
+	// TODO: remove variables that are not referenced after simplification
+
 	for (const auto &completedFormula : completedFormulas)
 	{
 		ast::print(context.logger.outputStream(), completedFormula, printContext);
diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp
index 9c8f9c8..1d301dc 100644
--- a/tests/TestCompletion.cpp
+++ b/tests/TestCompletion.cpp
@@ -140,9 +140,9 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		anthem::translate("input", input, context);
 
 		CHECK(output.str() ==
-			"forall V1 (covered(V1) <-> exists U1, U2 (V1 = U1 and in(U1, U2)))\n"
+			"forall V1 (covered(V1) <-> exists U1 (in(V1, U1)))\n"
 			"forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n"
-			"forall U3 not (U3 in 1..n and not covered(U3))\n"
-			"forall U4, U5, U6 not (in(U4, U5) and in(U6, U5) and exists X1 (X1 in (U4 + U6) and in(X1, U5)))\n");
+			"forall U2 not (U2 in 1..n and not covered(U2))\n"
+			"forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
 	}
 }