MAYBE

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()
      Open