YES
Time: 0.002355
TRS:
 {U12(tt(), M, N) -> s plus(activate N, activate M),
       activate X -> X,
  U11(tt(), M, N) -> U12(tt(), activate M, activate N),
     plus(N, s M) -> U11(tt(), M, N),
     plus(N, 0()) -> N}
 DP:
  DP:
   {U12#(tt(), M, N) -> activate# M,
    U12#(tt(), M, N) -> activate# N,
    U12#(tt(), M, N) -> plus#(activate N, activate M),
    U11#(tt(), M, N) -> U12#(tt(), activate M, activate N),
    U11#(tt(), M, N) -> activate# M,
    U11#(tt(), M, N) -> activate# N,
       plus#(N, s M) -> U11#(tt(), M, N)}
  TRS:
  {U12(tt(), M, N) -> s plus(activate N, activate M),
        activate X -> X,
   U11(tt(), M, N) -> U12(tt(), activate M, activate N),
      plus(N, s M) -> U11(tt(), M, N),
      plus(N, 0()) -> N}
  EDG:
   {(plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> activate# N)
    (plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> activate# M)
    (plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> U12#(tt(), activate M, activate N))
    (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> activate# M)
    (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> activate# N)
    (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> plus#(activate N, activate M))
    (U12#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> U11#(tt(), M, N))}
   EDG:
    {(plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> activate# N)
     (plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> activate# M)
     (plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> U12#(tt(), activate M, activate N))
     (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> activate# M)
     (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> activate# N)
     (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> plus#(activate N, activate M))}
    EDG:
     {(plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> activate# N)
      (plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> activate# M)
      (plus#(N, s M) -> U11#(tt(), M, N), U11#(tt(), M, N) -> U12#(tt(), activate M, activate N))
      (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> activate# M)
      (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> activate# N)
      (U11#(tt(), M, N) -> U12#(tt(), activate M, activate N), U12#(tt(), M, N) -> plus#(activate N, activate M))}
     STATUS:
      arrows: 0.877551
      SCCS (0):