YES
Time: 0.009803
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:
  DP:
   {             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)}
  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)))}
  EDG:
   {(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#(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#(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#(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))), 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#(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#(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 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#(X2, X4))}
   SCCS (1):
    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 (5):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [plus](x0, x1) = x0 + 1,
       
       [s](x0) = 0,
       
       [plus#](x0, x1) = x0
      Strict:
       plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)
       2 + 0X1 + 0X3 + 0X2 + 1X4 >= 0 + 0X2 + 1X4
       plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))
       2 + 0X1 + 0X3 + 0X2 + 1X4 >= 1 + 0X3 + 0X2 + 1X4
       plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))
       2 + 0X1 + 0X3 + 0X2 + 1X4 >= 2 + 0X1 + 0X3 + 0X2 + 1X4
       plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)
       1 + 0X + 0Y + 1Z >= 0 + 0Y + 1Z
       plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))
       1 + 0X + 0Y + 1Z >= 1 + 0X + 0Y + 1Z
      Weak:
       
     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 (1):
       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 (2):
        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 (1):
           Scc:
            {plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))}
           SCC (1):
            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