MAYBE
Time: 0.269629
TRS:
 {      mark cons(X1, X2) -> cons(mark X1, X2),
                 mark f X -> a__f mark X,
                 mark g X -> a__g mark X,
                 mark s X -> s mark X,
                 mark 0() -> 0(),
         mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                   a__f X -> cons(mark X, f g X),
                   a__f X -> f X,
                   a__g X -> g X,
                 a__g s X -> s s a__g mark X,
                 a__g 0() -> s 0(),
           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# f X -> mark# X,
                   mark# f X -> a__f# mark X,
                   mark# g X -> mark# X,
                   mark# g X -> a__g# 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__f# X -> mark# X,
                   a__g# s X -> mark# X,
                   a__g# s X -> a__g# 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 f X -> a__f mark X,
                  mark g X -> a__g mark X,
                  mark s X -> s mark X,
                  mark 0() -> 0(),
          mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                    a__f X -> cons(mark X, f g X),
                    a__f X -> f X,
                    a__g X -> g X,
                  a__g s X -> s s a__g mark X,
                  a__g 0() -> s 0(),
            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}
  EDG:
   {(mark# g X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# g X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# g X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# g X -> mark# X, mark# s X -> mark# X)
    (mark# g X -> mark# X, mark# g X -> a__g# mark X)
    (mark# g X -> mark# X, mark# g X -> mark# X)
    (mark# g X -> mark# X, mark# f X -> a__f# mark X)
    (mark# g X -> mark# X, mark# f X -> mark# X)
    (mark# g X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (a__f# X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (a__f# X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__f# X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__f# X -> mark# X, mark# s X -> mark# X)
    (a__f# X -> mark# X, mark# g X -> a__g# mark X)
    (a__f# X -> mark# X, mark# g X -> mark# X)
    (a__f# X -> mark# X, mark# f X -> a__f# mark X)
    (a__f# X -> mark# X, mark# f X -> mark# X)
    (a__f# 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# g X -> a__g# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# g X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# f X -> a__f# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# f X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# f X -> a__f# mark X, a__f# X -> mark# X)
    (a__g# s X -> a__g# mark X, a__g# s X -> a__g# mark X)
    (a__g# s X -> a__g# mark X, a__g# s X -> mark# X)
    (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), 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)) -> 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)
    (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# g X -> a__g# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# g X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# f X -> a__f# mark X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, mark# f X -> mark# X)
    (a__sel#(s X, cons(Y, Z)) -> mark# Z, 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# g X -> a__g# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# g X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# f X -> a__f# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# f X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# f X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# f X -> a__f# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# g X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# g X -> a__g# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
    (mark# cons(X1, X2) -> mark# X1, 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) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# f X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# f X -> a__f# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# g X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# g X -> a__g# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# s 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# g X -> a__g# mark X, a__g# s X -> mark# X)
    (mark# g X -> a__g# mark X, a__g# s X -> a__g# 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# f X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# f X -> a__f# mark X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# g X -> mark# X)
    (a__sel#(0(), cons(X, Y)) -> mark# X, mark# g X -> a__g# 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__g# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (a__g# s X -> mark# X, mark# f X -> mark# X)
    (a__g# s X -> mark# X, mark# f X -> a__f# mark X)
    (a__g# s X -> mark# X, mark# g X -> mark# X)
    (a__g# s X -> mark# X, mark# g X -> a__g# mark X)
    (a__g# s X -> mark# X, mark# s X -> mark# X)
    (a__g# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (a__g# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (a__g# s X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# f X -> mark# X)
    (mark# s X -> mark# X, mark# f X -> a__f# mark X)
    (mark# s X -> mark# X, mark# g X -> mark# X)
    (mark# s X -> mark# X, mark# g X -> a__g# mark X)
    (mark# s X -> mark# X, mark# s X -> mark# X)
    (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# s X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
    (mark# f X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# f X -> mark# X, mark# f X -> mark# X)
    (mark# f X -> mark# X, mark# f X -> a__f# mark X)
    (mark# f X -> mark# X, mark# g X -> mark# X)
    (mark# f X -> mark# X, mark# g X -> a__g# mark X)
    (mark# f X -> mark# X, mark# s X -> mark# X)
    (mark# f X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# f X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# f X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))}
   STATUS:
    arrows: 0.562500
    SCCS (1):
     Scc:
      {      mark# cons(X1, X2) -> mark# X1,
                      mark# f X -> mark# X,
                      mark# f X -> a__f# mark X,
                      mark# g X -> mark# X,
                      mark# g X -> a__g# 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__f# X -> mark# X,
                      a__g# s X -> mark# X,
                      a__g# s X -> a__g# 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 (16):
      Strict:
       {      mark# cons(X1, X2) -> mark# X1,
                       mark# f X -> mark# X,
                       mark# f X -> a__f# mark X,
                       mark# g X -> mark# X,
                       mark# g X -> a__g# 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__f# X -> mark# X,
                       a__g# s X -> mark# X,
                       a__g# s X -> a__g# 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 f X -> a__f mark X,
                      mark g X -> a__g mark X,
                      mark s X -> s mark X,
                      mark 0() -> 0(),
              mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                        a__f X -> cons(mark X, f g X),
                        a__f X -> f X,
                        a__g X -> g X,
                      a__g s X -> s s a__g mark X,
                      a__g 0() -> s 0(),
                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