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)
  ADG 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)
   graph:
    unquote1#(cons1(X,Z)) -> unquote1#(Z) ->
    unquote1#(cons1(X,Z)) -> unquote1#(Z)
    unquote1#(cons1(X,Z)) -> unquote1#(Z) ->
    unquote1#(cons1(X,Z)) -> unquote#(X)
    unquote1#(cons1(X,Z)) -> unquote1#(Z) ->
    unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z))
    unquote1#(cons1(X,Z)) -> unquote#(X) ->
    unquote#(s1(X)) -> unquote#(X)
    unquote#(s1(X)) -> unquote#(X) ->
    unquote#(s1(X)) -> unquote#(X)
    quote1#(first(X,Z)) -> first1#(X,Z) ->
    first1#(s(X),cons(Y,Z)) -> first1#(X,Z)
    quote1#(first(X,Z)) -> first1#(X,Z) ->
    first1#(s(X),cons(Y,Z)) -> quote#(Y)
    quote1#(cons(X,Z)) -> quote1#(Z) ->
    quote1#(cons(X,Z)) -> quote1#(Z)
    quote1#(cons(X,Z)) -> quote1#(Z) ->
    quote1#(cons(X,Z)) -> quote#(X)
    quote1#(cons(X,Z)) -> quote1#(Z) ->
    quote1#(first(X,Z)) -> first1#(X,Z)
    quote1#(cons(X,Z)) -> quote#(X) -> quote#(s(X)) -> quote#(X)
    quote1#(cons(X,Z)) -> quote#(X) ->
    quote#(sel(X,Z)) -> sel1#(X,Z)
    first1#(s(X),cons(Y,Z)) -> first1#(X,Z) ->
    first1#(s(X),cons(Y,Z)) -> first1#(X,Z)
    first1#(s(X),cons(Y,Z)) -> first1#(X,Z) ->
    first1#(s(X),cons(Y,Z)) -> quote#(Y)
    first1#(s(X),cons(Y,Z)) -> quote#(Y) ->
    quote#(s(X)) -> quote#(X)
    first1#(s(X),cons(Y,Z)) -> quote#(Y) ->
    quote#(sel(X,Z)) -> sel1#(X,Z)
    quote#(sel(X,Z)) -> sel1#(X,Z) ->
    sel1#(s(X),cons(Y,Z)) -> sel1#(X,Z)
    quote#(sel(X,Z)) -> sel1#(X,Z) -> sel1#(0(),cons(X,Z)) -> quote#(X)
    quote#(s(X)) -> quote#(X) -> quote#(s(X)) -> quote#(X)
    quote#(s(X)) -> quote#(X) -> quote#(sel(X,Z)) -> sel1#(X,Z)
    sel1#(0(),cons(X,Z)) -> quote#(X) -> quote#(s(X)) -> quote#(X)
    sel1#(0(),cons(X,Z)) -> quote#(X) ->
    quote#(sel(X,Z)) -> sel1#(X,Z)
    sel1#(s(X),cons(Y,Z)) -> sel1#(X,Z) ->
    sel1#(s(X),cons(Y,Z)) -> sel1#(X,Z)
    sel1#(s(X),cons(Y,Z)) -> sel1#(X,Z) -> sel1#(0(),cons(X,Z)) -> quote#(X)
    from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X))
    first#(s(X),cons(Y,Z)) -> first#(X,Z) ->
    first#(s(X),cons(Y,Z)) -> first#(X,Z)
    sel#(s(X),cons(Y,Z)) -> sel#(X,Z) -> sel#(s(X),cons(Y,Z)) -> sel#(X,Z)
   SCC Processor:
    #sccs: 8
    #rules: 11
    #arcs: 27/256
    DPs:
     sel#(s(X),cons(Y,Z)) -> sel#(X,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)
    Open
    
    DPs:
     first#(s(X),cons(Y,Z)) -> first#(X,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)
    Open
    
    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
    
    DPs:
     quote1#(cons(X,Z)) -> quote1#(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)
    Open
    
    DPs:
     first1#(s(X),cons(Y,Z)) -> first1#(X,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)
    Open
    
    DPs:
     quote#(sel(X,Z)) -> sel1#(X,Z)
     sel1#(0(),cons(X,Z)) -> quote#(X)
     quote#(s(X)) -> quote#(X)
     sel1#(s(X),cons(Y,Z)) -> sel1#(X,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)
    Open
    
    DPs:
     unquote1#(cons1(X,Z)) -> 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)
    Open
    
    DPs:
     unquote#(s1(X)) -> unquote#(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