New interesting example

[fireball-separation.git] / ocaml / problems / w

diff --git a/ocaml/problems/w b/ocaml/problems/w
index ec35dd04a5075104c640c8bc176e9d24ab060bb7..c603cfb13cbfe0b421ea9a1d86c47083e32ad8b3 100644 (file)
--- a/ocaml/problems/w
+++ b/ocaml/problems/w
@@ -20,11 +20,11 @@ C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h)))\r
 C b (k. l. b) (e f) (b c d) (e e (b (k. l. b)) d) (e (k. l. b c) (k. l. b k) (b c)) d (e e (e e) (d (k. f)) (b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))))) (e e (b (k. l. b)) (b (k. l. b) (e f) (b c d)) (e e (b (k. l. b)) d (k. d) (b (k. l. b))) (k. b c k (l. e l) (e e (b (l. m. b)) k (l. k)) (f g (c (e h))) (k b (l. b) (f g (e f))) (c (e h))) (k. i (f g) (l. l)))\r
 #  ] (* NUMERIC    *) [\r
-N b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) a\r
-  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) a\r
-  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) a\r
-  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) a\r
-  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) a\r
+N b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) Z\r
+  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) Z\r
+  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) Z\r
+  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) Z\r
+  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) Z\r
 #  ];\r
 \r
 $!\r
@@ -41,11 +41,11 @@ C c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e
   c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g)\r
   e f (k. k) (g e) (e f (k. e)) (e f (k. e)) (h c (b (g e) h (k. c (l. m. m k l))))\r
 # ] (* NUMERIC    *) [\r
-N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. i) a\r
-  e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) a\r
-  e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) a\r
-  e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) a\r
-  g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f a\r
+N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. i) Z\r
+  e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) Z\r
+  e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) Z\r
+  e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) Z\r
+  g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f Z\r
 #  ]\r
  ];\r
 \r
@@ -66,3 +66,19 @@ N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e
 \r
 # todo:\r
   (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)\r
+\r
+\r
+$! new failing problem\r
+# it is backtracking, but it shouldn't\r
+# why? well, D occurs in some C's\r
+D (a b)\r
+C ((((((((a (v (y. y))) (v c)) ((x ((a (v (y. y))) (v c))) y)) (((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))) (((v (x. (v c))) (v (x. (v c)))) (((((z z) b) (c. a)) (z z)) (b c))))) (a. ((((z z) b)(c. a)) (z z)))) (y. (z z))) (((a (v (y. y))) w) (z. x))) (w. (z. (v (y. y)))))\r
+C ((((((((z z) b) (c. a)) (z z)) ((v (y. y)) a)) (v (y. y))) ((((a (v (y. y))) (v c)) (z z)) ((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))))) (z. ((v (y. y)) a)))\r
+C (((((((a (v (y. y))) w) (a b)) ((b (x. (b. a))) (b. (v. ((((z z) b) (c. a)) (z z)))))) (a. (z. (b. w)))) (x. (((w v) ((z z) (a (v (y. y))))) ((a (v (y. y))) (v c))))) (((z z) (a (v (y. y)))) (b. a)))\r
+C (((((((z z) b) (c. a)) (z z)) (b c)) (b. a)) (((v (x. (v c))) (((v (x. (v c))) ((z z) b)) (a. (w. (v. (z. (v (y. y)))))))) ((x ((a (v (y. y))) (v c))) (b. (c. y)))))\r
+C (((((((z z) b) (c. a)) (z z)) (b c)) (b. a)) (y. (x. z)))\r
+N ((((((((a (v (y. y))) w) (a b)) ((b (x. (b. a))) (b. (v. ((((z z) b) (c. a)) (z z)))))) (a. (z. (b. w)))) (x. (((w v)((z z) (a (v (y. y))))) ((a (v (y. y))) (v c))))) (((z z) (a (v (y. y)))) (b. a))) (w. ((((w v) ((z z) (a (v (y. y)))))((a (v (y. y))) (v c))) (((((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y)))))) ((z z) a)) (y. ((v c)((((z z) b) (c. a)) (w (c. (v c)))))))))) Z\r
+N (((((((a (v (y. y))) (v c)) ((x ((a (v (y. y))) (v c))) y)) (((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))) (((v (x. (v c))) (v (x. (v c)))) (((((z z) b) (c. a)) (z z)) (b c))))) (a. ((((z z) b) (c. a)) (z z)))) (y. (z z))) (((a (v (y. y))) w) (z. x))) Z\r
+N (((((((z z) b) (c. a)) (z z)) ((v (y. y)) a)) (v (y. y))) ((((a (v (y. y))) (v c)) (z z)) ((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))))) Z\r
+N (((((((z z) b) (c. a)) (z z)) (b c)) (b. a)) (y. (x ((z z) a)))) Z\r
+N (((((((z z) b) (c. a)) (z z)) (b c)) (x. (((z z) b) (c. a)))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))) Z\r