YES
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)))}
 DP:
  Strict:
   {             plus#(s(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)),
                 plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z),
    plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, 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#(X2, X4)}
  Weak:
  {             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)))}
  EDG:
   {(plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X2, X4))
    (plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)))
    (plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))))
    (plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z), plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z))
    (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#(X1, plus(X3, plus(X2, X4))), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X2, X4))
    (plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, 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))), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))))
    (plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z))
    (plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), 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(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)))
    (plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s(X), plus(Y, Z)) -> 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#(X1, plus(X3, plus(X2, X4))))
    (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#(X2, X4), 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(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(X), plus(Y, Z)) -> 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))))
    (plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X3, 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#(X3, plus(X2, X4)), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X2, X4))
    (plus#(s(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)), plus#(s(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)))
    (plus#(s(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)), 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#(X1, plus(X3, plus(X2, X4))))
    (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(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X2, X4))}
   SCCS:
    Scc:
     {             plus#(s(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)),
                   plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z),
      plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, 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#(X2, X4)}
    SCC:
     Strict:
      {             plus#(s(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)),
                    plus#(s(X), plus(Y, Z)) -> plus#(s(s(Y)), Z),
       plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, 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#(X2, X4)}
     Weak:
     {             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)))}
     POLY:
      Argument Filtering:
       pi(s) = [], pi(plus#) = [1], pi(plus) = [1]
      Usable Rules:
       {}
      Interpretation:
       [plus#](x0) = x0 + 1,
       [plus](x0) = x0 + 1
      Strict:
       {             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)))}
      Weak:
       {             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)))}
      EDG:
       {(plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))))
        (plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)))
        (plus#(s(X), plus(Y, Z)) -> plus#(X, plus(s(s(Y)), Z)), plus#(s(X), plus(Y, Z)) -> plus#(X, 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#(X1, plus(X3, plus(X2, X4))))}
       SCCS:
        Scc:
         {             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)))}
        SCC:
         Strict:
          {             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)))}
         Weak:
         {             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)))}
         SPSC:
          Simple Projection:
           pi(plus#) = 0
          Strict:
           {plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))}
          EDG:
           {(plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))))}
           SCCS:
            Scc:
             {plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))}
            SCC:
             Strict:
              {plus#(s(X1), plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))}
             Weak:
             {             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)))}
             SPSC:
              Simple Projection:
               pi(plus#) = 0
              Strict:
               {}
              Qed