]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems/q
Moved all problems in problems folder. Last ones in "w"
[fireball-separation.git] / ocaml / problems / q
diff --git a/ocaml/problems/q b/ocaml/problems/q
new file mode 100644 (file)
index 0000000..9f43235
--- /dev/null
@@ -0,0 +1,66 @@
+$! q1\r
+C a d e\r
+N a b\r
+  a c\r
+\r
+$! q2\r
+C a d e\r
+N a b\r
+\r
+$! q3\r
+D x y\r
+C a d e f\r
+N a b\r
+\r
+$! q4\r
+C f (x.a b c d)\r
+N a b\r
+\r
+$! q5\r
+D x y\r
+C (y. x)\r
+N x\r
+\r
+$! q6\r
+D x w\r
+C (y. x z)\r
+N y\r
+\r
+$! q7\r
+D (b (c d (e f f k.(g e))) f)\r
+C (g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (f d k.g (b (g (e f)) (b (g (e f)) (e f)) (g (e f) (g e h)))) k.l.(h f (b i)))\r
+  (g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (b (g (e f))) k.l.(g f (k f f (k f f m.(g k)))))\r
+  (b (g (e f)) f k.e k.l.(f d (e f)) (c d (e f f k.(g e)) (g k.(e f f))) (h f (i (h k.(i b l.m.n.e)))))\r
+N (f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)\r
+  (f d (e f) k.e k.l.(c d) (b (g e) k.h) (d k.e) (f d (e f) k.e) a)\r
+  (g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (g e h) (g f (e f f (e f f k.(g e))) (g (e f)) (b (c d (e f f k.(g e))) (b (g (e f)) (e f)) (b (g (e f)) k.l.e))) a)\r
+\r
+################################################################################\r
+\r
+$! q8\r
+D x a\r
+C y (x b c)\r
+N j\r
+\r
+$! q9\r
+D x a\r
+C y x\r
+N a (y a b b b)\r
+\r
+$! q11\r
+D x y\r
+C a (x z)\r
+\r
+$! q10\r
+D b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f) (k. e (f g))) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c)))\r
+C e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c))) (c f (k. b (l. c)) (k. l. b (m. c))) (k. l. b (m. c) d (l (f k) (m. k)) (m. n. c)) (c f (k. b (l. c)) (k. b (l. c) d) (k. c k))\r
+  e (f g) (k. g) (c f) (k. i) (k. l. h) (k. l. m. n. m) (b (k. c) (k. l. b (m. c)) (k. c f)) (k. l. m. k (f g) (n. g) (c f) (n. k))\r
+  b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c))\r
+  b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (b (k. c) (k. e) (k. l. m. b (n. c))) (e (f g) (k. g) (c f) (k. i) (k. l. h) (k. l. m. n. m) (b (k. c) (k. l. b (m. c)) (k. c f)) (k. l. m. k (f g) (n. g) (c f) (n. k)))\r
+  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f) (k. e (f g)))\r
+\r
+N b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))\r
+  b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c)))) (k. e (f g) (l. g) (c f) (l. k) (l. m. h))\r
+  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. m. n. o. p. o) (e (f g) (k. g) (c f) (k. i) f)\r
+  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)\r
+  e (f g) (k. g) (c f) (k. e) (k. b (l. c)) (c f (k. b (l. c)) (k. l. b (m. k))) (k. b (l. k)) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))\r