MAYBE
Time: 0.036079
TRS:
 {                   dbl X -> n__dbl X,
                   dbl 0() -> 0(),
                   dbl s X -> s n__s n__dbl activate X,
                       s X -> n__s X,
                activate X -> X,
           activate n__s X -> s X,
         activate n__dbl X -> dbl activate X,
        activate n__dbls X -> dbls activate X,
   activate n__sel(X1, X2) -> sel(activate X1, activate X2),
  activate n__indx(X1, X2) -> indx(activate X1, X2),
        activate n__from X -> from X,
                    dbls X -> n__dbls X,
                dbls nil() -> nil(),
           dbls cons(X, Y) -> cons(n__dbl activate X, n__dbls activate Y),
               sel(X1, X2) -> n__sel(X1, X2),
      sel(0(), cons(X, Y)) -> activate X,
      sel(s X, cons(Y, Z)) -> sel(activate X, activate Z),
              indx(X1, X2) -> n__indx(X1, X2),
            indx(nil(), X) -> nil(),
       indx(cons(X, Y), Z) -> cons(n__sel(activate X, activate Z), n__indx(activate Y, activate Z)),
                    from X -> cons(activate X, n__from n__s activate X),
                    from X -> n__from X}
 DP:
  DP:
   {                 dbl# s X -> s# n__s n__dbl activate X,
                     dbl# s X -> activate# X,
             activate# n__s X -> s# X,
           activate# n__dbl X -> dbl# activate X,
           activate# n__dbl X -> activate# X,
          activate# n__dbls X -> activate# X,
          activate# n__dbls X -> dbls# activate X,
     activate# n__sel(X1, X2) -> activate# X1,
     activate# n__sel(X1, X2) -> activate# X2,
     activate# n__sel(X1, X2) -> sel#(activate X1, activate X2),
    activate# n__indx(X1, X2) -> activate# X1,
    activate# n__indx(X1, X2) -> indx#(activate X1, X2),
          activate# n__from X -> from# X,
             dbls# cons(X, Y) -> activate# X,
             dbls# cons(X, Y) -> activate# Y,
        sel#(0(), cons(X, Y)) -> activate# X,
        sel#(s X, cons(Y, Z)) -> activate# X,
        sel#(s X, cons(Y, Z)) -> activate# Z,
        sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z),
         indx#(cons(X, Y), Z) -> activate# X,
         indx#(cons(X, Y), Z) -> activate# Y,
         indx#(cons(X, Y), Z) -> activate# Z,
                      from# X -> activate# X}
  TRS:
  {                   dbl X -> n__dbl X,
                    dbl 0() -> 0(),
                    dbl s X -> s n__s n__dbl activate X,
                        s X -> n__s X,
                 activate X -> X,
            activate n__s X -> s X,
          activate n__dbl X -> dbl activate X,
         activate n__dbls X -> dbls activate X,
    activate n__sel(X1, X2) -> sel(activate X1, activate X2),
   activate n__indx(X1, X2) -> indx(activate X1, X2),
         activate n__from X -> from X,
                     dbls X -> n__dbls X,
                 dbls nil() -> nil(),
            dbls cons(X, Y) -> cons(n__dbl activate X, n__dbls activate Y),
                sel(X1, X2) -> n__sel(X1, X2),
       sel(0(), cons(X, Y)) -> activate X,
       sel(s X, cons(Y, Z)) -> sel(activate X, activate Z),
               indx(X1, X2) -> n__indx(X1, X2),
             indx(nil(), X) -> nil(),
        indx(cons(X, Y), Z) -> cons(n__sel(activate X, activate Z), n__indx(activate Y, activate Z)),
                     from X -> cons(activate X, n__from n__s activate X),
                     from X -> n__from X}
  UR:
   {                   dbl X -> n__dbl X,
                     dbl 0() -> 0(),
                     dbl s X -> s n__s n__dbl activate X,
                         s X -> n__s X,
                  activate X -> X,
             activate n__s X -> s X,
           activate n__dbl X -> dbl activate X,
          activate n__dbls X -> dbls activate X,
     activate n__sel(X1, X2) -> sel(activate X1, activate X2),
    activate n__indx(X1, X2) -> indx(activate X1, X2),
          activate n__from X -> from X,
                      dbls X -> n__dbls X,
                  dbls nil() -> nil(),
             dbls cons(X, Y) -> cons(n__dbl activate X, n__dbls activate Y),
                 sel(X1, X2) -> n__sel(X1, X2),
        sel(0(), cons(X, Y)) -> activate X,
        sel(s X, cons(Y, Z)) -> sel(activate X, activate Z),
                indx(X1, X2) -> n__indx(X1, X2),
              indx(nil(), X) -> nil(),
         indx(cons(X, Y), Z) -> cons(n__sel(activate X, activate Z), n__indx(activate Y, activate Z)),
                      from X -> cons(activate X, n__from n__s activate X),
                      from X -> n__from X,
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {
     (activate# n__dbls X -> dbls# activate X, dbls# cons(X, Y) -> activate# Y)
     (activate# n__dbls X -> dbls# activate X, dbls# cons(X, Y) -> activate# X)
     (sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z), sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z))
     (sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z), sel#(s X, cons(Y, Z)) -> activate# Z)
     (sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z), sel#(s X, cons(Y, Z)) -> activate# X)
     (sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z), sel#(0(), cons(X, Y)) -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__indx(X1, X2) -> activate# X1)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__sel(X1, X2) -> activate# X2)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__sel(X1, X2) -> activate# X1)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbls X -> dbls# activate X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbls X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> dbl# activate X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X)
     (activate# n__dbls X -> activate# X, activate# n__from X -> from# X)
     (activate# n__dbls X -> activate# X, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (activate# n__dbls X -> activate# X, activate# n__indx(X1, X2) -> activate# X1)
     (activate# n__dbls X -> activate# X, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (activate# n__dbls X -> activate# X, activate# n__sel(X1, X2) -> activate# X2)
     (activate# n__dbls X -> activate# X, activate# n__sel(X1, X2) -> activate# X1)
     (activate# n__dbls X -> activate# X, activate# n__dbls X -> dbls# activate X)
     (activate# n__dbls X -> activate# X, activate# n__dbls X -> activate# X)
     (activate# n__dbls X -> activate# X, activate# n__dbl X -> activate# X)
     (activate# n__dbls X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (activate# n__dbls X -> activate# X, activate# n__s X -> s# X)
     (dbls# cons(X, Y) -> activate# X, activate# n__from X -> from# X)
     (dbls# cons(X, Y) -> activate# X, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (dbls# cons(X, Y) -> activate# X, activate# n__indx(X1, X2) -> activate# X1)
     (dbls# cons(X, Y) -> activate# X, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (dbls# cons(X, Y) -> activate# X, activate# n__sel(X1, X2) -> activate# X2)
     (dbls# cons(X, Y) -> activate# X, activate# n__sel(X1, X2) -> activate# X1)
     (dbls# cons(X, Y) -> activate# X, activate# n__dbls X -> dbls# activate X)
     (dbls# cons(X, Y) -> activate# X, activate# n__dbls X -> activate# X)
     (dbls# cons(X, Y) -> activate# X, activate# n__dbl X -> activate# X)
     (dbls# cons(X, Y) -> activate# X, activate# n__dbl X -> dbl# activate X)
     (dbls# cons(X, Y) -> activate# X, activate# n__s X -> s# X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__from X -> from# X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__indx(X1, X2) -> activate# X1)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__sel(X1, X2) -> activate# X2)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__sel(X1, X2) -> activate# X1)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__dbls X -> dbls# activate X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__dbls X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> dbl# activate X)
     (sel#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X)
     (from# X -> activate# X, activate# n__from X -> from# X)
     (from# X -> activate# X, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (from# X -> activate# X, activate# n__indx(X1, X2) -> activate# X1)
     (from# X -> activate# X, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (from# X -> activate# X, activate# n__sel(X1, X2) -> activate# X2)
     (from# X -> activate# X, activate# n__sel(X1, X2) -> activate# X1)
     (from# X -> activate# X, activate# n__dbls X -> dbls# activate X)
     (from# X -> activate# X, activate# n__dbls X -> activate# X)
     (from# X -> activate# X, activate# n__dbl X -> activate# X)
     (from# X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (from# X -> activate# X, activate# n__s X -> s# X)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__from X -> from# X)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__indx(X1, X2) -> activate# X1)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__sel(X1, X2) -> activate# X2)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__sel(X1, X2) -> activate# X1)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__dbls X -> dbls# activate X)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__dbls X -> activate# X)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
     (activate# n__sel(X1, X2) -> activate# X1, activate# n__s X -> s# X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__from X -> from# X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (dbls# cons(X, Y) -> activate# Y, activate# n__indx(X1, X2) -> activate# X1)
     (dbls# cons(X, Y) -> activate# Y, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (dbls# cons(X, Y) -> activate# Y, activate# n__sel(X1, X2) -> activate# X2)
     (dbls# cons(X, Y) -> activate# Y, activate# n__sel(X1, X2) -> activate# X1)
     (dbls# cons(X, Y) -> activate# Y, activate# n__dbls X -> dbls# activate X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__dbls X -> activate# X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__dbl X -> activate# X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__dbl X -> dbl# activate X)
     (dbls# cons(X, Y) -> activate# Y, activate# n__s X -> s# X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__s X -> s# X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__dbl X -> dbl# activate X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__dbl X -> activate# X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__dbls X -> activate# X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__dbls X -> dbls# activate X)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__sel(X1, X2) -> activate# X1)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__sel(X1, X2) -> activate# X2)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__indx(X1, X2) -> activate# X1)
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (indx#(cons(X, Y), Z) -> activate# Y, activate# n__from X -> from# X)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__s X -> s# X)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__dbl X -> dbl# activate X)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__dbl X -> activate# X)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__dbls X -> activate# X)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__dbls X -> dbls# activate X)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__sel(X1, X2) -> activate# X1)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__sel(X1, X2) -> activate# X2)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__indx(X1, X2) -> activate# X1)
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (activate# n__indx(X1, X2) -> activate# X1, activate# n__from X -> from# X)
     (activate# n__indx(X1, X2) -> indx#(activate X1, X2), indx#(cons(X, Y), Z) -> activate# X)
     (activate# n__indx(X1, X2) -> indx#(activate X1, X2), indx#(cons(X, Y), Z) -> activate# Y)
     (activate# n__indx(X1, X2) -> indx#(activate X1, X2), indx#(cons(X, Y), Z) -> activate# Z)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__s X -> s# X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__dbl X -> dbl# activate X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__dbl X -> activate# X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__dbls X -> activate# X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__dbls X -> dbls# activate X)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__sel(X1, X2) -> activate# X1)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__sel(X1, X2) -> activate# X2)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__indx(X1, X2) -> activate# X1)
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (indx#(cons(X, Y), Z) -> activate# X, activate# n__from X -> from# X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__s X -> s# X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__dbl X -> dbl# activate X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__dbl X -> activate# X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__dbls X -> activate# X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__dbls X -> dbls# activate X)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__sel(X1, X2) -> activate# X1)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__sel(X1, X2) -> activate# X2)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__indx(X1, X2) -> activate# X1)
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (sel#(0(), cons(X, Y)) -> activate# X, activate# n__from X -> from# X)
     (activate# n__from X -> from# X, from# X -> activate# X)
     (activate# n__dbl X -> activate# X, activate# n__s X -> s# X)
     (activate# n__dbl X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (activate# n__dbl X -> activate# X, activate# n__dbl X -> activate# X)
     (activate# n__dbl X -> activate# X, activate# n__dbls X -> activate# X)
     (activate# n__dbl X -> activate# X, activate# n__dbls X -> dbls# activate X)
     (activate# n__dbl X -> activate# X, activate# n__sel(X1, X2) -> activate# X1)
     (activate# n__dbl X -> activate# X, activate# n__sel(X1, X2) -> activate# X2)
     (activate# n__dbl X -> activate# X, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (activate# n__dbl X -> activate# X, activate# n__indx(X1, X2) -> activate# X1)
     (activate# n__dbl X -> activate# X, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (activate# n__dbl X -> activate# X, activate# n__from X -> from# X)
     (dbl# s X -> activate# X, activate# n__s X -> s# X)
     (dbl# s X -> activate# X, activate# n__dbl X -> dbl# activate X)
     (dbl# s X -> activate# X, activate# n__dbl X -> activate# X)
     (dbl# s X -> activate# X, activate# n__dbls X -> activate# X)
     (dbl# s X -> activate# X, activate# n__dbls X -> dbls# activate X)
     (dbl# s X -> activate# X, activate# n__sel(X1, X2) -> activate# X1)
     (dbl# s X -> activate# X, activate# n__sel(X1, X2) -> activate# X2)
     (dbl# s X -> activate# X, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (dbl# s X -> activate# X, activate# n__indx(X1, X2) -> activate# X1)
     (dbl# s X -> activate# X, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (dbl# s X -> activate# X, activate# n__from X -> from# X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__s X -> s# X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__dbl X -> dbl# activate X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__dbl X -> activate# X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__dbls X -> activate# X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__dbls X -> dbls# activate X)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__sel(X1, X2) -> activate# X1)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__sel(X1, X2) -> activate# X2)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__indx(X1, X2) -> activate# X1)
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (indx#(cons(X, Y), Z) -> activate# Z, activate# n__from X -> from# X)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__s X -> s# X)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__dbl X -> dbl# activate X)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__dbl X -> activate# X)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__dbls X -> activate# X)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__dbls X -> dbls# activate X)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__sel(X1, X2) -> activate# X1)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__sel(X1, X2) -> activate# X2)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__sel(X1, X2) -> sel#(activate X1, activate X2))
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__indx(X1, X2) -> activate# X1)
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__indx(X1, X2) -> indx#(activate X1, X2))
     (activate# n__sel(X1, X2) -> activate# X2, activate# n__from X -> from# X)
     (activate# n__sel(X1, X2) -> sel#(activate X1, activate X2), sel#(0(), cons(X, Y)) -> activate# X)
     (activate# n__sel(X1, X2) -> sel#(activate X1, activate X2), sel#(s X, cons(Y, Z)) -> activate# X)
     (activate# n__sel(X1, X2) -> sel#(activate X1, activate X2), sel#(s X, cons(Y, Z)) -> activate# Z)
     (activate# n__sel(X1, X2) -> sel#(activate X1, activate X2), sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z))
     (activate# n__dbl X -> dbl# activate X, dbl# s X -> s# n__s n__dbl activate X)
     (activate# n__dbl X -> dbl# activate X, dbl# s X -> activate# X)
    }
    STATUS:
     arrows: 0.657845
     SCCS (1):
      Scc:
       {                 dbl# s X -> activate# X,
               activate# n__dbl X -> dbl# activate X,
               activate# n__dbl X -> activate# X,
              activate# n__dbls X -> activate# X,
              activate# n__dbls X -> dbls# activate X,
         activate# n__sel(X1, X2) -> activate# X1,
         activate# n__sel(X1, X2) -> activate# X2,
         activate# n__sel(X1, X2) -> sel#(activate X1, activate X2),
        activate# n__indx(X1, X2) -> activate# X1,
        activate# n__indx(X1, X2) -> indx#(activate X1, X2),
              activate# n__from X -> from# X,
                 dbls# cons(X, Y) -> activate# X,
                 dbls# cons(X, Y) -> activate# Y,
            sel#(0(), cons(X, Y)) -> activate# X,
            sel#(s X, cons(Y, Z)) -> activate# X,
            sel#(s X, cons(Y, Z)) -> activate# Z,
            sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z),
             indx#(cons(X, Y), Z) -> activate# X,
             indx#(cons(X, Y), Z) -> activate# Y,
             indx#(cons(X, Y), Z) -> activate# Z,
                          from# X -> activate# X}
      
      SCC (21):
       Strict:
        {                 dbl# s X -> activate# X,
                activate# n__dbl X -> dbl# activate X,
                activate# n__dbl X -> activate# X,
               activate# n__dbls X -> activate# X,
               activate# n__dbls X -> dbls# activate X,
          activate# n__sel(X1, X2) -> activate# X1,
          activate# n__sel(X1, X2) -> activate# X2,
          activate# n__sel(X1, X2) -> sel#(activate X1, activate X2),
         activate# n__indx(X1, X2) -> activate# X1,
         activate# n__indx(X1, X2) -> indx#(activate X1, X2),
               activate# n__from X -> from# X,
                  dbls# cons(X, Y) -> activate# X,
                  dbls# cons(X, Y) -> activate# Y,
             sel#(0(), cons(X, Y)) -> activate# X,
             sel#(s X, cons(Y, Z)) -> activate# X,
             sel#(s X, cons(Y, Z)) -> activate# Z,
             sel#(s X, cons(Y, Z)) -> sel#(activate X, activate Z),
              indx#(cons(X, Y), Z) -> activate# X,
              indx#(cons(X, Y), Z) -> activate# Y,
              indx#(cons(X, Y), Z) -> activate# Z,
                           from# X -> activate# X}
       Weak:
       {                   dbl X -> n__dbl X,
                         dbl 0() -> 0(),
                         dbl s X -> s n__s n__dbl activate X,
                             s X -> n__s X,
                      activate X -> X,
                 activate n__s X -> s X,
               activate n__dbl X -> dbl activate X,
              activate n__dbls X -> dbls activate X,
         activate n__sel(X1, X2) -> sel(activate X1, activate X2),
        activate n__indx(X1, X2) -> indx(activate X1, X2),
              activate n__from X -> from X,
                          dbls X -> n__dbls X,
                      dbls nil() -> nil(),
                 dbls cons(X, Y) -> cons(n__dbl activate X, n__dbls activate Y),
                     sel(X1, X2) -> n__sel(X1, X2),
            sel(0(), cons(X, Y)) -> activate X,
            sel(s X, cons(Y, Z)) -> sel(activate X, activate Z),
                    indx(X1, X2) -> n__indx(X1, X2),
                  indx(nil(), X) -> nil(),
             indx(cons(X, Y), Z) -> cons(n__sel(activate X, activate Z), n__indx(activate Y, activate Z)),
                          from X -> cons(activate X, n__from n__s activate X),
                          from X -> n__from X}
       Fail