From: acondolu Date: Sun, 16 Jul 2017 13:41:49 +0000 (+0200) Subject: Commented out problem, it is (still) failing because div occurs in conv X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad04cfb31b56860cace4ab9969892942e931172d;p=fireball-separation.git Commented out problem, it is (still) failing because div occurs in conv --- diff --git a/ocaml/problems/w b/ocaml/problems/w index c603cfb..c10a3f6 100644 --- a/ocaml/problems/w +++ b/ocaml/problems/w @@ -68,17 +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 # 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 + 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