MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { f_0(x) -> a() , f_1(x) -> g_1(x, x) , g_1(s(x), y) -> b(f_0(y), g_1(x, y)) , f_2(x) -> g_2(x, x) , g_2(s(x), y) -> b(f_1(y), g_2(x, y)) , f_3(x) -> g_3(x, x) , g_3(s(x), y) -> b(f_2(y), g_3(x, y)) , f_4(x) -> g_4(x, x) , g_4(s(x), y) -> b(f_3(y), g_4(x, y)) , f_5(x) -> g_5(x, x) , g_5(s(x), y) -> b(f_4(y), g_5(x, y)) , f_6(x) -> g_6(x, x) , g_6(s(x), y) -> b(f_5(y), g_6(x, y)) , f_7(x) -> g_7(x, x) , g_7(s(x), y) -> b(f_6(y), g_7(x, y)) , f_8(x) -> g_8(x, x) , g_8(s(x), y) -> b(f_7(y), g_8(x, y)) , f_9(x) -> g_9(x, x) , g_9(s(x), y) -> b(f_8(y), g_9(x, y)) , f_10(x) -> g_10(x, x) , g_10(s(x), y) -> b(f_9(y), g_10(x, y)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { f_0^#(x) -> c_1() , f_1^#(x) -> c_2(g_1^#(x, x)) , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y)) , f_2^#(x) -> c_4(g_2^#(x, x)) , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y)) , f_3^#(x) -> c_6(g_3^#(x, x)) , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y)) , f_4^#(x) -> c_8(g_4^#(x, x)) , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y)) , f_5^#(x) -> c_10(g_5^#(x, x)) , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) , f_6^#(x) -> c_12(g_6^#(x, x)) , g_6^#(s(x), y) -> c_13(f_5^#(y), g_6^#(x, y)) , f_7^#(x) -> c_14(g_7^#(x, x)) , g_7^#(s(x), y) -> c_15(f_6^#(y), g_7^#(x, y)) , f_8^#(x) -> c_16(g_8^#(x, x)) , g_8^#(s(x), y) -> c_17(f_7^#(y), g_8^#(x, y)) , f_9^#(x) -> c_18(g_9^#(x, x)) , g_9^#(s(x), y) -> c_19(f_8^#(y), g_9^#(x, y)) , f_10^#(x) -> c_20(g_10^#(x, x)) , g_10^#(s(x), y) -> c_21(f_9^#(y), g_10^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f_0^#(x) -> c_1() , f_1^#(x) -> c_2(g_1^#(x, x)) , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y)) , f_2^#(x) -> c_4(g_2^#(x, x)) , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y)) , f_3^#(x) -> c_6(g_3^#(x, x)) , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y)) , f_4^#(x) -> c_8(g_4^#(x, x)) , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y)) , f_5^#(x) -> c_10(g_5^#(x, x)) , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) , f_6^#(x) -> c_12(g_6^#(x, x)) , g_6^#(s(x), y) -> c_13(f_5^#(y), g_6^#(x, y)) , f_7^#(x) -> c_14(g_7^#(x, x)) , g_7^#(s(x), y) -> c_15(f_6^#(y), g_7^#(x, y)) , f_8^#(x) -> c_16(g_8^#(x, x)) , g_8^#(s(x), y) -> c_17(f_7^#(y), g_8^#(x, y)) , f_9^#(x) -> c_18(g_9^#(x, x)) , g_9^#(s(x), y) -> c_19(f_8^#(y), g_9^#(x, y)) , f_10^#(x) -> c_20(g_10^#(x, x)) , g_10^#(s(x), y) -> c_21(f_9^#(y), g_10^#(x, y)) } Strict Trs: { f_0(x) -> a() , f_1(x) -> g_1(x, x) , g_1(s(x), y) -> b(f_0(y), g_1(x, y)) , f_2(x) -> g_2(x, x) , g_2(s(x), y) -> b(f_1(y), g_2(x, y)) , f_3(x) -> g_3(x, x) , g_3(s(x), y) -> b(f_2(y), g_3(x, y)) , f_4(x) -> g_4(x, x) , g_4(s(x), y) -> b(f_3(y), g_4(x, y)) , f_5(x) -> g_5(x, x) , g_5(s(x), y) -> b(f_4(y), g_5(x, y)) , f_6(x) -> g_6(x, x) , g_6(s(x), y) -> b(f_5(y), g_6(x, y)) , f_7(x) -> g_7(x, x) , g_7(s(x), y) -> b(f_6(y), g_7(x, y)) , f_8(x) -> g_8(x, x) , g_8(s(x), y) -> b(f_7(y), g_8(x, y)) , f_9(x) -> g_9(x, x) , g_9(s(x), y) -> b(f_8(y), g_9(x, y)) , f_10(x) -> g_10(x, x) , g_10(s(x), y) -> b(f_9(y), g_10(x, y)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1} by applications of Pre({1}) = {3}. Here rules are labeled as follows: DPs: { 1: f_0^#(x) -> c_1() , 2: f_1^#(x) -> c_2(g_1^#(x, x)) , 3: g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y)) , 4: f_2^#(x) -> c_4(g_2^#(x, x)) , 5: g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y)) , 6: f_3^#(x) -> c_6(g_3^#(x, x)) , 7: g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y)) , 8: f_4^#(x) -> c_8(g_4^#(x, x)) , 9: g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y)) , 10: f_5^#(x) -> c_10(g_5^#(x, x)) , 11: g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) , 12: f_6^#(x) -> c_12(g_6^#(x, x)) , 13: g_6^#(s(x), y) -> c_13(f_5^#(y), g_6^#(x, y)) , 14: f_7^#(x) -> c_14(g_7^#(x, x)) , 15: g_7^#(s(x), y) -> c_15(f_6^#(y), g_7^#(x, y)) , 16: f_8^#(x) -> c_16(g_8^#(x, x)) , 17: g_8^#(s(x), y) -> c_17(f_7^#(y), g_8^#(x, y)) , 18: f_9^#(x) -> c_18(g_9^#(x, x)) , 19: g_9^#(s(x), y) -> c_19(f_8^#(y), g_9^#(x, y)) , 20: f_10^#(x) -> c_20(g_10^#(x, x)) , 21: g_10^#(s(x), y) -> c_21(f_9^#(y), g_10^#(x, y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f_1^#(x) -> c_2(g_1^#(x, x)) , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y)) , f_2^#(x) -> c_4(g_2^#(x, x)) , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y)) , f_3^#(x) -> c_6(g_3^#(x, x)) , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y)) , f_4^#(x) -> c_8(g_4^#(x, x)) , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y)) , f_5^#(x) -> c_10(g_5^#(x, x)) , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) , f_6^#(x) -> c_12(g_6^#(x, x)) , g_6^#(s(x), y) -> c_13(f_5^#(y), g_6^#(x, y)) , f_7^#(x) -> c_14(g_7^#(x, x)) , g_7^#(s(x), y) -> c_15(f_6^#(y), g_7^#(x, y)) , f_8^#(x) -> c_16(g_8^#(x, x)) , g_8^#(s(x), y) -> c_17(f_7^#(y), g_8^#(x, y)) , f_9^#(x) -> c_18(g_9^#(x, x)) , g_9^#(s(x), y) -> c_19(f_8^#(y), g_9^#(x, y)) , f_10^#(x) -> c_20(g_10^#(x, x)) , g_10^#(s(x), y) -> c_21(f_9^#(y), g_10^#(x, y)) } Strict Trs: { f_0(x) -> a() , f_1(x) -> g_1(x, x) , g_1(s(x), y) -> b(f_0(y), g_1(x, y)) , f_2(x) -> g_2(x, x) , g_2(s(x), y) -> b(f_1(y), g_2(x, y)) , f_3(x) -> g_3(x, x) , g_3(s(x), y) -> b(f_2(y), g_3(x, y)) , f_4(x) -> g_4(x, x) , g_4(s(x), y) -> b(f_3(y), g_4(x, y)) , f_5(x) -> g_5(x, x) , g_5(s(x), y) -> b(f_4(y), g_5(x, y)) , f_6(x) -> g_6(x, x) , g_6(s(x), y) -> b(f_5(y), g_6(x, y)) , f_7(x) -> g_7(x, x) , g_7(s(x), y) -> b(f_6(y), g_7(x, y)) , f_8(x) -> g_8(x, x) , g_8(s(x), y) -> b(f_7(y), g_8(x, y)) , f_9(x) -> g_9(x, x) , g_9(s(x), y) -> b(f_8(y), g_9(x, y)) , f_10(x) -> g_10(x, x) , g_10(s(x), y) -> b(f_9(y), g_10(x, y)) } Weak DPs: { f_0^#(x) -> c_1() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..