$?
D x y
C x BOMB

$?
D x y z
C x BOMB z
  x y y

$!
 (* DISPLAY PROBLEM (main) - measure=965
    Discriminating sets (deltas):
    0 <> 1 <> 2 <> 3 <> 4
 *)(* DIVERGENT  *)
D 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)) (k. b c d (l. c (l k)) (b c (l. e e) (b c d (l. e l) (e e (b (l. m. b)) d (l. d))) (l. c)))
#   (* CONVERGENT *) [
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)) (e e (b (k. l. b)) (k. e k)) (k. e e) (k. g (l. g (m. b c)) (l. i (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))) (b c (k. c (e h)))
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)) (e e (b (k. l. b)) (k. e k)) (k. e e)
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)) 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
#  ];

$!
 problem_of
 (* DISPLAY PROBLEM (main) - measure=561
    Discriminating sets (deltas):
    0 <> 1 <> 2 <> 3 <> 4
 *)(* DIVERGENT  *)
D b (c b) (k. d) (e f (k. e) (k. b) (f d)) (e f (k. g k) d) (k. c k (c k g))
#   (* CONVERGENT *) [
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))) (k. g) (e f (k. k (g e) h) b (e (k. g) (h c (g c) f)))
  e f (k. k) (k. l. c b) (k. l. l (k b) g) (k. e f (l. l)) (h c (c (k. l. l b k) (k. l. d) (e f (k. k) (g e))) (k. g e (g e))) (k. g (l. e f g) (l. h c) (g (l. e f g) (l. h c)))
  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))) (k. l. g l (g l) (m. c b))
  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) 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
#  ]
 ];

# This fails, but shouldnt: commented out
# $!
 D x PAC PAC PAC PAC PAC a
 C x PAC PAC PAC PAC PAC b
 N y x
   y z
# In general:
  DIV x (n times PAC) a
  CON x (n times PAC) b
  1 y (m times lambda. x) 0
  2 y z 0
  when x steps on the n+1-th argument,
  y must apply n+m+1 variables
  Thus special_k must be >=n+m+1

# todo:
  (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)


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