MAYBE
Time: 0.064947
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))}
       Fail
      
      
      
      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))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1) = 0,
         
         [le](x0, x1) = x0 + x1 + 1,
         
         [cons](x0, x1) = x0 + x1,
         
         [ack](x0, x1) = 0,
         
         [d](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [numbers] = 0,
         
         [nr] = 1,
         
         [true] = 0,
         
         [nil] = 0,
         
         [false] = 0,
         
         [le#](x0, x1) = x0
        Strict:
         le#(s x, s y) -> le#(x, y)
         1 + 0x + 1y >= 0 + 0x + 1y
        Weak:
         ack(s x, s y) -> ack(x, ack(s x, y))
         0 + 0x + 0y >= 0 + 0x + 0y
         ack(s x, 0()) -> ack(x, s 0())
         0 + 0x >= 0 + 0x
         ack(0(), x) -> s x
         0 + 0x >= 1 + 1x
         nr() -> ack(s s s s s s 0(), 0())
         1 >= 0
         le(s x, s y) -> le(x, y)
         3 + 1x + 1y >= 1 + 1x + 1y
         le(s x, 0()) -> false()
         3 + 1x >= 0
         le(0(), y) -> true()
         2 + 1y >= 0
         if(false(), x) -> nil()
         0 + 0x >= 0
         if(true(), x) -> cons(x, d s x)
         0 + 0x >= 2 + 2x
         numbers() -> d 0()
         0 >= 2
         d x -> if(le(x, nr()), x)
         1 + 1x >= 0 + 0x
       Qed
     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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1) = x0 + 1,
        
        [le](x0, x1) = x0 + 1,
        
        [cons](x0, x1) = x0 + x1,
        
        [ack](x0, x1) = x0 + 1,
        
        [d](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [numbers] = 0,
        
        [nr] = 0,
        
        [true] = 1,
        
        [nil] = 0,
        
        [false] = 1,
        
        [ack#](x0, x1) = x0
       Strict:
        ack#(s x, s y) -> ack#(s x, y)
        1 + 1x + 0y >= 1 + 1x + 0y
        ack#(s x, s y) -> ack#(x, ack(s x, y))
        1 + 1x + 0y >= 0 + 1x + 0y
        ack#(s x, 0()) -> ack#(x, s 0())
        1 + 1x >= 0 + 1x
       Weak:
        ack(s x, s y) -> ack(x, ack(s x, y))
        2 + 1x + 0y >= 1 + 1x + 0y
        ack(s x, 0()) -> ack(x, s 0())
        2 + 1x >= 1 + 1x
        ack(0(), x) -> s x
        2 + 0x >= 1 + 1x
        nr() -> ack(s s s s s s 0(), 0())
        0 >= 8
        le(s x, s y) -> le(x, y)
        2 + 1x + 0y >= 1 + 1x + 0y
        le(s x, 0()) -> false()
        2 + 1x >= 1
        le(0(), y) -> true()
        2 + 0y >= 1
        if(false(), x) -> nil()
        2 + 0x >= 0
        if(true(), x) -> cons(x, d s x)
        2 + 0x >= 2 + 2x
        numbers() -> d 0()
        0 >= 2
        d x -> if(le(x, nr()), x)
        1 + 1x >= 2 + 1x
      SCCS (1):
       Scc:
        {ack#(s x, s y) -> ack#(s x, y)}
       
       SCC (1):
        Strict:
         {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))}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [if](x0, x1) = 0,
          
          [le](x0, x1) = x0 + x1 + 1,
          
          [cons](x0, x1) = x0 + x1,
          
          [ack](x0, x1) = x0,
          
          [d](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [0] = 1,
          
          [numbers] = 0,
          
          [nr] = 1,
          
          [true] = 0,
          
          [nil] = 0,
          
          [false] = 0,
          
          [ack#](x0, x1) = x0 + 1
         Strict:
          ack#(s x, s y) -> ack#(s x, y)
          2 + 0x + 1y >= 1 + 0x + 1y
         Weak:
          ack(s x, s y) -> ack(x, ack(s x, y))
          1 + 0x + 1y >= 0 + 0x + 1y
          ack(s x, 0()) -> ack(x, s 0())
          1 + 0x >= 2 + 0x
          ack(0(), x) -> s x
          0 + 1x >= 1 + 1x
          nr() -> ack(s s s s s s 0(), 0())
          1 >= 1
          le(s x, s y) -> le(x, y)
          3 + 1x + 1y >= 1 + 1x + 1y
          le(s x, 0()) -> false()
          3 + 1x >= 0
          le(0(), y) -> true()
          2 + 1y >= 0
          if(false(), x) -> nil()
          0 + 0x >= 0
          if(true(), x) -> cons(x, d s x)
          0 + 0x >= 2 + 2x
          numbers() -> d 0()
          0 >= 2
          d x -> if(le(x, nr()), x)
          1 + 1x >= 0 + 0x
        Qed