MAYBE
ignored inputs:
(COMMENT a system of beta reduction for the lambda calculus via explicit substitution )
(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>)) ]
Check confluence by parallel closed criterion
left-linear
uniform
BCPs:
(0 on 0(out)): 
   {  |- < (sub <[a][]X_1,[]Y_1>) <= (app <(lam [a][]X_1),[]Y_1>) => (sub <[a][]X_1,[]Y_1>) >,
     a#X_1 |- < (sub <[a][(a b)]X_1,[]Y_1>) <= (app <(lam [b][]X_1),[]Y_1>) => (sub <[b][]X_1,[]Y_1>) > }
(0 on 1(in)): 
   {  |- < (sub <[a](sub <[a][]X,[]Y_1>),[]Z_1>) <= (sub <[a](app <(lam [a][]X),[]Y_1>),[]Z_1>) => (app <(sub <[a](lam [a][]X),[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) >,
      |- < (sub <[b](sub <[a][]X,[]Y_1>),[]Z_1>) <= (sub <[b](app <(lam [a][]X),[]Y_1>),[]Z_1>) => (app <(sub <[b](lam [a][]X),[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>) > }
(1 on 1(out)): 
   {  |- < (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) <= (sub <[a](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) >,
     a#Y_1,a#X_1 |- < (app <(sub <[a][(a b)]X_1,[]Z_1>),(sub <[a][(a b)]Y_1,[]Z_1>)>) <= (sub <[b](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[b][]X_1,[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>) > }
(1 on 3(out)): 
   { a#X,a#Y |- < (app <(sub <[a][]X,[]Y_1>),(sub <[a][]Y,[]Y_1>)>) <= (sub <[a](app <[]X,[]Y>),[]Y_1>) => (app <[]X,[]Y>) >,
     a#Y,a#X,b#Y,b#X |- < (app <(sub <[a][]X,[]Y_1>),(sub <[a][]Y,[]Y_1>)>) <= (sub <[b](app <[(a b)]X,[(a b)]Y>),[]Y_1>) => (app <[(a b)]X,[(a b)]Y>) > }
(2 on 2(out)): 
   {  |- < []X_1 <= (sub <[a]a,[]X_1>) => []X_1 >,
      |- < []X_1 <= (sub <[b]b,[]X_1>) => []X_1 > }
(3 on 1(out)): 
   { a#X_1,a#Y_1 |- < (app <[]X_1,[]Y_1>) <= (sub <[a](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) >,
     b#Y_1,a#X_1,a#Y_1,b#X_1 |- < (app <[(a b)]X_1,[(a b)]Y_1>) <= (sub <[b](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[b][]X_1,[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>) > }
(3 on 3(out)): 
   { a#X_1 |- < []X_1 <= (sub <[a][]X_1,[]Y_1>) => []X_1 >,
     b#X_1,a#X_1 |- < [(a b)]X_1 <= (sub <[b][]X_1,[]Y_1>) => []X_1 > }
(3 on 4(out)): 
   { a#X_1,b#Y_1 |- < (lam [b][]X_1) <= (sub <[a](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[a][]X_1,[]Y_1>)) >,
     a#X_1,c#Y_1 |- < (lam [c][]X_1) <= (sub <[a](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[a][]X_1,[]Y_1>)) >,
     a#Y_1,b#X_1 |- < (lam [b][(a b)]X_1) <= (sub <[b](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[b][]X_1,[]Y_1>)) >,
     a#Y_1,c#X_1 |- < (lam [c][(a c)]X_1) <= (sub <[c](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[c][]X_1,[]Y_1>)) >,
     c#Y_1,b#X_1,a#X_1 |- < (lam [c][(a b)]X_1) <= (sub <[b](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[b][]X_1,[]Y_1>)) >,
     b#Y_1,c#X_1,a#X_1 |- < (lam [b][(a c)]X_1) <= (sub <[c](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[c][]X_1,[]Y_1>)) >,
     d#Y_1,c#X_1,a#X_1 |- < (lam [d][(a c)]X_1) <= (sub <[c](lam [d][]X_1),[]Y_1>) => (lam [d](sub <[c][]X_1,[]Y_1>)) > }
(4 on 3(out)): 
   { a#X,b#Y_1 |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[a](lam [b][]X),[]Y_1>) => (lam [b][]X) >,
     a#X,b#Y_1 |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[b](lam [a][(a b)]X),[]Y_1>) => (lam [a][(a b)]X) >,
     c#X,b#Y_1,a#X |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[c](lam [b][(a c)]X),[]Y_1>) => (lam [b][(a c)]X) > }
(4 on 4(out)): 
   { b#Y_1 |- < (lam [b](sub <[a][]X_1,[]Y_1>)) <= (sub <[a](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[a][]X_1,[]Y_1>)) >,
     b#X_1,b#Y_1,c#Y_1 |- < (lam [b](sub <[a][(b c)]X_1,[]Y_1>)) <= (sub <[a](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[a][]X_1,[]Y_1>)) >,
     a#Y_1,b#Y_1 |- < (lam [b](sub <[a][(a b)]X_1,[]Y_1>)) <= (sub <[b](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[b][]X_1,[]Y_1>)) >,
     a#X_1,b#Y_1 |- < (lam [b](sub <[a][(a c)]X_1,[]Y_1>)) <= (sub <[c](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[c][]X_1,[]Y_1>)) >,
     b#Y_1,a#Y_1,b#X_1 |- < (lam [b](sub <[a][(c a)(a b)]X_1,[]Y_1>)) <= (sub <[c](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[c][]X_1,[]Y_1>)) >,
     a#X_1,c#Y_1,b#Y_1 |- < (lam [b](sub <[a][(b a)(a c)]X_1,[]Y_1>)) <= (sub <[b](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[b][]X_1,[]Y_1>)) >,
     a#X_1,b#Y_1,d#Y_1,b#X_1 |- < (lam [b](sub <[a][(b d)(a c)]X_1,[]Y_1>)) <= (sub <[c](lam [d][]X_1),[]Y_1>) => (lam [d](sub <[c][]X_1,[]Y_1>)) > }
inBCP:  |- <  (sub <[a](sub <[a][]X,[]Y_1>),[]Z_1>),   (app <(sub <[a](lam [a][]X),[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>)  > is not closed
failed to show all BCPs are parallel closed
result: MAYBE
time: 18 msec.