MAYBE

Problem:
 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)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   and#(tt(),X) -> activate#(X)
   plus#(N,s(M)) -> plus#(N,M)
   x#(N,s(M)) -> x#(N,M)
   x#(N,s(M)) -> plus#(x(N,M),N)
  TRS:
   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)
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    and#(tt(),X) -> activate#(X)
    plus#(N,s(M)) -> plus#(N,M)
    x#(N,s(M)) -> x#(N,M)
    x#(N,s(M)) -> plus#(x(N,M),N)
   TRS:
    f11(x,y) -> x
    f11(x,y) -> y
    x(N,0()) -> 0()
    x(N,s(M)) -> plus(x(N,M),N)
    plus(N,0()) -> N
    plus(N,s(M)) -> s(plus(N,M))
   CDG Processor:
    DPs:
     and#(tt(),X) -> activate#(X)
     plus#(N,s(M)) -> plus#(N,M)
     x#(N,s(M)) -> x#(N,M)
     x#(N,s(M)) -> plus#(x(N,M),N)
    TRS:
     f11(x,y) -> x
     f11(x,y) -> y
     x(N,0()) -> 0()
     x(N,s(M)) -> plus(x(N,M),N)
     plus(N,0()) -> N
     plus(N,s(M)) -> s(plus(N,M))
    graph:
     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)
     x#(N,s(M)) -> plus#(x(N,M),N) -> plus#(N,s(M)) -> plus#(N,M)
     plus#(N,s(M)) -> plus#(N,M) -> plus#(N,s(M)) -> plus#(N,M)
    Restore Modifier:
     DPs:
      and#(tt(),X) -> activate#(X)
      plus#(N,s(M)) -> plus#(N,M)
      x#(N,s(M)) -> x#(N,M)
      x#(N,s(M)) -> plus#(x(N,M),N)
     TRS:
      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)
      activate(X) -> X
     SCC Processor:
      #sccs: 2
      #rules: 2
      #arcs: 4/16
      DPs:
       x#(N,s(M)) -> x#(N,M)
      TRS:
       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)
       activate(X) -> X
      Open
      
      DPs:
       plus#(N,s(M)) -> plus#(N,M)
      TRS:
       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)
       activate(X) -> X
      Open