$! p2
N x y
  x z
  x (y z)

$! p4
N x y
  x (a. a x)
  y (y z)

$! p5
N a (x. x a) b
  b (x. x b) a

$! p6
N a (x. x a) b
  b (x. x b) (c a)

$! p7
N a (x. (x a) (a x x a) (x x) )

$! p8
N x x (x x)

$! p9
N x x (x x x) (x x (x x)) (x x (x x x)) x x

$! p10
N x (y (x a b c))

$! p11
N x x
  x (y.y)

$! p12
N x x (x x)
  x x (x (y.y))

$! p13
N x x (x x (x x x x x (x x)))

$! p14
N a (a a (a (a a)) (a (a a)))

$! 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)))

$! p16:
N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))

$! p17
N b a
  b (c.a)

$! 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)

$! p19
N a (a a) (a a a (a (a (a a) a)) a)

$! 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)))))

$! 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)))

$! 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))))

$! p23
# (* diverging tests *) (* test p23 leads to test p24 *)
N z z z
  z (z z) (x. x)

$! 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)

$! 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)

$! 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))

$! 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))

$! 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)))))

$! 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)

$! 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)))

$! 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)))))))

$! 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))))
#  (* "(((((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

$! 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)))

$! 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))


$! p37
  issue with eta-equality of terms in ps
N x (a y) z
  x (a z. y z) w
  a c