MAYBE
Time: 0.008023
TRS:
 {            fst(X1, X2) -> n__fst(X1, X2),
              fst(0(), Z) -> nil(),
     fst(s X, cons(Y, Z)) -> cons(Y, n__fst(activate X, activate Z)),
               activate X -> X,
  activate n__fst(X1, X2) -> fst(activate X1, activate X2),
       activate n__from X -> from activate X,
          activate n__s X -> s X,
  activate n__add(X1, X2) -> add(activate X1, activate X2),
        activate n__len X -> len activate X,
                      s X -> n__s X,
                   from X -> cons(X, n__from n__s X),
                   from X -> n__from X,
              add(X1, X2) -> n__add(X1, X2),
              add(0(), X) -> X,
              add(s X, Y) -> s n__add(activate X, Y),
                    len X -> n__len X,
                len nil() -> 0(),
           len cons(X, Z) -> s n__len activate Z}
 DP:
  DP:
   {   fst#(s X, cons(Y, Z)) -> activate# Z,
       fst#(s X, cons(Y, Z)) -> activate# X,
    activate# n__fst(X1, X2) -> fst#(activate X1, activate X2),
    activate# n__fst(X1, X2) -> activate# X1,
    activate# n__fst(X1, X2) -> activate# X2,
         activate# n__from X -> activate# X,
         activate# n__from X -> from# activate X,
            activate# n__s X -> s# X,
    activate# n__add(X1, X2) -> activate# X1,
    activate# n__add(X1, X2) -> activate# X2,
    activate# n__add(X1, X2) -> add#(activate X1, activate X2),
          activate# n__len X -> activate# X,
          activate# n__len X -> len# activate X,
                add#(s X, Y) -> activate# X,
                add#(s X, Y) -> s# n__add(activate X, Y),
             len# cons(X, Z) -> activate# Z,
             len# cons(X, Z) -> s# n__len activate Z}
  TRS:
  {            fst(X1, X2) -> n__fst(X1, X2),
               fst(0(), Z) -> nil(),
      fst(s X, cons(Y, Z)) -> cons(Y, n__fst(activate X, activate Z)),
                activate X -> X,
   activate n__fst(X1, X2) -> fst(activate X1, activate X2),
        activate n__from X -> from activate X,
           activate n__s X -> s X,
   activate n__add(X1, X2) -> add(activate X1, activate X2),
         activate n__len X -> len activate X,
                       s X -> n__s X,
                    from X -> cons(X, n__from n__s X),
                    from X -> n__from X,
               add(X1, X2) -> n__add(X1, X2),
               add(0(), X) -> X,
               add(s X, Y) -> s n__add(activate X, Y),
                     len X -> n__len X,
                 len nil() -> 0(),
            len cons(X, Z) -> s n__len activate Z}
  UR:
   {            fst(X1, X2) -> n__fst(X1, X2),
                fst(0(), Z) -> nil(),
       fst(s X, cons(Y, Z)) -> cons(Y, n__fst(activate X, activate Z)),
                 activate X -> X,
    activate n__fst(X1, X2) -> fst(activate X1, activate X2),
         activate n__from X -> from activate X,
            activate n__s X -> s X,
    activate n__add(X1, X2) -> add(activate X1, activate X2),
          activate n__len X -> len activate X,
                        s X -> n__s X,
                     from X -> cons(X, n__from n__s X),
                     from X -> n__from X,
                add(X1, X2) -> n__add(X1, X2),
                add(0(), X) -> X,
                add(s X, Y) -> s n__add(activate X, Y),
                      len X -> n__len X,
                  len nil() -> 0(),
             len cons(X, Z) -> s n__len activate Z,
                    a(x, y) -> x,
                    a(x, y) -> y}
   EDG:
    {(activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> s# n__add(activate X, Y))
     (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> activate# X)
     (activate# n__len X -> len# activate X, len# cons(X, Z) -> s# n__len activate Z)
     (activate# n__len X -> len# activate X, len# cons(X, Z) -> activate# Z)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__len X -> len# activate X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__len X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__s X -> s# X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__from X -> from# activate X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__from X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__fst(X1, X2) -> activate# X2)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__fst(X1, X2) -> activate# X1)
     (activate# n__add(X1, X2) -> activate# X2, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (activate# n__add(X1, X2) -> activate# X1, activate# n__len X -> len# activate X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__len X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__s X -> s# X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__from X -> from# activate X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__from X -> activate# X)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__fst(X1, X2) -> activate# X2)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__fst(X1, X2) -> activate# X1)
     (activate# n__add(X1, X2) -> activate# X1, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (activate# n__from X -> activate# X, activate# n__len X -> len# activate X)
     (activate# n__from X -> activate# X, activate# n__len X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__from X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__from X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__from X -> activate# X, activate# n__s X -> s# 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__fst(X1, X2) -> activate# X2)
     (activate# n__from X -> activate# X, activate# n__fst(X1, X2) -> activate# X1)
     (activate# n__from X -> activate# X, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (activate# n__len X -> activate# X, activate# n__len X -> len# activate X)
     (activate# n__len X -> activate# X, activate# n__len X -> activate# X)
     (activate# n__len X -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__len X -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__len X -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__len X -> activate# X, activate# n__s X -> s# X)
     (activate# n__len X -> activate# X, activate# n__from X -> from# activate X)
     (activate# n__len X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__len X -> activate# X, activate# n__fst(X1, X2) -> activate# X2)
     (activate# n__len X -> activate# X, activate# n__fst(X1, X2) -> activate# X1)
     (activate# n__len X -> activate# X, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__len X -> len# activate X)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__len X -> activate# X)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X2)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> activate# X1)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# activate X)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> activate# X)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__fst(X1, X2) -> activate# X2)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__fst(X1, X2) -> activate# X1)
     (fst#(s X, cons(Y, Z)) -> activate# Z, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (len# cons(X, Z) -> activate# Z, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (len# cons(X, Z) -> activate# Z, activate# n__fst(X1, X2) -> activate# X1)
     (len# cons(X, Z) -> activate# Z, activate# n__fst(X1, X2) -> activate# X2)
     (len# cons(X, Z) -> activate# Z, activate# n__from X -> activate# X)
     (len# cons(X, Z) -> activate# Z, activate# n__from X -> from# activate X)
     (len# cons(X, Z) -> activate# Z, activate# n__s X -> s# X)
     (len# cons(X, Z) -> activate# Z, activate# n__add(X1, X2) -> activate# X1)
     (len# cons(X, Z) -> activate# Z, activate# n__add(X1, X2) -> activate# X2)
     (len# cons(X, Z) -> activate# Z, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (len# cons(X, Z) -> activate# Z, activate# n__len X -> activate# X)
     (len# cons(X, Z) -> activate# Z, activate# n__len X -> len# activate X)
     (add#(s X, Y) -> activate# X, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (add#(s X, Y) -> activate# X, activate# n__fst(X1, X2) -> activate# X1)
     (add#(s X, Y) -> activate# X, activate# n__fst(X1, X2) -> activate# X2)
     (add#(s X, Y) -> activate# X, activate# n__from X -> activate# X)
     (add#(s X, Y) -> activate# X, activate# n__from X -> from# activate X)
     (add#(s X, Y) -> activate# X, activate# n__s X -> s# X)
     (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (add#(s X, Y) -> activate# X, activate# n__len X -> activate# X)
     (add#(s X, Y) -> activate# X, activate# n__len X -> len# activate X)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__fst(X1, X2) -> activate# X1)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__fst(X1, X2) -> activate# X2)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__from X -> activate# X)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__from X -> from# activate X)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X1)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> activate# X2)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__len X -> activate# X)
     (fst#(s X, cons(Y, Z)) -> activate# X, activate# n__len X -> len# activate X)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__fst(X1, X2) -> activate# X1)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__fst(X1, X2) -> activate# X2)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__from X -> activate# X)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__from X -> from# activate X)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__s X -> s# X)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__len X -> activate# X)
     (activate# n__fst(X1, X2) -> activate# X1, activate# n__len X -> len# activate X)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__fst(X1, X2) -> fst#(activate X1, activate X2))
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__fst(X1, X2) -> activate# X1)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__fst(X1, X2) -> activate# X2)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__from X -> activate# X)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__from X -> from# activate X)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__s X -> s# X)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2))
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__len X -> activate# X)
     (activate# n__fst(X1, X2) -> activate# X2, activate# n__len X -> len# activate X)
     (activate# n__fst(X1, X2) -> fst#(activate X1, activate X2), fst#(s X, cons(Y, Z)) -> activate# Z)
     (activate# n__fst(X1, X2) -> fst#(activate X1, activate X2), fst#(s X, cons(Y, Z)) -> activate# X)}
    STATUS:
     arrows: 0.598616
     SCCS (1):
      Scc:
       {   fst#(s X, cons(Y, Z)) -> activate# Z,
           fst#(s X, cons(Y, Z)) -> activate# X,
        activate# n__fst(X1, X2) -> fst#(activate X1, activate X2),
        activate# n__fst(X1, X2) -> activate# X1,
        activate# n__fst(X1, X2) -> activate# X2,
             activate# n__from X -> activate# X,
        activate# n__add(X1, X2) -> activate# X1,
        activate# n__add(X1, X2) -> activate# X2,
        activate# n__add(X1, X2) -> add#(activate X1, activate X2),
              activate# n__len X -> activate# X,
              activate# n__len X -> len# activate X,
                    add#(s X, Y) -> activate# X,
                 len# cons(X, Z) -> activate# Z}
      
      SCC (13):
       Strict:
        {   fst#(s X, cons(Y, Z)) -> activate# Z,
            fst#(s X, cons(Y, Z)) -> activate# X,
         activate# n__fst(X1, X2) -> fst#(activate X1, activate X2),
         activate# n__fst(X1, X2) -> activate# X1,
         activate# n__fst(X1, X2) -> activate# X2,
              activate# n__from X -> activate# X,
         activate# n__add(X1, X2) -> activate# X1,
         activate# n__add(X1, X2) -> activate# X2,
         activate# n__add(X1, X2) -> add#(activate X1, activate X2),
               activate# n__len X -> activate# X,
               activate# n__len X -> len# activate X,
                     add#(s X, Y) -> activate# X,
                  len# cons(X, Z) -> activate# Z}
       Weak:
       {            fst(X1, X2) -> n__fst(X1, X2),
                    fst(0(), Z) -> nil(),
           fst(s X, cons(Y, Z)) -> cons(Y, n__fst(activate X, activate Z)),
                     activate X -> X,
        activate n__fst(X1, X2) -> fst(activate X1, activate X2),
             activate n__from X -> from activate X,
                activate n__s X -> s X,
        activate n__add(X1, X2) -> add(activate X1, activate X2),
              activate n__len X -> len activate X,
                            s X -> n__s X,
                         from X -> cons(X, n__from n__s X),
                         from X -> n__from X,
                    add(X1, X2) -> n__add(X1, X2),
                    add(0(), X) -> X,
                    add(s X, Y) -> s n__add(activate X, Y),
                          len X -> n__len X,
                      len nil() -> 0(),
                 len cons(X, Z) -> s n__len activate Z}
       Open