MAYBE 1054.15/297.89 MAYBE 1054.15/297.89 1054.15/297.89 We are left with following problem, upon which TcT provides the 1054.15/297.89 certificate MAYBE. 1054.15/297.89 1054.15/297.89 Strict Trs: 1054.15/297.89 { f(x, 0(), 0()) -> s(x) 1054.15/297.89 , f(0(), y, 0()) -> s(y) 1054.15/297.89 , f(0(), 0(), z) -> s(z) 1054.15/297.89 , f(0(), s(0()), s(0())) -> s(s(0())) 1054.15/297.89 , f(0(), s(0()), s(s(z))) -> f(0(), s(0()), z) 1054.15/297.89 , f(0(), s(s(y)), s(0())) -> f(0(), y, s(0())) 1054.15/297.89 , f(0(), s(s(y)), s(s(z))) -> f(0(), y, f(0(), s(s(y)), s(z))) 1054.15/297.89 , f(s(x), 0(), s(z)) -> f(x, s(0()), z) 1054.15/297.89 , f(s(x), s(y), 0()) -> f(x, y, s(0())) 1054.15/297.89 , f(s(x), s(y), s(z)) -> f(x, y, f(s(x), s(y), z)) 1054.15/297.89 , f(s(0()), y, z) -> f(0(), s(y), s(z)) } 1054.15/297.89 Obligation: 1054.15/297.89 runtime complexity 1054.15/297.89 Answer: 1054.15/297.89 MAYBE 1054.15/297.89 1054.15/297.89 None of the processors succeeded. 1054.15/297.89 1054.15/297.89 Details of failed attempt(s): 1054.15/297.89 ----------------------------- 1054.15/297.89 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1054.15/297.89 following reason: 1054.15/297.89 1054.15/297.89 Computation stopped due to timeout after 297.0 seconds. 1054.15/297.89 1054.15/297.89 2) 'Best' failed due to the following reason: 1054.15/297.89 1054.15/297.89 None of the processors succeeded. 1054.15/297.89 1054.15/297.89 Details of failed attempt(s): 1054.15/297.89 ----------------------------- 1054.15/297.89 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1054.15/297.89 seconds)' failed due to the following reason: 1054.15/297.89 1054.15/297.89 Computation stopped due to timeout after 148.0 seconds. 1054.15/297.89 1054.15/297.89 2) 'Best' failed due to the following reason: 1054.15/297.89 1054.15/297.89 None of the processors succeeded. 1054.15/297.89 1054.15/297.89 Details of failed attempt(s): 1054.15/297.89 ----------------------------- 1054.15/297.89 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1054.15/297.89 to the following reason: 1054.15/297.89 1054.15/297.89 The processor is inapplicable, reason: 1054.15/297.89 Processor only applicable for innermost runtime complexity analysis 1054.15/297.89 1054.15/297.89 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1054.15/297.89 following reason: 1054.15/297.89 1054.15/297.89 The processor is inapplicable, reason: 1054.15/297.89 Processor only applicable for innermost runtime complexity analysis 1054.15/297.89 1054.15/297.89 1054.15/297.89 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1054.15/297.89 failed due to the following reason: 1054.15/297.89 1054.15/297.89 None of the processors succeeded. 1054.15/297.89 1054.15/297.89 Details of failed attempt(s): 1054.15/297.89 ----------------------------- 1054.15/297.89 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1054.15/297.89 failed due to the following reason: 1054.15/297.89 1054.15/297.89 match-boundness of the problem could not be verified. 1054.15/297.89 1054.15/297.89 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1054.15/297.89 failed due to the following reason: 1054.15/297.89 1054.15/297.89 match-boundness of the problem could not be verified. 1054.15/297.89 1054.15/297.89 1054.15/297.89 1054.15/297.89 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1054.15/297.89 the following reason: 1054.15/297.89 1054.15/297.89 We add the following weak dependency pairs: 1054.15/297.89 1054.15/297.89 Strict DPs: 1054.15/297.89 { f^#(x, 0(), 0()) -> c_1(x) 1054.15/297.89 , f^#(0(), y, 0()) -> c_2(y) 1054.15/297.89 , f^#(0(), 0(), z) -> c_3(z) 1054.15/297.89 , f^#(0(), s(0()), s(0())) -> c_4() 1054.15/297.89 , f^#(0(), s(0()), s(s(z))) -> c_5(f^#(0(), s(0()), z)) 1054.15/297.89 , f^#(0(), s(s(y)), s(0())) -> c_6(f^#(0(), y, s(0()))) 1054.15/297.89 , f^#(0(), s(s(y)), s(s(z))) -> 1054.15/297.89 c_7(f^#(0(), y, f(0(), s(s(y)), s(z)))) 1054.15/297.89 , f^#(s(x), 0(), s(z)) -> c_8(f^#(x, s(0()), z)) 1054.15/297.89 , f^#(s(x), s(y), 0()) -> c_9(f^#(x, y, s(0()))) 1054.15/297.89 , f^#(s(x), s(y), s(z)) -> c_10(f^#(x, y, f(s(x), s(y), z))) 1054.15/297.89 , f^#(s(0()), y, z) -> c_11(f^#(0(), s(y), s(z))) } 1054.15/297.89 1054.15/297.89 and mark the set of starting terms. 1054.15/297.89 1054.15/297.89 We are left with following problem, upon which TcT provides the 1054.15/297.89 certificate MAYBE. 1054.15/297.89 1054.15/297.89 Strict DPs: 1054.15/297.89 { f^#(x, 0(), 0()) -> c_1(x) 1054.15/297.89 , f^#(0(), y, 0()) -> c_2(y) 1054.15/297.89 , f^#(0(), 0(), z) -> c_3(z) 1054.15/297.89 , f^#(0(), s(0()), s(0())) -> c_4() 1054.15/297.89 , f^#(0(), s(0()), s(s(z))) -> c_5(f^#(0(), s(0()), z)) 1054.15/297.89 , f^#(0(), s(s(y)), s(0())) -> c_6(f^#(0(), y, s(0()))) 1054.15/297.89 , f^#(0(), s(s(y)), s(s(z))) -> 1054.15/297.89 c_7(f^#(0(), y, f(0(), s(s(y)), s(z)))) 1054.15/297.89 , f^#(s(x), 0(), s(z)) -> c_8(f^#(x, s(0()), z)) 1054.15/297.89 , f^#(s(x), s(y), 0()) -> c_9(f^#(x, y, s(0()))) 1054.15/297.89 , f^#(s(x), s(y), s(z)) -> c_10(f^#(x, y, f(s(x), s(y), z))) 1054.15/297.89 , f^#(s(0()), y, z) -> c_11(f^#(0(), s(y), s(z))) } 1054.15/297.89 Strict Trs: 1054.15/297.89 { f(x, 0(), 0()) -> s(x) 1054.15/297.89 , f(0(), y, 0()) -> s(y) 1054.15/297.89 , f(0(), 0(), z) -> s(z) 1054.15/297.89 , f(0(), s(0()), s(0())) -> s(s(0())) 1054.15/297.89 , f(0(), s(0()), s(s(z))) -> f(0(), s(0()), z) 1054.15/297.89 , f(0(), s(s(y)), s(0())) -> f(0(), y, s(0())) 1054.15/297.89 , f(0(), s(s(y)), s(s(z))) -> f(0(), y, f(0(), s(s(y)), s(z))) 1054.15/297.89 , f(s(x), 0(), s(z)) -> f(x, s(0()), z) 1054.15/297.89 , f(s(x), s(y), 0()) -> f(x, y, s(0())) 1054.15/297.89 , f(s(x), s(y), s(z)) -> f(x, y, f(s(x), s(y), z)) 1054.15/297.89 , f(s(0()), y, z) -> f(0(), s(y), s(z)) } 1054.15/297.89 Obligation: 1054.15/297.89 runtime complexity 1054.15/297.89 Answer: 1054.15/297.89 MAYBE 1054.15/297.89 1054.15/297.89 We estimate the number of application of {4} by applications of 1054.15/297.89 Pre({4}) = {1,2,3,5,6,7,8,9,10,11}. Here rules are labeled as 1054.15/297.89 follows: 1054.15/297.89 1054.15/297.89 DPs: 1054.15/297.89 { 1: f^#(x, 0(), 0()) -> c_1(x) 1054.15/297.89 , 2: f^#(0(), y, 0()) -> c_2(y) 1054.15/297.89 , 3: f^#(0(), 0(), z) -> c_3(z) 1054.15/297.89 , 4: f^#(0(), s(0()), s(0())) -> c_4() 1054.15/297.89 , 5: f^#(0(), s(0()), s(s(z))) -> c_5(f^#(0(), s(0()), z)) 1054.15/297.89 , 6: f^#(0(), s(s(y)), s(0())) -> c_6(f^#(0(), y, s(0()))) 1054.15/297.89 , 7: f^#(0(), s(s(y)), s(s(z))) -> 1054.15/297.89 c_7(f^#(0(), y, f(0(), s(s(y)), s(z)))) 1054.15/297.89 , 8: f^#(s(x), 0(), s(z)) -> c_8(f^#(x, s(0()), z)) 1054.15/297.89 , 9: f^#(s(x), s(y), 0()) -> c_9(f^#(x, y, s(0()))) 1054.15/297.89 , 10: f^#(s(x), s(y), s(z)) -> c_10(f^#(x, y, f(s(x), s(y), z))) 1054.15/297.89 , 11: f^#(s(0()), y, z) -> c_11(f^#(0(), s(y), s(z))) } 1054.15/297.89 1054.15/297.89 We are left with following problem, upon which TcT provides the 1054.15/297.89 certificate MAYBE. 1054.15/297.89 1054.15/297.89 Strict DPs: 1054.15/297.89 { f^#(x, 0(), 0()) -> c_1(x) 1054.15/297.89 , f^#(0(), y, 0()) -> c_2(y) 1054.15/297.89 , f^#(0(), 0(), z) -> c_3(z) 1054.15/297.89 , f^#(0(), s(0()), s(s(z))) -> c_5(f^#(0(), s(0()), z)) 1054.15/297.89 , f^#(0(), s(s(y)), s(0())) -> c_6(f^#(0(), y, s(0()))) 1054.15/297.89 , f^#(0(), s(s(y)), s(s(z))) -> 1054.15/297.89 c_7(f^#(0(), y, f(0(), s(s(y)), s(z)))) 1054.15/297.89 , f^#(s(x), 0(), s(z)) -> c_8(f^#(x, s(0()), z)) 1054.15/297.89 , f^#(s(x), s(y), 0()) -> c_9(f^#(x, y, s(0()))) 1054.15/297.89 , f^#(s(x), s(y), s(z)) -> c_10(f^#(x, y, f(s(x), s(y), z))) 1054.15/297.89 , f^#(s(0()), y, z) -> c_11(f^#(0(), s(y), s(z))) } 1054.15/297.89 Strict Trs: 1054.15/297.89 { f(x, 0(), 0()) -> s(x) 1054.15/297.89 , f(0(), y, 0()) -> s(y) 1054.15/297.89 , f(0(), 0(), z) -> s(z) 1054.15/297.89 , f(0(), s(0()), s(0())) -> s(s(0())) 1054.15/297.89 , f(0(), s(0()), s(s(z))) -> f(0(), s(0()), z) 1054.15/297.89 , f(0(), s(s(y)), s(0())) -> f(0(), y, s(0())) 1054.15/297.89 , f(0(), s(s(y)), s(s(z))) -> f(0(), y, f(0(), s(s(y)), s(z))) 1054.15/297.89 , f(s(x), 0(), s(z)) -> f(x, s(0()), z) 1054.15/297.89 , f(s(x), s(y), 0()) -> f(x, y, s(0())) 1054.15/297.89 , f(s(x), s(y), s(z)) -> f(x, y, f(s(x), s(y), z)) 1054.15/297.89 , f(s(0()), y, z) -> f(0(), s(y), s(z)) } 1054.15/297.89 Weak DPs: { f^#(0(), s(0()), s(0())) -> c_4() } 1054.15/297.89 Obligation: 1054.15/297.89 runtime complexity 1054.15/297.89 Answer: 1054.15/297.89 MAYBE 1054.15/297.89 1054.15/297.89 Empty strict component of the problem is NOT empty. 1054.15/297.89 1054.15/297.89 1054.15/297.89 Arrrr.. 1055.32/298.76 EOF