YES

Problem:
 a__and(tt(),X) -> mark(X)
 a__plus(N,0()) -> mark(N)
 a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
 mark(and(X1,X2)) -> a__and(mark(X1),X2)
 mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
 mark(tt()) -> tt()
 mark(0()) -> 0()
 mark(s(X)) -> s(mark(X))
 a__and(X1,X2) -> and(X1,X2)
 a__plus(X1,X2) -> plus(X1,X2)

Proof:
 DP Processor:
  DPs:
   a__and#(tt(),X) -> mark#(X)
   a__plus#(N,0()) -> mark#(N)
   a__plus#(N,s(M)) -> mark#(M)
   a__plus#(N,s(M)) -> mark#(N)
   a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M))
   mark#(and(X1,X2)) -> mark#(X1)
   mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
   mark#(plus(X1,X2)) -> mark#(X2)
   mark#(plus(X1,X2)) -> mark#(X1)
   mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
   mark#(s(X)) -> mark#(X)
  TRS:
   a__and(tt(),X) -> mark(X)
   a__plus(N,0()) -> mark(N)
   a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
   mark(and(X1,X2)) -> a__and(mark(X1),X2)
   mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
   mark(tt()) -> tt()
   mark(0()) -> 0()
   mark(s(X)) -> s(mark(X))
   a__and(X1,X2) -> and(X1,X2)
   a__plus(X1,X2) -> plus(X1,X2)
  TDG Processor:
   DPs:
    a__and#(tt(),X) -> mark#(X)
    a__plus#(N,0()) -> mark#(N)
    a__plus#(N,s(M)) -> mark#(M)
    a__plus#(N,s(M)) -> mark#(N)
    a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M))
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    mark#(plus(X1,X2)) -> mark#(X2)
    mark#(plus(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X)
   TRS:
    a__and(tt(),X) -> mark(X)
    a__plus(N,0()) -> mark(N)
    a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
    mark(and(X1,X2)) -> a__and(mark(X1),X2)
    mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
    mark(tt()) -> tt()
    mark(0()) -> 0()
    mark(s(X)) -> s(mark(X))
    a__and(X1,X2) -> and(X1,X2)
    a__plus(X1,X2) -> plus(X1,X2)
   graph:
    a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M)) ->
    a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M))
    a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M)) ->
    a__plus#(N,s(M)) -> mark#(N)
    a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M)) ->
    a__plus#(N,s(M)) -> mark#(M)
    a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M)) ->
    a__plus#(N,0()) -> mark#(N)
    a__plus#(N,s(M)) -> mark#(N) -> mark#(s(X)) -> mark#(X)
    a__plus#(N,s(M)) -> mark#(N) ->
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    a__plus#(N,s(M)) -> mark#(N) -> mark#(plus(X1,X2)) -> mark#(X1)
    a__plus#(N,s(M)) -> mark#(N) -> mark#(plus(X1,X2)) -> mark#(X2)
    a__plus#(N,s(M)) -> mark#(N) ->
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    a__plus#(N,s(M)) -> mark#(N) -> mark#(and(X1,X2)) -> mark#(X1)
    a__plus#(N,s(M)) -> mark#(M) -> mark#(s(X)) -> mark#(X)
    a__plus#(N,s(M)) -> mark#(M) ->
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    a__plus#(N,s(M)) -> mark#(M) -> mark#(plus(X1,X2)) -> mark#(X1)
    a__plus#(N,s(M)) -> mark#(M) -> mark#(plus(X1,X2)) -> mark#(X2)
    a__plus#(N,s(M)) -> mark#(M) ->
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    a__plus#(N,s(M)) -> mark#(M) -> mark#(and(X1,X2)) -> mark#(X1)
    a__plus#(N,0()) -> mark#(N) -> mark#(s(X)) -> mark#(X)
    a__plus#(N,0()) -> mark#(N) ->
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    a__plus#(N,0()) -> mark#(N) -> mark#(plus(X1,X2)) -> mark#(X1)
    a__plus#(N,0()) -> mark#(N) -> mark#(plus(X1,X2)) -> mark#(X2)
    a__plus#(N,0()) -> mark#(N) ->
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    a__plus#(N,0()) -> mark#(N) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2)) ->
    a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M))
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2)) ->
    a__plus#(N,s(M)) -> mark#(N)
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2)) ->
    a__plus#(N,s(M)) -> mark#(M)
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2)) ->
    a__plus#(N,0()) -> mark#(N)
    mark#(plus(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(plus(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(plus(X1,X2)) -> mark#(X2)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2) -> a__and#(tt(),X) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) ->
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X) -> mark#(plus(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(plus(X1,X2)) -> mark#(X2)
    mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1)
    a__and#(tt(),X) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__and#(tt(),X) -> mark#(X) ->
    mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
    a__and#(tt(),X) -> mark#(X) -> mark#(plus(X1,X2)) -> mark#(X1)
    a__and#(tt(),X) -> mark#(X) -> mark#(plus(X1,X2)) -> mark#(X2)
    a__and#(tt(),X) -> mark#(X) ->
    mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
    a__and#(tt(),X) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1)
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [a__plus#](x0, x1) = x0 + x1 + 5,
     
     [mark#](x0) = x0,
     
     [a__and#](x0, x1) = x0 + x1 + 6,
     
     [plus](x0, x1) = 5x0 + x1 + 5,
     
     [and](x0, x1) = x0 + x1 + 6,
     
     [s](x0) = x0 + 1,
     
     [a__plus](x0, x1) = 5x0 + x1 + 5,
     
     [0] = 0,
     
     [mark](x0) = x0,
     
     [a__and](x0, x1) = x0 + x1 + 6,
     
     [tt] = 0
    orientation:
     a__and#(tt(),X) = X + 6 >= X = mark#(X)
     
     a__plus#(N,0()) = N + 5 >= N = mark#(N)
     
     a__plus#(N,s(M)) = M + N + 5 >= M = mark#(M)
     
     a__plus#(N,s(M)) = M + N + 5 >= N = mark#(N)
     
     a__plus#(N,s(M)) = M + N + 5 >= M + N + 5 = a__plus#(mark(N),mark(M))
     
     mark#(and(X1,X2)) = X1 + X2 + 6 >= X1 = mark#(X1)
     
     mark#(and(X1,X2)) = X1 + X2 + 6 >= X1 + X2 + 6 = a__and#(mark(X1),X2)
     
     mark#(plus(X1,X2)) = 5X1 + X2 + 5 >= X2 = mark#(X2)
     
     mark#(plus(X1,X2)) = 5X1 + X2 + 5 >= X1 = mark#(X1)
     
     mark#(plus(X1,X2)) = 5X1 + X2 + 5 >= X1 + X2 + 5 = a__plus#(mark(X1),mark(X2))
     
     mark#(s(X)) = X + 1 >= X = mark#(X)
     
     a__and(tt(),X) = X + 6 >= X = mark(X)
     
     a__plus(N,0()) = 5N + 5 >= N = mark(N)
     
     a__plus(N,s(M)) = M + 5N + 5 >= M + 5N + 5 = s(a__plus(mark(N),mark(M)))
     
     mark(and(X1,X2)) = X1 + X2 + 6 >= X1 + X2 + 6 = a__and(mark(X1),X2)
     
     mark(plus(X1,X2)) = 5X1 + X2 + 5 >= 5X1 + X2 + 5 = a__plus(mark(X1),mark(X2))
     
     mark(tt()) = 0 >= 0 = tt()
     
     mark(0()) = 0 >= 0 = 0()
     
     mark(s(X)) = X + 1 >= X + 1 = s(mark(X))
     
     a__and(X1,X2) = X1 + X2 + 6 >= X1 + X2 + 6 = and(X1,X2)
     
     a__plus(X1,X2) = 5X1 + X2 + 5 >= 5X1 + X2 + 5 = plus(X1,X2)
    problem:
     DPs:
      a__and#(tt(),X) -> mark#(X)
      a__plus#(N,0()) -> mark#(N)
      a__plus#(N,s(M)) -> mark#(M)
      a__plus#(N,s(M)) -> mark#(N)
      a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M))
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
      mark#(plus(X1,X2)) -> mark#(X2)
      mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
      mark#(s(X)) -> mark#(X)
     TRS:
      a__and(tt(),X) -> mark(X)
      a__plus(N,0()) -> mark(N)
      a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
      mark(and(X1,X2)) -> a__and(mark(X1),X2)
      mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
      mark(tt()) -> tt()
      mark(0()) -> 0()
      mark(s(X)) -> s(mark(X))
      a__and(X1,X2) -> and(X1,X2)
      a__plus(X1,X2) -> plus(X1,X2)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [a__plus#](x0, x1) = x0 + 1x1 + 0,
      
      [mark#](x0) = x0,
      
      [a__and#](x0, x1) = x0 + 1x1 + 0,
      
      [plus](x0, x1) = 3x0 + 2x1 + 6,
      
      [and](x0, x1) = x0 + 7x1 + 4,
      
      [s](x0) = x0 + 4,
      
      [a__plus](x0, x1) = 3x0 + 2x1 + 6,
      
      [0] = 0,
      
      [mark](x0) = x0 + 3,
      
      [a__and](x0, x1) = x0 + 7x1 + 4,
      
      [tt] = 4
     orientation:
      a__and#(tt(),X) = 1X + 4 >= X = mark#(X)
      
      a__plus#(N,0()) = N + 1 >= N = mark#(N)
      
      a__plus#(N,s(M)) = 1M + N + 5 >= M = mark#(M)
      
      a__plus#(N,s(M)) = 1M + N + 5 >= N = mark#(N)
      
      a__plus#(N,s(M)) = 1M + N + 5 >= 1M + N + 4 = a__plus#(mark(N),mark(M))
      
      mark#(and(X1,X2)) = X1 + 7X2 + 4 >= X1 = mark#(X1)
      
      mark#(and(X1,X2)) = X1 + 7X2 + 4 >= X1 + 1X2 + 3 = a__and#(mark(X1),X2)
      
      mark#(plus(X1,X2)) = 3X1 + 2X2 + 6 >= X2 = mark#(X2)
      
      mark#(plus(X1,X2)) = 3X1 + 2X2 + 6 >= X1 + 1X2 + 4 = a__plus#(mark(X1),mark(X2))
      
      mark#(s(X)) = X + 4 >= X = mark#(X)
      
      a__and(tt(),X) = 7X + 4 >= X + 3 = mark(X)
      
      a__plus(N,0()) = 3N + 6 >= N + 3 = mark(N)
      
      a__plus(N,s(M)) = 2M + 3N + 6 >= 2M + 3N + 6 = s(a__plus(mark(N),mark(M)))
      
      mark(and(X1,X2)) = X1 + 7X2 + 4 >= X1 + 7X2 + 4 = a__and(mark(X1),X2)
      
      mark(plus(X1,X2)) = 3X1 + 2X2 + 6 >= 3X1 + 2X2 + 6 = a__plus(mark(X1),mark(X2))
      
      mark(tt()) = 4 >= 4 = tt()
      
      mark(0()) = 3 >= 0 = 0()
      
      mark(s(X)) = X + 4 >= X + 4 = s(mark(X))
      
      a__and(X1,X2) = X1 + 7X2 + 4 >= X1 + 7X2 + 4 = and(X1,X2)
      
      a__plus(X1,X2) = 3X1 + 2X2 + 6 >= 3X1 + 2X2 + 6 = plus(X1,X2)
     problem:
      DPs:
       a__plus#(N,0()) -> mark#(N)
       a__plus#(N,s(M)) -> mark#(N)
       a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M))
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
       mark#(s(X)) -> mark#(X)
      TRS:
       a__and(tt(),X) -> mark(X)
       a__plus(N,0()) -> mark(N)
       a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
       mark(and(X1,X2)) -> a__and(mark(X1),X2)
       mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
       mark(tt()) -> tt()
       mark(0()) -> 0()
       mark(s(X)) -> s(mark(X))
       a__and(X1,X2) -> and(X1,X2)
       a__plus(X1,X2) -> plus(X1,X2)
     SCC Processor:
      #sccs: 2
      #rules: 3
      #arcs: 57/36
      DPs:
       a__plus#(N,s(M)) -> a__plus#(mark(N),mark(M))
      TRS:
       a__and(tt(),X) -> mark(X)
       a__plus(N,0()) -> mark(N)
       a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
       mark(and(X1,X2)) -> a__and(mark(X1),X2)
       mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
       mark(tt()) -> tt()
       mark(0()) -> 0()
       mark(s(X)) -> s(mark(X))
       a__and(X1,X2) -> and(X1,X2)
       a__plus(X1,X2) -> plus(X1,X2)
      KBO Processor:
       argument filtering:
        pi(tt) = []
        pi(a__and) = [1]
        pi(mark) = [0]
        pi(0) = []
        pi(a__plus) = [0,1]
        pi(s) = [0]
        pi(and) = [1]
        pi(plus) = [0,1]
        pi(a__plus#) = 1
       weight function:
        w0 = 1
        w(a__plus#) = w(plus) = w(and) = w(s) = w(a__plus) = w(0) = w(
        a__and) = w(tt) = 1
        w(mark) = 0
       precedence:
        mark > a__plus ~ a__and > a__plus# ~ plus ~ and ~ s ~ 0 ~ tt
       problem:
        DPs:
         
        TRS:
         a__and(tt(),X) -> mark(X)
         a__plus(N,0()) -> mark(N)
         a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
         mark(and(X1,X2)) -> a__and(mark(X1),X2)
         mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
         mark(tt()) -> tt()
         mark(0()) -> 0()
         mark(s(X)) -> s(mark(X))
         a__and(X1,X2) -> and(X1,X2)
         a__plus(X1,X2) -> plus(X1,X2)
       Qed
      
      DPs:
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(s(X)) -> mark#(X)
      TRS:
       a__and(tt(),X) -> mark(X)
       a__plus(N,0()) -> mark(N)
       a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
       mark(and(X1,X2)) -> a__and(mark(X1),X2)
       mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
       mark(tt()) -> tt()
       mark(0()) -> 0()
       mark(s(X)) -> s(mark(X))
       a__and(X1,X2) -> and(X1,X2)
       a__plus(X1,X2) -> plus(X1,X2)
      Subterm Criterion Processor:
       simple projection:
        pi(mark#) = 0
       problem:
        DPs:
         
        TRS:
         a__and(tt(),X) -> mark(X)
         a__plus(N,0()) -> mark(N)
         a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
         mark(and(X1,X2)) -> a__and(mark(X1),X2)
         mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
         mark(tt()) -> tt()
         mark(0()) -> 0()
         mark(s(X)) -> s(mark(X))
         a__and(X1,X2) -> and(X1,X2)
         a__plus(X1,X2) -> plus(X1,X2)
       Qed