MAYBE 770.71/297.12 MAYBE 770.71/297.12 770.71/297.12 We are left with following problem, upon which TcT provides the 770.71/297.12 certificate MAYBE. 770.71/297.12 770.71/297.12 Strict Trs: 770.71/297.12 { app(X1, X2) -> n__app(X1, X2) 770.71/297.12 , app(nil(), YS) -> YS 770.71/297.12 , app(cons(X, XS), YS) -> cons(X, n__app(activate(XS), YS)) 770.71/297.12 , nil() -> n__nil() 770.71/297.12 , activate(X) -> X 770.71/297.12 , activate(n__app(X1, X2)) -> app(activate(X1), activate(X2)) 770.71/297.12 , activate(n__from(X)) -> from(activate(X)) 770.71/297.12 , activate(n__s(X)) -> s(activate(X)) 770.71/297.12 , activate(n__nil()) -> nil() 770.71/297.12 , activate(n__zWadr(X1, X2)) -> zWadr(activate(X1), activate(X2)) 770.71/297.12 , activate(n__prefix(X)) -> prefix(activate(X)) 770.71/297.12 , from(X) -> cons(X, n__from(n__s(X))) 770.71/297.12 , from(X) -> n__from(X) 770.71/297.12 , zWadr(X1, X2) -> n__zWadr(X1, X2) 770.71/297.12 , zWadr(XS, nil()) -> nil() 770.71/297.12 , zWadr(nil(), YS) -> nil() 770.71/297.12 , zWadr(cons(X, XS), cons(Y, YS)) -> 770.71/297.12 cons(app(Y, cons(X, n__nil())), 770.71/297.12 n__zWadr(activate(XS), activate(YS))) 770.71/297.12 , prefix(L) -> cons(nil(), n__zWadr(L, n__prefix(L))) 770.71/297.12 , prefix(X) -> n__prefix(X) 770.71/297.12 , s(X) -> n__s(X) } 770.71/297.12 Obligation: 770.71/297.12 runtime complexity 770.71/297.12 Answer: 770.71/297.12 MAYBE 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 770.71/297.12 following reason: 770.71/297.12 770.71/297.12 Computation stopped due to timeout after 297.0 seconds. 770.71/297.12 770.71/297.12 2) 'Best' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 770.71/297.12 seconds)' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'empty' failed due to the following reason: 770.71/297.12 770.71/297.12 Empty strict component of the problem is NOT empty. 770.71/297.12 770.71/297.12 2) 'With Problem ...' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'empty' failed due to the following reason: 770.71/297.12 770.71/297.12 Empty strict component of the problem is NOT empty. 770.71/297.12 770.71/297.12 2) 'Fastest' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'With Problem ...' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'empty' failed due to the following reason: 770.71/297.12 770.71/297.12 Empty strict component of the problem is NOT empty. 770.71/297.12 770.71/297.12 2) 'With Problem ...' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'empty' failed due to the following reason: 770.71/297.12 770.71/297.12 Empty strict component of the problem is NOT empty. 770.71/297.12 770.71/297.12 2) 'With Problem ...' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'empty' failed due to the following reason: 770.71/297.12 770.71/297.12 Empty strict component of the problem is NOT empty. 770.71/297.12 770.71/297.12 2) 'With Problem ...' failed due to the following reason: 770.71/297.12 770.71/297.12 Empty strict component of the problem is NOT empty. 770.71/297.12 770.71/297.12 770.71/297.12 770.71/297.12 770.71/297.12 2) 'With Problem ...' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'empty' failed due to the following reason: 770.71/297.12 770.71/297.12 Empty strict component of the problem is NOT empty. 770.71/297.12 770.71/297.12 2) 'With Problem ...' failed due to the following reason: 770.71/297.12 770.71/297.12 Empty strict component of the problem is NOT empty. 770.71/297.12 770.71/297.12 770.71/297.12 770.71/297.12 770.71/297.12 770.71/297.12 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 770.71/297.12 failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 770.71/297.12 failed due to the following reason: 770.71/297.12 770.71/297.12 match-boundness of the problem could not be verified. 770.71/297.12 770.71/297.12 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 770.71/297.12 failed due to the following reason: 770.71/297.12 770.71/297.12 match-boundness of the problem could not be verified. 770.71/297.12 770.71/297.12 770.71/297.12 3) 'Best' failed due to the following reason: 770.71/297.12 770.71/297.12 None of the processors succeeded. 770.71/297.12 770.71/297.12 Details of failed attempt(s): 770.71/297.12 ----------------------------- 770.71/297.12 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 770.71/297.12 following reason: 770.71/297.12 770.71/297.12 The processor is inapplicable, reason: 770.71/297.12 Processor only applicable for innermost runtime complexity analysis 770.71/297.12 770.71/297.12 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 770.71/297.12 to the following reason: 770.71/297.12 770.71/297.12 The processor is inapplicable, reason: 770.71/297.12 Processor only applicable for innermost runtime complexity analysis 770.71/297.12 770.71/297.12 770.71/297.12 770.71/297.12 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 770.71/297.12 the following reason: 770.71/297.12 770.71/297.12 We add the following weak dependency pairs: 770.71/297.12 770.71/297.12 Strict DPs: 770.71/297.12 { app^#(X1, X2) -> c_1(X1, X2) 770.71/297.12 , app^#(nil(), YS) -> c_2(YS) 770.71/297.12 , app^#(cons(X, XS), YS) -> c_3(X, activate^#(XS), YS) 770.71/297.12 , activate^#(X) -> c_5(X) 770.71/297.12 , activate^#(n__app(X1, X2)) -> 770.71/297.12 c_6(app^#(activate(X1), activate(X2))) 770.71/297.12 , activate^#(n__from(X)) -> c_7(from^#(activate(X))) 770.71/297.12 , activate^#(n__s(X)) -> c_8(s^#(activate(X))) 770.71/297.12 , activate^#(n__nil()) -> c_9(nil^#()) 770.71/297.12 , activate^#(n__zWadr(X1, X2)) -> 770.71/297.12 c_10(zWadr^#(activate(X1), activate(X2))) 770.71/297.12 , activate^#(n__prefix(X)) -> c_11(prefix^#(activate(X))) 770.71/297.12 , nil^#() -> c_4() 770.71/297.12 , from^#(X) -> c_12(X, X) 770.71/297.12 , from^#(X) -> c_13(X) 770.71/297.12 , s^#(X) -> c_20(X) 770.71/297.12 , zWadr^#(X1, X2) -> c_14(X1, X2) 770.71/297.12 , zWadr^#(XS, nil()) -> c_15(nil^#()) 770.71/297.12 , zWadr^#(nil(), YS) -> c_16(nil^#()) 770.71/297.12 , zWadr^#(cons(X, XS), cons(Y, YS)) -> 770.71/297.12 c_17(app^#(Y, cons(X, n__nil())), activate^#(XS), activate^#(YS)) 770.71/297.12 , prefix^#(L) -> c_18(nil^#(), L, L) 770.71/297.12 , prefix^#(X) -> c_19(X) } 770.71/297.12 770.71/297.12 and mark the set of starting terms. 770.71/297.12 770.71/297.12 We are left with following problem, upon which TcT provides the 770.71/297.12 certificate MAYBE. 770.71/297.12 770.71/297.12 Strict DPs: 770.71/297.12 { app^#(X1, X2) -> c_1(X1, X2) 770.71/297.12 , app^#(nil(), YS) -> c_2(YS) 770.71/297.12 , app^#(cons(X, XS), YS) -> c_3(X, activate^#(XS), YS) 770.71/297.12 , activate^#(X) -> c_5(X) 770.71/297.12 , activate^#(n__app(X1, X2)) -> 770.71/297.12 c_6(app^#(activate(X1), activate(X2))) 770.71/297.12 , activate^#(n__from(X)) -> c_7(from^#(activate(X))) 770.71/297.12 , activate^#(n__s(X)) -> c_8(s^#(activate(X))) 770.71/297.12 , activate^#(n__nil()) -> c_9(nil^#()) 770.71/297.12 , activate^#(n__zWadr(X1, X2)) -> 770.71/297.12 c_10(zWadr^#(activate(X1), activate(X2))) 770.71/297.12 , activate^#(n__prefix(X)) -> c_11(prefix^#(activate(X))) 770.71/297.12 , nil^#() -> c_4() 770.71/297.12 , from^#(X) -> c_12(X, X) 770.71/297.12 , from^#(X) -> c_13(X) 770.71/297.12 , s^#(X) -> c_20(X) 770.71/297.12 , zWadr^#(X1, X2) -> c_14(X1, X2) 770.71/297.12 , zWadr^#(XS, nil()) -> c_15(nil^#()) 770.71/297.12 , zWadr^#(nil(), YS) -> c_16(nil^#()) 770.71/297.12 , zWadr^#(cons(X, XS), cons(Y, YS)) -> 770.71/297.12 c_17(app^#(Y, cons(X, n__nil())), activate^#(XS), activate^#(YS)) 770.71/297.12 , prefix^#(L) -> c_18(nil^#(), L, L) 770.71/297.12 , prefix^#(X) -> c_19(X) } 770.71/297.12 Strict Trs: 770.71/297.12 { app(X1, X2) -> n__app(X1, X2) 770.71/297.12 , app(nil(), YS) -> YS 770.71/297.12 , app(cons(X, XS), YS) -> cons(X, n__app(activate(XS), YS)) 770.71/297.12 , nil() -> n__nil() 770.71/297.12 , activate(X) -> X 770.71/297.12 , activate(n__app(X1, X2)) -> app(activate(X1), activate(X2)) 770.71/297.12 , activate(n__from(X)) -> from(activate(X)) 770.71/297.12 , activate(n__s(X)) -> s(activate(X)) 770.71/297.12 , activate(n__nil()) -> nil() 770.71/297.12 , activate(n__zWadr(X1, X2)) -> zWadr(activate(X1), activate(X2)) 770.71/297.12 , activate(n__prefix(X)) -> prefix(activate(X)) 770.71/297.12 , from(X) -> cons(X, n__from(n__s(X))) 770.71/297.12 , from(X) -> n__from(X) 770.71/297.12 , zWadr(X1, X2) -> n__zWadr(X1, X2) 770.71/297.12 , zWadr(XS, nil()) -> nil() 770.71/297.12 , zWadr(nil(), YS) -> nil() 770.71/297.12 , zWadr(cons(X, XS), cons(Y, YS)) -> 770.71/297.12 cons(app(Y, cons(X, n__nil())), 770.71/297.12 n__zWadr(activate(XS), activate(YS))) 770.71/297.12 , prefix(L) -> cons(nil(), n__zWadr(L, n__prefix(L))) 770.71/297.12 , prefix(X) -> n__prefix(X) 770.71/297.12 , s(X) -> n__s(X) } 770.71/297.12 Obligation: 770.71/297.12 runtime complexity 770.71/297.12 Answer: 770.71/297.12 MAYBE 770.71/297.12 770.71/297.12 We estimate the number of application of {11} by applications of 770.71/297.12 Pre({11}) = {1,2,3,4,8,12,13,14,15,16,17,19,20}. Here rules are 770.71/297.12 labeled as follows: 770.71/297.12 770.71/297.12 DPs: 770.71/297.12 { 1: app^#(X1, X2) -> c_1(X1, X2) 770.71/297.12 , 2: app^#(nil(), YS) -> c_2(YS) 770.71/297.12 , 3: app^#(cons(X, XS), YS) -> c_3(X, activate^#(XS), YS) 770.71/297.12 , 4: activate^#(X) -> c_5(X) 770.71/297.12 , 5: activate^#(n__app(X1, X2)) -> 770.71/297.12 c_6(app^#(activate(X1), activate(X2))) 770.71/297.12 , 6: activate^#(n__from(X)) -> c_7(from^#(activate(X))) 770.71/297.12 , 7: activate^#(n__s(X)) -> c_8(s^#(activate(X))) 770.71/297.12 , 8: activate^#(n__nil()) -> c_9(nil^#()) 770.71/297.12 , 9: activate^#(n__zWadr(X1, X2)) -> 770.71/297.12 c_10(zWadr^#(activate(X1), activate(X2))) 770.71/297.12 , 10: activate^#(n__prefix(X)) -> c_11(prefix^#(activate(X))) 770.71/297.12 , 11: nil^#() -> c_4() 770.71/297.12 , 12: from^#(X) -> c_12(X, X) 770.71/297.12 , 13: from^#(X) -> c_13(X) 770.71/297.12 , 14: s^#(X) -> c_20(X) 770.71/297.12 , 15: zWadr^#(X1, X2) -> c_14(X1, X2) 770.71/297.12 , 16: zWadr^#(XS, nil()) -> c_15(nil^#()) 770.71/297.12 , 17: zWadr^#(nil(), YS) -> c_16(nil^#()) 770.71/297.12 , 18: zWadr^#(cons(X, XS), cons(Y, YS)) -> 770.71/297.12 c_17(app^#(Y, cons(X, n__nil())), activate^#(XS), activate^#(YS)) 770.71/297.12 , 19: prefix^#(L) -> c_18(nil^#(), L, L) 770.71/297.12 , 20: prefix^#(X) -> c_19(X) } 770.71/297.12 770.71/297.12 We are left with following problem, upon which TcT provides the 770.71/297.12 certificate MAYBE. 770.71/297.12 770.71/297.12 Strict DPs: 770.71/297.12 { app^#(X1, X2) -> c_1(X1, X2) 770.71/297.12 , app^#(nil(), YS) -> c_2(YS) 770.71/297.12 , app^#(cons(X, XS), YS) -> c_3(X, activate^#(XS), YS) 770.71/297.12 , activate^#(X) -> c_5(X) 770.71/297.12 , activate^#(n__app(X1, X2)) -> 770.71/297.12 c_6(app^#(activate(X1), activate(X2))) 770.71/297.12 , activate^#(n__from(X)) -> c_7(from^#(activate(X))) 770.71/297.12 , activate^#(n__s(X)) -> c_8(s^#(activate(X))) 770.71/297.12 , activate^#(n__nil()) -> c_9(nil^#()) 770.71/297.12 , activate^#(n__zWadr(X1, X2)) -> 770.71/297.12 c_10(zWadr^#(activate(X1), activate(X2))) 770.71/297.12 , activate^#(n__prefix(X)) -> c_11(prefix^#(activate(X))) 770.71/297.12 , from^#(X) -> c_12(X, X) 770.71/297.12 , from^#(X) -> c_13(X) 770.71/297.12 , s^#(X) -> c_20(X) 770.71/297.12 , zWadr^#(X1, X2) -> c_14(X1, X2) 770.71/297.12 , zWadr^#(XS, nil()) -> c_15(nil^#()) 770.71/297.13 , zWadr^#(nil(), YS) -> c_16(nil^#()) 770.71/297.13 , zWadr^#(cons(X, XS), cons(Y, YS)) -> 770.71/297.13 c_17(app^#(Y, cons(X, n__nil())), activate^#(XS), activate^#(YS)) 770.71/297.13 , prefix^#(L) -> c_18(nil^#(), L, L) 770.71/297.13 , prefix^#(X) -> c_19(X) } 770.71/297.13 Strict Trs: 770.71/297.13 { app(X1, X2) -> n__app(X1, X2) 770.71/297.13 , app(nil(), YS) -> YS 770.71/297.13 , app(cons(X, XS), YS) -> cons(X, n__app(activate(XS), YS)) 770.71/297.13 , nil() -> n__nil() 770.71/297.13 , activate(X) -> X 770.71/297.13 , activate(n__app(X1, X2)) -> app(activate(X1), activate(X2)) 770.71/297.13 , activate(n__from(X)) -> from(activate(X)) 770.71/297.13 , activate(n__s(X)) -> s(activate(X)) 770.71/297.13 , activate(n__nil()) -> nil() 770.71/297.13 , activate(n__zWadr(X1, X2)) -> zWadr(activate(X1), activate(X2)) 770.71/297.13 , activate(n__prefix(X)) -> prefix(activate(X)) 770.71/297.13 , from(X) -> cons(X, n__from(n__s(X))) 770.71/297.13 , from(X) -> n__from(X) 770.71/297.13 , zWadr(X1, X2) -> n__zWadr(X1, X2) 770.71/297.13 , zWadr(XS, nil()) -> nil() 770.71/297.13 , zWadr(nil(), YS) -> nil() 770.71/297.13 , zWadr(cons(X, XS), cons(Y, YS)) -> 770.71/297.13 cons(app(Y, cons(X, n__nil())), 770.71/297.13 n__zWadr(activate(XS), activate(YS))) 770.71/297.13 , prefix(L) -> cons(nil(), n__zWadr(L, n__prefix(L))) 770.71/297.13 , prefix(X) -> n__prefix(X) 770.71/297.13 , s(X) -> n__s(X) } 770.71/297.13 Weak DPs: { nil^#() -> c_4() } 770.71/297.13 Obligation: 770.71/297.13 runtime complexity 770.71/297.13 Answer: 770.71/297.13 MAYBE 770.71/297.13 770.71/297.13 We estimate the number of application of {8,15,16} by applications 770.71/297.13 of Pre({8,15,16}) = {1,2,3,4,9,11,12,13,14,17,18,19}. Here rules 770.71/297.13 are labeled as follows: 770.71/297.13 770.71/297.13 DPs: 770.71/297.13 { 1: app^#(X1, X2) -> c_1(X1, X2) 770.71/297.13 , 2: app^#(nil(), YS) -> c_2(YS) 770.71/297.13 , 3: app^#(cons(X, XS), YS) -> c_3(X, activate^#(XS), YS) 770.71/297.13 , 4: activate^#(X) -> c_5(X) 770.71/297.13 , 5: activate^#(n__app(X1, X2)) -> 770.71/297.13 c_6(app^#(activate(X1), activate(X2))) 770.71/297.13 , 6: activate^#(n__from(X)) -> c_7(from^#(activate(X))) 770.71/297.13 , 7: activate^#(n__s(X)) -> c_8(s^#(activate(X))) 770.71/297.13 , 8: activate^#(n__nil()) -> c_9(nil^#()) 770.71/297.13 , 9: activate^#(n__zWadr(X1, X2)) -> 770.71/297.13 c_10(zWadr^#(activate(X1), activate(X2))) 770.71/297.13 , 10: activate^#(n__prefix(X)) -> c_11(prefix^#(activate(X))) 770.71/297.13 , 11: from^#(X) -> c_12(X, X) 770.71/297.13 , 12: from^#(X) -> c_13(X) 770.71/297.13 , 13: s^#(X) -> c_20(X) 770.71/297.13 , 14: zWadr^#(X1, X2) -> c_14(X1, X2) 770.71/297.13 , 15: zWadr^#(XS, nil()) -> c_15(nil^#()) 770.71/297.13 , 16: zWadr^#(nil(), YS) -> c_16(nil^#()) 770.71/297.13 , 17: zWadr^#(cons(X, XS), cons(Y, YS)) -> 770.71/297.13 c_17(app^#(Y, cons(X, n__nil())), activate^#(XS), activate^#(YS)) 770.71/297.13 , 18: prefix^#(L) -> c_18(nil^#(), L, L) 770.71/297.13 , 19: prefix^#(X) -> c_19(X) 770.71/297.13 , 20: nil^#() -> c_4() } 770.71/297.13 770.71/297.13 We are left with following problem, upon which TcT provides the 770.71/297.13 certificate MAYBE. 770.71/297.13 770.71/297.13 Strict DPs: 770.71/297.13 { app^#(X1, X2) -> c_1(X1, X2) 770.71/297.13 , app^#(nil(), YS) -> c_2(YS) 770.71/297.13 , app^#(cons(X, XS), YS) -> c_3(X, activate^#(XS), YS) 770.71/297.13 , activate^#(X) -> c_5(X) 770.71/297.13 , activate^#(n__app(X1, X2)) -> 770.71/297.13 c_6(app^#(activate(X1), activate(X2))) 770.71/297.13 , activate^#(n__from(X)) -> c_7(from^#(activate(X))) 770.71/297.13 , activate^#(n__s(X)) -> c_8(s^#(activate(X))) 770.71/297.13 , activate^#(n__zWadr(X1, X2)) -> 770.71/297.13 c_10(zWadr^#(activate(X1), activate(X2))) 770.71/297.13 , activate^#(n__prefix(X)) -> c_11(prefix^#(activate(X))) 770.71/297.13 , from^#(X) -> c_12(X, X) 770.71/297.13 , from^#(X) -> c_13(X) 770.71/297.13 , s^#(X) -> c_20(X) 770.71/297.13 , zWadr^#(X1, X2) -> c_14(X1, X2) 770.71/297.13 , zWadr^#(cons(X, XS), cons(Y, YS)) -> 770.71/297.13 c_17(app^#(Y, cons(X, n__nil())), activate^#(XS), activate^#(YS)) 770.71/297.13 , prefix^#(L) -> c_18(nil^#(), L, L) 770.71/297.13 , prefix^#(X) -> c_19(X) } 770.71/297.13 Strict Trs: 770.71/297.13 { app(X1, X2) -> n__app(X1, X2) 770.71/297.13 , app(nil(), YS) -> YS 770.71/297.13 , app(cons(X, XS), YS) -> cons(X, n__app(activate(XS), YS)) 770.71/297.13 , nil() -> n__nil() 770.71/297.13 , activate(X) -> X 770.71/297.13 , activate(n__app(X1, X2)) -> app(activate(X1), activate(X2)) 770.71/297.13 , activate(n__from(X)) -> from(activate(X)) 770.71/297.13 , activate(n__s(X)) -> s(activate(X)) 770.71/297.13 , activate(n__nil()) -> nil() 770.71/297.13 , activate(n__zWadr(X1, X2)) -> zWadr(activate(X1), activate(X2)) 770.71/297.13 , activate(n__prefix(X)) -> prefix(activate(X)) 770.71/297.13 , from(X) -> cons(X, n__from(n__s(X))) 770.71/297.13 , from(X) -> n__from(X) 770.71/297.13 , zWadr(X1, X2) -> n__zWadr(X1, X2) 770.71/297.13 , zWadr(XS, nil()) -> nil() 770.71/297.13 , zWadr(nil(), YS) -> nil() 770.71/297.13 , zWadr(cons(X, XS), cons(Y, YS)) -> 770.71/297.13 cons(app(Y, cons(X, n__nil())), 770.71/297.13 n__zWadr(activate(XS), activate(YS))) 770.71/297.13 , prefix(L) -> cons(nil(), n__zWadr(L, n__prefix(L))) 770.71/297.13 , prefix(X) -> n__prefix(X) 770.71/297.13 , s(X) -> n__s(X) } 770.71/297.13 Weak DPs: 770.71/297.13 { activate^#(n__nil()) -> c_9(nil^#()) 770.71/297.13 , nil^#() -> c_4() 770.71/297.13 , zWadr^#(XS, nil()) -> c_15(nil^#()) 770.71/297.13 , zWadr^#(nil(), YS) -> c_16(nil^#()) } 770.71/297.13 Obligation: 770.71/297.13 runtime complexity 770.71/297.13 Answer: 770.71/297.13 MAYBE 770.71/297.13 770.71/297.13 Empty strict component of the problem is NOT empty. 770.71/297.13 770.71/297.13 770.71/297.13 Arrrr.. 770.85/297.22 EOF