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)))
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [plus#](x0, x1) = x1,
    
    [plus](x0, x1) = x0 + x1 + 1,
    
    [s](x0) = x0
   orientation:
    plus#(s(X),plus(Y,Z)) = Y + Z + 1 >= Z = plus#(s(s(Y)),Z)
    
    plus#(s(X),plus(Y,Z)) = Y + Z + 1 >= Y + Z + 1 = plus#(X,plus(s(s(Y)),Z))
    
    plus#(s(X1),plus(X2,plus(X3,X4))) = X2 + X3 + X4 + 2 >= X4 = plus#(X2,X4)
    
    plus#(s(X1),plus(X2,plus(X3,X4))) = X2 + X3 + X4 + 2 >= X2 + X4 + 1 = plus#(X3,plus(X2,X4))
    
    plus#(s(X1),plus(X2,plus(X3,X4))) = X2 + X3 + X4 + 2 >= X2 + X3 + X4 + 2 = plus#(X1,plus(X3,plus(X2,X4)))
    
    plus(s(X),plus(Y,Z)) = X + Y + Z + 2 >= X + Y + Z + 2 = plus(X,plus(s(s(Y)),Z))
    
    plus(s(X1),plus(X2,plus(X3,X4))) = X1 + X2 + X3 + X4 + 3 >= X1 + X2 + X3 + X4 + 3 = plus(X1,plus(X3,plus(X2,X4)))
   problem:
    DPs:
     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)))
    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)))
   Subterm Criterion Processor:
    simple projection:
     pi(plus#) = 0
    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