MAYBE
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:
  Strict:
   {                  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)}
  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()}
  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)))
    (length#(n__cons(X, Y)) -> length1#(activate(Y)), length1#(X) -> activate#(X))
    (length#(n__cons(X, Y)) -> length1#(activate(Y)), length1#(X) -> length#(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))
    (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))}
   SCCS:
    Scc:
     {     activate#(n__from(X)) -> activate#(X),
              activate#(n__s(X)) -> activate#(X),
      activate#(n__cons(X1, X2)) -> activate#(X1)}
    Scc:
     {length#(n__cons(X, Y)) -> length1#(activate(Y)),
                 length1#(X) -> length#(activate(X))}
    SCC:
     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()}
     SPSC:
      Simple Projection:
       pi(activate#) = 0
      Strict:
       {     activate#(n__from(X)) -> activate#(X),
        activate#(n__cons(X1, X2)) -> activate#(X1)}
      EDG:
       {(activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1))
        (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> activate#(X))
        (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
        (activate#(n__from(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1))}
       SCCS:
        Scc:
         {     activate#(n__from(X)) -> activate#(X),
          activate#(n__cons(X1, X2)) -> activate#(X1)}
        SCC:
         Strict:
          {     activate#(n__from(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()}
         SPSC:
          Simple Projection:
           pi(activate#) = 0
          Strict:
           {activate#(n__cons(X1, X2)) -> activate#(X1)}
          EDG:
           {(activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1))}
           SCCS:
            Scc:
             {activate#(n__cons(X1, X2)) -> activate#(X1)}
            SCC:
             Strict:
              {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()}
             SPSC:
              Simple Projection:
               pi(activate#) = 0
              Strict:
               {}
              Qed
    SCC:
     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