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: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { a__sel^#(X1, X2) -> c_1(X1, X2) , a__sel^#(s(X), cons(Y, Z)) -> c_2(a__sel^#(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), X2) , mark^#(0()) -> c_6() , mark^#(nil()) -> c_7() , mark^#(first(X1, X2)) -> c_8(a__first^#(mark(X1), mark(X2))) , mark^#(from(X)) -> c_9(a__from^#(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^#(sel1(X1, X2)) -> c_15(a__sel1^#(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^#(quote1(X)) -> c_18(a__quote1^#(X)) , mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X))) , mark^#(unquote1(X)) -> c_20(a__unquote1^#(mark(X))) , mark^#(fcons(X1, X2)) -> c_21(a__fcons^#(mark(X1), mark(X2))) , a__first^#(X1, X2) -> c_22(X1, X2) , a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y), X, Z) , a__first^#(0(), Z) -> c_24() , a__from^#(X) -> c_25(mark^#(X), X) , a__from^#(X) -> c_26(X) , a__sel1^#(X1, X2) -> c_27(X1, X2) , a__sel1^#(s(X), cons(Y, Z)) -> c_28(a__sel1^#(mark(X), mark(Z))) , a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X)) , a__quote^#(X) -> c_30(X) , 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))) , a__first1^#(X1, X2) -> c_34(X1, X2) , a__first1^#(s(X), cons(Y, Z)) -> c_35(a__quote^#(Y), a__first1^#(mark(X), mark(Z))) , a__first1^#(0(), Z) -> c_36() , a__quote1^#(X) -> c_37(X) , 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))) , a__unquote^#(X) -> c_41(X) , a__unquote^#(01()) -> c_42() , a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X))) , a__unquote1^#(X) -> c_44(X) , a__unquote1^#(nil1()) -> c_45() , a__unquote1^#(cons1(X, Z)) -> c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z)))) , a__fcons^#(X, Z) -> c_47(mark^#(X), Z) , a__fcons^#(X1, X2) -> c_48(X1, X2) } 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(X1, X2) , a__sel^#(s(X), cons(Y, Z)) -> c_2(a__sel^#(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), X2) , mark^#(0()) -> c_6() , mark^#(nil()) -> c_7() , mark^#(first(X1, X2)) -> c_8(a__first^#(mark(X1), mark(X2))) , mark^#(from(X)) -> c_9(a__from^#(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^#(sel1(X1, X2)) -> c_15(a__sel1^#(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^#(quote1(X)) -> c_18(a__quote1^#(X)) , mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X))) , mark^#(unquote1(X)) -> c_20(a__unquote1^#(mark(X))) , mark^#(fcons(X1, X2)) -> c_21(a__fcons^#(mark(X1), mark(X2))) , a__first^#(X1, X2) -> c_22(X1, X2) , a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y), X, Z) , a__first^#(0(), Z) -> c_24() , a__from^#(X) -> c_25(mark^#(X), X) , a__from^#(X) -> c_26(X) , a__sel1^#(X1, X2) -> c_27(X1, X2) , a__sel1^#(s(X), cons(Y, Z)) -> c_28(a__sel1^#(mark(X), mark(Z))) , a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X)) , a__quote^#(X) -> c_30(X) , 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))) , a__first1^#(X1, X2) -> c_34(X1, X2) , a__first1^#(s(X), cons(Y, Z)) -> c_35(a__quote^#(Y), a__first1^#(mark(X), mark(Z))) , a__first1^#(0(), Z) -> c_36() , a__quote1^#(X) -> c_37(X) , 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))) , a__unquote^#(X) -> c_41(X) , a__unquote^#(01()) -> c_42() , a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X))) , a__unquote1^#(X) -> c_44(X) , a__unquote1^#(nil1()) -> c_45() , a__unquote1^#(cons1(X, Z)) -> c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z)))) , a__fcons^#(X, Z) -> c_47(mark^#(X), Z) , a__fcons^#(X1, X2) -> c_48(X1, X2) } 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: runtime complexity Answer: MAYBE We estimate the number of application of {6,7,10,12,24,32,36,39,42,45} by applications of Pre({6,7,10,12,24,32,36,39,42,45}) = {1,3,4,5,8,11,13,16,17,18,19,20,22,23,25,26,27,29,30,31,34,35,37,38,40,41,43,44,47,48}. Here rules are labeled as follows: DPs: { 1: a__sel^#(X1, X2) -> c_1(X1, X2) , 2: a__sel^#(s(X), cons(Y, Z)) -> c_2(a__sel^#(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), X2) , 6: mark^#(0()) -> c_6() , 7: mark^#(nil()) -> c_7() , 8: mark^#(first(X1, X2)) -> c_8(a__first^#(mark(X1), mark(X2))) , 9: mark^#(from(X)) -> c_9(a__from^#(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))) , 15: mark^#(sel1(X1, X2)) -> c_15(a__sel1^#(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))) , 18: mark^#(quote1(X)) -> c_18(a__quote1^#(X)) , 19: mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X))) , 20: mark^#(unquote1(X)) -> c_20(a__unquote1^#(mark(X))) , 21: mark^#(fcons(X1, X2)) -> c_21(a__fcons^#(mark(X1), mark(X2))) , 22: a__first^#(X1, X2) -> c_22(X1, X2) , 23: a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y), X, Z) , 24: a__first^#(0(), Z) -> c_24() , 25: a__from^#(X) -> c_25(mark^#(X), X) , 26: a__from^#(X) -> c_26(X) , 27: a__sel1^#(X1, X2) -> c_27(X1, X2) , 28: a__sel1^#(s(X), cons(Y, Z)) -> c_28(a__sel1^#(mark(X), mark(Z))) , 29: a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X)) , 30: a__quote^#(X) -> c_30(X) , 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))) , 34: a__first1^#(X1, X2) -> c_34(X1, X2) , 35: a__first1^#(s(X), cons(Y, Z)) -> c_35(a__quote^#(Y), a__first1^#(mark(X), mark(Z))) , 36: a__first1^#(0(), Z) -> c_36() , 37: a__quote1^#(X) -> c_37(X) , 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))) , 41: a__unquote^#(X) -> c_41(X) , 42: a__unquote^#(01()) -> c_42() , 43: a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X))) , 44: a__unquote1^#(X) -> c_44(X) , 45: a__unquote1^#(nil1()) -> c_45() , 46: a__unquote1^#(cons1(X, Z)) -> c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z)))) , 47: a__fcons^#(X, Z) -> c_47(mark^#(X), Z) , 48: a__fcons^#(X1, X2) -> c_48(X1, X2) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__sel^#(X1, X2) -> c_1(X1, X2) , a__sel^#(s(X), cons(Y, Z)) -> c_2(a__sel^#(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), X2) , mark^#(first(X1, X2)) -> c_8(a__first^#(mark(X1), mark(X2))) , mark^#(from(X)) -> c_9(a__from^#(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^#(sel1(X1, X2)) -> c_15(a__sel1^#(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^#(quote1(X)) -> c_18(a__quote1^#(X)) , mark^#(unquote(X)) -> c_19(a__unquote^#(mark(X))) , mark^#(unquote1(X)) -> c_20(a__unquote1^#(mark(X))) , mark^#(fcons(X1, X2)) -> c_21(a__fcons^#(mark(X1), mark(X2))) , a__first^#(X1, X2) -> c_22(X1, X2) , a__first^#(s(X), cons(Y, Z)) -> c_23(mark^#(Y), X, Z) , a__from^#(X) -> c_25(mark^#(X), X) , a__from^#(X) -> c_26(X) , a__sel1^#(X1, X2) -> c_27(X1, X2) , a__sel1^#(s(X), cons(Y, Z)) -> c_28(a__sel1^#(mark(X), mark(Z))) , a__sel1^#(0(), cons(X, Z)) -> c_29(a__quote^#(X)) , a__quote^#(X) -> c_30(X) , a__quote^#(s(X)) -> c_31(a__quote^#(X)) , a__quote^#(sel(X, Z)) -> c_33(a__sel1^#(mark(X), mark(Z))) , a__first1^#(X1, X2) -> c_34(X1, X2) , a__first1^#(s(X), cons(Y, Z)) -> c_35(a__quote^#(Y), a__first1^#(mark(X), mark(Z))) , a__quote1^#(X) -> c_37(X) , 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))) , a__unquote^#(X) -> c_41(X) , a__unquote^#(s1(X)) -> c_43(a__unquote^#(mark(X))) , a__unquote1^#(X) -> c_44(X) , a__unquote1^#(cons1(X, Z)) -> c_46(a__fcons^#(a__unquote(mark(X)), a__unquote1(mark(Z)))) , a__fcons^#(X, Z) -> c_47(mark^#(X), Z) , a__fcons^#(X1, X2) -> c_48(X1, X2) } 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) } Weak DPs: { mark^#(0()) -> c_6() , mark^#(nil()) -> c_7() , mark^#(nil1()) -> c_10() , mark^#(01()) -> c_12() , a__first^#(0(), Z) -> c_24() , a__quote^#(0()) -> c_32() , a__first1^#(0(), Z) -> c_36() , a__quote1^#(nil()) -> c_39() , a__unquote^#(01()) -> c_42() , a__unquote1^#(nil1()) -> c_45() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..