MAYBE
Time: 0.221463
TRS:
 {      mark cons(X1, X2) -> cons(mark X1, X2),
              mark from X -> a__from mark X,
                 mark s X -> s mark X,
                 mark 0() -> 0(),
         mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                a__from X -> cons(mark X, from s X),
                a__from X -> from X,
           a__sel(X1, X2) -> sel(X1, X2),
  a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
  a__sel(0(), cons(X, Y)) -> mark X}
 DP:
  DP:
   {      mark# cons(X1, X2) -> mark# X1,
                mark# from X -> mark# X,
                mark# from X -> a__from# mark X,
                   mark# s 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),
                  a__from# X -> 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),
    a__sel#(0(), cons(X, Y)) -> mark# X}
  TRS:
  {      mark cons(X1, X2) -> cons(mark X1, X2),
               mark from X -> a__from mark X,
                  mark s X -> s mark X,
                  mark 0() -> 0(),
          mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                 a__from X -> cons(mark X, from s X),
                 a__from X -> from X,
            a__sel(X1, X2) -> sel(X1, X2),
   a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
   a__sel(0(), cons(X, Y)) -> mark X}
  UR:
   {      mark cons(X1, X2) -> cons(mark X1, X2),
                mark from X -> a__from mark X,
                   mark s X -> s mark X,
                   mark 0() -> 0(),
           mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                  a__from X -> cons(mark X, from s X),
                  a__from X -> from X,
             a__sel(X1, X2) -> sel(X1, X2),
    a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
    a__sel(0(), cons(X, Y)) -> mark X,
                    a(x, y) -> x,
                    a(x, y) -> y}
   EDG:
    {(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# sel(X1, X2) -> mark# X2)
     (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# s X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# from X -> a__from# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# from X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# cons(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# from X -> a__from# mark X)
     (mark# s X -> mark# X, mark# from X -> mark# X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (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# sel(X1, X2) -> mark# X2)
     (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# s X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# from X -> a__from# mark X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# from X -> mark# X)
     (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# from X -> a__from# mark X, a__from# X -> mark# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# from X -> mark# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# from X -> a__from# mark X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# s X -> mark# X)
     (a__sel#(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (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) -> a__sel#(mark X1, mark X2))
     (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# from X -> mark# X)
     (a__from# X -> mark# X, mark# from X -> a__from# mark X)
     (a__from# X -> mark# X, mark# s X -> mark# X)
     (a__from# X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__from# X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# from X -> mark# X)
     (mark# from X -> mark# X, mark# from X -> a__from# mark X)
     (mark# from X -> mark# X, mark# s X -> mark# X)
     (mark# from X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# from X -> 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), a__sel#(s X, cons(Y, Z)) -> mark# X)
     (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)) -> a__sel#(mark X, mark Z))
     (a__sel#(s X, cons(Y, Z)) -> a__sel#(mark X, mark Z), a__sel#(0(), cons(X, Y)) -> mark# X)
     (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#(s X, cons(Y, Z)) -> mark# Z)
     (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#(0(), cons(X, Y)) -> mark# X)}
    STATUS:
     arrows: 0.500000
     SCCS (1):
      Scc:
       {      mark# cons(X1, X2) -> mark# X1,
                    mark# from X -> mark# X,
                    mark# from X -> a__from# mark X,
                       mark# s 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),
                      a__from# X -> 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),
        a__sel#(0(), cons(X, Y)) -> mark# X}
      
      SCC (12):
       Strict:
        {      mark# cons(X1, X2) -> mark# X1,
                     mark# from X -> mark# X,
                     mark# from X -> a__from# mark X,
                        mark# s 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),
                       a__from# X -> 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),
         a__sel#(0(), cons(X, Y)) -> mark# X}
       Weak:
       {      mark cons(X1, X2) -> cons(mark X1, X2),
                    mark from X -> a__from mark X,
                       mark s X -> s mark X,
                       mark 0() -> 0(),
               mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                      a__from X -> cons(mark X, from s X),
                      a__from X -> from X,
                 a__sel(X1, X2) -> sel(X1, X2),
        a__sel(s X, cons(Y, Z)) -> a__sel(mark X, mark Z),
        a__sel(0(), cons(X, Y)) -> mark X}
       Open