X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems%2Fw;h=c603cfb13cbfe0b421ea9a1d86c47083e32ad8b3;hb=3f5fd50fbe0c585e1d9aad84007fdbd82c573fa7;hp=d55e1b83dd9efe6b49811244731e37cce8d3eef5;hpb=dcb2ece094f794f4e9f4f98b92f378998e92a919;p=fireball-separation.git

diff --git a/ocaml/problems/w b/ocaml/problems/w
index d55e1b8..c603cfb 100644
--- a/ocaml/problems/w
+++ b/ocaml/problems/w
@@ -70,6 +70,7 @@ 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
 
 $! new failing problem
 # it is backtracking, but it shouldn't
+# why? well, D occurs in some C's
 D (a b)
 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)))))
 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)))