MAYBE 800.56/297.06 MAYBE 800.56/297.06 800.56/297.06 We are left with following problem, upon which TcT provides the 800.56/297.06 certificate MAYBE. 800.56/297.06 800.56/297.06 Strict Trs: 800.56/297.06 { active(zeros()) -> mark(cons(0(), zeros())) 800.56/297.06 , active(cons(X1, X2)) -> cons(active(X1), X2) 800.56/297.06 , active(U11(X1, X2)) -> U11(active(X1), X2) 800.56/297.06 , active(U11(tt(), L)) -> mark(U12(tt(), L)) 800.56/297.06 , active(U12(X1, X2)) -> U12(active(X1), X2) 800.56/297.06 , active(U12(tt(), L)) -> mark(s(length(L))) 800.56/297.06 , active(s(X)) -> s(active(X)) 800.56/297.06 , active(length(X)) -> length(active(X)) 800.56/297.06 , active(length(cons(N, L))) -> mark(U11(tt(), L)) 800.56/297.06 , active(length(nil())) -> mark(0()) 800.56/297.06 , active(U21(X1, X2, X3, X4)) -> U21(active(X1), X2, X3, X4) 800.56/297.06 , active(U21(tt(), IL, M, N)) -> mark(U22(tt(), IL, M, N)) 800.56/297.06 , active(U22(X1, X2, X3, X4)) -> U22(active(X1), X2, X3, X4) 800.56/297.06 , active(U22(tt(), IL, M, N)) -> mark(U23(tt(), IL, M, N)) 800.56/297.06 , active(U23(X1, X2, X3, X4)) -> U23(active(X1), X2, X3, X4) 800.56/297.06 , active(U23(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) 800.56/297.06 , active(take(X1, X2)) -> take(X1, active(X2)) 800.56/297.06 , active(take(X1, X2)) -> take(active(X1), X2) 800.56/297.06 , active(take(0(), IL)) -> mark(nil()) 800.56/297.06 , active(take(s(M), cons(N, IL))) -> mark(U21(tt(), IL, M, N)) 800.56/297.06 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 800.56/297.06 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 800.56/297.06 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 800.56/297.06 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 800.56/297.06 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 800.56/297.06 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 800.56/297.06 , s(mark(X)) -> mark(s(X)) 800.56/297.06 , s(ok(X)) -> ok(s(X)) 800.56/297.06 , length(mark(X)) -> mark(length(X)) 800.56/297.06 , length(ok(X)) -> ok(length(X)) 800.56/297.06 , U21(mark(X1), X2, X3, X4) -> mark(U21(X1, X2, X3, X4)) 800.56/297.06 , U21(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U21(X1, X2, X3, X4)) 800.56/297.06 , U22(mark(X1), X2, X3, X4) -> mark(U22(X1, X2, X3, X4)) 800.56/297.06 , U22(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U22(X1, X2, X3, X4)) 800.56/297.06 , U23(mark(X1), X2, X3, X4) -> mark(U23(X1, X2, X3, X4)) 800.56/297.06 , U23(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U23(X1, X2, X3, X4)) 800.56/297.06 , take(X1, mark(X2)) -> mark(take(X1, X2)) 800.56/297.06 , take(mark(X1), X2) -> mark(take(X1, X2)) 800.56/297.06 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 800.56/297.06 , proper(zeros()) -> ok(zeros()) 800.56/297.06 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 800.56/297.06 , proper(0()) -> ok(0()) 800.56/297.06 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 800.56/297.06 , proper(tt()) -> ok(tt()) 800.56/297.06 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 800.56/297.06 , proper(s(X)) -> s(proper(X)) 800.56/297.06 , proper(length(X)) -> length(proper(X)) 800.56/297.06 , proper(U21(X1, X2, X3, X4)) -> 800.56/297.06 U21(proper(X1), proper(X2), proper(X3), proper(X4)) 800.56/297.06 , proper(U22(X1, X2, X3, X4)) -> 800.56/297.06 U22(proper(X1), proper(X2), proper(X3), proper(X4)) 800.56/297.06 , proper(U23(X1, X2, X3, X4)) -> 800.56/297.06 U23(proper(X1), proper(X2), proper(X3), proper(X4)) 800.56/297.06 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 800.56/297.06 , proper(nil()) -> ok(nil()) 800.56/297.06 , top(mark(X)) -> top(proper(X)) 800.56/297.06 , top(ok(X)) -> top(active(X)) } 800.56/297.06 Obligation: 800.56/297.06 runtime complexity 800.56/297.06 Answer: 800.56/297.06 MAYBE 800.56/297.06 800.56/297.06 None of the processors succeeded. 800.56/297.06 800.56/297.06 Details of failed attempt(s): 800.56/297.06 ----------------------------- 800.56/297.06 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 800.56/297.06 following reason: 800.56/297.06 800.56/297.06 Computation stopped due to timeout after 297.0 seconds. 800.56/297.06 800.56/297.06 2) 'Best' failed due to the following reason: 800.56/297.06 800.56/297.06 None of the processors succeeded. 800.56/297.06 800.56/297.06 Details of failed attempt(s): 800.56/297.06 ----------------------------- 800.56/297.06 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 800.56/297.06 seconds)' failed due to the following reason: 800.56/297.06 800.56/297.06 Computation stopped due to timeout after 148.0 seconds. 800.56/297.06 800.56/297.06 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 800.56/297.06 failed due to the following reason: 800.56/297.06 800.56/297.06 Computation stopped due to timeout after 24.0 seconds. 800.56/297.06 800.56/297.06 3) 'Best' failed due to the following reason: 800.56/297.06 800.56/297.06 None of the processors succeeded. 800.56/297.06 800.56/297.06 Details of failed attempt(s): 800.56/297.06 ----------------------------- 800.56/297.06 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 800.56/297.06 to the following reason: 800.56/297.06 800.56/297.06 The processor is inapplicable, reason: 800.56/297.06 Processor only applicable for innermost runtime complexity analysis 800.56/297.06 800.56/297.06 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 800.56/297.06 following reason: 800.56/297.06 800.56/297.06 The processor is inapplicable, reason: 800.56/297.06 Processor only applicable for innermost runtime complexity analysis 800.56/297.06 800.56/297.06 800.56/297.06 800.56/297.06 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 800.56/297.06 the following reason: 800.56/297.06 800.56/297.06 We add the following weak dependency pairs: 800.56/297.06 800.56/297.06 Strict DPs: 800.56/297.06 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 800.56/297.06 , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 800.56/297.06 , active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 800.56/297.06 , active^#(U11(tt(), L)) -> c_4(U12^#(tt(), L)) 800.56/297.06 , active^#(U12(X1, X2)) -> c_5(U12^#(active(X1), X2)) 800.56/297.06 , active^#(U12(tt(), L)) -> c_6(s^#(length(L))) 800.56/297.06 , active^#(s(X)) -> c_7(s^#(active(X))) 800.56/297.06 , active^#(length(X)) -> c_8(length^#(active(X))) 800.56/297.06 , active^#(length(cons(N, L))) -> c_9(U11^#(tt(), L)) 800.56/297.06 , active^#(length(nil())) -> c_10() 800.56/297.06 , active^#(U21(X1, X2, X3, X4)) -> 800.56/297.06 c_11(U21^#(active(X1), X2, X3, X4)) 800.56/297.06 , active^#(U21(tt(), IL, M, N)) -> c_12(U22^#(tt(), IL, M, N)) 800.56/297.06 , active^#(U22(X1, X2, X3, X4)) -> 800.56/297.06 c_13(U22^#(active(X1), X2, X3, X4)) 800.56/297.06 , active^#(U22(tt(), IL, M, N)) -> c_14(U23^#(tt(), IL, M, N)) 800.56/297.06 , active^#(U23(X1, X2, X3, X4)) -> 800.56/297.06 c_15(U23^#(active(X1), X2, X3, X4)) 800.56/297.06 , active^#(U23(tt(), IL, M, N)) -> c_16(cons^#(N, take(M, IL))) 800.56/297.06 , active^#(take(X1, X2)) -> c_17(take^#(X1, active(X2))) 800.56/297.06 , active^#(take(X1, X2)) -> c_18(take^#(active(X1), X2)) 800.56/297.06 , active^#(take(0(), IL)) -> c_19() 800.56/297.06 , active^#(take(s(M), cons(N, IL))) -> c_20(U21^#(tt(), IL, M, N)) 800.56/297.06 , cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 800.56/297.06 , cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 800.56/297.06 , U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) 800.56/297.06 , U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) 800.56/297.06 , U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) 800.56/297.06 , U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) 800.56/297.06 , s^#(mark(X)) -> c_27(s^#(X)) 800.56/297.06 , s^#(ok(X)) -> c_28(s^#(X)) 800.56/297.06 , length^#(mark(X)) -> c_29(length^#(X)) 800.56/297.06 , length^#(ok(X)) -> c_30(length^#(X)) 800.56/297.06 , U21^#(mark(X1), X2, X3, X4) -> c_31(U21^#(X1, X2, X3, X4)) 800.56/297.06 , U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.06 c_32(U21^#(X1, X2, X3, X4)) 800.56/297.06 , U22^#(mark(X1), X2, X3, X4) -> c_33(U22^#(X1, X2, X3, X4)) 800.56/297.06 , U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.06 c_34(U22^#(X1, X2, X3, X4)) 800.56/297.06 , U23^#(mark(X1), X2, X3, X4) -> c_35(U23^#(X1, X2, X3, X4)) 800.56/297.06 , U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.06 c_36(U23^#(X1, X2, X3, X4)) 800.56/297.06 , take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) 800.56/297.06 , take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) 800.56/297.06 , take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) 800.56/297.06 , proper^#(zeros()) -> c_40() 800.56/297.06 , proper^#(cons(X1, X2)) -> c_41(cons^#(proper(X1), proper(X2))) 800.56/297.06 , proper^#(0()) -> c_42() 800.56/297.06 , proper^#(U11(X1, X2)) -> c_43(U11^#(proper(X1), proper(X2))) 800.56/297.06 , proper^#(tt()) -> c_44() 800.56/297.06 , proper^#(U12(X1, X2)) -> c_45(U12^#(proper(X1), proper(X2))) 800.56/297.06 , proper^#(s(X)) -> c_46(s^#(proper(X))) 800.56/297.06 , proper^#(length(X)) -> c_47(length^#(proper(X))) 800.56/297.06 , proper^#(U21(X1, X2, X3, X4)) -> 800.56/297.06 c_48(U21^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.06 , proper^#(U22(X1, X2, X3, X4)) -> 800.56/297.06 c_49(U22^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.06 , proper^#(U23(X1, X2, X3, X4)) -> 800.56/297.06 c_50(U23^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.06 , proper^#(take(X1, X2)) -> c_51(take^#(proper(X1), proper(X2))) 800.56/297.06 , proper^#(nil()) -> c_52() 800.56/297.06 , top^#(mark(X)) -> c_53(top^#(proper(X))) 800.56/297.06 , top^#(ok(X)) -> c_54(top^#(active(X))) } 800.56/297.06 800.56/297.06 and mark the set of starting terms. 800.56/297.06 800.56/297.06 We are left with following problem, upon which TcT provides the 800.56/297.06 certificate MAYBE. 800.56/297.06 800.56/297.06 Strict DPs: 800.56/297.06 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 800.56/297.06 , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 800.56/297.06 , active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 800.56/297.06 , active^#(U11(tt(), L)) -> c_4(U12^#(tt(), L)) 800.56/297.06 , active^#(U12(X1, X2)) -> c_5(U12^#(active(X1), X2)) 800.56/297.08 , active^#(U12(tt(), L)) -> c_6(s^#(length(L))) 800.56/297.08 , active^#(s(X)) -> c_7(s^#(active(X))) 800.56/297.08 , active^#(length(X)) -> c_8(length^#(active(X))) 800.56/297.08 , active^#(length(cons(N, L))) -> c_9(U11^#(tt(), L)) 800.56/297.08 , active^#(length(nil())) -> c_10() 800.56/297.08 , active^#(U21(X1, X2, X3, X4)) -> 800.56/297.08 c_11(U21^#(active(X1), X2, X3, X4)) 800.56/297.08 , active^#(U21(tt(), IL, M, N)) -> c_12(U22^#(tt(), IL, M, N)) 800.56/297.08 , active^#(U22(X1, X2, X3, X4)) -> 800.56/297.08 c_13(U22^#(active(X1), X2, X3, X4)) 800.56/297.08 , active^#(U22(tt(), IL, M, N)) -> c_14(U23^#(tt(), IL, M, N)) 800.56/297.08 , active^#(U23(X1, X2, X3, X4)) -> 800.56/297.08 c_15(U23^#(active(X1), X2, X3, X4)) 800.56/297.08 , active^#(U23(tt(), IL, M, N)) -> c_16(cons^#(N, take(M, IL))) 800.56/297.08 , active^#(take(X1, X2)) -> c_17(take^#(X1, active(X2))) 800.56/297.08 , active^#(take(X1, X2)) -> c_18(take^#(active(X1), X2)) 800.56/297.08 , active^#(take(0(), IL)) -> c_19() 800.56/297.08 , active^#(take(s(M), cons(N, IL))) -> c_20(U21^#(tt(), IL, M, N)) 800.56/297.08 , cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 800.56/297.08 , cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 800.56/297.08 , U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) 800.56/297.08 , U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) 800.56/297.08 , U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) 800.56/297.08 , U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) 800.56/297.08 , s^#(mark(X)) -> c_27(s^#(X)) 800.56/297.08 , s^#(ok(X)) -> c_28(s^#(X)) 800.56/297.08 , length^#(mark(X)) -> c_29(length^#(X)) 800.56/297.08 , length^#(ok(X)) -> c_30(length^#(X)) 800.56/297.08 , U21^#(mark(X1), X2, X3, X4) -> c_31(U21^#(X1, X2, X3, X4)) 800.56/297.08 , U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_32(U21^#(X1, X2, X3, X4)) 800.56/297.08 , U22^#(mark(X1), X2, X3, X4) -> c_33(U22^#(X1, X2, X3, X4)) 800.56/297.08 , U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_34(U22^#(X1, X2, X3, X4)) 800.56/297.08 , U23^#(mark(X1), X2, X3, X4) -> c_35(U23^#(X1, X2, X3, X4)) 800.56/297.08 , U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_36(U23^#(X1, X2, X3, X4)) 800.56/297.08 , take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) 800.56/297.08 , take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) 800.56/297.08 , take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) 800.56/297.08 , proper^#(zeros()) -> c_40() 800.56/297.08 , proper^#(cons(X1, X2)) -> c_41(cons^#(proper(X1), proper(X2))) 800.56/297.08 , proper^#(0()) -> c_42() 800.56/297.08 , proper^#(U11(X1, X2)) -> c_43(U11^#(proper(X1), proper(X2))) 800.56/297.08 , proper^#(tt()) -> c_44() 800.56/297.08 , proper^#(U12(X1, X2)) -> c_45(U12^#(proper(X1), proper(X2))) 800.56/297.08 , proper^#(s(X)) -> c_46(s^#(proper(X))) 800.56/297.08 , proper^#(length(X)) -> c_47(length^#(proper(X))) 800.56/297.08 , proper^#(U21(X1, X2, X3, X4)) -> 800.56/297.08 c_48(U21^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.08 , proper^#(U22(X1, X2, X3, X4)) -> 800.56/297.08 c_49(U22^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.08 , proper^#(U23(X1, X2, X3, X4)) -> 800.56/297.08 c_50(U23^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.08 , proper^#(take(X1, X2)) -> c_51(take^#(proper(X1), proper(X2))) 800.56/297.08 , proper^#(nil()) -> c_52() 800.56/297.08 , top^#(mark(X)) -> c_53(top^#(proper(X))) 800.56/297.08 , top^#(ok(X)) -> c_54(top^#(active(X))) } 800.56/297.08 Strict Trs: 800.56/297.08 { active(zeros()) -> mark(cons(0(), zeros())) 800.56/297.08 , active(cons(X1, X2)) -> cons(active(X1), X2) 800.56/297.08 , active(U11(X1, X2)) -> U11(active(X1), X2) 800.56/297.08 , active(U11(tt(), L)) -> mark(U12(tt(), L)) 800.56/297.08 , active(U12(X1, X2)) -> U12(active(X1), X2) 800.56/297.08 , active(U12(tt(), L)) -> mark(s(length(L))) 800.56/297.08 , active(s(X)) -> s(active(X)) 800.56/297.08 , active(length(X)) -> length(active(X)) 800.56/297.08 , active(length(cons(N, L))) -> mark(U11(tt(), L)) 800.56/297.08 , active(length(nil())) -> mark(0()) 800.56/297.08 , active(U21(X1, X2, X3, X4)) -> U21(active(X1), X2, X3, X4) 800.56/297.08 , active(U21(tt(), IL, M, N)) -> mark(U22(tt(), IL, M, N)) 800.56/297.08 , active(U22(X1, X2, X3, X4)) -> U22(active(X1), X2, X3, X4) 800.56/297.08 , active(U22(tt(), IL, M, N)) -> mark(U23(tt(), IL, M, N)) 800.56/297.08 , active(U23(X1, X2, X3, X4)) -> U23(active(X1), X2, X3, X4) 800.56/297.08 , active(U23(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) 800.56/297.08 , active(take(X1, X2)) -> take(X1, active(X2)) 800.56/297.08 , active(take(X1, X2)) -> take(active(X1), X2) 800.56/297.08 , active(take(0(), IL)) -> mark(nil()) 800.56/297.08 , active(take(s(M), cons(N, IL))) -> mark(U21(tt(), IL, M, N)) 800.56/297.08 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 800.56/297.08 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 800.56/297.08 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 800.56/297.08 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 800.56/297.08 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 800.56/297.08 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 800.56/297.08 , s(mark(X)) -> mark(s(X)) 800.56/297.08 , s(ok(X)) -> ok(s(X)) 800.56/297.08 , length(mark(X)) -> mark(length(X)) 800.56/297.08 , length(ok(X)) -> ok(length(X)) 800.56/297.08 , U21(mark(X1), X2, X3, X4) -> mark(U21(X1, X2, X3, X4)) 800.56/297.08 , U21(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U21(X1, X2, X3, X4)) 800.56/297.08 , U22(mark(X1), X2, X3, X4) -> mark(U22(X1, X2, X3, X4)) 800.56/297.08 , U22(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U22(X1, X2, X3, X4)) 800.56/297.08 , U23(mark(X1), X2, X3, X4) -> mark(U23(X1, X2, X3, X4)) 800.56/297.08 , U23(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U23(X1, X2, X3, X4)) 800.56/297.08 , take(X1, mark(X2)) -> mark(take(X1, X2)) 800.56/297.08 , take(mark(X1), X2) -> mark(take(X1, X2)) 800.56/297.08 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 800.56/297.08 , proper(zeros()) -> ok(zeros()) 800.56/297.08 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 800.56/297.08 , proper(0()) -> ok(0()) 800.56/297.08 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 800.56/297.08 , proper(tt()) -> ok(tt()) 800.56/297.08 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 800.56/297.08 , proper(s(X)) -> s(proper(X)) 800.56/297.08 , proper(length(X)) -> length(proper(X)) 800.56/297.08 , proper(U21(X1, X2, X3, X4)) -> 800.56/297.08 U21(proper(X1), proper(X2), proper(X3), proper(X4)) 800.56/297.08 , proper(U22(X1, X2, X3, X4)) -> 800.56/297.08 U22(proper(X1), proper(X2), proper(X3), proper(X4)) 800.56/297.08 , proper(U23(X1, X2, X3, X4)) -> 800.56/297.08 U23(proper(X1), proper(X2), proper(X3), proper(X4)) 800.56/297.08 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 800.56/297.08 , proper(nil()) -> ok(nil()) 800.56/297.08 , top(mark(X)) -> top(proper(X)) 800.56/297.08 , top(ok(X)) -> top(active(X)) } 800.56/297.08 Obligation: 800.56/297.08 runtime complexity 800.56/297.08 Answer: 800.56/297.08 MAYBE 800.56/297.08 800.56/297.08 Consider the dependency graph: 800.56/297.08 800.56/297.08 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) 800.56/297.08 800.56/297.08 2: active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 800.56/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 800.56/297.08 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 800.56/297.08 800.56/297.08 3: active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 800.56/297.08 -->_1 U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) :24 800.56/297.08 -->_1 U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) :23 800.56/297.08 800.56/297.08 4: active^#(U11(tt(), L)) -> c_4(U12^#(tt(), L)) 800.56/297.08 800.56/297.08 5: active^#(U12(X1, X2)) -> c_5(U12^#(active(X1), X2)) 800.56/297.08 -->_1 U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) :26 800.56/297.08 -->_1 U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) :25 800.56/297.08 800.56/297.08 6: active^#(U12(tt(), L)) -> c_6(s^#(length(L))) 800.56/297.08 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 800.56/297.08 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 800.56/297.08 800.56/297.08 7: active^#(s(X)) -> c_7(s^#(active(X))) 800.56/297.08 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 800.56/297.08 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 800.56/297.08 800.56/297.08 8: active^#(length(X)) -> c_8(length^#(active(X))) 800.56/297.08 -->_1 length^#(ok(X)) -> c_30(length^#(X)) :30 800.56/297.08 -->_1 length^#(mark(X)) -> c_29(length^#(X)) :29 800.56/297.08 800.56/297.08 9: active^#(length(cons(N, L))) -> c_9(U11^#(tt(), L)) 800.56/297.08 800.56/297.08 10: active^#(length(nil())) -> c_10() 800.56/297.08 800.56/297.08 11: active^#(U21(X1, X2, X3, X4)) -> 800.56/297.08 c_11(U21^#(active(X1), X2, X3, X4)) 800.56/297.08 -->_1 U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_32(U21^#(X1, X2, X3, X4)) :32 800.56/297.08 -->_1 U21^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_31(U21^#(X1, X2, X3, X4)) :31 800.56/297.08 800.56/297.08 12: active^#(U21(tt(), IL, M, N)) -> c_12(U22^#(tt(), IL, M, N)) 800.56/297.08 800.56/297.08 13: active^#(U22(X1, X2, X3, X4)) -> 800.56/297.08 c_13(U22^#(active(X1), X2, X3, X4)) 800.56/297.08 -->_1 U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_34(U22^#(X1, X2, X3, X4)) :34 800.56/297.08 -->_1 U22^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_33(U22^#(X1, X2, X3, X4)) :33 800.56/297.08 800.56/297.08 14: active^#(U22(tt(), IL, M, N)) -> c_14(U23^#(tt(), IL, M, N)) 800.56/297.08 800.56/297.08 15: active^#(U23(X1, X2, X3, X4)) -> 800.56/297.08 c_15(U23^#(active(X1), X2, X3, X4)) 800.56/297.08 -->_1 U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_36(U23^#(X1, X2, X3, X4)) :36 800.56/297.08 -->_1 U23^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_35(U23^#(X1, X2, X3, X4)) :35 800.56/297.08 800.56/297.08 16: active^#(U23(tt(), IL, M, N)) -> c_16(cons^#(N, take(M, IL))) 800.56/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 800.56/297.08 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 800.56/297.08 800.56/297.08 17: active^#(take(X1, X2)) -> c_17(take^#(X1, active(X2))) 800.56/297.08 -->_1 take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) :39 800.56/297.08 -->_1 take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) :38 800.56/297.08 -->_1 take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) :37 800.56/297.08 800.56/297.08 18: active^#(take(X1, X2)) -> c_18(take^#(active(X1), X2)) 800.56/297.08 -->_1 take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) :39 800.56/297.08 -->_1 take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) :38 800.56/297.08 -->_1 take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) :37 800.56/297.08 800.56/297.08 19: active^#(take(0(), IL)) -> c_19() 800.56/297.08 800.56/297.08 20: active^#(take(s(M), cons(N, IL))) -> 800.56/297.08 c_20(U21^#(tt(), IL, M, N)) 800.56/297.08 800.56/297.08 21: cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 800.56/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 800.56/297.08 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 800.56/297.08 800.56/297.08 22: cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 800.56/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 800.56/297.08 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 800.56/297.08 800.56/297.08 23: U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) 800.56/297.08 -->_1 U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) :24 800.56/297.08 -->_1 U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) :23 800.56/297.08 800.56/297.08 24: U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) 800.56/297.08 -->_1 U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) :24 800.56/297.08 -->_1 U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) :23 800.56/297.08 800.56/297.08 25: U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) 800.56/297.08 -->_1 U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) :26 800.56/297.08 -->_1 U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) :25 800.56/297.08 800.56/297.08 26: U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) 800.56/297.08 -->_1 U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) :26 800.56/297.08 -->_1 U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) :25 800.56/297.08 800.56/297.08 27: s^#(mark(X)) -> c_27(s^#(X)) 800.56/297.08 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 800.56/297.08 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 800.56/297.08 800.56/297.08 28: s^#(ok(X)) -> c_28(s^#(X)) 800.56/297.08 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 800.56/297.08 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 800.56/297.08 800.56/297.08 29: length^#(mark(X)) -> c_29(length^#(X)) 800.56/297.08 -->_1 length^#(ok(X)) -> c_30(length^#(X)) :30 800.56/297.08 -->_1 length^#(mark(X)) -> c_29(length^#(X)) :29 800.56/297.08 800.56/297.08 30: length^#(ok(X)) -> c_30(length^#(X)) 800.56/297.08 -->_1 length^#(ok(X)) -> c_30(length^#(X)) :30 800.56/297.08 -->_1 length^#(mark(X)) -> c_29(length^#(X)) :29 800.56/297.08 800.56/297.08 31: U21^#(mark(X1), X2, X3, X4) -> c_31(U21^#(X1, X2, X3, X4)) 800.56/297.08 -->_1 U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_32(U21^#(X1, X2, X3, X4)) :32 800.56/297.08 -->_1 U21^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_31(U21^#(X1, X2, X3, X4)) :31 800.56/297.08 800.56/297.08 32: U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_32(U21^#(X1, X2, X3, X4)) 800.56/297.08 -->_1 U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_32(U21^#(X1, X2, X3, X4)) :32 800.56/297.08 -->_1 U21^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_31(U21^#(X1, X2, X3, X4)) :31 800.56/297.08 800.56/297.08 33: U22^#(mark(X1), X2, X3, X4) -> c_33(U22^#(X1, X2, X3, X4)) 800.56/297.08 -->_1 U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_34(U22^#(X1, X2, X3, X4)) :34 800.56/297.08 -->_1 U22^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_33(U22^#(X1, X2, X3, X4)) :33 800.56/297.08 800.56/297.08 34: U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_34(U22^#(X1, X2, X3, X4)) 800.56/297.08 -->_1 U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_34(U22^#(X1, X2, X3, X4)) :34 800.56/297.08 -->_1 U22^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_33(U22^#(X1, X2, X3, X4)) :33 800.56/297.08 800.56/297.08 35: U23^#(mark(X1), X2, X3, X4) -> c_35(U23^#(X1, X2, X3, X4)) 800.56/297.08 -->_1 U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_36(U23^#(X1, X2, X3, X4)) :36 800.56/297.08 -->_1 U23^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_35(U23^#(X1, X2, X3, X4)) :35 800.56/297.08 800.56/297.08 36: U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_36(U23^#(X1, X2, X3, X4)) 800.56/297.08 -->_1 U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_36(U23^#(X1, X2, X3, X4)) :36 800.56/297.08 -->_1 U23^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_35(U23^#(X1, X2, X3, X4)) :35 800.56/297.08 800.56/297.08 37: take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) 800.56/297.08 -->_1 take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) :39 800.56/297.08 -->_1 take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) :38 800.56/297.08 -->_1 take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) :37 800.56/297.08 800.56/297.08 38: take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) 800.56/297.08 -->_1 take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) :39 800.56/297.08 -->_1 take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) :38 800.56/297.08 -->_1 take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) :37 800.56/297.08 800.56/297.08 39: take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) 800.56/297.08 -->_1 take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) :39 800.56/297.08 -->_1 take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) :38 800.56/297.08 -->_1 take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) :37 800.56/297.08 800.56/297.08 40: proper^#(zeros()) -> c_40() 800.56/297.08 800.56/297.08 41: proper^#(cons(X1, X2)) -> c_41(cons^#(proper(X1), proper(X2))) 800.56/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 800.56/297.08 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 800.56/297.08 800.56/297.08 42: proper^#(0()) -> c_42() 800.56/297.08 800.56/297.08 43: proper^#(U11(X1, X2)) -> c_43(U11^#(proper(X1), proper(X2))) 800.56/297.08 -->_1 U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) :24 800.56/297.08 -->_1 U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) :23 800.56/297.08 800.56/297.08 44: proper^#(tt()) -> c_44() 800.56/297.08 800.56/297.08 45: proper^#(U12(X1, X2)) -> c_45(U12^#(proper(X1), proper(X2))) 800.56/297.08 -->_1 U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) :26 800.56/297.08 -->_1 U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) :25 800.56/297.08 800.56/297.08 46: proper^#(s(X)) -> c_46(s^#(proper(X))) 800.56/297.08 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 800.56/297.08 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 800.56/297.08 800.56/297.08 47: proper^#(length(X)) -> c_47(length^#(proper(X))) 800.56/297.08 -->_1 length^#(ok(X)) -> c_30(length^#(X)) :30 800.56/297.08 -->_1 length^#(mark(X)) -> c_29(length^#(X)) :29 800.56/297.08 800.56/297.08 48: proper^#(U21(X1, X2, X3, X4)) -> 800.56/297.08 c_48(U21^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.08 -->_1 U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_32(U21^#(X1, X2, X3, X4)) :32 800.56/297.08 -->_1 U21^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_31(U21^#(X1, X2, X3, X4)) :31 800.56/297.08 800.56/297.08 49: proper^#(U22(X1, X2, X3, X4)) -> 800.56/297.08 c_49(U22^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.08 -->_1 U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_34(U22^#(X1, X2, X3, X4)) :34 800.56/297.08 -->_1 U22^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_33(U22^#(X1, X2, X3, X4)) :33 800.56/297.08 800.56/297.08 50: proper^#(U23(X1, X2, X3, X4)) -> 800.56/297.08 c_50(U23^#(proper(X1), proper(X2), proper(X3), proper(X4))) 800.56/297.08 -->_1 U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.56/297.08 c_36(U23^#(X1, X2, X3, X4)) :36 800.56/297.08 -->_1 U23^#(mark(X1), X2, X3, X4) -> 800.56/297.08 c_35(U23^#(X1, X2, X3, X4)) :35 800.56/297.08 800.56/297.08 51: proper^#(take(X1, X2)) -> c_51(take^#(proper(X1), proper(X2))) 800.56/297.08 -->_1 take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) :39 800.56/297.08 -->_1 take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) :38 800.56/297.08 -->_1 take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) :37 800.56/297.08 800.56/297.08 52: proper^#(nil()) -> c_52() 800.56/297.08 800.56/297.08 53: top^#(mark(X)) -> c_53(top^#(proper(X))) 800.56/297.08 -->_1 top^#(ok(X)) -> c_54(top^#(active(X))) :54 800.56/297.08 -->_1 top^#(mark(X)) -> c_53(top^#(proper(X))) :53 800.56/297.08 800.56/297.08 54: top^#(ok(X)) -> c_54(top^#(active(X))) 800.56/297.08 -->_1 top^#(ok(X)) -> c_54(top^#(active(X))) :54 800.56/297.08 -->_1 top^#(mark(X)) -> c_53(top^#(proper(X))) :53 800.56/297.08 800.56/297.08 800.56/297.08 Only the nodes 800.56/297.08 {1,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,39,38,40,42,44,52,53,54} 800.56/297.08 are reachable from nodes 800.56/297.08 {1,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,42,44,52,53,54} 800.56/297.08 that start derivation from marked basic terms. The nodes not 800.56/297.08 reachable are removed from the problem. 800.56/297.08 800.56/297.08 We are left with following problem, upon which TcT provides the 800.96/297.18 certificate MAYBE. 800.96/297.18 800.96/297.18 Strict DPs: 800.96/297.18 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 800.96/297.18 , cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 800.96/297.18 , cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 800.96/297.18 , U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) 800.96/297.18 , U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) 800.96/297.18 , U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) 800.96/297.18 , U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) 800.96/297.18 , s^#(mark(X)) -> c_27(s^#(X)) 800.96/297.18 , s^#(ok(X)) -> c_28(s^#(X)) 800.96/297.18 , length^#(mark(X)) -> c_29(length^#(X)) 800.96/297.18 , length^#(ok(X)) -> c_30(length^#(X)) 800.96/297.18 , U21^#(mark(X1), X2, X3, X4) -> c_31(U21^#(X1, X2, X3, X4)) 800.96/297.18 , U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_32(U21^#(X1, X2, X3, X4)) 800.96/297.18 , U22^#(mark(X1), X2, X3, X4) -> c_33(U22^#(X1, X2, X3, X4)) 800.96/297.18 , U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_34(U22^#(X1, X2, X3, X4)) 800.96/297.18 , U23^#(mark(X1), X2, X3, X4) -> c_35(U23^#(X1, X2, X3, X4)) 800.96/297.18 , U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_36(U23^#(X1, X2, X3, X4)) 800.96/297.18 , take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) 800.96/297.18 , take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) 800.96/297.18 , take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) 800.96/297.18 , proper^#(zeros()) -> c_40() 800.96/297.18 , proper^#(0()) -> c_42() 800.96/297.18 , proper^#(tt()) -> c_44() 800.96/297.18 , proper^#(nil()) -> c_52() 800.96/297.18 , top^#(mark(X)) -> c_53(top^#(proper(X))) 800.96/297.18 , top^#(ok(X)) -> c_54(top^#(active(X))) } 800.96/297.18 Strict Trs: 800.96/297.18 { active(zeros()) -> mark(cons(0(), zeros())) 800.96/297.18 , active(cons(X1, X2)) -> cons(active(X1), X2) 800.96/297.18 , active(U11(X1, X2)) -> U11(active(X1), X2) 800.96/297.18 , active(U11(tt(), L)) -> mark(U12(tt(), L)) 800.96/297.18 , active(U12(X1, X2)) -> U12(active(X1), X2) 800.96/297.18 , active(U12(tt(), L)) -> mark(s(length(L))) 800.96/297.18 , active(s(X)) -> s(active(X)) 800.96/297.18 , active(length(X)) -> length(active(X)) 800.96/297.18 , active(length(cons(N, L))) -> mark(U11(tt(), L)) 800.96/297.18 , active(length(nil())) -> mark(0()) 800.96/297.18 , active(U21(X1, X2, X3, X4)) -> U21(active(X1), X2, X3, X4) 800.96/297.18 , active(U21(tt(), IL, M, N)) -> mark(U22(tt(), IL, M, N)) 800.96/297.18 , active(U22(X1, X2, X3, X4)) -> U22(active(X1), X2, X3, X4) 800.96/297.18 , active(U22(tt(), IL, M, N)) -> mark(U23(tt(), IL, M, N)) 800.96/297.18 , active(U23(X1, X2, X3, X4)) -> U23(active(X1), X2, X3, X4) 800.96/297.18 , active(U23(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) 800.96/297.18 , active(take(X1, X2)) -> take(X1, active(X2)) 800.96/297.18 , active(take(X1, X2)) -> take(active(X1), X2) 800.96/297.18 , active(take(0(), IL)) -> mark(nil()) 800.96/297.18 , active(take(s(M), cons(N, IL))) -> mark(U21(tt(), IL, M, N)) 800.96/297.18 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 800.96/297.18 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 800.96/297.18 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 800.96/297.18 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 800.96/297.18 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 800.96/297.18 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 800.96/297.18 , s(mark(X)) -> mark(s(X)) 800.96/297.18 , s(ok(X)) -> ok(s(X)) 800.96/297.18 , length(mark(X)) -> mark(length(X)) 800.96/297.18 , length(ok(X)) -> ok(length(X)) 800.96/297.18 , U21(mark(X1), X2, X3, X4) -> mark(U21(X1, X2, X3, X4)) 800.96/297.18 , U21(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U21(X1, X2, X3, X4)) 800.96/297.18 , U22(mark(X1), X2, X3, X4) -> mark(U22(X1, X2, X3, X4)) 800.96/297.18 , U22(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U22(X1, X2, X3, X4)) 800.96/297.18 , U23(mark(X1), X2, X3, X4) -> mark(U23(X1, X2, X3, X4)) 800.96/297.18 , U23(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U23(X1, X2, X3, X4)) 800.96/297.18 , take(X1, mark(X2)) -> mark(take(X1, X2)) 800.96/297.18 , take(mark(X1), X2) -> mark(take(X1, X2)) 800.96/297.18 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 800.96/297.18 , proper(zeros()) -> ok(zeros()) 800.96/297.18 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 800.96/297.18 , proper(0()) -> ok(0()) 800.96/297.18 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 800.96/297.18 , proper(tt()) -> ok(tt()) 800.96/297.18 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 800.96/297.18 , proper(s(X)) -> s(proper(X)) 800.96/297.18 , proper(length(X)) -> length(proper(X)) 800.96/297.18 , proper(U21(X1, X2, X3, X4)) -> 800.96/297.18 U21(proper(X1), proper(X2), proper(X3), proper(X4)) 800.96/297.18 , proper(U22(X1, X2, X3, X4)) -> 800.96/297.18 U22(proper(X1), proper(X2), proper(X3), proper(X4)) 800.96/297.18 , proper(U23(X1, X2, X3, X4)) -> 800.96/297.18 U23(proper(X1), proper(X2), proper(X3), proper(X4)) 800.96/297.18 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 800.96/297.18 , proper(nil()) -> ok(nil()) 800.96/297.18 , top(mark(X)) -> top(proper(X)) 800.96/297.18 , top(ok(X)) -> top(active(X)) } 800.96/297.18 Obligation: 800.96/297.18 runtime complexity 800.96/297.18 Answer: 800.96/297.18 MAYBE 800.96/297.18 800.96/297.18 We estimate the number of application of {1,21,22,23,24} by 800.96/297.18 applications of Pre({1,21,22,23,24}) = {}. Here rules are labeled 800.96/297.18 as follows: 800.96/297.18 800.96/297.18 DPs: 800.96/297.18 { 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) 800.96/297.18 , 2: cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 800.96/297.18 , 3: cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 800.96/297.18 , 4: U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) 800.96/297.18 , 5: U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) 800.96/297.18 , 6: U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) 800.96/297.18 , 7: U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) 800.96/297.18 , 8: s^#(mark(X)) -> c_27(s^#(X)) 800.96/297.18 , 9: s^#(ok(X)) -> c_28(s^#(X)) 800.96/297.18 , 10: length^#(mark(X)) -> c_29(length^#(X)) 800.96/297.18 , 11: length^#(ok(X)) -> c_30(length^#(X)) 800.96/297.18 , 12: U21^#(mark(X1), X2, X3, X4) -> c_31(U21^#(X1, X2, X3, X4)) 800.96/297.18 , 13: U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_32(U21^#(X1, X2, X3, X4)) 800.96/297.18 , 14: U22^#(mark(X1), X2, X3, X4) -> c_33(U22^#(X1, X2, X3, X4)) 800.96/297.18 , 15: U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_34(U22^#(X1, X2, X3, X4)) 800.96/297.18 , 16: U23^#(mark(X1), X2, X3, X4) -> c_35(U23^#(X1, X2, X3, X4)) 800.96/297.18 , 17: U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_36(U23^#(X1, X2, X3, X4)) 800.96/297.18 , 18: take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) 800.96/297.18 , 19: take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) 800.96/297.18 , 20: take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) 800.96/297.18 , 21: proper^#(zeros()) -> c_40() 800.96/297.18 , 22: proper^#(0()) -> c_42() 800.96/297.18 , 23: proper^#(tt()) -> c_44() 800.96/297.18 , 24: proper^#(nil()) -> c_52() 800.96/297.18 , 25: top^#(mark(X)) -> c_53(top^#(proper(X))) 800.96/297.18 , 26: top^#(ok(X)) -> c_54(top^#(active(X))) } 800.96/297.18 800.96/297.18 We are left with following problem, upon which TcT provides the 800.96/297.18 certificate MAYBE. 800.96/297.18 800.96/297.18 Strict DPs: 800.96/297.18 { cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 800.96/297.18 , cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 800.96/297.18 , U11^#(mark(X1), X2) -> c_23(U11^#(X1, X2)) 800.96/297.18 , U11^#(ok(X1), ok(X2)) -> c_24(U11^#(X1, X2)) 800.96/297.18 , U12^#(mark(X1), X2) -> c_25(U12^#(X1, X2)) 800.96/297.18 , U12^#(ok(X1), ok(X2)) -> c_26(U12^#(X1, X2)) 800.96/297.18 , s^#(mark(X)) -> c_27(s^#(X)) 800.96/297.18 , s^#(ok(X)) -> c_28(s^#(X)) 800.96/297.18 , length^#(mark(X)) -> c_29(length^#(X)) 800.96/297.18 , length^#(ok(X)) -> c_30(length^#(X)) 800.96/297.18 , U21^#(mark(X1), X2, X3, X4) -> c_31(U21^#(X1, X2, X3, X4)) 800.96/297.18 , U21^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_32(U21^#(X1, X2, X3, X4)) 800.96/297.18 , U22^#(mark(X1), X2, X3, X4) -> c_33(U22^#(X1, X2, X3, X4)) 800.96/297.18 , U22^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_34(U22^#(X1, X2, X3, X4)) 800.96/297.18 , U23^#(mark(X1), X2, X3, X4) -> c_35(U23^#(X1, X2, X3, X4)) 800.96/297.18 , U23^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 800.96/297.18 c_36(U23^#(X1, X2, X3, X4)) 800.96/297.18 , take^#(X1, mark(X2)) -> c_37(take^#(X1, X2)) 800.96/297.18 , take^#(mark(X1), X2) -> c_38(take^#(X1, X2)) 800.96/297.18 , take^#(ok(X1), ok(X2)) -> c_39(take^#(X1, X2)) 800.96/297.18 , top^#(mark(X)) -> c_53(top^#(proper(X))) 800.96/297.18 , top^#(ok(X)) -> c_54(top^#(active(X))) } 800.96/297.18 Strict Trs: 800.96/297.18 { active(zeros()) -> mark(cons(0(), zeros())) 800.96/297.18 , active(cons(X1, X2)) -> cons(active(X1), X2) 800.96/297.18 , active(U11(X1, X2)) -> U11(active(X1), X2) 800.96/297.18 , active(U11(tt(), L)) -> mark(U12(tt(), L)) 800.96/297.18 , active(U12(X1, X2)) -> U12(active(X1), X2) 800.96/297.18 , active(U12(tt(), L)) -> mark(s(length(L))) 800.96/297.18 , active(s(X)) -> s(active(X)) 800.96/297.18 , active(length(X)) -> length(active(X)) 800.96/297.18 , active(length(cons(N, L))) -> mark(U11(tt(), L)) 800.96/297.18 , active(length(nil())) -> mark(0()) 800.96/297.18 , active(U21(X1, X2, X3, X4)) -> U21(active(X1), X2, X3, X4) 800.96/297.18 , active(U21(tt(), IL, M, N)) -> mark(U22(tt(), IL, M, N)) 800.96/297.18 , active(U22(X1, X2, X3, X4)) -> U22(active(X1), X2, X3, X4) 800.96/297.18 , active(U22(tt(), IL, M, N)) -> mark(U23(tt(), IL, M, N)) 800.96/297.18 , active(U23(X1, X2, X3, X4)) -> U23(active(X1), X2, X3, X4) 800.96/297.18 , active(U23(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) 800.96/297.18 , active(take(X1, X2)) -> take(X1, active(X2)) 800.96/297.18 , active(take(X1, X2)) -> take(active(X1), X2) 800.96/297.18 , active(take(0(), IL)) -> mark(nil()) 800.96/297.18 , active(take(s(M), cons(N, IL))) -> mark(U21(tt(), IL, M, N)) 800.96/297.18 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 800.96/297.18 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 800.96/297.18 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 800.96/297.18 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 800.96/297.18 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 800.96/297.18 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 800.96/297.18 , s(mark(X)) -> mark(s(X)) 800.96/297.18 , s(ok(X)) -> ok(s(X)) 800.96/297.18 , length(mark(X)) -> mark(length(X)) 800.96/297.18 , length(ok(X)) -> ok(length(X)) 800.96/297.18 , U21(mark(X1), X2, X3, X4) -> mark(U21(X1, X2, X3, X4)) 800.96/297.18 , U21(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U21(X1, X2, X3, X4)) 800.96/297.18 , U22(mark(X1), X2, X3, X4) -> mark(U22(X1, X2, X3, X4)) 800.96/297.18 , U22(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U22(X1, X2, X3, X4)) 800.96/297.18 , U23(mark(X1), X2, X3, X4) -> mark(U23(X1, X2, X3, X4)) 800.96/297.18 , U23(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U23(X1, X2, X3, X4)) 800.96/297.18 , take(X1, mark(X2)) -> mark(take(X1, X2)) 800.96/297.18 , take(mark(X1), X2) -> mark(take(X1, X2)) 800.96/297.18 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 800.96/297.18 , proper(zeros()) -> ok(zeros()) 800.96/297.18 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 800.96/297.18 , proper(0()) -> ok(0()) 800.96/297.18 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 800.96/297.18 , proper(tt()) -> ok(tt()) 800.96/297.18 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 800.96/297.18 , proper(s(X)) -> s(proper(X)) 800.96/297.18 , proper(length(X)) -> length(proper(X)) 800.96/297.18 , proper(U21(X1, X2, X3, X4)) -> 800.96/297.18 U21(proper(X1), proper(X2), proper(X3), proper(X4)) 800.96/297.18 , proper(U22(X1, X2, X3, X4)) -> 800.96/297.18 U22(proper(X1), proper(X2), proper(X3), proper(X4)) 800.96/297.18 , proper(U23(X1, X2, X3, X4)) -> 800.96/297.18 U23(proper(X1), proper(X2), proper(X3), proper(X4)) 800.96/297.18 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 800.96/297.18 , proper(nil()) -> ok(nil()) 800.96/297.18 , top(mark(X)) -> top(proper(X)) 800.96/297.18 , top(ok(X)) -> top(active(X)) } 800.96/297.18 Weak DPs: 800.96/297.18 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 800.96/297.18 , proper^#(zeros()) -> c_40() 800.96/297.18 , proper^#(0()) -> c_42() 800.96/297.18 , proper^#(tt()) -> c_44() 800.96/297.18 , proper^#(nil()) -> c_52() } 800.96/297.18 Obligation: 800.96/297.18 runtime complexity 800.96/297.18 Answer: 800.96/297.18 MAYBE 800.96/297.18 800.96/297.18 Empty strict component of the problem is NOT empty. 800.96/297.18 800.96/297.18 800.96/297.18 Arrrr.. 801.30/297.24 EOF