diff --git a/examples/example-0.lp b/examples/example-0.lp
new file mode 100644
index 0000000..fb3e9a0
--- /dev/null
+++ b/examples/example-0.lp
@@ -0,0 +1 @@
+q(X) :- p(X, Y).
diff --git a/examples/example-1.lp b/examples/example-1.lp
new file mode 100644
index 0000000..4f7855d
--- /dev/null
+++ b/examples/example-1.lp
@@ -0,0 +1 @@
+q(X + Y) :- p(X), p(Y).
diff --git a/examples/example-2-deadlock.spec b/examples/example-2-deadlock.spec
new file mode 100644
index 0000000..891825e
--- /dev/null
+++ b/examples/example-2-deadlock.spec
@@ -0,0 +1,20 @@
+axiom: forall X (isint(X) <-> exists N X = N).
+axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
+
+axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)).
+
+input: n -> integer.
+
+assumption: n >= 0.
+
+assertion: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
+
+
+
+lemma(forward): forall N N * N >= N.
+lemma(forward): forall X (q(X) -> exists N X = N).
+lemma(forward): forall X (p(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n)).
+lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and not p(N2 + 1))).
+lemma(forward): forall N2 (N2 >= 0 and not p(N2 + 1) -> (N2 + 1) * (N2 + 1) > 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): exists N2 (forall X (X = N2 -> (q(X) <-> N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n))).
diff --git a/examples/example-2.lp b/examples/example-2.lp
new file mode 100644
index 0000000..a17d173
--- /dev/null
+++ b/examples/example-2.lp
@@ -0,0 +1,2 @@
+p(X) :- X = 0..n, X * X <= n.
+q(X) :- p(X), not p(X + 1).
diff --git a/examples/example-2.spec b/examples/example-2.spec
new file mode 100644
index 0000000..d217fa7
--- /dev/null
+++ b/examples/example-2.spec
@@ -0,0 +1,29 @@
+axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
+
+axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)).
+
+input: n -> integer.
+
+assume: n >= 0.
+
+assert: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
+
+
+
+lemma(forward): forall N N * N >= N.
+lemma(forward): forall X (q(X) -> exists N X = N).
+lemma(forward): forall X (p(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n)).
+lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and not p(N2 + 1))).
+lemma(forward): forall N2 (N2 >= 0 and not p(N2 + 1) -> (N2 + 1) * (N2 + 1) > 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): exists N2 (forall X (X = N2 -> (q(X) <-> N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n))).
+lemma(forward): exists N2 p(N2).
+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 (N2 > N1 and N1 >= 0 and p(N2) -> p(N1)).
+
+lemma(forward): forall N (N >= 0 -> p(N)).
+
+lemma(forward): forall N2, N3 (q(N2) and N3 > N2 -> not q(N3)).