MAYBE
Time: 0.010202
TRS:
 {         fst(0(), Z) -> nil(),
  fst(s X, cons(Y, Z)) -> cons(Y, fst(X, Z)),
                from X -> cons(X, from s X),
           add(0(), X) -> X,
           add(s X, Y) -> s add(X, Y),
             len nil() -> 0(),
        len cons(X, Z) -> s len Z}
 DP:
  DP:
   {fst#(s X, cons(Y, Z)) -> fst#(X, Z),
                  from# X -> from# s X,
             add#(s X, Y) -> add#(X, Y),
          len# cons(X, Z) -> len# Z}
  TRS:
  {         fst(0(), Z) -> nil(),
   fst(s X, cons(Y, Z)) -> cons(Y, fst(X, Z)),
                 from X -> cons(X, from s X),
            add(0(), X) -> X,
            add(s X, Y) -> s add(X, Y),
              len nil() -> 0(),
         len cons(X, Z) -> s len Z}
  UR:
   {}
   EDG:
    {(from# X -> from# s X, from# X -> from# s X)
     (fst#(s X, cons(Y, Z)) -> fst#(X, Z), fst#(s X, cons(Y, Z)) -> fst#(X, Z))
     (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> add#(X, Y))
     (len# cons(X, Z) -> len# Z, len# cons(X, Z) -> len# Z)}
    STATUS:
     arrows: 0.750000
     SCCS (4):
      Scc:
       {fst#(s X, cons(Y, Z)) -> fst#(X, Z)}
      Scc:
       {add#(s X, Y) -> add#(X, Y)}
      Scc:
       {from# X -> from# s X}
      Scc:
       {len# cons(X, Z) -> len# Z}
      
      SCC (1):
       Strict:
        {fst#(s X, cons(Y, Z)) -> fst#(X, Z)}
       Weak:
       {         fst(0(), Z) -> nil(),
        fst(s X, cons(Y, Z)) -> cons(Y, fst(X, Z)),
                      from X -> cons(X, from s X),
                 add(0(), X) -> X,
                 add(s X, Y) -> s add(X, Y),
                   len nil() -> 0(),
              len cons(X, Z) -> s len Z}
       Open
      SCC (1):
       Strict:
        {add#(s X, Y) -> add#(X, Y)}
       Weak:
       {         fst(0(), Z) -> nil(),
        fst(s X, cons(Y, Z)) -> cons(Y, fst(X, Z)),
                      from X -> cons(X, from s X),
                 add(0(), X) -> X,
                 add(s X, Y) -> s add(X, Y),
                   len nil() -> 0(),
              len cons(X, Z) -> s len Z}
       Open
      SCC (1):
       Strict:
        {from# X -> from# s X}
       Weak:
       {         fst(0(), Z) -> nil(),
        fst(s X, cons(Y, Z)) -> cons(Y, fst(X, Z)),
                      from X -> cons(X, from s X),
                 add(0(), X) -> X,
                 add(s X, Y) -> s add(X, Y),
                   len nil() -> 0(),
              len cons(X, Z) -> s len Z}
       Open
      SCC (1):
       Strict:
        {len# cons(X, Z) -> len# Z}
       Weak:
       {         fst(0(), Z) -> nil(),
        fst(s X, cons(Y, Z)) -> cons(Y, fst(X, Z)),
                      from X -> cons(X, from s X),
                 add(0(), X) -> X,
                 add(s X, Y) -> s add(X, Y),
                   len nil() -> 0(),
              len cons(X, Z) -> s len Z}
       Open