YES

Problem:
 acka(y(),n) -> s(n)
 acka(a(m),y()) -> acka(m,s(0()))
 acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
 ackb(z(),n) -> s(n)
 ackb(b(m),z()) -> ackb(m,s(0()))
 ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
 s(n) -> a(n)
 s(n) -> b(n)
 0() -> y()
 0() -> z()

Proof:
 DP Processor:
  DPs:
   acka#(y(),n) -> s#(n)
   acka#(a(m),y()) -> 0#()
   acka#(a(m),y()) -> s#(0())
   acka#(a(m),y()) -> acka#(m,s(0()))
   acka#(a(m),a(n)) -> s#(m)
   acka#(a(m),a(n)) -> ackb#(s(m),n)
   acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
   ackb#(z(),n) -> s#(n)
   ackb#(b(m),z()) -> 0#()
   ackb#(b(m),z()) -> s#(0())
   ackb#(b(m),z()) -> ackb#(m,s(0()))
   ackb#(b(m),b(n)) -> s#(m)
   ackb#(b(m),b(n)) -> ackb#(s(m),n)
   ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
  TRS:
   acka(y(),n) -> s(n)
   acka(a(m),y()) -> acka(m,s(0()))
   acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
   ackb(z(),n) -> s(n)
   ackb(b(m),z()) -> ackb(m,s(0()))
   ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
   s(n) -> a(n)
   s(n) -> b(n)
   0() -> y()
   0() -> z()
  TDG Processor:
   DPs:
    acka#(y(),n) -> s#(n)
    acka#(a(m),y()) -> 0#()
    acka#(a(m),y()) -> s#(0())
    acka#(a(m),y()) -> acka#(m,s(0()))
    acka#(a(m),a(n)) -> s#(m)
    acka#(a(m),a(n)) -> ackb#(s(m),n)
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
    ackb#(z(),n) -> s#(n)
    ackb#(b(m),z()) -> 0#()
    ackb#(b(m),z()) -> s#(0())
    ackb#(b(m),z()) -> ackb#(m,s(0()))
    ackb#(b(m),b(n)) -> s#(m)
    ackb#(b(m),b(n)) -> ackb#(s(m),n)
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
   TRS:
    acka(y(),n) -> s(n)
    acka(a(m),y()) -> acka(m,s(0()))
    acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
    ackb(z(),n) -> s(n)
    ackb(b(m),z()) -> ackb(m,s(0()))
    ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
    s(n) -> a(n)
    s(n) -> b(n)
    0() -> y()
    0() -> z()
   graph:
    ackb#(b(m),b(n)) -> ackb#(s(m),n) ->
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
    ackb#(b(m),b(n)) -> ackb#(s(m),n) ->
    ackb#(b(m),b(n)) -> ackb#(s(m),n)
    ackb#(b(m),b(n)) -> ackb#(s(m),n) -> ackb#(b(m),b(n)) -> s#(m)
    ackb#(b(m),b(n)) -> ackb#(s(m),n) ->
    ackb#(b(m),z()) -> ackb#(m,s(0()))
    ackb#(b(m),b(n)) -> ackb#(s(m),n) ->
    ackb#(b(m),z()) -> s#(0())
    ackb#(b(m),b(n)) -> ackb#(s(m),n) -> ackb#(b(m),z()) -> 0#()
    ackb#(b(m),b(n)) -> ackb#(s(m),n) ->
    ackb#(z(),n) -> s#(n)
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),a(n)) -> ackb#(s(m),n)
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),a(n)) -> s#(m)
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),y()) -> acka#(m,s(0()))
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),y()) -> s#(0())
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),y()) -> 0#()
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(y(),n) -> s#(n)
    ackb#(b(m),z()) -> ackb#(m,s(0())) ->
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
    ackb#(b(m),z()) -> ackb#(m,s(0())) ->
    ackb#(b(m),b(n)) -> ackb#(s(m),n)
    ackb#(b(m),z()) -> ackb#(m,s(0())) ->
    ackb#(b(m),b(n)) -> s#(m)
    ackb#(b(m),z()) -> ackb#(m,s(0())) ->
    ackb#(b(m),z()) -> ackb#(m,s(0()))
    ackb#(b(m),z()) -> ackb#(m,s(0())) ->
    ackb#(b(m),z()) -> s#(0())
    ackb#(b(m),z()) -> ackb#(m,s(0())) -> ackb#(b(m),z()) -> 0#()
    ackb#(b(m),z()) -> ackb#(m,s(0())) -> ackb#(z(),n) -> s#(n)
    acka#(a(m),a(n)) -> ackb#(s(m),n) ->
    ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
    acka#(a(m),a(n)) -> ackb#(s(m),n) ->
    ackb#(b(m),b(n)) -> ackb#(s(m),n)
    acka#(a(m),a(n)) -> ackb#(s(m),n) -> ackb#(b(m),b(n)) -> s#(m)
    acka#(a(m),a(n)) -> ackb#(s(m),n) ->
    ackb#(b(m),z()) -> ackb#(m,s(0()))
    acka#(a(m),a(n)) -> ackb#(s(m),n) ->
    ackb#(b(m),z()) -> s#(0())
    acka#(a(m),a(n)) -> ackb#(s(m),n) -> ackb#(b(m),z()) -> 0#()
    acka#(a(m),a(n)) -> ackb#(s(m),n) ->
    ackb#(z(),n) -> s#(n)
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),a(n)) -> ackb#(s(m),n)
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),a(n)) -> s#(m)
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),y()) -> acka#(m,s(0()))
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),y()) -> s#(0())
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(a(m),y()) -> 0#()
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
    acka#(y(),n) -> s#(n)
    acka#(a(m),y()) -> acka#(m,s(0())) ->
    acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
    acka#(a(m),y()) -> acka#(m,s(0())) ->
    acka#(a(m),a(n)) -> ackb#(s(m),n)
    acka#(a(m),y()) -> acka#(m,s(0())) ->
    acka#(a(m),a(n)) -> s#(m)
    acka#(a(m),y()) -> acka#(m,s(0())) ->
    acka#(a(m),y()) -> acka#(m,s(0()))
    acka#(a(m),y()) -> acka#(m,s(0())) ->
    acka#(a(m),y()) -> s#(0())
    acka#(a(m),y()) -> acka#(m,s(0())) -> acka#(a(m),y()) -> 0#()
    acka#(a(m),y()) -> acka#(m,s(0())) -> acka#(y(),n) -> s#(n)
   SCC Processor:
    #sccs: 1
    #rules: 6
    #arcs: 42/196
    DPs:
     ackb#(b(m),b(n)) -> ackb#(s(m),n)
     ackb#(b(m),z()) -> ackb#(m,s(0()))
     ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
     acka#(a(m),y()) -> acka#(m,s(0()))
     acka#(a(m),a(n)) -> ackb#(s(m),n)
     acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
    TRS:
     acka(y(),n) -> s(n)
     acka(a(m),y()) -> acka(m,s(0()))
     acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
     ackb(z(),n) -> s(n)
     ackb(b(m),z()) -> ackb(m,s(0()))
     ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
     s(n) -> a(n)
     s(n) -> b(n)
     0() -> y()
     0() -> z()
    CDG Processor:
     DPs:
      ackb#(b(m),b(n)) -> ackb#(s(m),n)
      ackb#(b(m),z()) -> ackb#(m,s(0()))
      ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
      acka#(a(m),y()) -> acka#(m,s(0()))
      acka#(a(m),a(n)) -> ackb#(s(m),n)
      acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
     TRS:
      acka(y(),n) -> s(n)
      acka(a(m),y()) -> acka(m,s(0()))
      acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
      ackb(z(),n) -> s(n)
      ackb(b(m),z()) -> ackb(m,s(0()))
      ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
      s(n) -> a(n)
      s(n) -> b(n)
      0() -> y()
      0() -> z()
     graph:
      ackb#(b(m),b(n)) -> ackb#(s(m),n) ->
      ackb#(b(m),z()) -> ackb#(m,s(0()))
      ackb#(b(m),b(n)) -> ackb#(s(m),n) ->
      ackb#(b(m),b(n)) -> ackb#(s(m),n)
      ackb#(b(m),b(n)) -> ackb#(s(m),n) ->
      ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
      ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
      acka#(a(m),a(n)) -> ackb#(s(m),n)
      ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n)) ->
      acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
      ackb#(b(m),z()) -> ackb#(m,s(0())) ->
      ackb#(b(m),b(n)) -> ackb#(s(m),n)
      ackb#(b(m),z()) -> ackb#(m,s(0())) ->
      ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
      acka#(a(m),a(n)) -> ackb#(s(m),n) ->
      ackb#(b(m),z()) -> ackb#(m,s(0()))
      acka#(a(m),a(n)) -> ackb#(s(m),n) ->
      ackb#(b(m),b(n)) -> ackb#(s(m),n)
      acka#(a(m),a(n)) -> ackb#(s(m),n) ->
      ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
      acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
      acka#(a(m),a(n)) -> ackb#(s(m),n)
      acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n)) ->
      acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
      acka#(a(m),y()) -> acka#(m,s(0())) ->
      acka#(a(m),a(n)) -> ackb#(s(m),n)
      acka#(a(m),y()) -> acka#(m,s(0())) -> acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
     SCC Processor:
      #sccs: 1
      #rules: 5
      #arcs: 14/36
      DPs:
       ackb#(b(m),b(n)) -> ackb#(s(m),n)
       ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
       acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
       acka#(a(m),a(n)) -> ackb#(s(m),n)
       ackb#(b(m),z()) -> ackb#(m,s(0()))
      TRS:
       acka(y(),n) -> s(n)
       acka(a(m),y()) -> acka(m,s(0()))
       acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
       ackb(z(),n) -> s(n)
       ackb(b(m),z()) -> ackb(m,s(0()))
       ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
       s(n) -> a(n)
       s(n) -> b(n)
       0() -> y()
       0() -> z()
      Arctic Interpretation Processor:
       dimension: 1
       usable rules:
        s(n) -> a(n)
        s(n) -> b(n)
       interpretation:
        [ackb#](x0, x1) = x0,
        
        [acka#](x0, x1) = x0 + 0,
        
        [b](x0) = 1x0 + 0,
        
        [z] = 0,
        
        [ackb](x0, x1) = 6x0 + x1 + 0,
        
        [0] = 6,
        
        [a](x0) = 1x0 + 0,
        
        [s](x0) = 1x0 + 0,
        
        [acka](x0, x1) = x0,
        
        [y] = 2
       orientation:
        ackb#(b(m),b(n)) = 1m + 0 >= 1m + 0 = ackb#(s(m),n)
        
        ackb#(b(m),b(n)) = 1m + 0 >= m + 0 = acka#(m,ackb(s(m),n))
        
        acka#(a(m),a(n)) = 1m + 0 >= m + 0 = acka#(m,ackb(s(m),n))
        
        acka#(a(m),a(n)) = 1m + 0 >= 1m + 0 = ackb#(s(m),n)
        
        ackb#(b(m),z()) = 1m + 0 >= m = ackb#(m,s(0()))
        
        acka(y(),n) = 2 >= 1n + 0 = s(n)
        
        acka(a(m),y()) = 1m + 0 >= m = acka(m,s(0()))
        
        acka(a(m),a(n)) = 1m + 0 >= m = acka(m,ackb(s(m),n))
        
        ackb(z(),n) = n + 6 >= 1n + 0 = s(n)
        
        ackb(b(m),z()) = 7m + 6 >= 6m + 7 = ackb(m,s(0()))
        
        ackb(b(m),b(n)) = 7m + 1n + 6 >= m = acka(m,ackb(s(m),n))
        
        s(n) = 1n + 0 >= 1n + 0 = a(n)
        
        s(n) = 1n + 0 >= 1n + 0 = b(n)
        
        0() = 6 >= 2 = y()
        
        0() = 6 >= 0 = z()
       problem:
        DPs:
         ackb#(b(m),b(n)) -> ackb#(s(m),n)
         ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
         acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
         acka#(a(m),a(n)) -> ackb#(s(m),n)
        TRS:
         acka(y(),n) -> s(n)
         acka(a(m),y()) -> acka(m,s(0()))
         acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
         ackb(z(),n) -> s(n)
         ackb(b(m),z()) -> ackb(m,s(0()))
         ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
         s(n) -> a(n)
         s(n) -> b(n)
         0() -> y()
         0() -> z()
       Restore Modifier:
        DPs:
         ackb#(b(m),b(n)) -> ackb#(s(m),n)
         ackb#(b(m),b(n)) -> acka#(m,ackb(s(m),n))
         acka#(a(m),a(n)) -> acka#(m,ackb(s(m),n))
         acka#(a(m),a(n)) -> ackb#(s(m),n)
        TRS:
         acka(y(),n) -> s(n)
         acka(a(m),y()) -> acka(m,s(0()))
         acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
         ackb(z(),n) -> s(n)
         ackb(b(m),z()) -> ackb(m,s(0()))
         ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
         s(n) -> a(n)
         s(n) -> b(n)
         0() -> y()
         0() -> z()
        Arctic Interpretation Processor:
         dimension: 1
         usable rules:
          s(n) -> a(n)
          s(n) -> b(n)
         interpretation:
          [ackb#](x0, x1) = x0 + 0,
          
          [acka#](x0, x1) = x0,
          
          [b](x0) = 1x0 + 4,
          
          [z] = 3,
          
          [ackb](x0, x1) = x1 + 0,
          
          [0] = 4,
          
          [a](x0) = 1x0 + 4,
          
          [s](x0) = 1x0 + 4,
          
          [acka](x0, x1) = 0,
          
          [y] = 5
         orientation:
          ackb#(b(m),b(n)) = 1m + 4 >= 1m + 4 = ackb#(s(m),n)
          
          ackb#(b(m),b(n)) = 1m + 4 >= m = acka#(m,ackb(s(m),n))
          
          acka#(a(m),a(n)) = 1m + 4 >= m = acka#(m,ackb(s(m),n))
          
          acka#(a(m),a(n)) = 1m + 4 >= 1m + 4 = ackb#(s(m),n)
          
          acka(y(),n) = 0 >= 1n + 4 = s(n)
          
          acka(a(m),y()) = 0 >= 0 = acka(m,s(0()))
          
          acka(a(m),a(n)) = 0 >= 0 = acka(m,ackb(s(m),n))
          
          ackb(z(),n) = n + 0 >= 1n + 4 = s(n)
          
          ackb(b(m),z()) = 3 >= 5 = ackb(m,s(0()))
          
          ackb(b(m),b(n)) = 1n + 4 >= 0 = acka(m,ackb(s(m),n))
          
          s(n) = 1n + 4 >= 1n + 4 = a(n)
          
          s(n) = 1n + 4 >= 1n + 4 = b(n)
          
          0() = 4 >= 5 = y()
          
          0() = 4 >= 3 = z()
         problem:
          DPs:
           ackb#(b(m),b(n)) -> ackb#(s(m),n)
           acka#(a(m),a(n)) -> ackb#(s(m),n)
          TRS:
           acka(y(),n) -> s(n)
           acka(a(m),y()) -> acka(m,s(0()))
           acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
           ackb(z(),n) -> s(n)
           ackb(b(m),z()) -> ackb(m,s(0()))
           ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
           s(n) -> a(n)
           s(n) -> b(n)
           0() -> y()
           0() -> z()
         Restore Modifier:
          DPs:
           ackb#(b(m),b(n)) -> ackb#(s(m),n)
           acka#(a(m),a(n)) -> ackb#(s(m),n)
          TRS:
           acka(y(),n) -> s(n)
           acka(a(m),y()) -> acka(m,s(0()))
           acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
           ackb(z(),n) -> s(n)
           ackb(b(m),z()) -> ackb(m,s(0()))
           ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
           s(n) -> a(n)
           s(n) -> b(n)
           0() -> y()
           0() -> z()
          SCC Processor:
           #sccs: 1
           #rules: 1
           #arcs: 12/4
           DPs:
            ackb#(b(m),b(n)) -> ackb#(s(m),n)
           TRS:
            acka(y(),n) -> s(n)
            acka(a(m),y()) -> acka(m,s(0()))
            acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
            ackb(z(),n) -> s(n)
            ackb(b(m),z()) -> ackb(m,s(0()))
            ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
            s(n) -> a(n)
            s(n) -> b(n)
            0() -> y()
            0() -> z()
           Subterm Criterion Processor:
            simple projection:
             pi(ackb#) = 1
            problem:
             DPs:
              
             TRS:
              acka(y(),n) -> s(n)
              acka(a(m),y()) -> acka(m,s(0()))
              acka(a(m),a(n)) -> acka(m,ackb(s(m),n))
              ackb(z(),n) -> s(n)
              ackb(b(m),z()) -> ackb(m,s(0()))
              ackb(b(m),b(n)) -> acka(m,ackb(s(m),n))
              s(n) -> a(n)
              s(n) -> b(n)
              0() -> y()
              0() -> z()
            Qed