diff --git a/examples/example-1.spec b/examples/example-1.spec
new file mode 100644
index 0000000..6c813c5
--- /dev/null
+++ b/examples/example-1.spec
@@ -0,0 +1,6 @@
+assert:
+	forall N
+	(
+		forall X (p(X) -> exists I exists M (I = M and I = X and I <= N))
+		-> forall X (q(X) -> exists I exists M (I = M and I = X and I <= 2 * N))
+	).