MAYBE
ignored inputs:
(COMMENT a system of beta eta reduction for the lambda calculus via orthogonal explicit substitution calculus )

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):  |- (sub <[a]b,[]Y>) -> b,
     (4): b#Y |- (sub <[a](lam [b][]X),[]Y>) -> (lam [b](sub <[a][]X,[]Y>)),
     (5): a#X |- (lam [a](app <[]X,a>)) -> []X ]
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>)>) > }
(0 on 5(in)): 
   {  |- < (lam [a](sub <[a][]X,a>)) <= (lam [a](app <(lam [a][]X),a>)) => (lam [a][]X) >,
     b#X |- < (lam [b](sub <[a][]X,b>)) <= (lam [b](app <(lam [a][]X),b>)) => (lam [a][]X) > }
(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>)>) > }
(2 on 2(out)): 
   {  |- < []X_1 <= (sub <[a]a,[]X_1>) => []X_1 >,
      |- < []X_1 <= (sub <[b]b,[]X_1>) => []X_1 > }
(3 on 3(out)): 
   {  |- < b <= (sub <[a]b,[]Y_1>) => b >,
      |- < b <= (sub <[c]b,[]Y_1>) => b > }
(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>)) > }
(5 on 0(in)): 
   { a#X |- < (app <[]X,[]Y_1>) <= (app <(lam [a](app <[]X,a>)),[]Y_1>) => (sub <[a](app <[]X,a>),[]Y_1>) >,
     b#X,a#X |- < (app <[]X,[]Y_1>) <= (app <(lam [b](app <[(a b)]X,b>)),[]Y_1>) => (sub <[b](app <[(a b)]X,b>),[]Y_1>) > }
(5 on 4(in)): 
   { a#X,a#Y_1 |- < (sub <[b][]X,[]Y_1>) <= (sub <[b](lam [a](app <[]X,a>)),[]Y_1>) => (lam [a](sub <[b](app <[]X,a>),[]Y_1>)) >,
     a#X,a#Y_1 |- < (sub <[c][]X,[]Y_1>) <= (sub <[c](lam [a](app <[]X,a>)),[]Y_1>) => (lam [a](sub <[c](app <[]X,a>),[]Y_1>)) >,
     b#X,b#Y_1,a#X |- < (sub <[a][]X,[]Y_1>) <= (sub <[a](lam [b](app <[(a b)]X,b>)),[]Y_1>) => (lam [b](sub <[a](app <[(a b)]X,b>),[]Y_1>)) >,
     b#X,b#Y_1,a#X |- < (sub <[c][]X,[]Y_1>) <= (sub <[c](lam [b](app <[(a b)]X,b>)),[]Y_1>) => (lam [b](sub <[c](app <[(a b)]X,b>),[]Y_1>)) >,
     c#X,c#Y_1,a#X |- < (sub <[b][]X,[]Y_1>) <= (sub <[b](lam [c](app <[(a c)]X,c>)),[]Y_1>) => (lam [c](sub <[b](app <[(a c)]X,c>),[]Y_1>)) >,
     c#X,c#Y_1,a#X |- < (sub <[a][]X,[]Y_1>) <= (sub <[a](lam [c](app <[(a c)]X,c>)),[]Y_1>) => (lam [c](sub <[a](app <[(a c)]X,c>),[]Y_1>)) >,
     c#X,c#Y_1,a#X |- < (sub <[d][]X,[]Y_1>) <= (sub <[d](lam [c](app <[(a c)]X,c>)),[]Y_1>) => (lam [c](sub <[d](app <[(a c)]X,c>),[]Y_1>)) > }
(5 on 5(out)): 
   { a#X_1 |- < []X_1 <= (lam [a](app <[]X_1,a>)) => []X_1 >,
     b#X_1,a#X_1 |- < [(a b)]X_1 <= (lam [b](app <[]X_1,b>)) => []X_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: 14 msec.