MAYBE 1049.33/297.04 MAYBE 1049.33/297.04 1049.33/297.04 We are left with following problem, upon which TcT provides the 1049.33/297.04 certificate MAYBE. 1049.33/297.04 1049.33/297.04 Strict Trs: 1049.33/297.04 { active(app(X1, X2)) -> app(X1, active(X2)) 1049.33/297.04 , active(app(X1, X2)) -> app(active(X1), X2) 1049.33/297.04 , active(app(nil(), YS)) -> mark(YS) 1049.33/297.04 , active(app(cons(X, XS), YS)) -> mark(cons(X, app(XS, YS))) 1049.33/297.04 , active(cons(X1, X2)) -> cons(active(X1), X2) 1049.33/297.04 , active(from(X)) -> mark(cons(X, from(s(X)))) 1049.33/297.04 , active(from(X)) -> from(active(X)) 1049.33/297.04 , active(s(X)) -> s(active(X)) 1049.33/297.04 , active(zWadr(X1, X2)) -> zWadr(X1, active(X2)) 1049.33/297.04 , active(zWadr(X1, X2)) -> zWadr(active(X1), X2) 1049.33/297.04 , active(zWadr(XS, nil())) -> mark(nil()) 1049.33/297.04 , active(zWadr(nil(), YS)) -> mark(nil()) 1049.33/297.04 , active(zWadr(cons(X, XS), cons(Y, YS))) -> 1049.33/297.04 mark(cons(app(Y, cons(X, nil())), zWadr(XS, YS))) 1049.33/297.04 , active(prefix(L)) -> mark(cons(nil(), zWadr(L, prefix(L)))) 1049.33/297.04 , active(prefix(X)) -> prefix(active(X)) 1049.33/297.04 , app(X1, mark(X2)) -> mark(app(X1, X2)) 1049.33/297.04 , app(mark(X1), X2) -> mark(app(X1, X2)) 1049.33/297.04 , app(ok(X1), ok(X2)) -> ok(app(X1, X2)) 1049.33/297.04 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1049.33/297.04 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1049.33/297.04 , from(mark(X)) -> mark(from(X)) 1049.33/297.04 , from(ok(X)) -> ok(from(X)) 1049.33/297.04 , s(mark(X)) -> mark(s(X)) 1049.33/297.04 , s(ok(X)) -> ok(s(X)) 1049.33/297.04 , zWadr(X1, mark(X2)) -> mark(zWadr(X1, X2)) 1049.33/297.04 , zWadr(mark(X1), X2) -> mark(zWadr(X1, X2)) 1049.33/297.04 , zWadr(ok(X1), ok(X2)) -> ok(zWadr(X1, X2)) 1049.33/297.04 , prefix(mark(X)) -> mark(prefix(X)) 1049.33/297.04 , prefix(ok(X)) -> ok(prefix(X)) 1049.33/297.04 , proper(app(X1, X2)) -> app(proper(X1), proper(X2)) 1049.33/297.04 , proper(nil()) -> ok(nil()) 1049.33/297.04 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1049.33/297.04 , proper(from(X)) -> from(proper(X)) 1049.33/297.04 , proper(s(X)) -> s(proper(X)) 1049.33/297.04 , proper(zWadr(X1, X2)) -> zWadr(proper(X1), proper(X2)) 1049.33/297.04 , proper(prefix(X)) -> prefix(proper(X)) 1049.33/297.04 , top(mark(X)) -> top(proper(X)) 1049.33/297.04 , top(ok(X)) -> top(active(X)) } 1049.33/297.04 Obligation: 1049.33/297.04 runtime complexity 1049.33/297.04 Answer: 1049.33/297.04 MAYBE 1049.33/297.04 1049.33/297.04 None of the processors succeeded. 1049.33/297.04 1049.33/297.04 Details of failed attempt(s): 1049.33/297.04 ----------------------------- 1049.33/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1049.33/297.04 following reason: 1049.33/297.04 1049.33/297.04 Computation stopped due to timeout after 297.0 seconds. 1049.33/297.04 1049.33/297.04 2) 'Best' failed due to the following reason: 1049.33/297.04 1049.33/297.04 None of the processors succeeded. 1049.33/297.04 1049.33/297.04 Details of failed attempt(s): 1049.33/297.04 ----------------------------- 1049.33/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1049.33/297.04 seconds)' failed due to the following reason: 1049.33/297.04 1049.33/297.04 Computation stopped due to timeout after 148.0 seconds. 1049.33/297.04 1049.33/297.04 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1049.33/297.04 failed due to the following reason: 1049.33/297.04 1049.33/297.04 None of the processors succeeded. 1049.33/297.04 1049.33/297.04 Details of failed attempt(s): 1049.33/297.04 ----------------------------- 1049.33/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1049.33/297.04 failed due to the following reason: 1049.33/297.04 1049.33/297.04 match-boundness of the problem could not be verified. 1049.33/297.04 1049.33/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1049.33/297.04 failed due to the following reason: 1049.33/297.04 1049.33/297.04 match-boundness of the problem could not be verified. 1049.33/297.04 1049.33/297.04 1049.33/297.04 3) 'Best' failed due to the following reason: 1049.33/297.04 1049.33/297.04 None of the processors succeeded. 1049.33/297.04 1049.33/297.04 Details of failed attempt(s): 1049.33/297.04 ----------------------------- 1049.33/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1049.33/297.04 following reason: 1049.33/297.04 1049.33/297.04 The processor is inapplicable, reason: 1049.33/297.04 Processor only applicable for innermost runtime complexity analysis 1049.33/297.04 1049.33/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1049.33/297.04 to the following reason: 1049.33/297.04 1049.33/297.04 The processor is inapplicable, reason: 1049.33/297.04 Processor only applicable for innermost runtime complexity analysis 1049.33/297.04 1049.33/297.04 1049.33/297.04 1049.33/297.04 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1049.33/297.04 the following reason: 1049.33/297.04 1049.33/297.04 We add the following weak dependency pairs: 1049.33/297.04 1049.33/297.04 Strict DPs: 1049.33/297.04 { active^#(app(X1, X2)) -> c_1(app^#(X1, active(X2))) 1049.33/297.04 , active^#(app(X1, X2)) -> c_2(app^#(active(X1), X2)) 1049.33/297.04 , active^#(app(nil(), YS)) -> c_3(YS) 1049.33/297.04 , active^#(app(cons(X, XS), YS)) -> c_4(cons^#(X, app(XS, YS))) 1049.33/297.04 , active^#(cons(X1, X2)) -> c_5(cons^#(active(X1), X2)) 1049.33/297.04 , active^#(from(X)) -> c_6(cons^#(X, from(s(X)))) 1049.33/297.04 , active^#(from(X)) -> c_7(from^#(active(X))) 1049.33/297.04 , active^#(s(X)) -> c_8(s^#(active(X))) 1049.33/297.04 , active^#(zWadr(X1, X2)) -> c_9(zWadr^#(X1, active(X2))) 1049.33/297.04 , active^#(zWadr(X1, X2)) -> c_10(zWadr^#(active(X1), X2)) 1049.33/297.04 , active^#(zWadr(XS, nil())) -> c_11() 1049.33/297.04 , active^#(zWadr(nil(), YS)) -> c_12() 1049.33/297.04 , active^#(zWadr(cons(X, XS), cons(Y, YS))) -> 1049.33/297.04 c_13(cons^#(app(Y, cons(X, nil())), zWadr(XS, YS))) 1049.33/297.04 , active^#(prefix(L)) -> c_14(cons^#(nil(), zWadr(L, prefix(L)))) 1049.33/297.04 , active^#(prefix(X)) -> c_15(prefix^#(active(X))) 1049.33/297.04 , app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) 1049.33/297.04 , app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) 1049.33/297.04 , app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) 1049.33/297.04 , cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) 1049.33/297.04 , cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) 1049.33/297.04 , from^#(mark(X)) -> c_21(from^#(X)) 1049.33/297.04 , from^#(ok(X)) -> c_22(from^#(X)) 1049.33/297.04 , s^#(mark(X)) -> c_23(s^#(X)) 1049.33/297.04 , s^#(ok(X)) -> c_24(s^#(X)) 1049.33/297.04 , zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) 1049.33/297.04 , zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) 1049.33/297.04 , zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) 1049.33/297.04 , prefix^#(mark(X)) -> c_28(prefix^#(X)) 1049.33/297.04 , prefix^#(ok(X)) -> c_29(prefix^#(X)) 1049.33/297.04 , proper^#(app(X1, X2)) -> c_30(app^#(proper(X1), proper(X2))) 1049.33/297.04 , proper^#(nil()) -> c_31() 1049.33/297.04 , proper^#(cons(X1, X2)) -> c_32(cons^#(proper(X1), proper(X2))) 1049.33/297.04 , proper^#(from(X)) -> c_33(from^#(proper(X))) 1049.33/297.04 , proper^#(s(X)) -> c_34(s^#(proper(X))) 1049.33/297.04 , proper^#(zWadr(X1, X2)) -> c_35(zWadr^#(proper(X1), proper(X2))) 1049.33/297.04 , proper^#(prefix(X)) -> c_36(prefix^#(proper(X))) 1049.33/297.04 , top^#(mark(X)) -> c_37(top^#(proper(X))) 1049.33/297.04 , top^#(ok(X)) -> c_38(top^#(active(X))) } 1049.33/297.04 1049.33/297.04 and mark the set of starting terms. 1049.33/297.04 1049.33/297.04 We are left with following problem, upon which TcT provides the 1049.33/297.04 certificate MAYBE. 1049.33/297.04 1049.33/297.04 Strict DPs: 1049.33/297.04 { active^#(app(X1, X2)) -> c_1(app^#(X1, active(X2))) 1049.33/297.04 , active^#(app(X1, X2)) -> c_2(app^#(active(X1), X2)) 1049.33/297.04 , active^#(app(nil(), YS)) -> c_3(YS) 1049.33/297.04 , active^#(app(cons(X, XS), YS)) -> c_4(cons^#(X, app(XS, YS))) 1049.33/297.04 , active^#(cons(X1, X2)) -> c_5(cons^#(active(X1), X2)) 1049.33/297.04 , active^#(from(X)) -> c_6(cons^#(X, from(s(X)))) 1049.33/297.04 , active^#(from(X)) -> c_7(from^#(active(X))) 1049.33/297.04 , active^#(s(X)) -> c_8(s^#(active(X))) 1049.33/297.04 , active^#(zWadr(X1, X2)) -> c_9(zWadr^#(X1, active(X2))) 1049.33/297.04 , active^#(zWadr(X1, X2)) -> c_10(zWadr^#(active(X1), X2)) 1049.33/297.04 , active^#(zWadr(XS, nil())) -> c_11() 1049.33/297.04 , active^#(zWadr(nil(), YS)) -> c_12() 1049.33/297.04 , active^#(zWadr(cons(X, XS), cons(Y, YS))) -> 1049.33/297.04 c_13(cons^#(app(Y, cons(X, nil())), zWadr(XS, YS))) 1049.33/297.04 , active^#(prefix(L)) -> c_14(cons^#(nil(), zWadr(L, prefix(L)))) 1049.33/297.04 , active^#(prefix(X)) -> c_15(prefix^#(active(X))) 1049.33/297.04 , app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) 1049.33/297.04 , app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) 1049.33/297.04 , app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) 1049.33/297.04 , cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) 1049.33/297.04 , cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) 1049.33/297.04 , from^#(mark(X)) -> c_21(from^#(X)) 1049.33/297.04 , from^#(ok(X)) -> c_22(from^#(X)) 1049.33/297.04 , s^#(mark(X)) -> c_23(s^#(X)) 1049.33/297.04 , s^#(ok(X)) -> c_24(s^#(X)) 1049.33/297.04 , zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) 1049.33/297.04 , zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) 1049.33/297.04 , zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) 1049.33/297.04 , prefix^#(mark(X)) -> c_28(prefix^#(X)) 1049.33/297.04 , prefix^#(ok(X)) -> c_29(prefix^#(X)) 1049.33/297.04 , proper^#(app(X1, X2)) -> c_30(app^#(proper(X1), proper(X2))) 1049.33/297.04 , proper^#(nil()) -> c_31() 1049.33/297.04 , proper^#(cons(X1, X2)) -> c_32(cons^#(proper(X1), proper(X2))) 1049.33/297.04 , proper^#(from(X)) -> c_33(from^#(proper(X))) 1049.33/297.04 , proper^#(s(X)) -> c_34(s^#(proper(X))) 1049.33/297.04 , proper^#(zWadr(X1, X2)) -> c_35(zWadr^#(proper(X1), proper(X2))) 1049.33/297.04 , proper^#(prefix(X)) -> c_36(prefix^#(proper(X))) 1049.33/297.04 , top^#(mark(X)) -> c_37(top^#(proper(X))) 1049.33/297.05 , top^#(ok(X)) -> c_38(top^#(active(X))) } 1049.33/297.05 Strict Trs: 1049.33/297.05 { active(app(X1, X2)) -> app(X1, active(X2)) 1049.33/297.05 , active(app(X1, X2)) -> app(active(X1), X2) 1049.33/297.05 , active(app(nil(), YS)) -> mark(YS) 1049.33/297.05 , active(app(cons(X, XS), YS)) -> mark(cons(X, app(XS, YS))) 1049.33/297.05 , active(cons(X1, X2)) -> cons(active(X1), X2) 1049.33/297.05 , active(from(X)) -> mark(cons(X, from(s(X)))) 1049.33/297.05 , active(from(X)) -> from(active(X)) 1049.33/297.05 , active(s(X)) -> s(active(X)) 1049.33/297.05 , active(zWadr(X1, X2)) -> zWadr(X1, active(X2)) 1049.33/297.05 , active(zWadr(X1, X2)) -> zWadr(active(X1), X2) 1049.33/297.05 , active(zWadr(XS, nil())) -> mark(nil()) 1049.33/297.05 , active(zWadr(nil(), YS)) -> mark(nil()) 1049.33/297.05 , active(zWadr(cons(X, XS), cons(Y, YS))) -> 1049.33/297.05 mark(cons(app(Y, cons(X, nil())), zWadr(XS, YS))) 1049.33/297.05 , active(prefix(L)) -> mark(cons(nil(), zWadr(L, prefix(L)))) 1049.33/297.05 , active(prefix(X)) -> prefix(active(X)) 1049.33/297.05 , app(X1, mark(X2)) -> mark(app(X1, X2)) 1049.33/297.05 , app(mark(X1), X2) -> mark(app(X1, X2)) 1049.33/297.05 , app(ok(X1), ok(X2)) -> ok(app(X1, X2)) 1049.33/297.05 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1049.33/297.05 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1049.33/297.05 , from(mark(X)) -> mark(from(X)) 1049.33/297.05 , from(ok(X)) -> ok(from(X)) 1049.33/297.05 , s(mark(X)) -> mark(s(X)) 1049.33/297.05 , s(ok(X)) -> ok(s(X)) 1049.33/297.05 , zWadr(X1, mark(X2)) -> mark(zWadr(X1, X2)) 1049.33/297.05 , zWadr(mark(X1), X2) -> mark(zWadr(X1, X2)) 1049.33/297.05 , zWadr(ok(X1), ok(X2)) -> ok(zWadr(X1, X2)) 1049.33/297.05 , prefix(mark(X)) -> mark(prefix(X)) 1049.33/297.05 , prefix(ok(X)) -> ok(prefix(X)) 1049.33/297.05 , proper(app(X1, X2)) -> app(proper(X1), proper(X2)) 1049.33/297.05 , proper(nil()) -> ok(nil()) 1049.33/297.05 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1049.33/297.05 , proper(from(X)) -> from(proper(X)) 1049.33/297.05 , proper(s(X)) -> s(proper(X)) 1049.33/297.05 , proper(zWadr(X1, X2)) -> zWadr(proper(X1), proper(X2)) 1049.33/297.05 , proper(prefix(X)) -> prefix(proper(X)) 1049.33/297.05 , top(mark(X)) -> top(proper(X)) 1049.33/297.05 , top(ok(X)) -> top(active(X)) } 1049.33/297.05 Obligation: 1049.33/297.05 runtime complexity 1049.33/297.05 Answer: 1049.33/297.05 MAYBE 1049.33/297.05 1049.33/297.05 Consider the dependency graph: 1049.33/297.05 1049.33/297.05 1: active^#(app(X1, X2)) -> c_1(app^#(X1, active(X2))) 1049.33/297.05 -->_1 app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) :18 1049.33/297.05 -->_1 app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) :17 1049.33/297.05 -->_1 app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) :16 1049.33/297.05 1049.33/297.05 2: active^#(app(X1, X2)) -> c_2(app^#(active(X1), X2)) 1049.33/297.05 -->_1 app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) :18 1049.33/297.05 -->_1 app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) :17 1049.33/297.05 -->_1 app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) :16 1049.33/297.05 1049.33/297.05 3: active^#(app(nil(), YS)) -> c_3(YS) 1049.33/297.05 -->_1 top^#(ok(X)) -> c_38(top^#(active(X))) :38 1049.33/297.05 -->_1 top^#(mark(X)) -> c_37(top^#(proper(X))) :37 1049.33/297.05 -->_1 proper^#(prefix(X)) -> c_36(prefix^#(proper(X))) :36 1049.33/297.05 -->_1 proper^#(zWadr(X1, X2)) -> 1049.33/297.05 c_35(zWadr^#(proper(X1), proper(X2))) :35 1049.33/297.05 -->_1 proper^#(s(X)) -> c_34(s^#(proper(X))) :34 1049.33/297.05 -->_1 proper^#(from(X)) -> c_33(from^#(proper(X))) :33 1049.33/297.05 -->_1 proper^#(cons(X1, X2)) -> 1049.33/297.05 c_32(cons^#(proper(X1), proper(X2))) :32 1049.33/297.05 -->_1 proper^#(app(X1, X2)) -> 1049.33/297.05 c_30(app^#(proper(X1), proper(X2))) :30 1049.33/297.05 -->_1 prefix^#(ok(X)) -> c_29(prefix^#(X)) :29 1049.33/297.05 -->_1 prefix^#(mark(X)) -> c_28(prefix^#(X)) :28 1049.33/297.05 -->_1 zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) :27 1049.33/297.05 -->_1 zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) :26 1049.33/297.05 -->_1 zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) :25 1049.33/297.05 -->_1 s^#(ok(X)) -> c_24(s^#(X)) :24 1049.33/297.05 -->_1 s^#(mark(X)) -> c_23(s^#(X)) :23 1049.33/297.05 -->_1 from^#(ok(X)) -> c_22(from^#(X)) :22 1049.33/297.05 -->_1 from^#(mark(X)) -> c_21(from^#(X)) :21 1049.33/297.05 -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20 1049.33/297.05 -->_1 cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) :19 1049.33/297.05 -->_1 app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) :18 1049.33/297.05 -->_1 app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) :17 1049.33/297.05 -->_1 app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) :16 1049.33/297.05 -->_1 active^#(prefix(X)) -> c_15(prefix^#(active(X))) :15 1049.33/297.05 -->_1 active^#(zWadr(cons(X, XS), cons(Y, YS))) -> 1049.33/297.05 c_13(cons^#(app(Y, cons(X, nil())), zWadr(XS, YS))) :13 1049.33/297.05 -->_1 active^#(zWadr(X1, X2)) -> c_10(zWadr^#(active(X1), X2)) :10 1049.33/297.05 -->_1 active^#(zWadr(X1, X2)) -> c_9(zWadr^#(X1, active(X2))) :9 1049.33/297.05 -->_1 active^#(s(X)) -> c_8(s^#(active(X))) :8 1049.33/297.05 -->_1 active^#(from(X)) -> c_7(from^#(active(X))) :7 1049.33/297.05 -->_1 active^#(from(X)) -> c_6(cons^#(X, from(s(X)))) :6 1049.33/297.05 -->_1 active^#(cons(X1, X2)) -> c_5(cons^#(active(X1), X2)) :5 1049.33/297.05 -->_1 active^#(app(cons(X, XS), YS)) -> 1049.33/297.05 c_4(cons^#(X, app(XS, YS))) :4 1049.33/297.05 -->_1 proper^#(nil()) -> c_31() :31 1049.33/297.05 -->_1 active^#(prefix(L)) -> 1049.33/297.05 c_14(cons^#(nil(), zWadr(L, prefix(L)))) :14 1049.33/297.05 -->_1 active^#(zWadr(nil(), YS)) -> c_12() :12 1049.33/297.05 -->_1 active^#(zWadr(XS, nil())) -> c_11() :11 1049.33/297.05 -->_1 active^#(app(nil(), YS)) -> c_3(YS) :3 1049.33/297.05 -->_1 active^#(app(X1, X2)) -> c_2(app^#(active(X1), X2)) :2 1049.33/297.05 -->_1 active^#(app(X1, X2)) -> c_1(app^#(X1, active(X2))) :1 1049.33/297.05 1049.33/297.05 4: active^#(app(cons(X, XS), YS)) -> c_4(cons^#(X, app(XS, YS))) 1049.33/297.05 -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20 1049.33/297.05 -->_1 cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) :19 1049.33/297.05 1049.33/297.05 5: active^#(cons(X1, X2)) -> c_5(cons^#(active(X1), X2)) 1049.33/297.05 -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20 1049.33/297.05 -->_1 cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) :19 1049.33/297.05 1049.33/297.05 6: active^#(from(X)) -> c_6(cons^#(X, from(s(X)))) 1049.33/297.05 -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20 1049.33/297.05 -->_1 cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) :19 1049.33/297.05 1049.33/297.05 7: active^#(from(X)) -> c_7(from^#(active(X))) 1049.33/297.05 -->_1 from^#(ok(X)) -> c_22(from^#(X)) :22 1049.33/297.05 -->_1 from^#(mark(X)) -> c_21(from^#(X)) :21 1049.33/297.05 1049.33/297.05 8: active^#(s(X)) -> c_8(s^#(active(X))) 1049.33/297.05 -->_1 s^#(ok(X)) -> c_24(s^#(X)) :24 1049.33/297.05 -->_1 s^#(mark(X)) -> c_23(s^#(X)) :23 1049.33/297.05 1049.33/297.05 9: active^#(zWadr(X1, X2)) -> c_9(zWadr^#(X1, active(X2))) 1049.33/297.05 -->_1 zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) :27 1049.33/297.05 -->_1 zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) :26 1049.33/297.05 -->_1 zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) :25 1049.33/297.05 1049.33/297.05 10: active^#(zWadr(X1, X2)) -> c_10(zWadr^#(active(X1), X2)) 1049.33/297.05 -->_1 zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) :27 1049.33/297.05 -->_1 zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) :26 1049.33/297.05 -->_1 zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) :25 1049.33/297.05 1049.33/297.05 11: active^#(zWadr(XS, nil())) -> c_11() 1049.33/297.05 1049.33/297.05 12: active^#(zWadr(nil(), YS)) -> c_12() 1049.33/297.05 1049.33/297.05 13: active^#(zWadr(cons(X, XS), cons(Y, YS))) -> 1049.33/297.05 c_13(cons^#(app(Y, cons(X, nil())), zWadr(XS, YS))) 1049.33/297.05 -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20 1049.33/297.05 -->_1 cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) :19 1049.33/297.05 1049.33/297.05 14: active^#(prefix(L)) -> c_14(cons^#(nil(), zWadr(L, prefix(L)))) 1049.33/297.05 1049.33/297.05 15: active^#(prefix(X)) -> c_15(prefix^#(active(X))) 1049.33/297.05 -->_1 prefix^#(ok(X)) -> c_29(prefix^#(X)) :29 1049.33/297.05 -->_1 prefix^#(mark(X)) -> c_28(prefix^#(X)) :28 1049.33/297.05 1049.33/297.05 16: app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) 1049.33/297.05 -->_1 app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) :18 1049.33/297.05 -->_1 app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) :17 1049.33/297.05 -->_1 app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) :16 1049.33/297.05 1049.33/297.05 17: app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) 1049.33/297.05 -->_1 app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) :18 1049.33/297.05 -->_1 app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) :17 1049.33/297.05 -->_1 app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) :16 1049.33/297.05 1049.33/297.05 18: app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) 1049.33/297.05 -->_1 app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) :18 1049.33/297.05 -->_1 app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) :17 1049.33/297.05 -->_1 app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) :16 1049.33/297.05 1049.33/297.05 19: cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) 1049.33/297.05 -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20 1049.33/297.05 -->_1 cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) :19 1049.33/297.05 1049.33/297.05 20: cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) 1049.33/297.05 -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20 1049.33/297.05 -->_1 cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) :19 1049.33/297.05 1049.33/297.05 21: from^#(mark(X)) -> c_21(from^#(X)) 1049.33/297.05 -->_1 from^#(ok(X)) -> c_22(from^#(X)) :22 1049.33/297.05 -->_1 from^#(mark(X)) -> c_21(from^#(X)) :21 1049.33/297.05 1049.33/297.05 22: from^#(ok(X)) -> c_22(from^#(X)) 1049.33/297.05 -->_1 from^#(ok(X)) -> c_22(from^#(X)) :22 1049.33/297.05 -->_1 from^#(mark(X)) -> c_21(from^#(X)) :21 1049.33/297.05 1049.33/297.05 23: s^#(mark(X)) -> c_23(s^#(X)) 1049.33/297.05 -->_1 s^#(ok(X)) -> c_24(s^#(X)) :24 1049.33/297.05 -->_1 s^#(mark(X)) -> c_23(s^#(X)) :23 1049.33/297.05 1049.33/297.05 24: s^#(ok(X)) -> c_24(s^#(X)) 1049.33/297.05 -->_1 s^#(ok(X)) -> c_24(s^#(X)) :24 1049.33/297.05 -->_1 s^#(mark(X)) -> c_23(s^#(X)) :23 1049.33/297.05 1049.33/297.05 25: zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) 1049.33/297.05 -->_1 zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) :27 1049.33/297.05 -->_1 zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) :26 1049.33/297.05 -->_1 zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) :25 1049.33/297.05 1049.33/297.05 26: zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) 1049.33/297.05 -->_1 zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) :27 1049.33/297.05 -->_1 zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) :26 1049.33/297.05 -->_1 zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) :25 1049.33/297.05 1049.33/297.05 27: zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) 1049.33/297.05 -->_1 zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) :27 1049.33/297.05 -->_1 zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) :26 1049.33/297.05 -->_1 zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) :25 1049.33/297.05 1049.33/297.05 28: prefix^#(mark(X)) -> c_28(prefix^#(X)) 1049.33/297.05 -->_1 prefix^#(ok(X)) -> c_29(prefix^#(X)) :29 1049.33/297.05 -->_1 prefix^#(mark(X)) -> c_28(prefix^#(X)) :28 1049.33/297.05 1049.33/297.05 29: prefix^#(ok(X)) -> c_29(prefix^#(X)) 1049.33/297.05 -->_1 prefix^#(ok(X)) -> c_29(prefix^#(X)) :29 1049.33/297.05 -->_1 prefix^#(mark(X)) -> c_28(prefix^#(X)) :28 1049.33/297.05 1049.33/297.05 30: proper^#(app(X1, X2)) -> c_30(app^#(proper(X1), proper(X2))) 1049.33/297.05 -->_1 app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) :18 1049.33/297.05 -->_1 app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) :17 1049.33/297.05 -->_1 app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) :16 1049.33/297.05 1049.33/297.05 31: proper^#(nil()) -> c_31() 1049.33/297.05 1049.33/297.05 32: proper^#(cons(X1, X2)) -> c_32(cons^#(proper(X1), proper(X2))) 1049.33/297.05 -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20 1049.33/297.05 -->_1 cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) :19 1049.33/297.05 1049.33/297.05 33: proper^#(from(X)) -> c_33(from^#(proper(X))) 1049.33/297.05 -->_1 from^#(ok(X)) -> c_22(from^#(X)) :22 1049.33/297.05 -->_1 from^#(mark(X)) -> c_21(from^#(X)) :21 1049.33/297.05 1049.33/297.05 34: proper^#(s(X)) -> c_34(s^#(proper(X))) 1049.33/297.05 -->_1 s^#(ok(X)) -> c_24(s^#(X)) :24 1049.33/297.05 -->_1 s^#(mark(X)) -> c_23(s^#(X)) :23 1049.33/297.05 1049.33/297.05 35: proper^#(zWadr(X1, X2)) -> 1049.33/297.05 c_35(zWadr^#(proper(X1), proper(X2))) 1049.33/297.05 -->_1 zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) :27 1049.33/297.05 -->_1 zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) :26 1049.33/297.05 -->_1 zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) :25 1049.33/297.05 1049.33/297.05 36: proper^#(prefix(X)) -> c_36(prefix^#(proper(X))) 1049.33/297.05 -->_1 prefix^#(ok(X)) -> c_29(prefix^#(X)) :29 1049.33/297.05 -->_1 prefix^#(mark(X)) -> c_28(prefix^#(X)) :28 1049.33/297.05 1049.33/297.05 37: top^#(mark(X)) -> c_37(top^#(proper(X))) 1049.33/297.05 -->_1 top^#(ok(X)) -> c_38(top^#(active(X))) :38 1049.33/297.05 -->_1 top^#(mark(X)) -> c_37(top^#(proper(X))) :37 1049.33/297.05 1049.33/297.05 38: top^#(ok(X)) -> c_38(top^#(active(X))) 1049.33/297.05 -->_1 top^#(ok(X)) -> c_38(top^#(active(X))) :38 1049.33/297.05 -->_1 top^#(mark(X)) -> c_37(top^#(proper(X))) :37 1049.33/297.05 1049.33/297.05 1049.33/297.05 Only the nodes {16,18,17,19,20,21,22,23,24,25,27,26,28,29,31,37,38} 1049.33/297.05 are reachable from nodes 1049.33/297.05 {16,17,18,19,20,21,22,23,24,25,26,27,28,29,31,37,38} that start 1049.33/297.05 derivation from marked basic terms. The nodes not reachable are 1049.33/297.05 removed from the problem. 1049.33/297.05 1049.33/297.05 We are left with following problem, upon which TcT provides the 1049.33/297.05 certificate MAYBE. 1049.33/297.05 1049.33/297.05 Strict DPs: 1049.33/297.05 { app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) 1049.33/297.05 , app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) 1049.33/297.05 , app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) 1049.33/297.05 , cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) 1049.33/297.05 , cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) 1049.33/297.05 , from^#(mark(X)) -> c_21(from^#(X)) 1049.33/297.05 , from^#(ok(X)) -> c_22(from^#(X)) 1049.33/297.05 , s^#(mark(X)) -> c_23(s^#(X)) 1049.33/297.05 , s^#(ok(X)) -> c_24(s^#(X)) 1049.33/297.05 , zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) 1049.33/297.05 , zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) 1049.33/297.05 , zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) 1049.33/297.05 , prefix^#(mark(X)) -> c_28(prefix^#(X)) 1049.33/297.05 , prefix^#(ok(X)) -> c_29(prefix^#(X)) 1049.33/297.05 , proper^#(nil()) -> c_31() 1049.33/297.05 , top^#(mark(X)) -> c_37(top^#(proper(X))) 1049.33/297.05 , top^#(ok(X)) -> c_38(top^#(active(X))) } 1049.33/297.05 Strict Trs: 1049.33/297.05 { active(app(X1, X2)) -> app(X1, active(X2)) 1049.33/297.05 , active(app(X1, X2)) -> app(active(X1), X2) 1049.33/297.05 , active(app(nil(), YS)) -> mark(YS) 1049.33/297.05 , active(app(cons(X, XS), YS)) -> mark(cons(X, app(XS, YS))) 1049.33/297.05 , active(cons(X1, X2)) -> cons(active(X1), X2) 1049.33/297.05 , active(from(X)) -> mark(cons(X, from(s(X)))) 1049.33/297.05 , active(from(X)) -> from(active(X)) 1049.33/297.05 , active(s(X)) -> s(active(X)) 1049.33/297.05 , active(zWadr(X1, X2)) -> zWadr(X1, active(X2)) 1049.33/297.05 , active(zWadr(X1, X2)) -> zWadr(active(X1), X2) 1049.33/297.05 , active(zWadr(XS, nil())) -> mark(nil()) 1049.33/297.05 , active(zWadr(nil(), YS)) -> mark(nil()) 1049.33/297.05 , active(zWadr(cons(X, XS), cons(Y, YS))) -> 1049.33/297.05 mark(cons(app(Y, cons(X, nil())), zWadr(XS, YS))) 1049.33/297.05 , active(prefix(L)) -> mark(cons(nil(), zWadr(L, prefix(L)))) 1049.33/297.05 , active(prefix(X)) -> prefix(active(X)) 1049.33/297.05 , app(X1, mark(X2)) -> mark(app(X1, X2)) 1049.33/297.05 , app(mark(X1), X2) -> mark(app(X1, X2)) 1049.33/297.05 , app(ok(X1), ok(X2)) -> ok(app(X1, X2)) 1049.33/297.05 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1049.33/297.05 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1049.33/297.05 , from(mark(X)) -> mark(from(X)) 1049.33/297.05 , from(ok(X)) -> ok(from(X)) 1049.33/297.05 , s(mark(X)) -> mark(s(X)) 1049.33/297.05 , s(ok(X)) -> ok(s(X)) 1049.33/297.05 , zWadr(X1, mark(X2)) -> mark(zWadr(X1, X2)) 1049.33/297.05 , zWadr(mark(X1), X2) -> mark(zWadr(X1, X2)) 1049.33/297.05 , zWadr(ok(X1), ok(X2)) -> ok(zWadr(X1, X2)) 1049.33/297.05 , prefix(mark(X)) -> mark(prefix(X)) 1049.33/297.05 , prefix(ok(X)) -> ok(prefix(X)) 1049.33/297.05 , proper(app(X1, X2)) -> app(proper(X1), proper(X2)) 1049.33/297.05 , proper(nil()) -> ok(nil()) 1049.33/297.05 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1049.33/297.05 , proper(from(X)) -> from(proper(X)) 1049.33/297.05 , proper(s(X)) -> s(proper(X)) 1049.33/297.05 , proper(zWadr(X1, X2)) -> zWadr(proper(X1), proper(X2)) 1049.33/297.05 , proper(prefix(X)) -> prefix(proper(X)) 1049.33/297.05 , top(mark(X)) -> top(proper(X)) 1049.33/297.05 , top(ok(X)) -> top(active(X)) } 1049.33/297.05 Obligation: 1049.33/297.05 runtime complexity 1049.33/297.05 Answer: 1049.33/297.05 MAYBE 1049.33/297.05 1049.33/297.05 We estimate the number of application of {15} by applications of 1049.33/297.05 Pre({15}) = {}. Here rules are labeled as follows: 1049.33/297.05 1049.33/297.05 DPs: 1049.33/297.05 { 1: app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) 1049.33/297.05 , 2: app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) 1049.33/297.05 , 3: app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) 1049.33/297.05 , 4: cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) 1049.33/297.05 , 5: cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) 1049.33/297.05 , 6: from^#(mark(X)) -> c_21(from^#(X)) 1049.33/297.05 , 7: from^#(ok(X)) -> c_22(from^#(X)) 1049.33/297.05 , 8: s^#(mark(X)) -> c_23(s^#(X)) 1049.33/297.05 , 9: s^#(ok(X)) -> c_24(s^#(X)) 1049.33/297.05 , 10: zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) 1049.33/297.05 , 11: zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) 1049.33/297.05 , 12: zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) 1049.33/297.05 , 13: prefix^#(mark(X)) -> c_28(prefix^#(X)) 1049.33/297.05 , 14: prefix^#(ok(X)) -> c_29(prefix^#(X)) 1049.33/297.05 , 15: proper^#(nil()) -> c_31() 1049.33/297.05 , 16: top^#(mark(X)) -> c_37(top^#(proper(X))) 1049.33/297.05 , 17: top^#(ok(X)) -> c_38(top^#(active(X))) } 1049.33/297.05 1049.33/297.05 We are left with following problem, upon which TcT provides the 1049.33/297.05 certificate MAYBE. 1049.33/297.05 1049.33/297.05 Strict DPs: 1049.33/297.05 { app^#(X1, mark(X2)) -> c_16(app^#(X1, X2)) 1049.33/297.05 , app^#(mark(X1), X2) -> c_17(app^#(X1, X2)) 1049.33/297.05 , app^#(ok(X1), ok(X2)) -> c_18(app^#(X1, X2)) 1049.33/297.05 , cons^#(mark(X1), X2) -> c_19(cons^#(X1, X2)) 1049.33/297.05 , cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) 1049.33/297.05 , from^#(mark(X)) -> c_21(from^#(X)) 1049.33/297.05 , from^#(ok(X)) -> c_22(from^#(X)) 1049.33/297.05 , s^#(mark(X)) -> c_23(s^#(X)) 1049.33/297.05 , s^#(ok(X)) -> c_24(s^#(X)) 1049.33/297.05 , zWadr^#(X1, mark(X2)) -> c_25(zWadr^#(X1, X2)) 1049.33/297.05 , zWadr^#(mark(X1), X2) -> c_26(zWadr^#(X1, X2)) 1049.33/297.05 , zWadr^#(ok(X1), ok(X2)) -> c_27(zWadr^#(X1, X2)) 1049.33/297.05 , prefix^#(mark(X)) -> c_28(prefix^#(X)) 1049.33/297.05 , prefix^#(ok(X)) -> c_29(prefix^#(X)) 1049.33/297.05 , top^#(mark(X)) -> c_37(top^#(proper(X))) 1049.33/297.05 , top^#(ok(X)) -> c_38(top^#(active(X))) } 1049.33/297.05 Strict Trs: 1049.33/297.05 { active(app(X1, X2)) -> app(X1, active(X2)) 1049.33/297.05 , active(app(X1, X2)) -> app(active(X1), X2) 1049.33/297.05 , active(app(nil(), YS)) -> mark(YS) 1049.33/297.05 , active(app(cons(X, XS), YS)) -> mark(cons(X, app(XS, YS))) 1049.33/297.05 , active(cons(X1, X2)) -> cons(active(X1), X2) 1049.33/297.05 , active(from(X)) -> mark(cons(X, from(s(X)))) 1049.33/297.05 , active(from(X)) -> from(active(X)) 1049.33/297.05 , active(s(X)) -> s(active(X)) 1049.33/297.05 , active(zWadr(X1, X2)) -> zWadr(X1, active(X2)) 1049.33/297.05 , active(zWadr(X1, X2)) -> zWadr(active(X1), X2) 1049.33/297.05 , active(zWadr(XS, nil())) -> mark(nil()) 1049.33/297.05 , active(zWadr(nil(), YS)) -> mark(nil()) 1049.33/297.05 , active(zWadr(cons(X, XS), cons(Y, YS))) -> 1049.33/297.05 mark(cons(app(Y, cons(X, nil())), zWadr(XS, YS))) 1049.33/297.05 , active(prefix(L)) -> mark(cons(nil(), zWadr(L, prefix(L)))) 1049.33/297.05 , active(prefix(X)) -> prefix(active(X)) 1049.33/297.05 , app(X1, mark(X2)) -> mark(app(X1, X2)) 1049.33/297.05 , app(mark(X1), X2) -> mark(app(X1, X2)) 1049.33/297.05 , app(ok(X1), ok(X2)) -> ok(app(X1, X2)) 1049.33/297.05 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1049.33/297.05 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1049.33/297.05 , from(mark(X)) -> mark(from(X)) 1049.33/297.05 , from(ok(X)) -> ok(from(X)) 1049.33/297.05 , s(mark(X)) -> mark(s(X)) 1049.33/297.05 , s(ok(X)) -> ok(s(X)) 1049.33/297.05 , zWadr(X1, mark(X2)) -> mark(zWadr(X1, X2)) 1049.33/297.05 , zWadr(mark(X1), X2) -> mark(zWadr(X1, X2)) 1049.33/297.05 , zWadr(ok(X1), ok(X2)) -> ok(zWadr(X1, X2)) 1049.33/297.05 , prefix(mark(X)) -> mark(prefix(X)) 1049.33/297.05 , prefix(ok(X)) -> ok(prefix(X)) 1049.33/297.05 , proper(app(X1, X2)) -> app(proper(X1), proper(X2)) 1049.33/297.05 , proper(nil()) -> ok(nil()) 1049.33/297.05 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1049.33/297.05 , proper(from(X)) -> from(proper(X)) 1049.33/297.05 , proper(s(X)) -> s(proper(X)) 1049.33/297.05 , proper(zWadr(X1, X2)) -> zWadr(proper(X1), proper(X2)) 1049.33/297.05 , proper(prefix(X)) -> prefix(proper(X)) 1049.33/297.05 , top(mark(X)) -> top(proper(X)) 1049.33/297.05 , top(ok(X)) -> top(active(X)) } 1049.33/297.05 Weak DPs: { proper^#(nil()) -> c_31() } 1049.33/297.05 Obligation: 1049.33/297.05 runtime complexity 1049.33/297.05 Answer: 1049.33/297.05 MAYBE 1049.33/297.05 1049.33/297.05 Empty strict component of the problem is NOT empty. 1049.33/297.05 1049.33/297.05 1049.33/297.05 Arrrr.. 1049.73/297.39 EOF