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

diff --git a/ocaml/problems/w b/ocaml/problems/w
index d55e1b8..c10a3f6 100644
--- a/ocaml/problems/w
+++ b/ocaml/problems/w
@@ -68,16 +68,17 @@ 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
   (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)
 
 
-$! new failing problem
+#$! new failing problem
 # it is backtracking, but it shouldn't
-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)))
-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)))
-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)))))
-C (((((((z z) b) (c. a)) (z z)) (b c)) (b. a)) (y. (x. z)))
-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
-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
-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
-N (((((((z z) b) (c. a)) (z z)) (b c)) (b. a)) (y. (x ((z z) a)))) Z
-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
+# 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)))
+ 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)))
+ 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)))))
+ C (((((((z z) b) (c. a)) (z z)) (b c)) (b. a)) (y. (x. z)))
+ 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
+ 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
+ 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
+ N (((((((z z) b) (c. a)) (z z)) (b c)) (b. a)) (y. (x ((z z) a)))) Z
+ 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