MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__app(X1, X2) -> app(X1, X2) , a__app(nil(), YS) -> mark(YS) , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) , mark(from(X)) -> a__from(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) , mark(prefix(X)) -> a__prefix(mark(X)) , a__from(X) -> cons(mark(X), from(s(X))) , a__from(X) -> from(X) , a__zWadr(X1, X2) -> zWadr(X1, X2) , a__zWadr(XS, nil()) -> nil() , a__zWadr(nil(), YS) -> nil() , a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) , a__prefix(X) -> prefix(X) } 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) '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 2) '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 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__app^#(X1, X2) -> c_1(X1, X2) , a__app^#(nil(), YS) -> c_2(mark^#(YS)) , a__app^#(cons(X, XS), YS) -> c_3(mark^#(X), XS, YS) , mark^#(nil()) -> c_4() , mark^#(cons(X1, X2)) -> c_5(mark^#(X1), X2) , mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2))) , mark^#(from(X)) -> c_7(a__from^#(mark(X))) , mark^#(s(X)) -> c_8(mark^#(X)) , mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2))) , mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X))) , a__from^#(X) -> c_11(mark^#(X), X) , a__from^#(X) -> c_12(X) , a__zWadr^#(X1, X2) -> c_13(X1, X2) , a__zWadr^#(XS, nil()) -> c_14() , a__zWadr^#(nil(), YS) -> c_15() , a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), XS, YS) , a__prefix^#(L) -> c_17(L, L) , a__prefix^#(X) -> c_18(X) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__app^#(X1, X2) -> c_1(X1, X2) , a__app^#(nil(), YS) -> c_2(mark^#(YS)) , a__app^#(cons(X, XS), YS) -> c_3(mark^#(X), XS, YS) , mark^#(nil()) -> c_4() , mark^#(cons(X1, X2)) -> c_5(mark^#(X1), X2) , mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2))) , mark^#(from(X)) -> c_7(a__from^#(mark(X))) , mark^#(s(X)) -> c_8(mark^#(X)) , mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2))) , mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X))) , a__from^#(X) -> c_11(mark^#(X), X) , a__from^#(X) -> c_12(X) , a__zWadr^#(X1, X2) -> c_13(X1, X2) , a__zWadr^#(XS, nil()) -> c_14() , a__zWadr^#(nil(), YS) -> c_15() , a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), XS, YS) , a__prefix^#(L) -> c_17(L, L) , a__prefix^#(X) -> c_18(X) } Strict Trs: { a__app(X1, X2) -> app(X1, X2) , a__app(nil(), YS) -> mark(YS) , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) , mark(from(X)) -> a__from(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) , mark(prefix(X)) -> a__prefix(mark(X)) , a__from(X) -> cons(mark(X), from(s(X))) , a__from(X) -> from(X) , a__zWadr(X1, X2) -> zWadr(X1, X2) , a__zWadr(XS, nil()) -> nil() , a__zWadr(nil(), YS) -> nil() , a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) , a__prefix(X) -> prefix(X) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {4,14,15} by applications of Pre({4,14,15}) = {1,2,3,5,8,9,11,12,13,16,17,18}. Here rules are labeled as follows: DPs: { 1: a__app^#(X1, X2) -> c_1(X1, X2) , 2: a__app^#(nil(), YS) -> c_2(mark^#(YS)) , 3: a__app^#(cons(X, XS), YS) -> c_3(mark^#(X), XS, YS) , 4: mark^#(nil()) -> c_4() , 5: mark^#(cons(X1, X2)) -> c_5(mark^#(X1), X2) , 6: mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2))) , 7: mark^#(from(X)) -> c_7(a__from^#(mark(X))) , 8: mark^#(s(X)) -> c_8(mark^#(X)) , 9: mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2))) , 10: mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X))) , 11: a__from^#(X) -> c_11(mark^#(X), X) , 12: a__from^#(X) -> c_12(X) , 13: a__zWadr^#(X1, X2) -> c_13(X1, X2) , 14: a__zWadr^#(XS, nil()) -> c_14() , 15: a__zWadr^#(nil(), YS) -> c_15() , 16: a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), XS, YS) , 17: a__prefix^#(L) -> c_17(L, L) , 18: a__prefix^#(X) -> c_18(X) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__app^#(X1, X2) -> c_1(X1, X2) , a__app^#(nil(), YS) -> c_2(mark^#(YS)) , a__app^#(cons(X, XS), YS) -> c_3(mark^#(X), XS, YS) , mark^#(cons(X1, X2)) -> c_5(mark^#(X1), X2) , mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2))) , mark^#(from(X)) -> c_7(a__from^#(mark(X))) , mark^#(s(X)) -> c_8(mark^#(X)) , mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2))) , mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X))) , a__from^#(X) -> c_11(mark^#(X), X) , a__from^#(X) -> c_12(X) , a__zWadr^#(X1, X2) -> c_13(X1, X2) , a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), XS, YS) , a__prefix^#(L) -> c_17(L, L) , a__prefix^#(X) -> c_18(X) } Strict Trs: { a__app(X1, X2) -> app(X1, X2) , a__app(nil(), YS) -> mark(YS) , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) , mark(from(X)) -> a__from(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) , mark(prefix(X)) -> a__prefix(mark(X)) , a__from(X) -> cons(mark(X), from(s(X))) , a__from(X) -> from(X) , a__zWadr(X1, X2) -> zWadr(X1, X2) , a__zWadr(XS, nil()) -> nil() , a__zWadr(nil(), YS) -> nil() , a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) , a__prefix(X) -> prefix(X) } Weak DPs: { mark^#(nil()) -> c_4() , a__zWadr^#(XS, nil()) -> c_14() , a__zWadr^#(nil(), YS) -> c_15() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..