From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 15 Jul 2017 14:41:39 +0000 (+0200)
Subject: Important: added special variable "Z" for zero.
X-Git-Tag: weak-reduction-separation~27
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38ecafd7f8a1b5137f642bfa433d27cef8de2908;p=fireball-separation.git

Important: added special variable "Z" for zero.

- Removed append_zero in Lambda4
- Now tests append "Z" at the end of ps'
- Manually appended "Z" at the end of all problems
- Removed tmp function in Lambda4, renamed to problem_of

(cherry picked from commit 82dd1911598932af386c4de46398624453e1fc31)
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 1e978f2..18b0bc0 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -675,7 +675,8 @@ type result = [
 ]
 
 let check p =
- (* check if there are duplicates in p.ps *)
+ (* TODO check if there are duplicates in p.ps
+     before it was: ps = sort_uniq ~compare:eta_compare (ps :> nf list) *)
  (* FIXME what about initial fragments? *)
  if (let rec f = function
      | [] -> false
@@ -742,25 +743,10 @@ let solve p =
   `Separable p_finale.sigma
 ;;
 
-let zero = `Var(0,0);;
-
-let append_zero =
- function
-  | `I _
-  | `Var _ as i -> cast_to_i_n_var (mk_app i zero)
-  | `N _ -> raise (Parser.ParsingError " numbers in ps")
-;;
-
-let tmp (label, div, conv, nums, var_names) =
- (* DA SPOSTARE NEI TEST: *)
- let ps = List.map append_zero nums in (* crea lista applicando zeri o dummies *)
- let ps = sort_uniq ~compare:eta_compare (ps :> nf list) in
- let ps = List.map (cast_to_i_n_var) ps in
-
- (* TODO: *)
- (* replace div with bottom in problem??? *)
- let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in
- if all_tms = [] then failwith "FIXME: empty problem";
+let problem_of (label, div, conv, ps, var_names) =
+ (* TODO: replace div with bottom in problem??? *)
+ let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ ps @ conv in
+ if all_tms = [] then failwith "problem_of: empty problem";
  let initialSpecialK = compute_special_k (Listx.from_list (all_tms :> nf list)) in
  let freshno = List.length var_names in
  let deltas =
@@ -768,29 +754,3 @@ let tmp (label, div, conv, nums, var_names) =
    [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
  {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label}
 ;;
-
-let problem_of ~div ~conv ~nums =
- let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in
- let all_tms, var_names = Parser.parse' all_tms in
- let div, (ps, conv) = match div with
-   | None -> None, list_cut (List.length nums, all_tms)
-   | Some _ -> Some (List.hd all_tms), list_cut (List.length nums, List.tl all_tms) in
-
- let div =
-  match div with
-   | None -> None
-   | Some (`I _ as t) -> Some t
-   | _ -> raise (Parser.ParsingError "div is not an inert or BOT in the initial problem") in
- let conv = Util.filter_map (
-  function
-  | #i_n_var as t -> Some t
-  | `Lam _ -> None
-  | _ -> raise (Parser.ParsingError "A term in conv is not i_n_var")
-  ) conv in
- let ps = List.map (
-  function
-   | #i_n_var as y -> y
-   | _ -> raise (Parser.ParsingError "A term in num is not i_n_var")
-  ) ps in
- tmp("missing label", div, conv, ps, var_names)
-;;
diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli
index c8a40bf..8e89903 100644
--- a/ocaml/lambda4.mli
+++ b/ocaml/lambda4.mli
@@ -7,9 +7,7 @@ type result = [
  | `Unseparable of string
 ]
 
-val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem
-(* the following will soon replace the one above *)
-val tmp: (string (* problem label *)
+val problem_of: (string (* problem label *)
 * Num.i_var option (* div *)
 * Num.i_n_var list (* conv *)
 * Num.i_n_var list (* ps *)
diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 902da8d..abd4309 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -148,11 +148,13 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j")
    let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in
    let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in
    let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in
+   let n_z = try Util.index_of "Z" free with Not_found -> min_int in
    let fix lev v =
     if v = lev + n_bot then failwith "Example with `Bottom"
      else if v = lev + n_pac then failwith "Example with `Pacman"
       else if v = lev + n_bomb then failwith "Example with `Bomb"
-       else `Var(v,1) in (* 1 by default when variable not applied *)
+       else if v = lev + n_z then `Var(lev, 0) (* FIXME why zero? *)
+         else `Var(v,1) in (* 1 by default when variable not applied *)
    (* Fix arity *)
    let open Num in
    let rec aux lev : nf -> nf = function
diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 0678a13..5f86177 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -44,6 +44,6 @@ let assert_depends x =
 if Array.length Sys.argv = 1
  then failwith "no command line args. Please use e.g. ./a.out problems/*"
 else Array.iteri (fun i filename -> if i > 0 then
- List.iter (assert_depends ++ Lambda4.tmp) (Parser.from_file filename)
+ List.iter (assert_depends ++ problem_of) (Parser.from_file filename)
  ) Sys.argv
 ;;
diff --git a/ocaml/problems/m b/ocaml/problems/m
index 64b6ad3..716e4d4 100644
--- a/ocaml/problems/m
+++ b/ocaml/problems/m
@@ -1,13 +1,13 @@
 $! m1
-N y z
-  x z
-  x (a k) u
-  x (a r)
-  x (a k) v
+N y z Z
+  x z Z
+  x (a k) u Z
+  x (a r) Z
+  x (a k) v Z
 
 $! m2
-N y z
-  x z
-  x (a k) u
-  x (a r)
-  x (a k) v
+N y z Z
+  x z Z
+  x (a k) u Z
+  x (a r) Z
+  x (a k) v Z
diff --git a/ocaml/problems/n b/ocaml/problems/n
index 2352457..25d5378 100644
--- a/ocaml/problems/n
+++ b/ocaml/problems/n
@@ -5,11 +5,11 @@ C 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
   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. l. m. c c g) (e c (b (k. f))) (k. f c)
   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)))))
-N 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
-  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
-  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
-  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
-  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"
+N 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 Z
+  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 Z
+  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 Z
+  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 Z
+  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 Z
 
 $! n2
 D b b (c d) (k. d e) (k. k) (k. l. b)
@@ -18,11 +18,11 @@ C 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 (
   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))
   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 (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))
-N 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
-  d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) a
-  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
-  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
-  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
+N 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))) Z
+  d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) Z
+  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))) Z
+  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) Z
+  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) Z
 
 $! n3
 D b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))
@@ -31,8 +31,8 @@ C b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (
   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)))
   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)
   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)
-N 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
-  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
-  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
-  f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a
-  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
+N 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)) Z
+  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)) Z
+  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) Z
+  f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) Z
+  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))))) Z
diff --git a/ocaml/problems/o b/ocaml/problems/o
new file mode 100644
index 0000000..95c3c3d
--- /dev/null
+++ b/ocaml/problems/o
@@ -0,0 +1,21 @@
+$! o1
+N x a b Z
+  x (_. BOT) c Z
+
+$! o2
+N x (y (_. BOT) a) c Z
+  x (y a PAC) d Z
+
+$! o3
+D y (x a1 BOMB c) (x BOMB b1 d)
+C y (x a2 BOMB c) (x BOMB b1 d)
+  y (x a1 BOMB c) (x BOMB b2 d)
+
+
+$! o4
+D x BOMB a1 c
+  x y BOMB d
+
+$! o6
+D x BOMB
+C x y
diff --git a/ocaml/problems/p b/ocaml/problems/p
index a2155a6..27315d0 100644
--- a/ocaml/problems/p
+++ b/ocaml/problems/p
@@ -1,171 +1,172 @@
 
 $! p2
-N x y
-  x z
-  x (y z)
+N x y Z
+  x z Z
+  x (y z) Z
 
 $! p4
-N x y
-  x (a. a x)
-  y (y z)
+N x y Z
+  x (a. a x) Z
+  y (y z) Z
 
 $! p5
-N a (x. x a) b
-  b (x. x b) a
+N a (x. x a) b Z
+  b (x. x b) a Z
 
 $! p6
-N a (x. x a) b
-  b (x. x b) (c a)
+N a (x. x a) b Z
+  b (x. x b) (c a) Z
 
 $! p7
-N a (x. (x a) (a x x a) (x x) )
+N a (x. (x a) (a x x a) (x x) ) Z
 
 $! p8
-N x x (x x)
+N x x (x x) Z
 
 $! p9
-N x x (x x x) (x x (x x)) (x x (x x x)) x x
+N x x (x x x) (x x (x x)) (x x (x x x)) x x Z
 
 $! p10
-N x (y (x a b c))
+N x (y (x a b c)) Z
 
 $! p11
-N x x
-  x (y.y)
+N x x Z
+  x (y.y) Z
 
 $! p12
-N x x (x x)
-  x x (x (y.y))
+N x x (x x) Z
+  x x (x (y.y)) Z
 
 $! p13
-N x x (x x (x x x x x (x x)))
+N x x (x x (x x x x x (x x))) Z
 
 $! p14
-N a (a a (a (a a)) (a (a a)))
+N a (a a (a (a a)) (a (a a))) Z
 
 $! p15
-N 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)))
+N 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))) Z
 
 $! p16:
-N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))
+N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) Z
 
 $! p17
-N b a
-  b (c.a)
+N b a Z
+  b (c.a) Z
 
 $! p18
-N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))
-  a a
-  a (a a)
+N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a)))) Z
+  a a Z
+  a (a a) Z
 
 $! p19
-N a (a a) (a a a (a (a (a a) a)) a)
+N a (a a) (a a a (a (a (a a) a)) a) Z
 
 $! p20
-N 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)))))
+N 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))))) Z
 
 $! p21
-N (((y z) (y z)) ((z (y z)) ((y z) (z z))))
-  (((z z) x) (y z))
-  ((z (y z)) ((y z) (z z)))
+N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) Z
+  (((z z) x) (y z)) Z
+  ((z (y z)) ((y z) (z z))) Z
 
 $! p22
-N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))
-  ((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)))))
-  (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))
+N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z
+  ((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))))) Z
+  (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z
 
 $! p23
 # (* diverging tests *) (* test p23 leads to test p24 *)
-N z z z
-  z (z z) (x. x)
+N z z z Z
+  z (z z) (x. x) Z
 
 $! p24
 # (* because of the last term, the magic number is 1 and we diverge
      but setting the magic number to 0 allows to solve the problem
      thus our strategy is incomplete *)
-N b b
-  b f
-  f b
-  a (x.x)
+N b b Z
+  b f Z
+  f b Z
+  a (x.x) Z
 
 $! p25
 # (* because of the last term, the magic number is 1 and we diverge
      but setting the magic number to 0 allows to solve the problem
      thus our strategy is incomplete *)
-N b b
-  b f
-  f b
-  f (x.x)
+N b b Z
+  b f Z
+  f b Z
+  f (x.x) Z
 
 $! p26
   (* BUG:
      0 (n (d (o.n) ...)))
      After instantiating n, the magic number (for d) should be 2, not 1! *)
-N (((x y) (z. (y. (y. z)))) (z. y))
-  (((x y) x) (y y))
+N (((x y) (z. (y. (y. z)))) (z. y)) Z
+  (((x y) x) (y y)) Z
 
 $! p27
-N (((((((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))))
-  ((((((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))
+N (((((((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)))) Z
+  ((((((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
+  (((((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
 
 $! p28
-N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))
-   (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))
+N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x))))) Z
+  (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x))))) Z
 
 $! p29
-N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))
-  (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)
+N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y)) Z
+  (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) Z
 
 $! p30
-N ((b c) (b. (z a)))
-  ((v (a. (z v))) ((y (b c)) ((z a) (v y))))
-  ((v (v. c)) z)
-  ((v y) (v (a. (z v))))
-  ((y (b c)) ((z a) (v y)))
+N ((b c) (b. (z a))) Z
+  ((v (a. (z v))) ((y (b c)) ((z a) (v y)))) Z
+  ((v (v. c)) z) Z
+  ((v y) (v (a. (z v)))) Z
+  ((y (b c)) ((z a) (v y))) Z
 
 $! p31
-N  (((((((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)))
-   ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))
-   (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))
-    (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))
-      ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))
-
-$! p32
-N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))
-  (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)
-  (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))
-  ((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))
-  ((((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)))))))
+N  (((((((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))) Z
+   ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) Z
+   (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) Z
+    (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) Z
+      ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) Z
+
+$? p32
+# should fail because the first and second terms are eta-eq
+N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) Z
+  (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) Z
+  (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) Z
+  ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) Z
+  ((((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))))))) Z
 
 $! p33
   (* Shows an error when the strategy that minimizes special_k is NOT used *)
-N ((((((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)))))))
-  ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))
-  (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))
-  (((((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))))
+N ((((((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))))))) Z
+  ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y)) Z
+  (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) Z
+  (((((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)))) Z
 #  (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)
 
 $! p34
-N 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
-  d (j. e) e (j. c f) (j. c j) b a
-  d (j. e) e (j. c f) b (b c (b c) (j. c f)) a
-  d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a
-  d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a
+N 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 Z
+  d (j. e) e (j. c f) (j. c j) b a Z
+  d (j. e) e (j. c f) b (b c (b c) (j. c f)) a Z
+  d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a Z
+  d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a Z
 
 $! p35
-N (((((((((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)))))))
-  ((((((((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))))))))))
-  ((((((((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)))
+N (((((((((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))))))) Z
+  ((((((((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)) Z (((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)))))))))) Z
+  ((((((((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))) Z
 
 $! p36
-N (((((((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))))))))
-  (((((((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)))
-  (((((((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))
+N (((((((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)))))))) Z
+  (((((((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))) Z
+  (((((((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)) Z
 
 
 $! p37
   issue with eta-equality of terms in ps
-N x (a y) z
-  x (a z. y z) w
-  a c
+N x (a y) z Z
+  x (a z. y z) w Z
+  a c Z
diff --git a/ocaml/problems/q b/ocaml/problems/q
index 9f43235..01ec754 100644
--- a/ocaml/problems/q
+++ b/ocaml/problems/q
@@ -1,20 +1,20 @@
 $! q1
 C a d e
-N a b
-  a c
+N a b Z
+  a c Z
 
 $! q2
 C a d e
-N a b
+N a b Z
 
 $! q3
 D x y
 C a d e f
-N a b
+N a b Z
 
 $! q4
 C f (x.a b c d)
-N a b
+N a b Z
 
 $! q5
 D x y
@@ -24,28 +24,28 @@ N x
 $! q6
 D x w
 C (y. x z)
-N y
+N y Z
 
 $! q7
 D (b (c d (e f f k.(g e))) f)
 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)))
   (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)))))
   (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)))))
-N (f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)
-  (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)
-  (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)
+N (f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a) Z
+  (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) Z
+  (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) Z
 
 ################################################################################
 
 $! q8
 D x a
 C y (x b c)
-N j
+N j Z
 
 $! q9
 D x a
 C y x
-N a (y a b b b)
+N a (y a b b b) Z
 
 $! q11
 D x y
@@ -59,8 +59,8 @@ 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.
   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)))
   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)))
 
-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)))
-  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))
-  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)
-  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)
-  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)))
+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))) Z
+  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)) Z
+  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) Z
+  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b) Z
+  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))) Z
diff --git a/ocaml/problems/w b/ocaml/problems/w
index ec35dd0..e86007c 100644
--- a/ocaml/problems/w
+++ b/ocaml/problems/w
@@ -20,11 +20,11 @@ C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h)))
 C b (k. l. b) (e f) (b c d) (e e (b (k. l. b)) d) (e (k. l. b c) (k. l. b k) (b c)) d (e e (e e) (d (k. f)) (b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))))) (e e (b (k. l. b)) (b (k. l. b) (e f) (b c d)) (e e (b (k. l. b)) d (k. d) (b (k. l. b))) (k. b c k (l. e l) (e e (b (l. m. b)) k (l. k)) (f g (c (e h))) (k b (l. b) (f g (e f))) (c (e h))) (k. i (f g) (l. l)))
 #  ] (* NUMERIC    *) [
-N b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) a
-  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) a
-  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) a
-  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) a
-  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) a
+N b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) Z
+  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) Z
+  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) Z
+  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) Z
+  b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) Z
 #  ];
 
 $!
@@ -41,11 +41,11 @@ C 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
   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))) (k. g)
   e f (k. k) (g e) (e f (k. e)) (e f (k. e)) (h c (b (g e) h (k. c (l. m. m k l))))
 # ] (* NUMERIC    *) [
-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))) (k. i) a
-  e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) a
-  e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) a
-  e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) a
-  g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f a
+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))) (k. i) Z
+  e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) Z
+  e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) Z
+  e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) Z
+  g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f Z
 #  ]
  ];
 
diff --git a/ocaml/test.ml b/ocaml/test.ml
index f5bf55a..da6dbda 100644
--- a/ocaml/test.ml
+++ b/ocaml/test.ml
@@ -1,4 +1,5 @@
 open Lambda4;;
+open Util;;
 
 let acaso l =
     let n = Random.int (List.length l) in
@@ -57,12 +58,14 @@ let rec repeat f n =
   ) in Lambda3.main [Lambda3.magic tms ["*"]]
 ;; *)
 let call_main4 div convs nums =
-  let _ = (
-  (match div with Some div -> prerr_endline ("DIV: " ^ div) | None -> ());
-  print_endline "CONV:"; List.iter prerr_endline convs;
-  print_endline "NUMS:"; List.iter prerr_endline nums;
-  prerr_newline ();
-  ) in Lambda4.solve (Lambda4.problem_of div convs nums)
+ let p = String.concat "\n" (
+  "$! randomly generated test" ::
+  ("D " ^ div) ::
+  List.map ((^) "C ") convs @
+  List.map (fun s -> "N " ^ s ^ " Z") nums
+ ) in
+ prerr_endline p;
+ (Lambda4.solve ++ Lambda4.problem_of ++ Parser.problem_of_string) p
 ;;
 
 let main =
@@ -80,7 +83,7 @@ let main =
   else *)
   repeat (fun _ ->
     let div, (conv, nums) = test4 complex vars in
-    call_main4 (Some div) conv nums
+    call_main4 div conv nums
   ) num
   ;