MAYBE 594.04/261.89 MAYBE 594.04/261.89 594.04/261.89 We are left with following problem, upon which TcT provides the 594.04/261.89 certificate MAYBE. 594.04/261.89 594.04/261.89 Strict Trs: 594.04/261.89 { f(x, empty()) -> x 594.04/261.89 , f(empty(), cons(a, k)) -> f(cons(a, k), k) 594.04/261.89 , f(cons(a, k), y) -> f(y, k) } 594.04/261.89 Obligation: 594.04/261.89 innermost runtime complexity 594.04/261.89 Answer: 594.04/261.89 MAYBE 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'Best' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 594.04/261.89 following reason: 594.04/261.89 594.04/261.89 We add the following weak dependency pairs: 594.04/261.89 594.04/261.89 Strict DPs: 594.04/261.89 { f^#(x, empty()) -> c_1() 594.04/261.89 , f^#(empty(), cons(a, k)) -> c_2(f^#(cons(a, k), k)) 594.04/261.89 , f^#(cons(a, k), y) -> c_3(f^#(y, k)) } 594.04/261.89 594.04/261.89 and mark the set of starting terms. 594.04/261.89 594.04/261.89 We are left with following problem, upon which TcT provides the 594.04/261.89 certificate MAYBE. 594.04/261.89 594.04/261.89 Strict DPs: 594.04/261.89 { f^#(x, empty()) -> c_1() 594.04/261.89 , f^#(empty(), cons(a, k)) -> c_2(f^#(cons(a, k), k)) 594.04/261.89 , f^#(cons(a, k), y) -> c_3(f^#(y, k)) } 594.04/261.89 Strict Trs: 594.04/261.89 { f(x, empty()) -> x 594.04/261.89 , f(empty(), cons(a, k)) -> f(cons(a, k), k) 594.04/261.89 , f(cons(a, k), y) -> f(y, k) } 594.04/261.89 Obligation: 594.04/261.89 innermost runtime complexity 594.04/261.89 Answer: 594.04/261.89 MAYBE 594.04/261.89 594.04/261.89 No rule is usable, rules are removed from the input problem. 594.04/261.89 594.04/261.89 We are left with following problem, upon which TcT provides the 594.04/261.89 certificate MAYBE. 594.04/261.89 594.04/261.89 Strict DPs: 594.04/261.89 { f^#(x, empty()) -> c_1() 594.04/261.89 , f^#(empty(), cons(a, k)) -> c_2(f^#(cons(a, k), k)) 594.04/261.89 , f^#(cons(a, k), y) -> c_3(f^#(y, k)) } 594.04/261.89 Obligation: 594.04/261.89 innermost runtime complexity 594.04/261.89 Answer: 594.04/261.89 MAYBE 594.04/261.89 594.04/261.89 The weightgap principle applies (using the following constant 594.04/261.89 growth matrix-interpretation) 594.04/261.89 594.04/261.89 The following argument positions are usable: 594.04/261.89 Uargs(c_2) = {1}, Uargs(c_3) = {1} 594.04/261.89 594.04/261.89 TcT has computed the following constructor-restricted matrix 594.04/261.89 interpretation. 594.04/261.89 594.04/261.89 [empty] = [0] 594.04/261.89 [0] 594.04/261.89 594.04/261.89 [cons](x1, x2) = [1 0] x1 + [0] 594.04/261.89 [0 0] [0] 594.04/261.89 594.04/261.89 [f^#](x1, x2) = [1] 594.04/261.89 [0] 594.04/261.89 594.04/261.89 [c_1] = [0] 594.04/261.89 [0] 594.04/261.89 594.04/261.89 [c_2](x1) = [1 0] x1 + [0] 594.04/261.89 [0 1] [2] 594.04/261.89 594.04/261.89 [c_3](x1) = [1 0] x1 + [1] 594.04/261.89 [0 1] [0] 594.04/261.89 594.04/261.89 The order satisfies the following ordering constraints: 594.04/261.89 594.04/261.89 [f^#(x, empty())] = [1] 594.04/261.89 [0] 594.04/261.89 > [0] 594.04/261.89 [0] 594.04/261.89 = [c_1()] 594.04/261.89 594.04/261.89 [f^#(empty(), cons(a, k))] = [1] 594.04/261.89 [0] 594.04/261.89 ? [1] 594.04/261.89 [2] 594.04/261.89 = [c_2(f^#(cons(a, k), k))] 594.04/261.89 594.04/261.89 [f^#(cons(a, k), y)] = [1] 594.04/261.89 [0] 594.04/261.89 ? [2] 594.04/261.89 [0] 594.04/261.89 = [c_3(f^#(y, k))] 594.04/261.89 594.04/261.89 594.04/261.89 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 594.04/261.89 594.04/261.89 We are left with following problem, upon which TcT provides the 594.04/261.89 certificate MAYBE. 594.04/261.89 594.04/261.89 Strict DPs: 594.04/261.89 { f^#(empty(), cons(a, k)) -> c_2(f^#(cons(a, k), k)) 594.04/261.89 , f^#(cons(a, k), y) -> c_3(f^#(y, k)) } 594.04/261.89 Weak DPs: { f^#(x, empty()) -> c_1() } 594.04/261.89 Obligation: 594.04/261.89 innermost runtime complexity 594.04/261.89 Answer: 594.04/261.89 MAYBE 594.04/261.89 594.04/261.89 The following weak DPs constitute a sub-graph of the DG that is 594.04/261.89 closed under successors. The DPs are removed. 594.04/261.89 594.04/261.89 { f^#(x, empty()) -> c_1() } 594.04/261.89 594.04/261.89 We are left with following problem, upon which TcT provides the 594.04/261.89 certificate MAYBE. 594.04/261.89 594.04/261.89 Strict DPs: 594.04/261.89 { f^#(empty(), cons(a, k)) -> c_2(f^#(cons(a, k), k)) 594.04/261.89 , f^#(cons(a, k), y) -> c_3(f^#(y, k)) } 594.04/261.89 Obligation: 594.04/261.89 innermost runtime complexity 594.04/261.89 Answer: 594.04/261.89 MAYBE 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'Fastest' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'Polynomial Path Order (PS)' failed due to the following reason: 594.04/261.89 594.04/261.89 The input cannot be shown compatible 594.04/261.89 594.04/261.89 594.04/261.89 2) 'Polynomial Path Order (PS)' failed due to the following reason: 594.04/261.89 594.04/261.89 The input cannot be shown compatible 594.04/261.89 594.04/261.89 3) 'Fastest (timeout of 24 seconds)' failed due to the following 594.04/261.89 reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 594.04/261.89 failed due to the following reason: 594.04/261.89 594.04/261.89 match-boundness of the problem could not be verified. 594.04/261.89 594.04/261.89 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 594.04/261.89 failed due to the following reason: 594.04/261.89 594.04/261.89 match-boundness of the problem could not be verified. 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 2) 'Best' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 594.04/261.89 seconds)' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'Fastest' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 2) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'empty' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 2) 'With Problem ...' failed due to the following reason: 594.04/261.89 594.04/261.89 Empty strict component of the problem is NOT empty. 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 2) 'Best' failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 594.04/261.89 to the following reason: 594.04/261.89 594.04/261.89 The input cannot be shown compatible 594.04/261.89 594.04/261.89 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 594.04/261.89 following reason: 594.04/261.89 594.04/261.89 The input cannot be shown compatible 594.04/261.89 594.04/261.89 594.04/261.89 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 594.04/261.89 failed due to the following reason: 594.04/261.89 594.04/261.89 None of the processors succeeded. 594.04/261.89 594.04/261.89 Details of failed attempt(s): 594.04/261.89 ----------------------------- 594.04/261.89 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 594.04/261.89 failed due to the following reason: 594.04/261.89 594.04/261.89 match-boundness of the problem could not be verified. 594.04/261.89 594.04/261.89 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 594.04/261.89 failed due to the following reason: 594.04/261.89 594.04/261.89 match-boundness of the problem could not be verified. 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 594.04/261.89 Arrrr.. 594.43/262.07 EOF