summaryrefslogtreecommitdiff
path: root/omega/examples/old_test/stodghil
diff options
context:
space:
mode:
authordhuth <derickhuth@gmail.com>2014-11-21 13:35:20 -0700
committerdhuth <derickhuth@gmail.com>2014-11-21 13:35:20 -0700
commita1834b22c43c282442b0cb164767e6c877cf0e5b (patch)
treebedc5be7d1bdb8d32c1868caa496a8a1530d8d8a /omega/examples/old_test/stodghil
parentded84bb4aec7461738e7b7033d782a518e2c606b (diff)
parenteb9236c5353785472ae132f27e1cfb9f1e4264a5 (diff)
downloadchill-a1834b22c43c282442b0cb164767e6c877cf0e5b.tar.gz
chill-a1834b22c43c282442b0cb164767e6c877cf0e5b.tar.bz2
chill-a1834b22c43c282442b0cb164767e6c877cf0e5b.zip
Merge branch 'master' into doe
Diffstat (limited to 'omega/examples/old_test/stodghil')
-rw-r--r--omega/examples/old_test/stodghil21
1 files changed, 21 insertions, 0 deletions
diff --git a/omega/examples/old_test/stodghil b/omega/examples/old_test/stodghil
new file mode 100644
index 0000000..99e9430
--- /dev/null
+++ b/omega/examples/old_test/stodghil
@@ -0,0 +1,21 @@
+symbolic n;
+
+S := {[k_w,j_w,l_w]->[k_r,j_r,l_r] : ((1 <= k_w) and (k_w <= n) and ((k_w + 1) <= j_w)
+and (j_w <= n)
+and ((k_w + 1) <= l_w) and (l_w <= j_w) and (1 <= k_r)
+and (k_r <= n) and ((k_r + 1) <= j_r) and (j_r <= n)
+and ((k_r + 1) <= l_r) and (l_r <= j_r) and ((k_w < k_r) or ((k_w = k_r)
+and (j_w < j_r)) or ((k_w = k_r) and (j_w = j_r) and (l_w < l_r)))
+and (j_w = j_r) and (l_w = l_r)
+and !exists(k_1 : ((1 <= k_1) and (k_1 <= n) and (k_w < k_1) and ((k_1 < k_r) or (k_1 = k_r))
+and (k_1 = j_r) and (k_1 = l_r)))
+and !exists(k_2,i_2 : ((1 <= k_2) and (k_2 <= n) and ((k_2 + 1) <= i_2) and (i_2 <= n) and (k_w < k_2) and ((k_2 < k_r) or (k_2 = k_r)) and (i_2 = j_r) and (k_2 = l_r)))
+and !exists(k_3,j_3,l_3 : ((1 <= k_3) and (k_3 <= n) and ((k_3 + 1) <= j_3)
+ and (j_3 <= n) and ((k_3 + 1) <= l_3) and (l_3 <= j_3)
+and ((k_w < k_3) or ((k_w = k_3) and (j_w < j_3)) or ((k_w = k_3)
+and (j_w = j_3) and (l_w < l_3)))
+and ((k_3 < k_r) or ((k_3 = k_r) and (j_3 < j_r)) or ((k_3 = k_r)
+and (j_3 = j_r) and (l_3 < l_r))) and (j_3 = j_r) and (l_3 = l_r))
+))};
+
+S;