MAYBE

Problem:
 ack(0(),n) -> s(n)
 ack(s(m),0()) -> ack(m,s(0()))
 ack(s(m),s(n)) -> ack(m,ack(s(m),n))
 s(x()) -> r(x())
 0() -> z()

Proof:
 DP Processor:
  DPs:
   ack#(0(),n) -> s#(n)
   ack#(s(m),0()) -> s#(0())
   ack#(s(m),0()) -> ack#(m,s(0()))
   ack#(s(m),s(n)) -> ack#(s(m),n)
   ack#(s(m),s(n)) -> ack#(m,ack(s(m),n))
  TRS:
   ack(0(),n) -> s(n)
   ack(s(m),0()) -> ack(m,s(0()))
   ack(s(m),s(n)) -> ack(m,ack(s(m),n))
   s(x()) -> r(x())
   0() -> z()
  TDG Processor:
   DPs:
    ack#(0(),n) -> s#(n)
    ack#(s(m),0()) -> s#(0())
    ack#(s(m),0()) -> ack#(m,s(0()))
    ack#(s(m),s(n)) -> ack#(s(m),n)
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n))
   TRS:
    ack(0(),n) -> s(n)
    ack(s(m),0()) -> ack(m,s(0()))
    ack(s(m),s(n)) -> ack(m,ack(s(m),n))
    s(x()) -> r(x())
    0() -> z()
   graph:
    ack#(s(m),s(n)) -> ack#(s(m),n) ->
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n))
    ack#(s(m),s(n)) -> ack#(s(m),n) ->
    ack#(s(m),s(n)) -> ack#(s(m),n)
    ack#(s(m),s(n)) -> ack#(s(m),n) ->
    ack#(s(m),0()) -> ack#(m,s(0()))
    ack#(s(m),s(n)) -> ack#(s(m),n) -> ack#(s(m),0()) -> s#(0())
    ack#(s(m),s(n)) -> ack#(s(m),n) -> ack#(0(),n) -> s#(n)
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n)) ->
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n))
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n)) ->
    ack#(s(m),s(n)) -> ack#(s(m),n)
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n)) ->
    ack#(s(m),0()) -> ack#(m,s(0()))
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n)) ->
    ack#(s(m),0()) -> s#(0())
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n)) -> ack#(0(),n) -> s#(n)
    ack#(s(m),0()) -> ack#(m,s(0())) ->
    ack#(s(m),s(n)) -> ack#(m,ack(s(m),n))
    ack#(s(m),0()) -> ack#(m,s(0())) ->
    ack#(s(m),s(n)) -> ack#(s(m),n)
    ack#(s(m),0()) -> ack#(m,s(0())) ->
    ack#(s(m),0()) -> ack#(m,s(0()))
    ack#(s(m),0()) -> ack#(m,s(0())) -> ack#(s(m),0()) -> s#(0())
    ack#(s(m),0()) -> ack#(m,s(0())) -> ack#(0(),n) -> s#(n)
   Restore Modifier:
    DPs:
     ack#(0(),n) -> s#(n)
     ack#(s(m),0()) -> s#(0())
     ack#(s(m),0()) -> ack#(m,s(0()))
     ack#(s(m),s(n)) -> ack#(s(m),n)
     ack#(s(m),s(n)) -> ack#(m,ack(s(m),n))
    TRS:
     ack(0(),n) -> s(n)
     ack(s(m),0()) -> ack(m,s(0()))
     ack(s(m),s(n)) -> ack(m,ack(s(m),n))
     s(x()) -> r(x())
     0() -> z()
    SCC Processor:
     #sccs: 1
     #rules: 3
     #arcs: 15/25
     DPs:
      ack#(s(m),s(n)) -> ack#(s(m),n)
      ack#(s(m),0()) -> ack#(m,s(0()))
      ack#(s(m),s(n)) -> ack#(m,ack(s(m),n))
     TRS:
      ack(0(),n) -> s(n)
      ack(s(m),0()) -> ack(m,s(0()))
      ack(s(m),s(n)) -> ack(m,ack(s(m),n))
      s(x()) -> r(x())
      0() -> z()
     Open