MAYBE
Time: 0.587565
TRS:
 {            cons(X1, X2) -> n__cons(X1, X2),
                    from X -> cons(X, n__from n__s X),
                    from X -> n__from X,
           length n__nil() -> 0(),
      length n__cons(X, Y) -> s length1 activate Y,
                       s X -> n__s X,
                 length1 X -> length activate X,
                activate X -> X,
        activate n__from X -> from activate X,
           activate n__s X -> s activate X,
         activate n__nil() -> nil(),
  activate n__cons(X1, X2) -> cons(activate X1, X2),
                     nil() -> n__nil()}
 DP:
  DP:
   {                  from# X -> cons#(X, n__from n__s X),
        length# n__cons(X, Y) -> s# length1 activate Y,
        length# n__cons(X, Y) -> length1# activate Y,
        length# n__cons(X, Y) -> activate# Y,
                   length1# X -> length# activate X,
                   length1# X -> activate# X,
          activate# n__from X -> from# activate X,
          activate# n__from X -> activate# X,
             activate# n__s X -> s# activate X,
             activate# n__s X -> activate# X,
           activate# n__nil() -> nil#(),
    activate# n__cons(X1, X2) -> cons#(activate X1, X2),
    activate# n__cons(X1, X2) -> activate# X1}
  TRS:
  {            cons(X1, X2) -> n__cons(X1, X2),
                     from X -> cons(X, n__from n__s X),
                     from X -> n__from X,
            length n__nil() -> 0(),
       length n__cons(X, Y) -> s length1 activate Y,
                        s X -> n__s X,
                  length1 X -> length activate X,
                 activate X -> X,
         activate n__from X -> from activate X,
            activate n__s X -> s activate X,
          activate n__nil() -> nil(),
   activate n__cons(X1, X2) -> cons(activate X1, X2),
                      nil() -> n__nil()}
  UR:
   {            cons(X1, X2) -> n__cons(X1, X2),
                      from X -> cons(X, n__from n__s X),
                      from X -> n__from X,
             length n__nil() -> 0(),
        length n__cons(X, Y) -> s length1 activate Y,
                         s X -> n__s X,
                   length1 X -> length activate X,
                  activate X -> X,
          activate n__from X -> from activate X,
             activate n__s X -> s activate X,
           activate n__nil() -> nil(),
    activate n__cons(X1, X2) -> cons(activate X1, X2),
                       nil() -> n__nil(),
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {(length1# X -> activate# X, activate# n__cons(X1, X2) -> activate# X1)
     (length1# X -> activate# X, activate# n__cons(X1, X2) -> cons#(activate X1, X2))
     (length1# X -> activate# X, activate# n__nil() -> nil#())
     (length1# X -> activate# X, activate# n__s X -> activate# X)
     (length1# X -> activate# X, activate# n__s X -> s# activate X)
     (length1# X -> activate# X, activate# n__from X -> activate# X)
     (length1# X -> activate# X, activate# n__from X -> from# activate X)
     (activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> activate# X1)
     (activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> cons#(activate X1, X2))
     (activate# n__s X -> activate# X, activate# n__nil() -> nil#())
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__s X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> from# activate X)
     (length# n__cons(X, Y) -> activate# Y, activate# n__cons(X1, X2) -> activate# X1)
     (length# n__cons(X, Y) -> activate# Y, activate# n__cons(X1, X2) -> cons#(activate X1, X2))
     (length# n__cons(X, Y) -> activate# Y, activate# n__nil() -> nil#())
     (length# n__cons(X, Y) -> activate# Y, activate# n__s X -> activate# X)
     (length# n__cons(X, Y) -> activate# Y, activate# n__s X -> s# activate X)
     (length# n__cons(X, Y) -> activate# Y, activate# n__from X -> activate# X)
     (length# n__cons(X, Y) -> activate# Y, activate# n__from X -> from# activate X)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> activate# X1)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> cons#(activate X1, X2))
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__nil() -> nil#())
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> activate# X)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> from# activate X)
     (activate# n__from X -> from# activate X, from# X -> cons#(X, n__from n__s X))
     (length1# X -> length# activate X, length# n__cons(X, Y) -> s# length1 activate Y)
     (length1# X -> length# activate X, length# n__cons(X, Y) -> length1# activate Y)
     (length1# X -> length# activate X, length# n__cons(X, Y) -> activate# Y)
     (length# n__cons(X, Y) -> length1# activate Y, length1# X -> length# activate X)
     (length# n__cons(X, Y) -> length1# activate Y, length1# X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__from X -> from# activate X)
     (activate# n__from X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__from X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__nil() -> nil#())
     (activate# n__from X -> activate# X, activate# n__cons(X1, X2) -> cons#(activate X1, X2))
     (activate# n__from X -> activate# X, activate# n__cons(X1, X2) -> activate# X1)}
    STATUS:
     arrows: 0.757396
     SCCS (2):
      Scc:
       {length# n__cons(X, Y) -> length1# activate Y,
                   length1# X -> length# activate X}
      Scc:
       {      activate# n__from X -> activate# X,
                 activate# n__s X -> activate# X,
        activate# n__cons(X1, X2) -> activate# X1}
      
      SCC (2):
       Strict:
        {length# n__cons(X, Y) -> length1# activate Y,
                    length1# X -> length# activate X}
       Weak:
       {            cons(X1, X2) -> n__cons(X1, X2),
                          from X -> cons(X, n__from n__s X),
                          from X -> n__from X,
                 length n__nil() -> 0(),
            length n__cons(X, Y) -> s length1 activate Y,
                             s X -> n__s X,
                       length1 X -> length activate X,
                      activate X -> X,
              activate n__from X -> from activate X,
                 activate n__s X -> s activate X,
               activate n__nil() -> nil(),
        activate n__cons(X1, X2) -> cons(activate X1, X2),
                           nil() -> n__nil()}
       Fail
      
      
      
      SCC (3):
       Strict:
        {      activate# n__from X -> activate# X,
                  activate# n__s X -> activate# X,
         activate# n__cons(X1, X2) -> activate# X1}
       Weak:
       {            cons(X1, X2) -> n__cons(X1, X2),
                          from X -> cons(X, n__from n__s X),
                          from X -> n__from X,
                 length n__nil() -> 0(),
            length n__cons(X, Y) -> s length1 activate Y,
                             s X -> n__s X,
                       length1 X -> length activate X,
                      activate X -> X,
              activate n__from X -> from activate X,
                 activate n__s X -> s activate X,
               activate n__nil() -> nil(),
        activate n__cons(X1, X2) -> cons(activate X1, X2),
                           nil() -> n__nil()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = 0,
         
         [n__cons](x0, x1) = x0 + 1,
         
         [n__from](x0) = x0 + 1,
         
         [n__s](x0) = x0 + 1,
         
         [from](x0) = x0 + 1,
         
         [length](x0) = x0 + 1,
         
         [s](x0) = 0,
         
         [length1](x0) = x0 + 1,
         
         [activate](x0) = x0 + 1,
         
         [0] = 0,
         
         [n__nil] = 1,
         
         [nil] = 0,
         
         [activate#](x0) = x0 + 1
        Strict:
         activate# n__cons(X1, X2) -> activate# X1
         2 + 1X1 + 0X2 >= 1 + 1X1
         activate# n__s X -> activate# X
         2 + 1X >= 1 + 1X
         activate# n__from X -> activate# X
         2 + 1X >= 1 + 1X
        Weak:
         nil() -> n__nil()
         0 >= 1
         activate n__cons(X1, X2) -> cons(activate X1, X2)
         2 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
         activate n__nil() -> nil()
         2 >= 0
         activate n__s X -> s activate X
         2 + 1X >= 0 + 0X
         activate n__from X -> from activate X
         2 + 1X >= 2 + 1X
         activate X -> X
         1 + 1X >= 1X
         length1 X -> length activate X
         1 + 1X >= 2 + 1X
         s X -> n__s X
         0 + 0X >= 1 + 1X
         length n__cons(X, Y) -> s length1 activate Y
         2 + 1X + 0Y >= 0 + 0Y
         length n__nil() -> 0()
         2 >= 0
         from X -> n__from X
         1 + 1X >= 1 + 1X
         from X -> cons(X, n__from n__s X)
         1 + 1X >= 0 + 0X
         cons(X1, X2) -> n__cons(X1, X2)
         0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2
       Qed