YES

Problem:
 plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
 plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))

Proof:
 DP Processor:
  DPs:
   plus#(s(X),plus(Y,Z)) -> plus#(s(s(Y)),Z)
   plus#(s(X),plus(Y,Z)) -> plus#(X,plus(s(s(Y)),Z))
   plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X2,X4)
   plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X3,plus(X2,X4))
   plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X1,plus(X3,plus(X2,X4)))
  TRS:
   plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
   plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))
  KBO Processor:
   argument filtering:
    pi(s) = [0]
    pi(plus) = [0,1]
    pi(plus#) = [0,1]
   usable rules:
    plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
    plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))
   weight function:
    w0 = 1
    w(plus#) = 1
    w(plus) = w(s) = 0
   precedence:
    plus# ~ plus ~ s
   problem:
    DPs:
     
    TRS:
     plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
     plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))
   Qed