YES
ignored inputs:
(COMMENT an orthogonal explicit substitution calculus for lambda terms )
(COMMENT Example 8 of [ SKAT15 , doi:10.4230/LIPIcs.RTA.2015.301 ] )

NRS:
   [ (0):  |- (sub <[a](app <[]X,[]Y>),[]Z>) -> (app <(sub <[a][]X,[]Z>),(sub <[a][]Y,[]Z>)>),
     (1):  |- (sub <[a]a,[]X>) -> []X,
     (2):  |- (sub <[a]b,[]X>) -> b,
     (3): 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)): 
   {  |- < (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 1(out)): 
   {  |- < []X_1 <= (sub <[a]a,[]X_1>) => []X_1 >,
      |- < []X_1 <= (sub <[b]b,[]X_1>) => []X_1 > }
(2 on 2(out)): 
   {  |- < b <= (sub <[a]b,[]X_1>) => b >,
      |- < b <= (sub <[c]b,[]X_1>) => b > }
(3 on 3(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>)) > }
all BCPs are parallel closed
result: YES
time: 7 msec.