MAYBE
ignored inputs:
(COMMENT a fragment of ML )
(COMMENT Example 43 of [ FG07 , doi:10.1016/j.ic.2006.12.002 ] )

NRS:
   [ (0):  |- (app <(lam [a][]X),[]Y>) -> (sub <[a][]X,[]Y>),
     (1):  |- (sub <[a](app <[]X,[]Y>),[]Z>) -> (app <(sub <[a][]X,[]Z>),(sub <[a][]Y,[]Z>)>),
     (2):  |- (sub <[a]a,[]X>) -> []X,
     (3): a#X |- (sub <[a][]X,[]Y>) -> []X,
     (4): b#Y |- (sub <[a](lam [b][]X),[]Y>) -> (lam [b](sub <[a][]X,[]Y>)),
     (5):  |- (let <[]X',[a][]X>) -> (sub <[a][]X,[]X'>),
     (6):  |- (letrec [f]<[a][]X',[]X>) -> (sub <[f][]X,(lam [a](letrec [f]<[a][]X',[]X'>))>),
     (7): a#Y |- (sub <[b](let <[]X',[a][]X>),[]Y>) -> (let <(sub <[b][]X',[]Y>),[a](sub <[b][]X,[]Y>)>),
     (8): f#Y,a#Y |- (sub <[b](letrec [f]<[a][]X',[]X>),[]Y>) -> (letrec [f]<[a](sub <[b][]X',[]Y>),(sub <[b][]X,[]Y>)>) ]
Check confluence by Knuth-Bendix criterion
uniform

writing to temporary file...
./run_snprover.sh ./SMLNJ-Vphn6k.trs
NO

Problem:
 app(pair_2(lam(lambda(X)),Y)) -> sub(pair_2(lambda(X),Y))
 sub(pair_2(lambda(app(pair_2(X,Y))),Z)) ->
 app(pair_2(sub(pair_2(lambda(X),Z)),sub(pair_2(lambda(Y),Z))))
 sub(pair_2(lambda(diamond()),X)) -> X
 sub(pair_2(lambda(X),Y)) -> X
 sub(pair_2(lambda(lam(lambda(X))),Y)) -> lam(lambda(sub(pair_2(lambda(X),Y))))
 let(pair_2(X',lambda(X))) -> sub(pair_2(lambda(X),X'))
 letrec(lambda(pair_2(lambda(X'),X))) ->
 sub(pair_2(lambda(X),lam(lambda(letrec(lambda(pair_2(lambda(X'),X')))))))
 sub(pair_2(lambda(let(pair_2(X',lambda(X)))),Y)) ->
 let(pair_2(sub(pair_2(lambda(X'),Y)),lambda(sub(pair_2(lambda(X),Y)))))
 sub(pair_2(lambda(letrec(lambda(pair_2(lambda(X'),X)))),Y)) ->
 letrec(lambda(pair_2(lambda(sub(pair_2(lambda(X'),Y))),sub(pair_2(lambda(X),Y)))))

Proof:
 Containment Processor:
  loop length: 1
  terms:
   letrec(lambda(pair_2(lambda(X'),X)))
  context: sub(pair_2(lambda(X),lam(lambda([]))))
  substitution:
   X -> X'
   X' -> X'
  Qed
termination proof failed
result: MAYBE
time: 6 msec.