diff --git a/examples/example-2.lemmas b/examples/example-2.lemmas
new file mode 100644
index 0000000..98929e4
--- /dev/null
+++ b/examples/example-2.lemmas
@@ -0,0 +1,20 @@
+# Multiplication with positive numbers preserves the order of integers
+axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
+
+# Induction principle instantiated for p.
+# This axiom is necessary because we use Vampire without higher-order reasoning
+axiom: forall N1 (p(N1) and forall N2 (N2 >= N1 and not p(N2) -> not p(N2 + 1)) -> forall N2 (N2 >= N1 -> p(N2))).
+#axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N p(N).
+
+lemma(forward): forall X (p(X) <-> exists N (X = N and N >= 0 and N * N <= n)).
+lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)).
+lemma(forward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 < N2 -> N1 * N1 < N2 * N2).
+lemma(forward): forall N (N >= 0 and p(N + 1) -> p(N)).
+lemma(forward): not p(n + 1).
+lemma(forward): forall N1, N2 (q(N1) and N2 > N1 -> not q(N2)).
+lemma(forward): forall N (N >= 0 and not p(N + 1) -> (N + 1) * (N + 1) > n).
+
+lemma(backward): forall N1, N2 (q(N1) and q(N2) -> N1 = N2).
+axiom: forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2).
+
+lemma(backward): forall X1 (q(X1) -> p(X1) and exists X2 (exists N (X2 = N + 1 and N = X1) and not p(X2))).
diff --git a/examples/example-2.spec b/examples/example-2.spec
index 57bebae..19aff64 100644
--- a/examples/example-2.spec
+++ b/examples/example-2.spec
@@ -7,27 +7,3 @@ output: q/1.
 
 # Verify that q computes the floor of the square root of n
 spec: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
-
-
-
-
-# Multiplication with positive numbers preserves the order of integers
-axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
-
-# Induction principle instantiated for p.
-# This axiom is necessary because we use Vampire without higher-order reasoning
-axiom: forall N1 (p(N1) and forall N2 (N2 >= N1 and not p(N2) -> not p(N2 + 1)) -> forall N2 (N2 >= N1 -> p(N2))).
-#axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N p(N).
-
-lemma(forward): forall X (p(X) <-> exists N (X = N and N >= 0 and N * N <= n)).
-lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)).
-lemma(forward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 < N2 -> N1 * N1 < N2 * N2).
-lemma(forward): forall N (N >= 0 and p(N + 1) -> p(N)).
-lemma(forward): not p(n + 1).
-lemma(forward): forall N1, N2 (q(N1) and N2 > N1 -> not q(N2)).
-lemma(forward): forall N (N >= 0 and not p(N + 1) -> (N + 1) * (N + 1) > n).
-
-lemma(backward): forall N1, N2 (q(N1) and q(N2) -> N1 = N2).
-axiom: forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2).
-
-lemma(backward): forall X1 (q(X1) -> p(X1) and exists X2 (exists N (X2 = N + 1 and N = X1) and not p(X2))).
diff --git a/examples/example-prime.lemmas b/examples/example-prime.lemmas
new file mode 100644
index 0000000..14235df
--- /dev/null
+++ b/examples/example-prime.lemmas
@@ -0,0 +1 @@
+lemma(backward): forall N (composite(N) <-> N > 1 and N <= n and exists I, J (I > 1 and J > 1 and I * J = N)).
diff --git a/examples/example-prime.spec b/examples/example-prime.spec
index bd63ee1..20238bc 100644
--- a/examples/example-prime.spec
+++ b/examples/example-prime.spec
@@ -5,8 +5,3 @@ assume: n >= 1.
 
 spec: forall X (prime(X) -> exists N (X = N)).
 spec: forall N (prime(N) <-> N > 1 and N <= n and not exists I, J (I > 1 and J > 1 and I * J = N)).
-
-
-
-
-lemma(backward): forall N (composite(N) <-> N > 1 and N <= n and exists I, J (I > 1 and J > 1 and I * J = N)).