MAYBE
Time: 0.028937
TRS:
 {                eq(X, Y) -> false(),
        eq(n__0(), n__0()) -> true(),
        eq(n__s X, n__s Y) -> eq(activate X, activate Y),
                activate X -> X,
           activate n__0() -> 0(),
           activate n__s X -> s X,
         activate n__inf X -> inf X,
  activate n__take(X1, X2) -> take(X1, X2),
      activate n__length X -> length X,
                       s X -> n__s X,
                     inf X -> cons(X, n__inf s X),
                     inf X -> n__inf X,
              take(X1, X2) -> n__take(X1, X2),
     take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
              take(0(), X) -> nil(),
                       0() -> n__0(),
                  length X -> n__length X,
         length cons(X, L) -> s n__length activate L,
              length nil() -> 0()}
 DP:
  DP:
   {      eq#(n__s X, n__s Y) -> eq#(activate X, activate Y),
          eq#(n__s X, n__s Y) -> activate# X,
          eq#(n__s X, n__s Y) -> activate# Y,
             activate# n__0() -> 0#(),
             activate# n__s X -> s# X,
           activate# n__inf X -> inf# X,
    activate# n__take(X1, X2) -> take#(X1, X2),
        activate# n__length X -> length# X,
                       inf# X -> s# X,
       take#(s X, cons(Y, L)) -> activate# X,
       take#(s X, cons(Y, L)) -> activate# Y,
       take#(s X, cons(Y, L)) -> activate# L,
           length# cons(X, L) -> activate# L,
           length# cons(X, L) -> s# n__length activate L,
                length# nil() -> 0#()}
  TRS:
  {                eq(X, Y) -> false(),
         eq(n__0(), n__0()) -> true(),
         eq(n__s X, n__s Y) -> eq(activate X, activate Y),
                 activate X -> X,
            activate n__0() -> 0(),
            activate n__s X -> s X,
          activate n__inf X -> inf X,
   activate n__take(X1, X2) -> take(X1, X2),
       activate n__length X -> length X,
                        s X -> n__s X,
                      inf X -> cons(X, n__inf s X),
                      inf X -> n__inf X,
               take(X1, X2) -> n__take(X1, X2),
      take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
               take(0(), X) -> nil(),
                        0() -> n__0(),
                   length X -> n__length X,
          length cons(X, L) -> s n__length activate L,
               length nil() -> 0()}
  EDG:
   {(take#(s X, cons(Y, L)) -> activate# Y, activate# n__length X -> length# X)
    (take#(s X, cons(Y, L)) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
    (take#(s X, cons(Y, L)) -> activate# Y, activate# n__inf X -> inf# X)
    (take#(s X, cons(Y, L)) -> activate# Y, activate# n__s X -> s# X)
    (take#(s X, cons(Y, L)) -> activate# Y, activate# n__0() -> 0#())
    (length# cons(X, L) -> activate# L, activate# n__length X -> length# X)
    (length# cons(X, L) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
    (length# cons(X, L) -> activate# L, activate# n__inf X -> inf# X)
    (length# cons(X, L) -> activate# L, activate# n__s X -> s# X)
    (length# cons(X, L) -> activate# L, activate# n__0() -> 0#())
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# L)
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# Y)
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# X)
    (eq#(n__s X, n__s Y) -> activate# X, activate# n__length X -> length# X)
    (eq#(n__s X, n__s Y) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
    (eq#(n__s X, n__s Y) -> activate# X, activate# n__inf X -> inf# X)
    (eq#(n__s X, n__s Y) -> activate# X, activate# n__s X -> s# X)
    (eq#(n__s X, n__s Y) -> activate# X, activate# n__0() -> 0#())
    (activate# n__inf X -> inf# X, inf# X -> s# X)
    (take#(s X, cons(Y, L)) -> activate# X, activate# n__0() -> 0#())
    (take#(s X, cons(Y, L)) -> activate# X, activate# n__s X -> s# X)
    (take#(s X, cons(Y, L)) -> activate# X, activate# n__inf X -> inf# X)
    (take#(s X, cons(Y, L)) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
    (take#(s X, cons(Y, L)) -> activate# X, activate# n__length X -> length# X)
    (activate# n__length X -> length# X, length# cons(X, L) -> activate# L)
    (activate# n__length X -> length# X, length# cons(X, L) -> s# n__length activate L)
    (activate# n__length X -> length# X, length# nil() -> 0#())
    (take#(s X, cons(Y, L)) -> activate# L, activate# n__0() -> 0#())
    (take#(s X, cons(Y, L)) -> activate# L, activate# n__s X -> s# X)
    (take#(s X, cons(Y, L)) -> activate# L, activate# n__inf X -> inf# X)
    (take#(s X, cons(Y, L)) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
    (take#(s X, cons(Y, L)) -> activate# L, activate# n__length X -> length# X)
    (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> eq#(activate X, activate Y))
    (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# X)
    (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# Y)
    (eq#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#())
    (eq#(n__s X, n__s Y) -> activate# Y, activate# n__s X -> s# X)
    (eq#(n__s X, n__s Y) -> activate# Y, activate# n__inf X -> inf# X)
    (eq#(n__s X, n__s Y) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
    (eq#(n__s X, n__s Y) -> activate# Y, activate# n__length X -> length# X)}
   STATUS:
    arrows: 0.822222
    SCCS (2):
     Scc:
      {eq#(n__s X, n__s Y) -> eq#(activate X, activate Y)}
     Scc:
      {activate# n__take(X1, X2) -> take#(X1, X2),
           activate# n__length X -> length# X,
          take#(s X, cons(Y, L)) -> activate# X,
          take#(s X, cons(Y, L)) -> activate# Y,
          take#(s X, cons(Y, L)) -> activate# L,
              length# cons(X, L) -> activate# L}
     
     SCC (1):
      Strict:
       {eq#(n__s X, n__s Y) -> eq#(activate X, activate Y)}
      Weak:
      {                eq(X, Y) -> false(),
             eq(n__0(), n__0()) -> true(),
             eq(n__s X, n__s Y) -> eq(activate X, activate Y),
                     activate X -> X,
                activate n__0() -> 0(),
                activate n__s X -> s X,
              activate n__inf X -> inf X,
       activate n__take(X1, X2) -> take(X1, X2),
           activate n__length X -> length X,
                            s X -> n__s X,
                          inf X -> cons(X, n__inf s X),
                          inf X -> n__inf X,
                   take(X1, X2) -> n__take(X1, X2),
          take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
                   take(0(), X) -> nil(),
                            0() -> n__0(),
                       length X -> n__length X,
              length cons(X, L) -> s n__length activate L,
                   length nil() -> 0()}
      Fail
     
     
     SCC (6):
      Strict:
       {activate# n__take(X1, X2) -> take#(X1, X2),
            activate# n__length X -> length# X,
           take#(s X, cons(Y, L)) -> activate# X,
           take#(s X, cons(Y, L)) -> activate# Y,
           take#(s X, cons(Y, L)) -> activate# L,
               length# cons(X, L) -> activate# L}
      Weak:
      {                eq(X, Y) -> false(),
             eq(n__0(), n__0()) -> true(),
             eq(n__s X, n__s Y) -> eq(activate X, activate Y),
                     activate X -> X,
                activate n__0() -> 0(),
                activate n__s X -> s X,
              activate n__inf X -> inf X,
       activate n__take(X1, X2) -> take(X1, X2),
           activate n__length X -> length X,
                            s X -> n__s X,
                          inf X -> cons(X, n__inf s X),
                          inf X -> n__inf X,
                   take(X1, X2) -> n__take(X1, X2),
          take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
                   take(0(), X) -> nil(),
                            0() -> n__0(),
                       length X -> n__length X,
              length cons(X, L) -> s n__length activate L,
                   length nil() -> 0()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [eq](x0, x1) = x0 + 1,
        
        [cons](x0, x1) = x0 + x1 + 1,
        
        [take](x0, x1) = x0 + x1,
        
        [n__take](x0, x1) = x0 + x1,
        
        [activate](x0) = 1,
        
        [n__s](x0) = 1,
        
        [n__inf](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [inf](x0) = 0,
        
        [length](x0) = 0,
        
        [n__length](x0) = x0,
        
        [true] = 0,
        
        [n__0] = 1,
        
        [false] = 0,
        
        [nil] = 0,
        
        [0] = 0,
        
        [take#](x0, x1) = x0 + x1,
        
        [activate#](x0) = x0,
        
        [length#](x0) = x0
       Strict:
        length# cons(X, L) -> activate# L
        1 + 1X + 1L >= 0 + 1L
        take#(s X, cons(Y, L)) -> activate# L
        2 + 1X + 1Y + 1L >= 0 + 1L
        take#(s X, cons(Y, L)) -> activate# Y
        2 + 1X + 1Y + 1L >= 0 + 1Y
        take#(s X, cons(Y, L)) -> activate# X
        2 + 1X + 1Y + 1L >= 0 + 1X
        activate# n__length X -> length# X
        0 + 1X >= 0 + 1X
        activate# n__take(X1, X2) -> take#(X1, X2)
        0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
       Weak:
        length nil() -> 0()
        0 >= 0
        length cons(X, L) -> s n__length activate L
        0 + 0X + 0L >= 2 + 0L
        length X -> n__length X
        0 + 0X >= 0 + 1X
        0() -> n__0()
        0 >= 1
        take(0(), X) -> nil()
        0 + 1X >= 0
        take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L))
        2 + 1X + 1Y + 1L >= 4 + 0X + 0Y + 0L
        take(X1, X2) -> n__take(X1, X2)
        0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
        inf X -> n__inf X
        0 + 0X >= 0 + 0X
        inf X -> cons(X, n__inf s X)
        0 + 0X >= 1 + 1X
        s X -> n__s X
        1 + 1X >= 1 + 0X
        activate n__length X -> length X
        1 + 0X >= 0 + 0X
        activate n__take(X1, X2) -> take(X1, X2)
        1 + 0X1 + 0X2 >= 0 + 1X1 + 1X2
        activate n__inf X -> inf X
        1 + 0X >= 0 + 0X
        activate n__s X -> s X
        1 + 0X >= 1 + 1X
        activate n__0() -> 0()
        1 >= 0
        activate X -> X
        1 + 0X >= 1X
        eq(n__s X, n__s Y) -> eq(activate X, activate Y)
        2 + 0X + 0Y >= 2 + 0X + 0Y
        eq(n__0(), n__0()) -> true()
        2 >= 0
        eq(X, Y) -> false()
        1 + 0X + 1Y >= 0
      SCCS (0):