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)))
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [plus#](x0, x1) = x1 + 0,
    
    [plus](x0, x1) = 1x1 + 0,
    
    [s](x0) = x0 + 3
   orientation:
    plus#(s(X),plus(Y,Z)) = 1Z + 0 >= Z + 0 = plus#(s(s(Y)),Z)
    
    plus#(s(X),plus(Y,Z)) = 1Z + 0 >= 1Z + 0 = plus#(X,plus(s(s(Y)),Z))
    
    plus#(s(X1),plus(X2,plus(X3,X4))) = 2X4 + 1 >= X4 + 0 = plus#(X2,X4)
    
    plus#(s(X1),plus(X2,plus(X3,X4))) = 2X4 + 1 >= 1X4 + 0 = plus#(X3,plus(X2,X4))
    
    plus#(s(X1),plus(X2,plus(X3,X4))) = 2X4 + 1 >= 2X4 + 1 = plus#(X1,plus(X3,plus(X2,X4)))
    
    plus(s(X),plus(Y,Z)) = 2Z + 1 >= 2Z + 1 = plus(X,plus(s(s(Y)),Z))
    
    plus(s(X1),plus(X2,plus(X3,X4))) = 3X4 + 2 >= 3X4 + 2 = plus(X1,plus(X3,plus(X2,X4)))
   problem:
    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#(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]
    weight function:
     w0 = 1
     w(plus#) = w(plus) = 1
     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