MAYBE
Time: 0.281700
TRS:
 {               a__dbl X -> dbl X,
               a__dbl 0() -> 0(),
               a__dbl s X -> s s dbl X,
                a__dbls X -> dbls X,
            a__dbls nil() -> nil(),
       a__dbls cons(X, Y) -> cons(dbl X, dbls Y),
                 mark 0() -> 0(),
                 mark s X -> s X,
               mark dbl X -> a__dbl mark X,
               mark nil() -> nil(),
        mark cons(X1, X2) -> cons(X1, X2),
              mark dbls X -> a__dbls mark X,
         mark sel(X1, X2) -> a__sel(mark X1, mark X2),
        mark indx(X1, X2) -> a__indx(mark X1, X2),
              mark from X -> a__from X,
           a__sel(X1, X2) -> sel(X1, X2),
  a__sel(0(), cons(X, Y)) -> mark X,
  a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
          a__indx(X1, X2) -> indx(X1, X2),
        a__indx(nil(), X) -> nil(),
   a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)),
                a__from X -> cons(X, from s X),
                a__from X -> from X}
 DP:
  DP:
   {             mark# dbl X -> a__dbl# mark X,
                 mark# dbl X -> mark# X,
                mark# dbls X -> a__dbls# mark X,
                mark# dbls X -> mark# X,
           mark# sel(X1, X2) -> mark# X1,
           mark# sel(X1, X2) -> mark# X2,
           mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
          mark# indx(X1, X2) -> mark# X1,
          mark# indx(X1, X2) -> a__indx#(mark X1, X2),
                mark# from X -> a__from# X,
    a__sel#(0(), cons(X, Y)) -> mark# X,
    a__sel#(s X, cons(Y, Z)) -> mark# X,
    a__sel#(s X, cons(Y, Z)) -> mark# Z,
    a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z)}
  TRS:
  {               a__dbl X -> dbl X,
                a__dbl 0() -> 0(),
                a__dbl s X -> s s dbl X,
                 a__dbls X -> dbls X,
             a__dbls nil() -> nil(),
        a__dbls cons(X, Y) -> cons(dbl X, dbls Y),
                  mark 0() -> 0(),
                  mark s X -> s X,
                mark dbl X -> a__dbl mark X,
                mark nil() -> nil(),
         mark cons(X1, X2) -> cons(X1, X2),
               mark dbls X -> a__dbls mark X,
          mark sel(X1, X2) -> a__sel(mark X1, mark X2),
         mark indx(X1, X2) -> a__indx(mark X1, X2),
               mark from X -> a__from X,
            a__sel(X1, X2) -> sel(X1, X2),
   a__sel(0(), cons(X, Y)) -> mark X,
   a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
           a__indx(X1, X2) -> indx(X1, X2),
         a__indx(nil(), X) -> nil(),
    a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)),
                 a__from X -> cons(X, from s X),
                 a__from X -> from X}
  EDG:
   {(mark# indx(X1, X2) -> mark# X1, mark# from X -> a__from# X)
    (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1)
    (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
    (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> mark# X)
    (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> a__dbls# mark X)
    (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
    (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z))
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> mark# Z)
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s X, cons(Y, Z)) -> mark# X)
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(0(), cons(X, Y)) -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z))
    (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> mark# Z)
    (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(s X, cons(Y, Z)) -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(0(), cons(X, Y)) -> mark# X)
    (mark# dbls X -> mark# X, mark# from X -> a__from# X)
    (mark# dbls X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# dbls X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (mark# dbls X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# dbls X -> mark# X, mark# dbls X -> mark# X)
    (mark# dbls X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (mark# dbls X -> mark# X, mark# dbl X -> mark# X)
    (mark# dbls X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# from X -> a__from# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> a__dbl# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbl X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> a__dbls# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# dbls X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# from X -> a__from# X)
    (mark# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X)
    (mark# dbl X -> mark# X, mark# dbl X -> mark# X)
    (mark# dbl X -> mark# X, mark# dbls X -> a__dbls# mark X)
    (mark# dbl X -> mark# X, mark# dbls X -> mark# X)
    (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# dbl X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# dbl X -> mark# X, mark# indx(X1, X2) -> mark# X1)
    (mark# dbl X -> mark# X, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# dbl X -> mark# X, mark# from X -> a__from# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> a__dbl# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbl X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> a__dbls# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# dbls X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> mark# X2)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> mark# X1)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# from X -> a__from# X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> a__dbls# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# sel(X1, X2) -> mark# X2, mark# from X -> a__from# X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> a__dbls# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> a__indx#(mark X1, X2))
    (mark# sel(X1, X2) -> mark# X1, mark# from X -> a__from# X)}
   STATUS:
    arrows: 0.551020
    SCCS (1):
     Scc:
      {             mark# dbl X -> mark# X,
                   mark# dbls X -> mark# X,
              mark# sel(X1, X2) -> mark# X1,
              mark# sel(X1, X2) -> mark# X2,
              mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
             mark# indx(X1, X2) -> mark# X1,
       a__sel#(0(), cons(X, Y)) -> mark# X,
       a__sel#(s X, cons(Y, Z)) -> mark# X,
       a__sel#(s X, cons(Y, Z)) -> mark# Z,
       a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z)}
     
     SCC (10):
      Strict:
       {             mark# dbl X -> mark# X,
                    mark# dbls X -> mark# X,
               mark# sel(X1, X2) -> mark# X1,
               mark# sel(X1, X2) -> mark# X2,
               mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
              mark# indx(X1, X2) -> mark# X1,
        a__sel#(0(), cons(X, Y)) -> mark# X,
        a__sel#(s X, cons(Y, Z)) -> mark# X,
        a__sel#(s X, cons(Y, Z)) -> mark# Z,
        a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z)}
      Weak:
      {               a__dbl X -> dbl X,
                    a__dbl 0() -> 0(),
                    a__dbl s X -> s s dbl X,
                     a__dbls X -> dbls X,
                 a__dbls nil() -> nil(),
            a__dbls cons(X, Y) -> cons(dbl X, dbls Y),
                      mark 0() -> 0(),
                      mark s X -> s X,
                    mark dbl X -> a__dbl mark X,
                    mark nil() -> nil(),
             mark cons(X1, X2) -> cons(X1, X2),
                   mark dbls X -> a__dbls mark X,
              mark sel(X1, X2) -> a__sel(mark X1, mark X2),
             mark indx(X1, X2) -> a__indx(mark X1, X2),
                   mark from X -> a__from X,
                a__sel(X1, X2) -> sel(X1, X2),
       a__sel(0(), cons(X, Y)) -> mark X,
       a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
               a__indx(X1, X2) -> indx(X1, X2),
             a__indx(nil(), X) -> nil(),
        a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)),
                     a__from X -> cons(X, from s X),
                     a__from X -> from X}
      Open