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