MAYBE 17.56/5.95 MAYBE 17.56/5.95 17.56/5.95 We are left with following problem, upon which TcT provides the 17.56/5.95 certificate MAYBE. 17.56/5.95 17.56/5.95 Strict Trs: 17.56/5.95 { f(0()) -> 1() 17.56/5.95 , f(s(x)) -> g(f(x)) 17.56/5.95 , f(s(x)) -> +(f(x), s(f(x))) 17.56/5.95 , g(x) -> +(x, s(x)) } 17.56/5.95 Obligation: 17.56/5.95 innermost runtime complexity 17.56/5.95 Answer: 17.56/5.95 MAYBE 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'Best' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'Best' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 17.56/5.95 seconds)' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'Fastest' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 2) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 2) 'Best' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 17.56/5.95 following reason: 17.56/5.95 17.56/5.95 The input cannot be shown compatible 17.56/5.95 17.56/5.95 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 17.56/5.95 to the following reason: 17.56/5.95 17.56/5.95 The input cannot be shown compatible 17.56/5.95 17.56/5.95 17.56/5.95 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 17.56/5.95 failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 17.56/5.95 failed due to the following reason: 17.56/5.95 17.56/5.95 match-boundness of the problem could not be verified. 17.56/5.95 17.56/5.95 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 17.56/5.95 failed due to the following reason: 17.56/5.95 17.56/5.95 match-boundness of the problem could not be verified. 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 2) 'With Problem ... (timeout of 297 seconds)' failed due to the 17.56/5.95 following reason: 17.56/5.95 17.56/5.95 We add the following dependency tuples: 17.56/5.95 17.56/5.95 Strict DPs: 17.56/5.95 { f^#(0()) -> c_1() 17.56/5.95 , f^#(s(x)) -> c_2(g^#(f(x)), f^#(x)) 17.56/5.95 , f^#(s(x)) -> c_3(f^#(x), f^#(x)) 17.56/5.95 , g^#(x) -> c_4() } 17.56/5.95 17.56/5.95 and mark the set of starting terms. 17.56/5.95 17.56/5.95 We are left with following problem, upon which TcT provides the 17.56/5.95 certificate MAYBE. 17.56/5.95 17.56/5.95 Strict DPs: 17.56/5.95 { f^#(0()) -> c_1() 17.56/5.95 , f^#(s(x)) -> c_2(g^#(f(x)), f^#(x)) 17.56/5.95 , f^#(s(x)) -> c_3(f^#(x), f^#(x)) 17.56/5.95 , g^#(x) -> c_4() } 17.56/5.95 Weak Trs: 17.56/5.95 { f(0()) -> 1() 17.56/5.95 , f(s(x)) -> g(f(x)) 17.56/5.95 , f(s(x)) -> +(f(x), s(f(x))) 17.56/5.95 , g(x) -> +(x, s(x)) } 17.56/5.95 Obligation: 17.56/5.95 innermost runtime complexity 17.56/5.95 Answer: 17.56/5.95 MAYBE 17.56/5.95 17.56/5.95 We estimate the number of application of {1,4} by applications of 17.56/5.95 Pre({1,4}) = {2,3}. Here rules are labeled as follows: 17.56/5.95 17.56/5.95 DPs: 17.56/5.95 { 1: f^#(0()) -> c_1() 17.56/5.95 , 2: f^#(s(x)) -> c_2(g^#(f(x)), f^#(x)) 17.56/5.95 , 3: f^#(s(x)) -> c_3(f^#(x), f^#(x)) 17.56/5.95 , 4: g^#(x) -> c_4() } 17.56/5.95 17.56/5.95 We are left with following problem, upon which TcT provides the 17.56/5.95 certificate MAYBE. 17.56/5.95 17.56/5.95 Strict DPs: 17.56/5.95 { f^#(s(x)) -> c_2(g^#(f(x)), f^#(x)) 17.56/5.95 , f^#(s(x)) -> c_3(f^#(x), f^#(x)) } 17.56/5.95 Weak DPs: 17.56/5.95 { f^#(0()) -> c_1() 17.56/5.95 , g^#(x) -> c_4() } 17.56/5.95 Weak Trs: 17.56/5.95 { f(0()) -> 1() 17.56/5.95 , f(s(x)) -> g(f(x)) 17.56/5.95 , f(s(x)) -> +(f(x), s(f(x))) 17.56/5.95 , g(x) -> +(x, s(x)) } 17.56/5.95 Obligation: 17.56/5.95 innermost runtime complexity 17.56/5.95 Answer: 17.56/5.95 MAYBE 17.56/5.95 17.56/5.95 The following weak DPs constitute a sub-graph of the DG that is 17.56/5.95 closed under successors. The DPs are removed. 17.56/5.95 17.56/5.95 { f^#(0()) -> c_1() 17.56/5.95 , g^#(x) -> c_4() } 17.56/5.95 17.56/5.95 We are left with following problem, upon which TcT provides the 17.56/5.95 certificate MAYBE. 17.56/5.95 17.56/5.95 Strict DPs: 17.56/5.95 { f^#(s(x)) -> c_2(g^#(f(x)), f^#(x)) 17.56/5.95 , f^#(s(x)) -> c_3(f^#(x), f^#(x)) } 17.56/5.95 Weak Trs: 17.56/5.95 { f(0()) -> 1() 17.56/5.95 , f(s(x)) -> g(f(x)) 17.56/5.95 , f(s(x)) -> +(f(x), s(f(x))) 17.56/5.95 , g(x) -> +(x, s(x)) } 17.56/5.95 Obligation: 17.56/5.95 innermost runtime complexity 17.56/5.95 Answer: 17.56/5.95 MAYBE 17.56/5.95 17.56/5.95 Due to missing edges in the dependency-graph, the right-hand sides 17.56/5.95 of following rules could be simplified: 17.56/5.95 17.56/5.95 { f^#(s(x)) -> c_2(g^#(f(x)), f^#(x)) } 17.56/5.95 17.56/5.95 We are left with following problem, upon which TcT provides the 17.56/5.95 certificate MAYBE. 17.56/5.95 17.56/5.95 Strict DPs: 17.56/5.95 { f^#(s(x)) -> c_1(f^#(x), f^#(x)) 17.56/5.95 , f^#(s(x)) -> c_2(f^#(x)) } 17.56/5.95 Weak Trs: 17.56/5.95 { f(0()) -> 1() 17.56/5.95 , f(s(x)) -> g(f(x)) 17.56/5.95 , f(s(x)) -> +(f(x), s(f(x))) 17.56/5.95 , g(x) -> +(x, s(x)) } 17.56/5.95 Obligation: 17.56/5.95 innermost runtime complexity 17.56/5.95 Answer: 17.56/5.95 MAYBE 17.56/5.95 17.56/5.95 No rule is usable, rules are removed from the input problem. 17.56/5.95 17.56/5.95 We are left with following problem, upon which TcT provides the 17.56/5.95 certificate MAYBE. 17.56/5.95 17.56/5.95 Strict DPs: 17.56/5.95 { f^#(s(x)) -> c_1(f^#(x), f^#(x)) 17.56/5.95 , f^#(s(x)) -> c_2(f^#(x)) } 17.56/5.95 Obligation: 17.56/5.95 innermost runtime complexity 17.56/5.95 Answer: 17.56/5.95 MAYBE 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'Fastest' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'With Problem ...' failed due to the following reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'empty' failed due to the following reason: 17.56/5.95 17.56/5.95 Empty strict component of the problem is NOT empty. 17.56/5.95 17.56/5.95 2) 'Polynomial Path Order (PS)' failed due to the following reason: 17.56/5.95 17.56/5.95 The input cannot be shown compatible 17.56/5.95 17.56/5.95 17.56/5.95 2) 'Polynomial Path Order (PS)' failed due to the following reason: 17.56/5.95 17.56/5.95 The input cannot be shown compatible 17.56/5.95 17.56/5.95 3) 'Fastest (timeout of 24 seconds)' failed due to the following 17.56/5.95 reason: 17.56/5.95 17.56/5.95 None of the processors succeeded. 17.56/5.95 17.56/5.95 Details of failed attempt(s): 17.56/5.95 ----------------------------- 17.56/5.95 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 17.56/5.95 failed due to the following reason: 17.56/5.95 17.56/5.95 match-boundness of the problem could not be verified. 17.56/5.95 17.56/5.95 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 17.56/5.95 failed due to the following reason: 17.56/5.95 17.56/5.95 match-boundness of the problem could not be verified. 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 17.56/5.95 Arrrr.. 17.56/5.96 EOF