MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { 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, Z)) -> mark(X)
  , mark(s(X)) -> s(mark(X))
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(nil()) -> nil()
  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
  , mark(from(X)) -> a__from(mark(X))
  , mark(nil1()) -> nil1()
  , mark(cons1(X1, X2)) -> cons1(mark(X1), mark(X2))
  , mark(01()) -> 01()
  , mark(s1(X)) -> s1(mark(X))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2))
  , mark(quote(X)) -> a__quote(X)
  , mark(first1(X1, X2)) -> a__first1(mark(X1), mark(X2))
  , mark(quote1(X)) -> a__quote1(X)
  , mark(unquote(X)) -> a__unquote(mark(X))
  , mark(unquote1(X)) -> a__unquote1(mark(X))
  , mark(fcons(X1, X2)) -> a__fcons(mark(X1), mark(X2))
  , a__first(X1, X2) -> first(X1, X2)
  , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
  , a__first(0(), Z) -> nil()
  , a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , a__sel1(X1, X2) -> sel1(X1, X2)
  , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z))
  , a__sel1(0(), cons(X, Z)) -> a__quote(X)
  , a__quote(X) -> quote(X)
  , a__quote(s(X)) -> s1(a__quote(X))
  , a__quote(0()) -> 01()
  , a__quote(sel(X, Z)) -> a__sel1(mark(X), mark(Z))
  , a__first1(X1, X2) -> first1(X1, X2)
  , a__first1(s(X), cons(Y, Z)) ->
    cons1(a__quote(Y), a__first1(mark(X), mark(Z)))
  , a__first1(0(), Z) -> nil1()
  , a__quote1(X) -> quote1(X)
  , a__quote1(cons(X, Z)) -> cons1(a__quote(X), a__quote1(Z))
  , a__quote1(nil()) -> nil1()
  , a__quote1(first(X, Z)) -> a__first1(mark(X), mark(Z))
  , a__unquote(X) -> unquote(X)
  , a__unquote(01()) -> 0()
  , a__unquote(s1(X)) -> s(a__unquote(mark(X)))
  , a__unquote1(X) -> unquote1(X)
  , a__unquote1(nil1()) -> nil()
  , a__unquote1(cons1(X, Z)) ->
    a__fcons(a__unquote(mark(X)), a__unquote1(mark(Z)))
  , a__fcons(X, Z) -> cons(mark(X), Z)
  , a__fcons(X1, X2) -> fcons(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { a__sel^#(X1, X2) -> c_1()
  , a__sel^#(s(X), cons(Y, Z)) ->
    c_2(a__sel^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__sel^#(0(), cons(X, Z)) -> c_3(mark^#(X))
  , mark^#(s(X)) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(0()) -> c_6()
  , mark^#(nil()) -> c_7()
  , mark^#(first(X1, X2)) ->
    c_8(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(from(X)) -> c_9(a__from^#(mark(X)), mark^#(X))
  , mark^#(nil1()) -> c_10()
  , mark^#(cons1(X1, X2)) -> c_11(mark^#(X1), mark^#(X2))
  , mark^#(01()) -> c_12()
  , mark^#(s1(X)) -> c_13(mark^#(X))
  , mark^#(sel(X1, X2)) ->
    c_14(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(sel1(X1, X2)) ->
    c_15(a__sel1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quote(X)) -> c_16(a__quote^#(X))
  , mark^#(first1(X1, X2)) ->
    c_17(a__first1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quote1(X)) -> c_18(a__quote1^#(X))
  , mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X)), mark^#(X))
  , mark^#(unquote1(X)) -> c_20(a__unquote1^#(mark(X)), mark^#(X))
  , mark^#(fcons(X1, X2)) ->
    c_21(a__fcons^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , a__first^#(X1, X2) -> c_22()
  , a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y))
  , a__first^#(0(), Z) -> c_24()
  , a__from^#(X) -> c_25(mark^#(X))
  , a__from^#(X) -> c_26()
  , a__sel1^#(X1, X2) -> c_27()
  , a__sel1^#(s(X), cons(Y, Z)) ->
    c_28(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X))
  , a__quote^#(X) -> c_30()
  , a__quote^#(s(X)) -> c_31(a__quote^#(X))
  , a__quote^#(0()) -> c_32()
  , a__quote^#(sel(X, Z)) ->
    c_33(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__first1^#(X1, X2) -> c_34()
  , a__first1^#(s(X), cons(Y, Z)) ->
    c_35(a__quote^#(Y),
         a__first1^#(mark(X), mark(Z)),
         mark^#(X),
         mark^#(Z))
  , a__first1^#(0(), Z) -> c_36()
  , a__quote1^#(X) -> c_37()
  , a__quote1^#(cons(X, Z)) -> c_38(a__quote^#(X), a__quote1^#(Z))
  , a__quote1^#(nil()) -> c_39()
  , a__quote1^#(first(X, Z)) ->
    c_40(a__first1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__unquote^#(X) -> c_41()
  , a__unquote^#(01()) -> c_42()
  , a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X)), mark^#(X))
  , a__unquote1^#(X) -> c_44()
  , a__unquote1^#(nil1()) -> c_45()
  , a__unquote1^#(cons1(X, Z)) ->
    c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z))),
         a__unquote^#(mark(X)),
         mark^#(X),
         a__unquote1^#(mark(Z)),
         mark^#(Z))
  , a__fcons^#(X, Z) -> c_47(mark^#(X))
  , a__fcons^#(X1, X2) -> c_48() }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { a__sel^#(X1, X2) -> c_1()
  , a__sel^#(s(X), cons(Y, Z)) ->
    c_2(a__sel^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__sel^#(0(), cons(X, Z)) -> c_3(mark^#(X))
  , mark^#(s(X)) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(0()) -> c_6()
  , mark^#(nil()) -> c_7()
  , mark^#(first(X1, X2)) ->
    c_8(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(from(X)) -> c_9(a__from^#(mark(X)), mark^#(X))
  , mark^#(nil1()) -> c_10()
  , mark^#(cons1(X1, X2)) -> c_11(mark^#(X1), mark^#(X2))
  , mark^#(01()) -> c_12()
  , mark^#(s1(X)) -> c_13(mark^#(X))
  , mark^#(sel(X1, X2)) ->
    c_14(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(sel1(X1, X2)) ->
    c_15(a__sel1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quote(X)) -> c_16(a__quote^#(X))
  , mark^#(first1(X1, X2)) ->
    c_17(a__first1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quote1(X)) -> c_18(a__quote1^#(X))
  , mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X)), mark^#(X))
  , mark^#(unquote1(X)) -> c_20(a__unquote1^#(mark(X)), mark^#(X))
  , mark^#(fcons(X1, X2)) ->
    c_21(a__fcons^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , a__first^#(X1, X2) -> c_22()
  , a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y))
  , a__first^#(0(), Z) -> c_24()
  , a__from^#(X) -> c_25(mark^#(X))
  , a__from^#(X) -> c_26()
  , a__sel1^#(X1, X2) -> c_27()
  , a__sel1^#(s(X), cons(Y, Z)) ->
    c_28(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X))
  , a__quote^#(X) -> c_30()
  , a__quote^#(s(X)) -> c_31(a__quote^#(X))
  , a__quote^#(0()) -> c_32()
  , a__quote^#(sel(X, Z)) ->
    c_33(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__first1^#(X1, X2) -> c_34()
  , a__first1^#(s(X), cons(Y, Z)) ->
    c_35(a__quote^#(Y),
         a__first1^#(mark(X), mark(Z)),
         mark^#(X),
         mark^#(Z))
  , a__first1^#(0(), Z) -> c_36()
  , a__quote1^#(X) -> c_37()
  , a__quote1^#(cons(X, Z)) -> c_38(a__quote^#(X), a__quote1^#(Z))
  , a__quote1^#(nil()) -> c_39()
  , a__quote1^#(first(X, Z)) ->
    c_40(a__first1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__unquote^#(X) -> c_41()
  , a__unquote^#(01()) -> c_42()
  , a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X)), mark^#(X))
  , a__unquote1^#(X) -> c_44()
  , a__unquote1^#(nil1()) -> c_45()
  , a__unquote1^#(cons1(X, Z)) ->
    c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z))),
         a__unquote^#(mark(X)),
         mark^#(X),
         a__unquote1^#(mark(Z)),
         mark^#(Z))
  , a__fcons^#(X, Z) -> c_47(mark^#(X))
  , a__fcons^#(X1, X2) -> c_48() }
Weak Trs:
  { 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, Z)) -> mark(X)
  , mark(s(X)) -> s(mark(X))
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(nil()) -> nil()
  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
  , mark(from(X)) -> a__from(mark(X))
  , mark(nil1()) -> nil1()
  , mark(cons1(X1, X2)) -> cons1(mark(X1), mark(X2))
  , mark(01()) -> 01()
  , mark(s1(X)) -> s1(mark(X))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2))
  , mark(quote(X)) -> a__quote(X)
  , mark(first1(X1, X2)) -> a__first1(mark(X1), mark(X2))
  , mark(quote1(X)) -> a__quote1(X)
  , mark(unquote(X)) -> a__unquote(mark(X))
  , mark(unquote1(X)) -> a__unquote1(mark(X))
  , mark(fcons(X1, X2)) -> a__fcons(mark(X1), mark(X2))
  , a__first(X1, X2) -> first(X1, X2)
  , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
  , a__first(0(), Z) -> nil()
  , a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , a__sel1(X1, X2) -> sel1(X1, X2)
  , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z))
  , a__sel1(0(), cons(X, Z)) -> a__quote(X)
  , a__quote(X) -> quote(X)
  , a__quote(s(X)) -> s1(a__quote(X))
  , a__quote(0()) -> 01()
  , a__quote(sel(X, Z)) -> a__sel1(mark(X), mark(Z))
  , a__first1(X1, X2) -> first1(X1, X2)
  , a__first1(s(X), cons(Y, Z)) ->
    cons1(a__quote(Y), a__first1(mark(X), mark(Z)))
  , a__first1(0(), Z) -> nil1()
  , a__quote1(X) -> quote1(X)
  , a__quote1(cons(X, Z)) -> cons1(a__quote(X), a__quote1(Z))
  , a__quote1(nil()) -> nil1()
  , a__quote1(first(X, Z)) -> a__first1(mark(X), mark(Z))
  , a__unquote(X) -> unquote(X)
  , a__unquote(01()) -> 0()
  , a__unquote(s1(X)) -> s(a__unquote(mark(X)))
  , a__unquote1(X) -> unquote1(X)
  , a__unquote1(nil1()) -> nil()
  , a__unquote1(cons1(X, Z)) ->
    a__fcons(a__unquote(mark(X)), a__unquote1(mark(Z)))
  , a__fcons(X, Z) -> cons(mark(X), Z)
  , a__fcons(X1, X2) -> fcons(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{1,6,7,10,12,22,24,26,27,30,32,34,36,37,39,41,42,44,45,48} by
applications of
Pre({1,6,7,10,12,22,24,26,27,30,32,34,36,37,39,41,42,44,45,48}) =
{2,3,4,5,8,9,11,13,14,15,16,17,18,19,20,21,23,25,28,29,31,33,35,38,40,43,46,47}.
Here rules are labeled as follows:

  DPs:
    { 1: a__sel^#(X1, X2) -> c_1()
    , 2: a__sel^#(s(X), cons(Y, Z)) ->
         c_2(a__sel^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
    , 3: a__sel^#(0(), cons(X, Z)) -> c_3(mark^#(X))
    , 4: mark^#(s(X)) -> c_4(mark^#(X))
    , 5: mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
    , 6: mark^#(0()) -> c_6()
    , 7: mark^#(nil()) -> c_7()
    , 8: mark^#(first(X1, X2)) ->
         c_8(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 9: mark^#(from(X)) -> c_9(a__from^#(mark(X)), mark^#(X))
    , 10: mark^#(nil1()) -> c_10()
    , 11: mark^#(cons1(X1, X2)) -> c_11(mark^#(X1), mark^#(X2))
    , 12: mark^#(01()) -> c_12()
    , 13: mark^#(s1(X)) -> c_13(mark^#(X))
    , 14: mark^#(sel(X1, X2)) ->
          c_14(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 15: mark^#(sel1(X1, X2)) ->
          c_15(a__sel1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 16: mark^#(quote(X)) -> c_16(a__quote^#(X))
    , 17: mark^#(first1(X1, X2)) ->
          c_17(a__first1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 18: mark^#(quote1(X)) -> c_18(a__quote1^#(X))
    , 19: mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X)), mark^#(X))
    , 20: mark^#(unquote1(X)) ->
          c_20(a__unquote1^#(mark(X)), mark^#(X))
    , 21: mark^#(fcons(X1, X2)) ->
          c_21(a__fcons^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 22: a__first^#(X1, X2) -> c_22()
    , 23: a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y))
    , 24: a__first^#(0(), Z) -> c_24()
    , 25: a__from^#(X) -> c_25(mark^#(X))
    , 26: a__from^#(X) -> c_26()
    , 27: a__sel1^#(X1, X2) -> c_27()
    , 28: a__sel1^#(s(X), cons(Y, Z)) ->
          c_28(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
    , 29: a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X))
    , 30: a__quote^#(X) -> c_30()
    , 31: a__quote^#(s(X)) -> c_31(a__quote^#(X))
    , 32: a__quote^#(0()) -> c_32()
    , 33: a__quote^#(sel(X, Z)) ->
          c_33(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
    , 34: a__first1^#(X1, X2) -> c_34()
    , 35: a__first1^#(s(X), cons(Y, Z)) ->
          c_35(a__quote^#(Y),
               a__first1^#(mark(X), mark(Z)),
               mark^#(X),
               mark^#(Z))
    , 36: a__first1^#(0(), Z) -> c_36()
    , 37: a__quote1^#(X) -> c_37()
    , 38: a__quote1^#(cons(X, Z)) ->
          c_38(a__quote^#(X), a__quote1^#(Z))
    , 39: a__quote1^#(nil()) -> c_39()
    , 40: a__quote1^#(first(X, Z)) ->
          c_40(a__first1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
    , 41: a__unquote^#(X) -> c_41()
    , 42: a__unquote^#(01()) -> c_42()
    , 43: a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X)), mark^#(X))
    , 44: a__unquote1^#(X) -> c_44()
    , 45: a__unquote1^#(nil1()) -> c_45()
    , 46: a__unquote1^#(cons1(X, Z)) ->
          c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z))),
               a__unquote^#(mark(X)),
               mark^#(X),
               a__unquote1^#(mark(Z)),
               mark^#(Z))
    , 47: a__fcons^#(X, Z) -> c_47(mark^#(X))
    , 48: a__fcons^#(X1, X2) -> c_48() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { a__sel^#(s(X), cons(Y, Z)) ->
    c_2(a__sel^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__sel^#(0(), cons(X, Z)) -> c_3(mark^#(X))
  , mark^#(s(X)) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(first(X1, X2)) ->
    c_8(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(from(X)) -> c_9(a__from^#(mark(X)), mark^#(X))
  , mark^#(cons1(X1, X2)) -> c_11(mark^#(X1), mark^#(X2))
  , mark^#(s1(X)) -> c_13(mark^#(X))
  , mark^#(sel(X1, X2)) ->
    c_14(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(sel1(X1, X2)) ->
    c_15(a__sel1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quote(X)) -> c_16(a__quote^#(X))
  , mark^#(first1(X1, X2)) ->
    c_17(a__first1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quote1(X)) -> c_18(a__quote1^#(X))
  , mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X)), mark^#(X))
  , mark^#(unquote1(X)) -> c_20(a__unquote1^#(mark(X)), mark^#(X))
  , mark^#(fcons(X1, X2)) ->
    c_21(a__fcons^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y))
  , a__from^#(X) -> c_25(mark^#(X))
  , a__sel1^#(s(X), cons(Y, Z)) ->
    c_28(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X))
  , a__quote^#(s(X)) -> c_31(a__quote^#(X))
  , a__quote^#(sel(X, Z)) ->
    c_33(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__first1^#(s(X), cons(Y, Z)) ->
    c_35(a__quote^#(Y),
         a__first1^#(mark(X), mark(Z)),
         mark^#(X),
         mark^#(Z))
  , a__quote1^#(cons(X, Z)) -> c_38(a__quote^#(X), a__quote1^#(Z))
  , a__quote1^#(first(X, Z)) ->
    c_40(a__first1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X)), mark^#(X))
  , a__unquote1^#(cons1(X, Z)) ->
    c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z))),
         a__unquote^#(mark(X)),
         mark^#(X),
         a__unquote1^#(mark(Z)),
         mark^#(Z))
  , a__fcons^#(X, Z) -> c_47(mark^#(X)) }
Weak DPs:
  { a__sel^#(X1, X2) -> c_1()
  , mark^#(0()) -> c_6()
  , mark^#(nil()) -> c_7()
  , mark^#(nil1()) -> c_10()
  , mark^#(01()) -> c_12()
  , a__first^#(X1, X2) -> c_22()
  , a__first^#(0(), Z) -> c_24()
  , a__from^#(X) -> c_26()
  , a__sel1^#(X1, X2) -> c_27()
  , a__quote^#(X) -> c_30()
  , a__quote^#(0()) -> c_32()
  , a__first1^#(X1, X2) -> c_34()
  , a__first1^#(0(), Z) -> c_36()
  , a__quote1^#(X) -> c_37()
  , a__quote1^#(nil()) -> c_39()
  , a__unquote^#(X) -> c_41()
  , a__unquote^#(01()) -> c_42()
  , a__unquote1^#(X) -> c_44()
  , a__unquote1^#(nil1()) -> c_45()
  , a__fcons^#(X1, X2) -> c_48() }
Weak Trs:
  { 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, Z)) -> mark(X)
  , mark(s(X)) -> s(mark(X))
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(nil()) -> nil()
  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
  , mark(from(X)) -> a__from(mark(X))
  , mark(nil1()) -> nil1()
  , mark(cons1(X1, X2)) -> cons1(mark(X1), mark(X2))
  , mark(01()) -> 01()
  , mark(s1(X)) -> s1(mark(X))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2))
  , mark(quote(X)) -> a__quote(X)
  , mark(first1(X1, X2)) -> a__first1(mark(X1), mark(X2))
  , mark(quote1(X)) -> a__quote1(X)
  , mark(unquote(X)) -> a__unquote(mark(X))
  , mark(unquote1(X)) -> a__unquote1(mark(X))
  , mark(fcons(X1, X2)) -> a__fcons(mark(X1), mark(X2))
  , a__first(X1, X2) -> first(X1, X2)
  , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
  , a__first(0(), Z) -> nil()
  , a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , a__sel1(X1, X2) -> sel1(X1, X2)
  , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z))
  , a__sel1(0(), cons(X, Z)) -> a__quote(X)
  , a__quote(X) -> quote(X)
  , a__quote(s(X)) -> s1(a__quote(X))
  , a__quote(0()) -> 01()
  , a__quote(sel(X, Z)) -> a__sel1(mark(X), mark(Z))
  , a__first1(X1, X2) -> first1(X1, X2)
  , a__first1(s(X), cons(Y, Z)) ->
    cons1(a__quote(Y), a__first1(mark(X), mark(Z)))
  , a__first1(0(), Z) -> nil1()
  , a__quote1(X) -> quote1(X)
  , a__quote1(cons(X, Z)) -> cons1(a__quote(X), a__quote1(Z))
  , a__quote1(nil()) -> nil1()
  , a__quote1(first(X, Z)) -> a__first1(mark(X), mark(Z))
  , a__unquote(X) -> unquote(X)
  , a__unquote(01()) -> 0()
  , a__unquote(s1(X)) -> s(a__unquote(mark(X)))
  , a__unquote1(X) -> unquote1(X)
  , a__unquote1(nil1()) -> nil()
  , a__unquote1(cons1(X, Z)) ->
    a__fcons(a__unquote(mark(X)), a__unquote1(mark(Z)))
  , a__fcons(X, Z) -> cons(mark(X), Z)
  , a__fcons(X1, X2) -> fcons(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ a__sel^#(X1, X2) -> c_1()
, mark^#(0()) -> c_6()
, mark^#(nil()) -> c_7()
, mark^#(nil1()) -> c_10()
, mark^#(01()) -> c_12()
, a__first^#(X1, X2) -> c_22()
, a__first^#(0(), Z) -> c_24()
, a__from^#(X) -> c_26()
, a__sel1^#(X1, X2) -> c_27()
, a__quote^#(X) -> c_30()
, a__quote^#(0()) -> c_32()
, a__first1^#(X1, X2) -> c_34()
, a__first1^#(0(), Z) -> c_36()
, a__quote1^#(X) -> c_37()
, a__quote1^#(nil()) -> c_39()
, a__unquote^#(X) -> c_41()
, a__unquote^#(01()) -> c_42()
, a__unquote1^#(X) -> c_44()
, a__unquote1^#(nil1()) -> c_45()
, a__fcons^#(X1, X2) -> c_48() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { a__sel^#(s(X), cons(Y, Z)) ->
    c_2(a__sel^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__sel^#(0(), cons(X, Z)) -> c_3(mark^#(X))
  , mark^#(s(X)) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(first(X1, X2)) ->
    c_8(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(from(X)) -> c_9(a__from^#(mark(X)), mark^#(X))
  , mark^#(cons1(X1, X2)) -> c_11(mark^#(X1), mark^#(X2))
  , mark^#(s1(X)) -> c_13(mark^#(X))
  , mark^#(sel(X1, X2)) ->
    c_14(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(sel1(X1, X2)) ->
    c_15(a__sel1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quote(X)) -> c_16(a__quote^#(X))
  , mark^#(first1(X1, X2)) ->
    c_17(a__first1^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quote1(X)) -> c_18(a__quote1^#(X))
  , mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X)), mark^#(X))
  , mark^#(unquote1(X)) -> c_20(a__unquote1^#(mark(X)), mark^#(X))
  , mark^#(fcons(X1, X2)) ->
    c_21(a__fcons^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y))
  , a__from^#(X) -> c_25(mark^#(X))
  , a__sel1^#(s(X), cons(Y, Z)) ->
    c_28(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X))
  , a__quote^#(s(X)) -> c_31(a__quote^#(X))
  , a__quote^#(sel(X, Z)) ->
    c_33(a__sel1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__first1^#(s(X), cons(Y, Z)) ->
    c_35(a__quote^#(Y),
         a__first1^#(mark(X), mark(Z)),
         mark^#(X),
         mark^#(Z))
  , a__quote1^#(cons(X, Z)) -> c_38(a__quote^#(X), a__quote1^#(Z))
  , a__quote1^#(first(X, Z)) ->
    c_40(a__first1^#(mark(X), mark(Z)), mark^#(X), mark^#(Z))
  , a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X)), mark^#(X))
  , a__unquote1^#(cons1(X, Z)) ->
    c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z))),
         a__unquote^#(mark(X)),
         mark^#(X),
         a__unquote1^#(mark(Z)),
         mark^#(Z))
  , a__fcons^#(X, Z) -> c_47(mark^#(X)) }
Weak Trs:
  { 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, Z)) -> mark(X)
  , mark(s(X)) -> s(mark(X))
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(nil()) -> nil()
  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
  , mark(from(X)) -> a__from(mark(X))
  , mark(nil1()) -> nil1()
  , mark(cons1(X1, X2)) -> cons1(mark(X1), mark(X2))
  , mark(01()) -> 01()
  , mark(s1(X)) -> s1(mark(X))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2))
  , mark(quote(X)) -> a__quote(X)
  , mark(first1(X1, X2)) -> a__first1(mark(X1), mark(X2))
  , mark(quote1(X)) -> a__quote1(X)
  , mark(unquote(X)) -> a__unquote(mark(X))
  , mark(unquote1(X)) -> a__unquote1(mark(X))
  , mark(fcons(X1, X2)) -> a__fcons(mark(X1), mark(X2))
  , a__first(X1, X2) -> first(X1, X2)
  , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
  , a__first(0(), Z) -> nil()
  , a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , a__sel1(X1, X2) -> sel1(X1, X2)
  , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z))
  , a__sel1(0(), cons(X, Z)) -> a__quote(X)
  , a__quote(X) -> quote(X)
  , a__quote(s(X)) -> s1(a__quote(X))
  , a__quote(0()) -> 01()
  , a__quote(sel(X, Z)) -> a__sel1(mark(X), mark(Z))
  , a__first1(X1, X2) -> first1(X1, X2)
  , a__first1(s(X), cons(Y, Z)) ->
    cons1(a__quote(Y), a__first1(mark(X), mark(Z)))
  , a__first1(0(), Z) -> nil1()
  , a__quote1(X) -> quote1(X)
  , a__quote1(cons(X, Z)) -> cons1(a__quote(X), a__quote1(Z))
  , a__quote1(nil()) -> nil1()
  , a__quote1(first(X, Z)) -> a__first1(mark(X), mark(Z))
  , a__unquote(X) -> unquote(X)
  , a__unquote(01()) -> 0()
  , a__unquote(s1(X)) -> s(a__unquote(mark(X)))
  , a__unquote1(X) -> unquote1(X)
  , a__unquote1(nil1()) -> nil()
  , a__unquote1(cons1(X, Z)) ->
    a__fcons(a__unquote(mark(X)), a__unquote1(mark(Z)))
  , a__fcons(X, Z) -> cons(mark(X), Z)
  , a__fcons(X1, X2) -> fcons(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..