MAYBE
TRS:
 {           from(X) -> cons(X, from(s(X))),
  length(cons(X, Y)) -> s(length1(Y)),
       length(nil()) -> 0(),
          length1(X) -> length(X)}
 DP:
  Strict:
   {           from#(X) -> from#(s(X)),
    length#(cons(X, Y)) -> length1#(Y),
            length1#(X) -> length#(X)}
  Weak:
  {           from(X) -> cons(X, from(s(X))),
   length(cons(X, Y)) -> s(length1(Y)),
        length(nil()) -> 0(),
           length1(X) -> length(X)}
  EDG:
   {(length1#(X) -> length#(X), length#(cons(X, Y)) -> length1#(Y))
    (from#(X) -> from#(s(X)), from#(X) -> from#(s(X)))
    (length#(cons(X, Y)) -> length1#(Y), length1#(X) -> length#(X))}
   SCCS:
    Scc:
     {length#(cons(X, Y)) -> length1#(Y),
              length1#(X) -> length#(X)}
    Scc:
     {from#(X) -> from#(s(X))}
    SCC:
     Strict:
      {length#(cons(X, Y)) -> length1#(Y),
               length1#(X) -> length#(X)}
     Weak:
     {           from(X) -> cons(X, from(s(X))),
      length(cons(X, Y)) -> s(length1(Y)),
           length(nil()) -> 0(),
              length1(X) -> length(X)}
     SPSC:
      Simple Projection:
       pi(length1#) = 0, pi(length#) = 0
      Strict:
       {length1#(X) -> length#(X)}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {from#(X) -> from#(s(X))}
     Weak:
     {           from(X) -> cons(X, from(s(X))),
      length(cons(X, Y)) -> s(length1(Y)),
           length(nil()) -> 0(),
              length1(X) -> length(X)}
     Fail