diff --git a/examples/coloring-1.lp b/examples/coloring-1.lp
new file mode 100644
index 0000000..a86373e
--- /dev/null
+++ b/examples/coloring-1.lp
@@ -0,0 +1,12 @@
+% After eliminating the super-easy aggregate expression from the rule
+%
+% {color(X,Z) : color(Z)} = 1 :- vertex(X).
+%
+% we get 4 rules:
+
+{color(X,Z)} :- vertex(X), color(Z).
+:- color(X,Z1), color(X,Z2), vertex(X), color(Z1), color(Z2), Z1 != Z2.
+aux(X) :- vertex(X), color(Z), color(X,Z).
+:- vertex(X), not aux(X).
+
+:- edge(X,Y), color(X,Z), color(Y,Z).
diff --git a/examples/coloring.spec b/examples/coloring.spec
new file mode 100644
index 0000000..2f42853
--- /dev/null
+++ b/examples/coloring.spec
@@ -0,0 +1,14 @@
+input: vertex/1, edge/2, color/1.
+
+output: color/2.
+
+# edge/2 is a set of pairs of vertices
+assume: forall X, Y (edge(X,Y) -> vertex(X) and vertex(Y)).
+
+# color/2 is a function from vertices to colors
+spec: forall X, Z (color(X,Z) -> vertex(X) and color(Z)).
+spec: forall X (vertex(X) -> exists Z color(X,Z)).
+spec: forall X, Z1, Z2 (color(X,Z1) and color(X,Z2) -> Z1 = Z2).
+
+# adjacent vertices have different colors
+spec: not exists X, Y, Z (edge(X,Y) and color(X,Z) and color(Y,Z)).