MAYBE
Time: 0.006848
TRS:
 {           from X -> cons(X, from s X),
  length cons(X, Y) -> s length1 Y,
       length nil() -> 0(),
          length1 X -> length X}
 DP:
  DP:
   {           from# X -> from# s X,
    length# cons(X, Y) -> length1# Y,
            length1# X -> length# X}
  TRS:
  {           from X -> cons(X, from s X),
   length cons(X, Y) -> s length1 Y,
        length nil() -> 0(),
           length1 X -> length X}
  UR:
   {}
   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)}
    STATUS:
     arrows: 0.666667
     SCCS (2):
      Scc:
       {from# X -> from# s X}
      Scc:
       {length# cons(X, Y) -> length1# Y,
                length1# X -> length# X}
      
      SCC (1):
       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}
       Open
      SCC (2):
       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}
       Open