MAYBE
Time: 0.005451
TRS:
 {           d x -> if(le(x, nr()), x),
       numbers() -> d 0(),
   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))}
 DP:
  DP:
   {          d# x -> if#(le(x, nr()), x),
              d# x -> le#(x, nr()),
              d# x -> nr#(),
        numbers#() -> d# 0(),
    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#(x, ack(s x, y)),
    ack#(s x, s y) -> ack#(s x, y)}
  TRS:
  {           d x -> if(le(x, nr()), x),
        numbers() -> d 0(),
    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))}
  UR:
   {   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)),
          a(z, w) -> z,
          a(z, w) -> w}
   EDG:
    {(numbers#() -> d# 0(), d# x -> nr#())
     (numbers#() -> d# 0(), d# x -> le#(x, nr()))
     (numbers#() -> d# 0(), d# x -> if#(le(x, nr()), x))
     (if#(true(), x) -> d# s x, d# x -> nr#())
     (if#(true(), x) -> d# s x, d# x -> le#(x, nr()))
     (if#(true(), x) -> d# s x, d# x -> if#(le(x, nr()), x))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (d# x -> if#(le(x, nr()), x), if#(true(), x) -> d# s x)
     (nr#() -> ack#(s s s s s s 0(), 0()), ack#(s x, 0()) -> ack#(x, s 0()))
     (d# x -> le#(x, nr()), le#(s x, s y) -> le#(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#(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))
     (d# x -> nr#(), nr#() -> ack#(s s s s s s 0(), 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, 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))}
    STATUS:
     arrows: 0.820000
     SCCS (3):
      Scc:
       {          d# x -> if#(le(x, nr()), x),
        if#(true(), x) -> d# s x}
      Scc:
       {le#(s x, s y) -> le#(x, y)}
      Scc:
       {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#(s x, y)}
      
      
      SCC (2):
       Strict:
        {          d# x -> if#(le(x, nr()), x),
         if#(true(), x) -> d# s x}
       Weak:
       {           d x -> if(le(x, nr()), x),
             numbers() -> d 0(),
         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
      
      
      
      SCC (1):
       Strict:
        {le#(s x, s y) -> le#(x, y)}
       Weak:
       {           d x -> if(le(x, nr()), x),
             numbers() -> d 0(),
         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
      SCC (3):
       Strict:
        {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#(s x, y)}
       Weak:
       {           d x -> if(le(x, nr()), x),
             numbers() -> d 0(),
         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