MAYBE

Problem:
 numbers() -> d(0())
 d(x) -> if(le(x,nr()),x)
 if(true(),x) -> cons(x,d(s(x)))
 if(false(),x) -> nil()
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 nr() -> ack(s(s(s(s(s(s(0())))))),0())
 ack(0(),x) -> s(x)
 ack(s(x),0()) -> ack(x,s(0()))
 ack(s(x),s(y)) -> ack(x,ack(s(x),y))

Proof:
 DP Processor:
  DPs:
   numbers#() -> d#(0())
   d#(x) -> nr#()
   d#(x) -> le#(x,nr())
   d#(x) -> if#(le(x,nr()),x)
   if#(true(),x) -> d#(s(x))
   le#(s(x),s(y)) -> le#(x,y)
   nr#() -> ack#(s(s(s(s(s(s(0())))))),0())
   ack#(s(x),0()) -> ack#(x,s(0()))
   ack#(s(x),s(y)) -> ack#(s(x),y)
   ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
  TRS:
   numbers() -> d(0())
   d(x) -> if(le(x,nr()),x)
   if(true(),x) -> cons(x,d(s(x)))
   if(false(),x) -> nil()
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   nr() -> ack(s(s(s(s(s(s(0())))))),0())
   ack(0(),x) -> s(x)
   ack(s(x),0()) -> ack(x,s(0()))
   ack(s(x),s(y)) -> ack(x,ack(s(x),y))
  Usable Rule Processor:
   DPs:
    numbers#() -> d#(0())
    d#(x) -> nr#()
    d#(x) -> le#(x,nr())
    d#(x) -> if#(le(x,nr()),x)
    if#(true(),x) -> d#(s(x))
    le#(s(x),s(y)) -> le#(x,y)
    nr#() -> ack#(s(s(s(s(s(s(0())))))),0())
    ack#(s(x),0()) -> ack#(x,s(0()))
    ack#(s(x),s(y)) -> ack#(s(x),y)
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
   TRS:
    nr() -> ack(s(s(s(s(s(s(0())))))),0())
    ack(s(x),0()) -> ack(x,s(0()))
    ack(0(),x) -> s(x)
    ack(s(x),s(y)) -> ack(x,ack(s(x),y))
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
   Open