diff --git a/N-Queens/ProB2UI_Queens20_TLA.png b/N-Queens/ProB2UI_Queens20_TLA.png
new file mode 100644
index 0000000000000000000000000000000000000000..37c70b2d76c5d7791b5e757983e1710db91ca1a0
Binary files /dev/null and b/N-Queens/ProB2UI_Queens20_TLA.png differ
diff --git a/N-Queens/queens_20.tla b/N-Queens/queens_20.tla
new file mode 100644
index 0000000000000000000000000000000000000000..31ade87e132738dedd8555b438b1db1cb25830d7
--- /dev/null
+++ b/N-Queens/queens_20.tla
@@ -0,0 +1,25 @@
+---- MODULE queens_20 ----
+
+EXTENDS Naturals, FiniteSets
+
+VARIABLE queens, n, solved
+----
+
+Init == /\ queens=[i \in 1..2 |-> 0]
+        /\ n=20
+        /\ solved = 0
+
+Solve == /\ solved=0
+         /\ queens' \in [1..n -> 1..n]
+         /\ \A i \in 1..n : (\A j \in 2..n : i<j => queens'[i] # queens'[j] /\ queens'[i]+i-j # queens'[j] /\ queens'[i]-i+j # queens'[j])
+         /\ solved'=1
+         /\ n'=n
+Spec == Init /\ [] [Solve]_<<n,queens>>
+
+VISB_JSON_FILE == "queens_20_tla.json"
+
+=======
+\* Generated at Tue Jun 22 21:06:17 CEST 2010
+\* TLC takes 2 seconds for n-6, 12 seconds to solve for n=7 
+\* and 4 minutes 9 seconds for n=8, 1h45min47sec for n=9
+\* ProB takes 0.01 seconds for n=8, both on MacBook Pro 3.06 GHz
diff --git a/N-Queens/queens_20_tla.json b/N-Queens/queens_20_tla.json
new file mode 100644
index 0000000000000000000000000000000000000000..fd6f2950bc2eee08f6397c0032fccba647ade3ff
--- /dev/null
+++ b/N-Queens/queens_20_tla.json
@@ -0,0 +1,14 @@
+{
+  "svg":"queens_20.svg",
+  "definitions":[
+    { "name":"VISB_SVG_UPDATES1",
+      "value" : "ran(%i.(i:1..20|rec(`id`:\"svgQueen\"^TO_STRING(i), y:IF i:dom(queens) THEN 45*queens(i)-45 ELSE 0 END, visibility: IF i:dom(queens) THEN \"visible\" ELSE \"hidden\" END)))"
+    },
+    { "name":"VISB_SVG_UPDATES2",
+      "value" : "ran(%i.(i:1..20|rec(`id`:\"gTiles\"^TO_STRING(i), visibility: IF i<=n  THEN \"visible\" ELSE \"hidden\" END)))"
+    }
+  ],
+"events": [
+  ]
+}
+