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))
  TDG 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))
   graph:
    ack#(s(x),s(y)) -> ack#(s(x),y) ->
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
    ack#(s(x),s(y)) -> ack#(s(x),y) ->
    ack#(s(x),s(y)) -> ack#(s(x),y)
    ack#(s(x),s(y)) -> ack#(s(x),y) ->
    ack#(s(x),0()) -> ack#(x,s(0()))
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
    ack#(s(x),s(y)) -> ack#(s(x),y)
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
    ack#(s(x),0()) -> ack#(x,s(0()))
    ack#(s(x),0()) -> ack#(x,s(0())) ->
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
    ack#(s(x),0()) -> ack#(x,s(0())) ->
    ack#(s(x),s(y)) -> ack#(s(x),y)
    ack#(s(x),0()) -> ack#(x,s(0())) -> ack#(s(x),0()) -> ack#(x,s(0()))
    if#(true(),x) -> d#(s(x)) -> d#(x) -> if#(le(x,nr()),x)
    if#(true(),x) -> d#(s(x)) -> d#(x) -> le#(x,nr())
    if#(true(),x) -> d#(s(x)) -> d#(x) -> nr#()
    le#(s(x),s(y)) -> le#(x,y) ->
    le#(s(x),s(y)) -> le#(x,y)
    nr#() -> ack#(s(s(s(s(s(s(0())))))),0()) ->
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
    nr#() -> ack#(s(s(s(s(s(s(0())))))),0()) ->
    ack#(s(x),s(y)) -> ack#(s(x),y)
    nr#() -> ack#(s(s(s(s(s(s(0())))))),0()) ->
    ack#(s(x),0()) -> ack#(x,s(0()))
    d#(x) -> if#(le(x,nr()),x) -> if#(true(),x) -> d#(s(x))
    d#(x) -> le#(x,nr()) -> le#(s(x),s(y)) -> le#(x,y)
    d#(x) -> nr#() -> nr#() -> ack#(s(s(s(s(s(s(0())))))),0())
    numbers#() -> d#(0()) -> d#(x) -> if#(le(x,nr()),x)
    numbers#() -> d#(0()) -> d#(x) -> le#(x,nr())
    numbers#() -> d#(0()) -> d#(x) -> nr#()
   SCC Processor:
    #sccs: 3
    #rules: 6
    #arcs: 22/100
    DPs:
     if#(true(),x) -> d#(s(x))
     d#(x) -> if#(le(x,nr()),x)
    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))
    Open
    
    DPs:
     le#(s(x),s(y)) -> le#(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))
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      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))
     Qed
    
    DPs:
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),0()) -> ack#(x,s(0()))
     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))
    Subterm Criterion Processor:
     simple projection:
      pi(ack#) = 0
     problem:
      DPs:
       ack#(s(x),s(y)) -> 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))
     Subterm Criterion Processor:
      simple projection:
       pi(ack#) = 1
      problem:
       DPs:
        
       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))
      Qed