MAYBE

Problem:
 sel(s(X),cons(Y,Z)) -> sel(X,Z)
 sel(0(),cons(X,Z)) -> X
 first(0(),Z) -> nil()
 first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
 from(X) -> cons(X,from(s(X)))
 sel1(s(X),cons(Y,Z)) -> sel1(X,Z)
 sel1(0(),cons(X,Z)) -> quote(X)
 first1(0(),Z) -> nil1()
 first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z))
 quote(0()) -> 01()
 quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z))
 quote1(nil()) -> nil1()
 quote(s(X)) -> s1(quote(X))
 quote(sel(X,Z)) -> sel1(X,Z)
 quote1(first(X,Z)) -> first1(X,Z)
 unquote(01()) -> 0()
 unquote(s1(X)) -> s(unquote(X))
 unquote1(nil1()) -> nil()
 unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
 fcons(X,Z) -> cons(X,Z)

Proof:
 DP Processor:
  DPs:
   sel#(s(X),cons(Y,Z)) -> sel#(X,Z)
   first#(s(X),cons(Y,Z)) -> first#(X,Z)
   from#(X) -> from#(s(X))
   sel1#(s(X),cons(Y,Z)) -> sel1#(X,Z)
   sel1#(0(),cons(X,Z)) -> quote#(X)
   first1#(s(X),cons(Y,Z)) -> first1#(X,Z)
   first1#(s(X),cons(Y,Z)) -> quote#(Y)
   quote1#(cons(X,Z)) -> quote1#(Z)
   quote1#(cons(X,Z)) -> quote#(X)
   quote#(s(X)) -> quote#(X)
   quote#(sel(X,Z)) -> sel1#(X,Z)
   quote1#(first(X,Z)) -> first1#(X,Z)
   unquote#(s1(X)) -> unquote#(X)
   unquote1#(cons1(X,Z)) -> unquote1#(Z)
   unquote1#(cons1(X,Z)) -> unquote#(X)
   unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z))
  TRS:
   sel(s(X),cons(Y,Z)) -> sel(X,Z)
   sel(0(),cons(X,Z)) -> X
   first(0(),Z) -> nil()
   first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
   from(X) -> cons(X,from(s(X)))
   sel1(s(X),cons(Y,Z)) -> sel1(X,Z)
   sel1(0(),cons(X,Z)) -> quote(X)
   first1(0(),Z) -> nil1()
   first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z))
   quote(0()) -> 01()
   quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z))
   quote1(nil()) -> nil1()
   quote(s(X)) -> s1(quote(X))
   quote(sel(X,Z)) -> sel1(X,Z)
   quote1(first(X,Z)) -> first1(X,Z)
   unquote(01()) -> 0()
   unquote(s1(X)) -> s(unquote(X))
   unquote1(nil1()) -> nil()
   unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
   fcons(X,Z) -> cons(X,Z)
  Usable Rule Processor:
   DPs:
    sel#(s(X),cons(Y,Z)) -> sel#(X,Z)
    first#(s(X),cons(Y,Z)) -> first#(X,Z)
    from#(X) -> from#(s(X))
    sel1#(s(X),cons(Y,Z)) -> sel1#(X,Z)
    sel1#(0(),cons(X,Z)) -> quote#(X)
    first1#(s(X),cons(Y,Z)) -> first1#(X,Z)
    first1#(s(X),cons(Y,Z)) -> quote#(Y)
    quote1#(cons(X,Z)) -> quote1#(Z)
    quote1#(cons(X,Z)) -> quote#(X)
    quote#(s(X)) -> quote#(X)
    quote#(sel(X,Z)) -> sel1#(X,Z)
    quote1#(first(X,Z)) -> first1#(X,Z)
    unquote#(s1(X)) -> unquote#(X)
    unquote1#(cons1(X,Z)) -> unquote1#(Z)
    unquote1#(cons1(X,Z)) -> unquote#(X)
    unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z))
   TRS:
    unquote1(nil1()) -> nil()
    unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
    fcons(X,Z) -> cons(X,Z)
    unquote(01()) -> 0()
    unquote(s1(X)) -> s(unquote(X))
   CDG Processor:
    DPs:
     sel#(s(X),cons(Y,Z)) -> sel#(X,Z)
     first#(s(X),cons(Y,Z)) -> first#(X,Z)
     from#(X) -> from#(s(X))
     sel1#(s(X),cons(Y,Z)) -> sel1#(X,Z)
     sel1#(0(),cons(X,Z)) -> quote#(X)
     first1#(s(X),cons(Y,Z)) -> first1#(X,Z)
     first1#(s(X),cons(Y,Z)) -> quote#(Y)
     quote1#(cons(X,Z)) -> quote1#(Z)
     quote1#(cons(X,Z)) -> quote#(X)
     quote#(s(X)) -> quote#(X)
     quote#(sel(X,Z)) -> sel1#(X,Z)
     quote1#(first(X,Z)) -> first1#(X,Z)
     unquote#(s1(X)) -> unquote#(X)
     unquote1#(cons1(X,Z)) -> unquote1#(Z)
     unquote1#(cons1(X,Z)) -> unquote#(X)
     unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z))
    TRS:
     unquote1(nil1()) -> nil()
     unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
     fcons(X,Z) -> cons(X,Z)
     unquote(01()) -> 0()
     unquote(s1(X)) -> s(unquote(X))
    graph:
     from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X))
    Restore Modifier:
     DPs:
      sel#(s(X),cons(Y,Z)) -> sel#(X,Z)
      first#(s(X),cons(Y,Z)) -> first#(X,Z)
      from#(X) -> from#(s(X))
      sel1#(s(X),cons(Y,Z)) -> sel1#(X,Z)
      sel1#(0(),cons(X,Z)) -> quote#(X)
      first1#(s(X),cons(Y,Z)) -> first1#(X,Z)
      first1#(s(X),cons(Y,Z)) -> quote#(Y)
      quote1#(cons(X,Z)) -> quote1#(Z)
      quote1#(cons(X,Z)) -> quote#(X)
      quote#(s(X)) -> quote#(X)
      quote#(sel(X,Z)) -> sel1#(X,Z)
      quote1#(first(X,Z)) -> first1#(X,Z)
      unquote#(s1(X)) -> unquote#(X)
      unquote1#(cons1(X,Z)) -> unquote1#(Z)
      unquote1#(cons1(X,Z)) -> unquote#(X)
      unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z))
     TRS:
      sel(s(X),cons(Y,Z)) -> sel(X,Z)
      sel(0(),cons(X,Z)) -> X
      first(0(),Z) -> nil()
      first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
      from(X) -> cons(X,from(s(X)))
      sel1(s(X),cons(Y,Z)) -> sel1(X,Z)
      sel1(0(),cons(X,Z)) -> quote(X)
      first1(0(),Z) -> nil1()
      first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z))
      quote(0()) -> 01()
      quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z))
      quote1(nil()) -> nil1()
      quote(s(X)) -> s1(quote(X))
      quote(sel(X,Z)) -> sel1(X,Z)
      quote1(first(X,Z)) -> first1(X,Z)
      unquote(01()) -> 0()
      unquote(s1(X)) -> s(unquote(X))
      unquote1(nil1()) -> nil()
      unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
      fcons(X,Z) -> cons(X,Z)
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 1/256
      DPs:
       from#(X) -> from#(s(X))
      TRS:
       sel(s(X),cons(Y,Z)) -> sel(X,Z)
       sel(0(),cons(X,Z)) -> X
       first(0(),Z) -> nil()
       first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
       from(X) -> cons(X,from(s(X)))
       sel1(s(X),cons(Y,Z)) -> sel1(X,Z)
       sel1(0(),cons(X,Z)) -> quote(X)
       first1(0(),Z) -> nil1()
       first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z))
       quote(0()) -> 01()
       quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z))
       quote1(nil()) -> nil1()
       quote(s(X)) -> s1(quote(X))
       quote(sel(X,Z)) -> sel1(X,Z)
       quote1(first(X,Z)) -> first1(X,Z)
       unquote(01()) -> 0()
       unquote(s1(X)) -> s(unquote(X))
       unquote1(nil1()) -> nil()
       unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
       fcons(X,Z) -> cons(X,Z)
      Open