MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { test(x_0, y) -> True() , test(x_0, y) -> False() , append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) , match_0(l1_2, l2_1, Nil()) -> l2_1 , match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) , part(a_4, l_3) -> match_1(a_4, l_3, l_3) , match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) , match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) , match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) , match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) , match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) , quick(l_5) -> match_4(l_5, l_5) , match_4(l_5, Nil()) -> Nil() , match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) , match_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2))) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { test^#(x_0, y) -> c_1() , test^#(x_0, y) -> c_2() , append^#(l1_2, l2_1) -> c_3(match_0^#(l1_2, l2_1, l1_2)) , match_0^#(l1_2, l2_1, Nil()) -> c_4() , match_0^#(l1_2, l2_1, Cons(x, l)) -> c_5(append^#(l, l2_1)) , part^#(a_4, l_3) -> c_6(match_1^#(a_4, l_3, l_3)) , match_1^#(a_4, l_3, Nil()) -> c_7() , match_1^#(a_4, l_3, Cons(x, l')) -> c_8(match_2^#(x, l', a_4, l_3, part(a_4, l')), part^#(a_4, l')) , match_2^#(x, l', a_4, l_3, Pair(l1, l2)) -> c_9(match_3^#(l1, l2, x, l', a_4, l_3, test(a_4, x)), test^#(a_4, x)) , match_3^#(l1, l2, x, l', a_4, l_3, True()) -> c_10() , match_3^#(l1, l2, x, l', a_4, l_3, False()) -> c_11() , quick^#(l_5) -> c_12(match_4^#(l_5, l_5)) , match_4^#(l_5, Nil()) -> c_13() , match_4^#(l_5, Cons(a, l')) -> c_14(match_5^#(a, l', l_5, part(a, l')), part^#(a, l')) , match_5^#(a, l', l_5, Pair(l1, l2)) -> c_15(append^#(quick(l1), Cons(a, quick(l2))), quick^#(l1), quick^#(l2)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { test^#(x_0, y) -> c_1() , test^#(x_0, y) -> c_2() , append^#(l1_2, l2_1) -> c_3(match_0^#(l1_2, l2_1, l1_2)) , match_0^#(l1_2, l2_1, Nil()) -> c_4() , match_0^#(l1_2, l2_1, Cons(x, l)) -> c_5(append^#(l, l2_1)) , part^#(a_4, l_3) -> c_6(match_1^#(a_4, l_3, l_3)) , match_1^#(a_4, l_3, Nil()) -> c_7() , match_1^#(a_4, l_3, Cons(x, l')) -> c_8(match_2^#(x, l', a_4, l_3, part(a_4, l')), part^#(a_4, l')) , match_2^#(x, l', a_4, l_3, Pair(l1, l2)) -> c_9(match_3^#(l1, l2, x, l', a_4, l_3, test(a_4, x)), test^#(a_4, x)) , match_3^#(l1, l2, x, l', a_4, l_3, True()) -> c_10() , match_3^#(l1, l2, x, l', a_4, l_3, False()) -> c_11() , quick^#(l_5) -> c_12(match_4^#(l_5, l_5)) , match_4^#(l_5, Nil()) -> c_13() , match_4^#(l_5, Cons(a, l')) -> c_14(match_5^#(a, l', l_5, part(a, l')), part^#(a, l')) , match_5^#(a, l', l_5, Pair(l1, l2)) -> c_15(append^#(quick(l1), Cons(a, quick(l2))), quick^#(l1), quick^#(l2)) } Weak Trs: { test(x_0, y) -> True() , test(x_0, y) -> False() , append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) , match_0(l1_2, l2_1, Nil()) -> l2_1 , match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) , part(a_4, l_3) -> match_1(a_4, l_3, l_3) , match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) , match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) , match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) , match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) , match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) , quick(l_5) -> match_4(l_5, l_5) , match_4(l_5, Nil()) -> Nil() , match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) , match_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,7,10,11,13} by applications of Pre({1,2,4,7,10,11,13}) = {3,6,9,12}. Here rules are labeled as follows: DPs: { 1: test^#(x_0, y) -> c_1() , 2: test^#(x_0, y) -> c_2() , 3: append^#(l1_2, l2_1) -> c_3(match_0^#(l1_2, l2_1, l1_2)) , 4: match_0^#(l1_2, l2_1, Nil()) -> c_4() , 5: match_0^#(l1_2, l2_1, Cons(x, l)) -> c_5(append^#(l, l2_1)) , 6: part^#(a_4, l_3) -> c_6(match_1^#(a_4, l_3, l_3)) , 7: match_1^#(a_4, l_3, Nil()) -> c_7() , 8: match_1^#(a_4, l_3, Cons(x, l')) -> c_8(match_2^#(x, l', a_4, l_3, part(a_4, l')), part^#(a_4, l')) , 9: match_2^#(x, l', a_4, l_3, Pair(l1, l2)) -> c_9(match_3^#(l1, l2, x, l', a_4, l_3, test(a_4, x)), test^#(a_4, x)) , 10: match_3^#(l1, l2, x, l', a_4, l_3, True()) -> c_10() , 11: match_3^#(l1, l2, x, l', a_4, l_3, False()) -> c_11() , 12: quick^#(l_5) -> c_12(match_4^#(l_5, l_5)) , 13: match_4^#(l_5, Nil()) -> c_13() , 14: match_4^#(l_5, Cons(a, l')) -> c_14(match_5^#(a, l', l_5, part(a, l')), part^#(a, l')) , 15: match_5^#(a, l', l_5, Pair(l1, l2)) -> c_15(append^#(quick(l1), Cons(a, quick(l2))), quick^#(l1), quick^#(l2)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(l1_2, l2_1) -> c_3(match_0^#(l1_2, l2_1, l1_2)) , match_0^#(l1_2, l2_1, Cons(x, l)) -> c_5(append^#(l, l2_1)) , part^#(a_4, l_3) -> c_6(match_1^#(a_4, l_3, l_3)) , match_1^#(a_4, l_3, Cons(x, l')) -> c_8(match_2^#(x, l', a_4, l_3, part(a_4, l')), part^#(a_4, l')) , match_2^#(x, l', a_4, l_3, Pair(l1, l2)) -> c_9(match_3^#(l1, l2, x, l', a_4, l_3, test(a_4, x)), test^#(a_4, x)) , quick^#(l_5) -> c_12(match_4^#(l_5, l_5)) , match_4^#(l_5, Cons(a, l')) -> c_14(match_5^#(a, l', l_5, part(a, l')), part^#(a, l')) , match_5^#(a, l', l_5, Pair(l1, l2)) -> c_15(append^#(quick(l1), Cons(a, quick(l2))), quick^#(l1), quick^#(l2)) } Weak DPs: { test^#(x_0, y) -> c_1() , test^#(x_0, y) -> c_2() , match_0^#(l1_2, l2_1, Nil()) -> c_4() , match_1^#(a_4, l_3, Nil()) -> c_7() , match_3^#(l1, l2, x, l', a_4, l_3, True()) -> c_10() , match_3^#(l1, l2, x, l', a_4, l_3, False()) -> c_11() , match_4^#(l_5, Nil()) -> c_13() } Weak Trs: { test(x_0, y) -> True() , test(x_0, y) -> False() , append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) , match_0(l1_2, l2_1, Nil()) -> l2_1 , match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) , part(a_4, l_3) -> match_1(a_4, l_3, l_3) , match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) , match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) , match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) , match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) , match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) , quick(l_5) -> match_4(l_5, l_5) , match_4(l_5, Nil()) -> Nil() , match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) , match_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {5} by applications of Pre({5}) = {4}. Here rules are labeled as follows: DPs: { 1: append^#(l1_2, l2_1) -> c_3(match_0^#(l1_2, l2_1, l1_2)) , 2: match_0^#(l1_2, l2_1, Cons(x, l)) -> c_5(append^#(l, l2_1)) , 3: part^#(a_4, l_3) -> c_6(match_1^#(a_4, l_3, l_3)) , 4: match_1^#(a_4, l_3, Cons(x, l')) -> c_8(match_2^#(x, l', a_4, l_3, part(a_4, l')), part^#(a_4, l')) , 5: match_2^#(x, l', a_4, l_3, Pair(l1, l2)) -> c_9(match_3^#(l1, l2, x, l', a_4, l_3, test(a_4, x)), test^#(a_4, x)) , 6: quick^#(l_5) -> c_12(match_4^#(l_5, l_5)) , 7: match_4^#(l_5, Cons(a, l')) -> c_14(match_5^#(a, l', l_5, part(a, l')), part^#(a, l')) , 8: match_5^#(a, l', l_5, Pair(l1, l2)) -> c_15(append^#(quick(l1), Cons(a, quick(l2))), quick^#(l1), quick^#(l2)) , 9: test^#(x_0, y) -> c_1() , 10: test^#(x_0, y) -> c_2() , 11: match_0^#(l1_2, l2_1, Nil()) -> c_4() , 12: match_1^#(a_4, l_3, Nil()) -> c_7() , 13: match_3^#(l1, l2, x, l', a_4, l_3, True()) -> c_10() , 14: match_3^#(l1, l2, x, l', a_4, l_3, False()) -> c_11() , 15: match_4^#(l_5, Nil()) -> c_13() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(l1_2, l2_1) -> c_3(match_0^#(l1_2, l2_1, l1_2)) , match_0^#(l1_2, l2_1, Cons(x, l)) -> c_5(append^#(l, l2_1)) , part^#(a_4, l_3) -> c_6(match_1^#(a_4, l_3, l_3)) , match_1^#(a_4, l_3, Cons(x, l')) -> c_8(match_2^#(x, l', a_4, l_3, part(a_4, l')), part^#(a_4, l')) , quick^#(l_5) -> c_12(match_4^#(l_5, l_5)) , match_4^#(l_5, Cons(a, l')) -> c_14(match_5^#(a, l', l_5, part(a, l')), part^#(a, l')) , match_5^#(a, l', l_5, Pair(l1, l2)) -> c_15(append^#(quick(l1), Cons(a, quick(l2))), quick^#(l1), quick^#(l2)) } Weak DPs: { test^#(x_0, y) -> c_1() , test^#(x_0, y) -> c_2() , match_0^#(l1_2, l2_1, Nil()) -> c_4() , match_1^#(a_4, l_3, Nil()) -> c_7() , match_2^#(x, l', a_4, l_3, Pair(l1, l2)) -> c_9(match_3^#(l1, l2, x, l', a_4, l_3, test(a_4, x)), test^#(a_4, x)) , match_3^#(l1, l2, x, l', a_4, l_3, True()) -> c_10() , match_3^#(l1, l2, x, l', a_4, l_3, False()) -> c_11() , match_4^#(l_5, Nil()) -> c_13() } Weak Trs: { test(x_0, y) -> True() , test(x_0, y) -> False() , append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) , match_0(l1_2, l2_1, Nil()) -> l2_1 , match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) , part(a_4, l_3) -> match_1(a_4, l_3, l_3) , match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) , match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) , match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) , match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) , match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) , quick(l_5) -> match_4(l_5, l_5) , match_4(l_5, Nil()) -> Nil() , match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) , match_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2))) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { test^#(x_0, y) -> c_1() , test^#(x_0, y) -> c_2() , match_0^#(l1_2, l2_1, Nil()) -> c_4() , match_1^#(a_4, l_3, Nil()) -> c_7() , match_2^#(x, l', a_4, l_3, Pair(l1, l2)) -> c_9(match_3^#(l1, l2, x, l', a_4, l_3, test(a_4, x)), test^#(a_4, x)) , match_3^#(l1, l2, x, l', a_4, l_3, True()) -> c_10() , match_3^#(l1, l2, x, l', a_4, l_3, False()) -> c_11() , match_4^#(l_5, Nil()) -> c_13() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(l1_2, l2_1) -> c_3(match_0^#(l1_2, l2_1, l1_2)) , match_0^#(l1_2, l2_1, Cons(x, l)) -> c_5(append^#(l, l2_1)) , part^#(a_4, l_3) -> c_6(match_1^#(a_4, l_3, l_3)) , match_1^#(a_4, l_3, Cons(x, l')) -> c_8(match_2^#(x, l', a_4, l_3, part(a_4, l')), part^#(a_4, l')) , quick^#(l_5) -> c_12(match_4^#(l_5, l_5)) , match_4^#(l_5, Cons(a, l')) -> c_14(match_5^#(a, l', l_5, part(a, l')), part^#(a, l')) , match_5^#(a, l', l_5, Pair(l1, l2)) -> c_15(append^#(quick(l1), Cons(a, quick(l2))), quick^#(l1), quick^#(l2)) } Weak Trs: { test(x_0, y) -> True() , test(x_0, y) -> False() , append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) , match_0(l1_2, l2_1, Nil()) -> l2_1 , match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) , part(a_4, l_3) -> match_1(a_4, l_3, l_3) , match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) , match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) , match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) , match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) , match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) , quick(l_5) -> match_4(l_5, l_5) , match_4(l_5, Nil()) -> Nil() , match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) , match_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2))) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { match_1^#(a_4, l_3, Cons(x, l')) -> c_8(match_2^#(x, l', a_4, l_3, part(a_4, l')), part^#(a_4, l')) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(l1_2, l2_1) -> c_1(match_0^#(l1_2, l2_1, l1_2)) , match_0^#(l1_2, l2_1, Cons(x, l)) -> c_2(append^#(l, l2_1)) , part^#(a_4, l_3) -> c_3(match_1^#(a_4, l_3, l_3)) , match_1^#(a_4, l_3, Cons(x, l')) -> c_4(part^#(a_4, l')) , quick^#(l_5) -> c_5(match_4^#(l_5, l_5)) , match_4^#(l_5, Cons(a, l')) -> c_6(match_5^#(a, l', l_5, part(a, l')), part^#(a, l')) , match_5^#(a, l', l_5, Pair(l1, l2)) -> c_7(append^#(quick(l1), Cons(a, quick(l2))), quick^#(l1), quick^#(l2)) } Weak Trs: { test(x_0, y) -> True() , test(x_0, y) -> False() , append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) , match_0(l1_2, l2_1, Nil()) -> l2_1 , match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) , part(a_4, l_3) -> match_1(a_4, l_3, l_3) , match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) , match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) , match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) , match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) , match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) , quick(l_5) -> match_4(l_5, l_5) , match_4(l_5, Nil()) -> Nil() , match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) , match_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..