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