MAYBE
Time: 0.001510
TRS:
 {  activate X -> X,
  and(tt(), X) -> activate X,
  plus(N, 0()) -> N,
  plus(N, s M) -> s plus(N, M),
     x(N, 0()) -> 0(),
     x(N, s M) -> plus(x(N, M), N)}
 DP:
  DP:
   {and#(tt(), X) -> activate# X,
    plus#(N, s M) -> plus#(N, M),
       x#(N, s M) -> plus#(x(N, M), N),
       x#(N, s M) -> x#(N, M)}
  TRS:
  {  activate X -> X,
   and(tt(), X) -> activate X,
   plus(N, 0()) -> N,
   plus(N, s M) -> s plus(N, M),
      x(N, 0()) -> 0(),
      x(N, s M) -> plus(x(N, M), N)}
  EDG:
   {(x#(N, s M) -> plus#(x(N, M), N), plus#(N, s M) -> plus#(N, M))
    (x#(N, s M) -> x#(N, M), x#(N, s M) -> x#(N, M))
    (x#(N, s M) -> x#(N, M), x#(N, s M) -> plus#(x(N, M), N))
    (plus#(N, s M) -> plus#(N, M), plus#(N, s M) -> plus#(N, M))}
   EDG:
    {(x#(N, s M) -> plus#(x(N, M), N), plus#(N, s M) -> plus#(N, M))
     (x#(N, s M) -> x#(N, M), x#(N, s M) -> x#(N, M))
     (x#(N, s M) -> x#(N, M), x#(N, s M) -> plus#(x(N, M), N))
     (plus#(N, s M) -> plus#(N, M), plus#(N, s M) -> plus#(N, M))}
    EDG:
     {(x#(N, s M) -> plus#(x(N, M), N), plus#(N, s M) -> plus#(N, M))
      (x#(N, s M) -> x#(N, M), x#(N, s M) -> x#(N, M))
      (x#(N, s M) -> x#(N, M), x#(N, s M) -> plus#(x(N, M), N))
      (plus#(N, s M) -> plus#(N, M), plus#(N, s M) -> plus#(N, M))}
     EDG:
      {(x#(N, s M) -> plus#(x(N, M), N), plus#(N, s M) -> plus#(N, M))
       (x#(N, s M) -> x#(N, M), x#(N, s M) -> x#(N, M))
       (x#(N, s M) -> x#(N, M), x#(N, s M) -> plus#(x(N, M), N))
       (plus#(N, s M) -> plus#(N, M), plus#(N, s M) -> plus#(N, M))}
      STATUS:
       arrows: 0.750000
       SCCS (2):
        Scc:
         {x#(N, s M) -> x#(N, M)}
        Scc:
         {plus#(N, s M) -> plus#(N, M)}
        
        SCC (1):
         Strict:
          {x#(N, s M) -> x#(N, M)}
         Weak:
         {  activate X -> X,
          and(tt(), X) -> activate X,
          plus(N, 0()) -> N,
          plus(N, s M) -> s plus(N, M),
             x(N, 0()) -> 0(),
             x(N, s M) -> plus(x(N, M), N)}
         Open
        
        SCC (1):
         Strict:
          {plus#(N, s M) -> plus#(N, M)}
         Weak:
         {  activate X -> X,
          and(tt(), X) -> activate X,
          plus(N, 0()) -> N,
          plus(N, s M) -> s plus(N, M),
             x(N, 0()) -> 0(),
             x(N, s M) -> plus(x(N, M), N)}
         Open