ocaml/problems.ml

   1 open Lambda4;;
   2 let magic strings = problem_of None [] strings;;
   3 let solve_many = List.iter solve;;
   4
   5 let p2 = magic [ "x y"; "x z" ; "x (y z)"]
   6
   7 let p4 = magic
   8   [ "x y"; "x (a. a x)" ; "y (y z)" ]
   9
  10 let p5 = magic
  11   ["a (x. x a) b"; "b (x. x b) a"]
  12 ;;
  13
  14 let p6 = magic
  15   ["a (x. x a) b"; "b (x. x b) (c a)"]
  16
  17 ;;
  18
  19 let p7 = magic
  20   ["a (x. (x a)(a x x a)(x x) )"]
  21
  22 ;;
  23
  24 let p8 = magic
  25   ["x x (x x)"]
  26
  27 ;;
  28
  29 let p9 = magic
  30   ["x x (x x x) (x x (x x)) (x x (x x x)) x x"]
  31
  32 ;;
  33
  34 let p10 = magic
  35   ["x (y (x a b c))"]
  36
  37 ;;
  38
  39 let p11 = magic
  40   ["x x"; "x (y.y)"]
  41
  42 ;;
  43
  44 let p12 = magic
  45   ["x x (x x)"; "x x (x (y.y))"]
  46
  47 ;;
  48
  49 let p13 = magic
  50   ["x x (x x (x x x x x (x x)))"]
  51
  52 ;;
  53
  54 let p14 = magic
  55   ["a (a a (a (a a)) (a (a a)))"]
  56
  57 ;;
  58
  59 let p15 = magic
  60   ["a (a (a a)) (a a (a a) (a (a (a a))) (a (a a)) (a a (a a) (a (a (a a))) (a (a a)))) (a a (a a) (a (a (a a))) (a (a a)))"]
  61
  62 ;;
  63
  64 let p16 = magic
  65   ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"]
  66
  67 ;;
  68
  69 let p17 = magic
  70   ["b a"; "b (c.a)"]
  71
  72 ;;
  73
  74 let p18 = magic
  75   ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"]
  76
  77 ;;
  78
  79 let p19 = magic
  80   ["a (a a) (a a a (a (a (a a) a)) a)"]
  81
  82 ;;
  83
  84 let p20 = magic
  85   ["a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))"];;
  86
  87 let p21 = magic
  88   ["(((y z) (y z)) ((z (y z)) ((y z) (z z))))";
  89    "(((z z) x) (y z))";
  90    "((z (y z)) ((y z) (z z)))"
  91 ] ;;
  92
  93 let p22 = magic
  94 ["((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))";
  95 "((z y) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) ((x y) (z z)))))";
  96 "(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ;;
  97
  98 (* diverging tests *)
  99 (* test p23 leads to test p24 *)
 100 let p23 = magic
 101 ["z z z"; "z (z z) (x. x)"] ;;
 102
 103 (* because of the last term, the magic number is 1 and we diverge;
 104    but setting the magic number to 0 allows to solve the problem;
 105    thus our strategy is incomplete *)
 106 let p24 = magic
 107 ["b b"; "b f"; "f b"; "a (x.x)"] ;;
 108
 109 (* because of the last term, the magic number is 1 and we diverge;
 110    but setting the magic number to 0 allows to solve the problem;
 111    thus our strategy is incomplete *)
 112 let p25 = magic
 113 ["b b"; "b f"; "f b"; "f (x.x)"] ;;
 114
 115 (* BUG:
 116    0 (n (d (o.n) ...)))
 117    After instantiating n, the magic number (for d) should be 2, not 1! *)
 118 let p26 = magic
 119 ["(((x y) (z. (y. (y. z)))) (z. y))";
 120 "(((x y) x) (y y))"] ;;
 121
 122 let p27 = magic
 123 ["(((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))))";
 124 "((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))";
 125 "(((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))"] ;;
 126
 127 let p28 = magic
 128 ["((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))";
 129  "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ;;
 130
 131 let p29 = magic
 132 ["((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))";
 133 "(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ;;
 134
 135 let p30 = magic
 136 ["((b c) (b. (z a)))";
 137 "((v (a. (z v))) ((y (b c)) ((z a) (v y))))";
 138 "((v (v. c)) z)";
 139 "((v y) (v (a. (z v))))";
 140 "((y (b c)) ((z a) (v y)))"] ;;
 141
 142 let p31 = magic
 143 [" (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))";
 144 "((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))";
 145 "(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))";
 146 "(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))";
 147 "((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"] ;;
 148
 149 let p32 = magic
 150 ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
 151 "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)";
 152 "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
 153 "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
 154 "((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))"
 155 ] ;;
 156
 157 (* Shows an error when the strategy that minimizes special_k is NOT used *)
 158 let p33 = magic
 159 [
 160 "((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b))) (((y (y (v w))) z) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)))) (b c)) (((v w) (z (a (c. y)))) ((y b) (b (z (a (c. y)))))))";
 161 "((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))";
 162 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))";
 163 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) (b (z (a (c. y))))) ((c b) (b. (b w))))";
 164 (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)
 165 ] ;;
 166
 167 let p34 = magic [
 168 "b c (b c) (c (d (j. e))) (b c (b c) (j.c f)) (b f (j. k. d)) (b (j. k. l. b c (b c)) (b g)) a";
 169 "d (j. e) e (j. c f) (j. c j) b a";
 170 "d (j. e) e (j. c f) b (b c (b c) (j. c f)) a";
 171 "d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a";
 172 "d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a";
 173 ] ;;
 174 (* 0: (b c (b c) (c (d j.e)) (b c (b c) j.(c f)) (b f j.k.d) (b j.k.l.(b c (b c)) (b g)) a)
 175 1: (d j.e e j.(c f) j.(c j) b a)
 176 2: (d j.e e j.(c f) b (b c (b c) j.(c f)) a)
 177 3: (d j.e e j.(c f) b (b c (b c) j.(c f) (g b)) a)
 178 4: (d j.e e j.(c f) b j.k.(j l.e e l.(k f) b) a) *)
 179
 180 let p35 = magic [
 181 "(((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (z (z b))) ((y y) (((b z) v) (a ((v (y y)) (v (y y)))))))";
 182 "((((((((a b) z) w) (((b z) v) (a ((v (y y)) (v (y y)))))) ((y y) ((y (v (y y))) b))) ((((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) (((((c (a b)) (y y)) (y (v (y y)))) (z w)) ((w (((v (y y)) (v (y y))) a)) (w (z ((y (v (y y))) b)))))) (z w))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (c (a b)))) (((((b z) (c b)) (c ((v (y y)) (v (y y))))) (((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) ((c b) (z (z b))))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b)))))) (((((w ((a b) z)) (a ((v (y y)) (v (y y))))) (((v (y y)) (v (y y))) a)) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b))))))) (b z))) ((x ((c b) (c b))) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y))))))))))";
 183 "((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (v (y y)))"
 184 ] ;;
 185
 186 let p36 = magic
 187 [
 188 "(((((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (((y c) (x a)) (v (((y a) (((z v) (y a)) (b a))) z)))) ((b a) (b a))) ((a c) (b (((y a) (((z v) (y a)) (b a))) (z a))))) ((((((b (((y a) (((z v) (y a)) (b a))) z)) (c ((y (x a)) ((z v) (y a))))) (v (((y a) (((z v) (y a)) (b a))) z))) (((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))) ((x a) (((y a) (((z v) (y a)) (b a))) z)))) ((c ((y (x a)) ((z v) (y a)))) (b (((y a) (((z v) (y a)) (b a))) z)))) ((((b (z a)) (y a)) (y c)) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))))))))";
 189 "(((((((z v) (y a)) (b a)) w) b) (((b a) ((((z v) (y a)) (b a)) w)) ((((z v) (y a)) (b a)) w))) (((b a) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) w)) (((c y) a) v)))";
 190 "(((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x))"
 191 ] ;;
 192
 193 (* issue with eta-equality of terms in ps *)
 194 let p37 = magic
 195   ["x (a y) z"; "x (a z. y z) w"; "a c"]
 196   ;;
 197
 198 (**********************)
 199
 200 let q1 () = problem_of
 201  None
 202  ["a d e"]
 203  ["a b"; "a c"]
 204  ;;
 205
 206 let q2 () = problem_of
 207  None
 208  ["a d e"]
 209  ["a b" ]
 210  ;;
 211
 212 let q3 () = problem_of
 213  (Some "x")
 214  ["a d e f"]
 215  ["a b" ]
 216  ;;
 217
 218 let q4 () = problem_of
 219  None
 220  ["f (x.a b c d)"]
 221  ["a b" ]
 222  ;;
 223
 224 let q5 () = problem_of
 225  (Some"x")
 226  ["(y. x)"]
 227  ["x"]
 228  ;;
 229
 230 let q6 () = problem_of
 231  (Some"x")
 232  ["(y. x z)"]
 233  ["y"]
 234  ;;
 235
 236 let q7 () = problem_of
 237  (Some "(b (c d (e f f k.(g e))) f)")
 238  ["(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)))";
 239   "(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)))))";
 240   "(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)))))"]
 241  ["(f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)";
 242   "(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)";
 243   "(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)"]
 244  ;;
 245
 246 (**********************)
 247
 248 let q8 () = problem_of
 249  (Some"x a")
 250  ["y (x b c)"] ["j"]
 251 ;;
 252
 253 let q9 () = problem_of
 254  (Some"x a")
 255  ["y x"] ["a (y a b b b)"]
 256 ;;
 257
 258 let q11 () = problem_of
 259  (Some "x y")
 260  ["a (x z)"] [] ;;
 261
 262 let q10 () = problem_of
 263  (Some "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)
 264 (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
 265  (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c)))")
 266 ["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))";
 267 "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))";
 268 "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))";
 269 "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)))";
 270 "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)))"]
 271 [
 272 "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)))";
 273 "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))";
 274 "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)";
 275 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)";
 276 "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)))";
 277 ] ;;
 278
 279 let m1 () = problem_of None []
 280  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 281
 282 ;;
 283
 284 let m2 () = problem_of None []
 285  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 286
 287 ;;
 288
 289
 290 let n1 () = problem_of (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (g (k. c e) (k. i) (c b) (f c) b)")
 291 [
 292 "b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. i))";
 293 "g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. l. g (m. c e) (m. i) (c b) (l c) b) (e c (d d (d c)) (c e (k. f)) (b (c b) (k. l. c b d) (c e) (k. l. m. f)))";
 294 "b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e))";
 295 "b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. l. m. c c g) (e c (b (k. f))) (k. f c)";
 296 "c (c e) (e c (d d (d c)) (k. c e (f c))) (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. c e (l. f) (k (l. c e) (l. i)))) (k. l. l (m. c e) (m. i) (c b) (f c) b) (k. l. c k) (f (f c) (b (c b) (k. l. c b d) (c e)) (b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. l. m. c c g) (e c (b (k. f)))))";
 297 ] [
 298 "b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (h (g (k. c e) (k. i) (c b) (c (c e)))) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a";
 299 "c c g (k. b (c b) (l. m. c b k) (c e)) (k. b (c b) (l. m. c b d) (c k) b) (k. e c (d h) k) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a";
 300 "d h (b (c b) (k. l. c b d) (c e)) (k. g (l. c e) (l. i) (c b) (k c) b) d b (b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (k. c)) a";
 301 "g (k. c e) (k. d d) (k. k k) (e c (d d (d c)) i) (k. g (l. k e) (l. d d)) (g i (b (c b) (k. l. c b d) (e c (d d (d c)) (k. c e (f c)) (k. k (c k) (l. m. c k d) (c e) k (g (l. c e) (l. i) (c k)) (l. c))))) (c b) a";
 302 "g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e) a"
 303 ] ;;
 304
 305 let n2 () = problem_of
 306 (Some"b b (c d) (k. d e) (k. k) (k. l. b)")
 307 [
 308 "b b (d e (k. d e)) (g (k. e) (k. k)) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (k. k (k k) (l. l))) (f (e (c d))) (b b (d e (k. d e)) (b b) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))))) (d e (k. d e) g (i (k. k)))";
 309 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (d (g (de) (g (k. e)) h) (g (k. b b)))";
 310 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. l. l) (k. g (d e) (l. m. m))";
 311 "b b (d e (k. d e)) (g (k. e) (k. k)) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (k. k (k k) (l. l))) (f (e (c d))) (b b (d e (k. d e)) (b b) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h)))))";
 312 "d (g (d e) (g (k. e)) h) (g (g (d e)) (d e (k. d e) (k. b (l. h)) (k. l. d e))) (b (k. h) (k. k e (l. m. b b)) (k. k (k k) (l. l))) (k. b) (b b (k. l. i)(k. c))";
 313 ] [
 314 "b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (e (b b (c d))) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (g (k. e) (k. k))) (k. l. d (g (d k) (g (m. k)) h) (d k (m. n. b b))) (e (c d) (e (c d))) a";
 315 "d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) a";
 316 "d e (k. d e) (k. b (l. h)) (k. l. d e) (d (g (d e) (g (k. e)) h) (g (d e) (k. l. l))) a";
 317 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (k. l. m. b b) a";
 318 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (b (b b) (d (g(d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (e (b b (c d))) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (g (k. e) (k. k)))) (k. d e (l. d e) f) a";
 319 ]
 320 ;;
 321
 322 let n3 () = problem_of
 323 (Some"b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))")
 324 [
 325 "b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) (k. l. l (m. l))";
 326 "c d e (f i) (e e) (g e) (k. l. e) (k. c (g (k (l. i)))) (c d e (k. k))";
 327 "f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (c d e (f i) (e e) (f (k. h))) (g e (b (k. i)) (e e (e e)))";
 328 "f (k. f) (k. f) (k. e) (c d e (f i) (e e) (g e)) (k. e e) (k. l. m. e) (k. e)";
 329 "g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f)";
 330 ][
 331 "b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) a";
 332 "c d e (f i) (e e) (g e) (b (g (k. e e)) (k. c (g (h (l. i))) (l. f l))) (k. f (l. f) (l. f)) a";
 333 "e e (k. k d e (l. l)) (g e) (c d e b (e e (c (c d e f)))) (d (e e (k. k d e (l. l))) (k. k i)) (k. i (l. c (c d e f))) (k. h) a";
 334 "f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a";
 335 "g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f) (f (k. f) (k. f) (k. l. l) (c (k. i (l. c (c d e f))))) a";
 336 ] ;;
 337
 338 (* main ([p34]);; *)
 339
 340 solve_many ([
 341  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;
 342  p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ;
 343  p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ;
 344  p34 ;
 345  p35 ;
 346  p36 ;
 347  p37 ;
 348  p24 ; p25 ;
 349 ] @ List.map ((|>) ()) ([
 350  q1 ; q2; (*q3;*) q4 ; q5 ; q6 ;
 351  q7 ;
 352  q8 ;
 353  q9 ;
 354  q10 ;
 355  q11 ;
 356  m1 ;
 357  m2 ;
 358 ] @ [
 359  n1 ;
 360  n2 ;
 361  n3
 362 ]));;