MAYBE 1011.26/297.07 MAYBE 1011.26/297.07 1011.26/297.07 We are left with following problem, upon which TcT provides the 1011.26/297.07 certificate MAYBE. 1011.26/297.07 1011.26/297.07 Strict Trs: 1011.26/297.07 { letexp(x, y) -> letexp(Cons(Cons(Nil(), Nil()), x), y) 1011.26/297.07 , goal(x, y) -> letexp(x, y) } 1011.26/297.07 Obligation: 1011.26/297.07 innermost runtime complexity 1011.26/297.07 Answer: 1011.26/297.07 MAYBE 1011.26/297.07 1011.26/297.07 None of the processors succeeded. 1011.26/297.07 1011.26/297.07 Details of failed attempt(s): 1011.26/297.07 ----------------------------- 1011.26/297.07 1) 'empty' failed due to the following reason: 1011.26/297.07 1011.26/297.07 Empty strict component of the problem is NOT empty. 1011.26/297.07 1011.26/297.07 2) 'Best' failed due to the following reason: 1011.26/297.07 1011.26/297.07 None of the processors succeeded. 1011.26/297.07 1011.26/297.07 Details of failed attempt(s): 1011.26/297.07 ----------------------------- 1011.26/297.07 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1011.26/297.07 following reason: 1011.26/297.07 1011.26/297.07 Computation stopped due to timeout after 297.0 seconds. 1011.26/297.07 1011.26/297.07 2) 'Best' failed due to the following reason: 1011.26/297.07 1011.26/297.07 None of the processors succeeded. 1011.26/297.07 1011.26/297.07 Details of failed attempt(s): 1011.26/297.07 ----------------------------- 1011.26/297.07 1) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1011.26/297.07 failed due to the following reason: 1011.26/297.07 1011.26/297.07 Computation stopped due to timeout after 24.0 seconds. 1011.26/297.07 1011.26/297.07 2) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1011.26/297.07 seconds)' failed due to the following reason: 1011.26/297.07 1011.26/297.07 We use the processor 'matrix interpretation of dimension 1' to 1011.26/297.07 orient following rules strictly. 1011.26/297.07 1011.26/297.07 Trs: { goal(x, y) -> letexp(x, y) } 1011.26/297.07 1011.26/297.07 The induced complexity on above rules (modulo remaining rules) is 1011.26/297.07 YES(?,O(n^1)) . These rules are moved into the corresponding weak 1011.26/297.07 component(s). 1011.26/297.07 1011.26/297.07 Sub-proof: 1011.26/297.07 ---------- 1011.26/297.07 The following argument positions are usable: 1011.26/297.07 none 1011.26/297.07 1011.26/297.07 TcT has computed the following constructor-based matrix 1011.26/297.07 interpretation satisfying not(EDA). 1011.26/297.07 1011.26/297.07 [letexp](x1, x2) = [7] x1 + [7] x2 + [3] 1011.26/297.07 1011.26/297.07 [Cons](x1, x2) = [1] x1 + [1] x2 + [0] 1011.26/297.07 1011.26/297.07 [Nil] = [0] 1011.26/297.07 1011.26/297.07 [goal](x1, x2) = [7] x1 + [7] x2 + [7] 1011.26/297.07 1011.26/297.07 The order satisfies the following ordering constraints: 1011.26/297.07 1011.26/297.07 [letexp(x, y)] = [7] x + [7] y + [3] 1011.26/297.07 >= [7] x + [7] y + [3] 1011.26/297.07 = [letexp(Cons(Cons(Nil(), Nil()), x), y)] 1011.26/297.07 1011.26/297.07 [goal(x, y)] = [7] x + [7] y + [7] 1011.26/297.07 > [7] x + [7] y + [3] 1011.26/297.07 = [letexp(x, y)] 1011.26/297.07 1011.26/297.07 1011.26/297.07 We return to the main proof. 1011.26/297.07 1011.26/297.07 We are left with following problem, upon which TcT provides the 1011.26/297.07 certificate MAYBE. 1011.26/297.08 1011.26/297.08 Strict Trs: 1011.26/297.08 { letexp(x, y) -> letexp(Cons(Cons(Nil(), Nil()), x), y) } 1011.26/297.08 Weak Trs: { goal(x, y) -> letexp(x, y) } 1011.26/297.08 Obligation: 1011.26/297.08 innermost runtime complexity 1011.26/297.08 Answer: 1011.26/297.08 MAYBE 1011.26/297.08 1011.26/297.08 None of the processors succeeded. 1011.26/297.08 1011.26/297.08 Details of failed attempt(s): 1011.26/297.08 ----------------------------- 1011.26/297.08 1) 'empty' failed due to the following reason: 1011.26/297.08 1011.26/297.08 Empty strict component of the problem is NOT empty. 1011.26/297.08 1011.26/297.08 2) 'With Problem ...' failed due to the following reason: 1011.26/297.08 1011.26/297.08 None of the processors succeeded. 1011.26/297.08 1011.26/297.08 Details of failed attempt(s): 1011.26/297.08 ----------------------------- 1011.26/297.08 1) 'empty' failed due to the following reason: 1011.26/297.08 1011.26/297.08 Empty strict component of the problem is NOT empty. 1011.26/297.08 1011.26/297.08 2) 'Fastest' failed due to the following reason: 1011.26/297.08 1011.26/297.08 None of the processors succeeded. 1011.26/297.08 1011.26/297.08 Details of failed attempt(s): 1011.26/297.08 ----------------------------- 1011.26/297.08 1) 'With Problem ...' failed due to the following reason: 1011.26/297.08 1011.26/297.08 None of the processors succeeded. 1011.26/297.08 1011.26/297.08 Details of failed attempt(s): 1011.26/297.08 ----------------------------- 1011.26/297.08 1) 'empty' failed due to the following reason: 1011.26/297.08 1011.26/297.08 Empty strict component of the problem is NOT empty. 1011.26/297.08 1011.26/297.08 2) 'With Problem ...' failed due to the following reason: 1011.26/297.08 1011.26/297.08 None of the processors succeeded. 1011.26/297.08 1011.26/297.08 Details of failed attempt(s): 1011.26/297.08 ----------------------------- 1011.26/297.08 1) 'empty' failed due to the following reason: 1011.26/297.08 1011.26/297.08 Empty strict component of the problem is NOT empty. 1011.26/297.08 1011.26/297.08 2) 'With Problem ...' failed due to the following reason: 1011.26/297.08 1011.26/297.08 None of the processors succeeded. 1011.26/297.08 1011.26/297.08 Details of failed attempt(s): 1011.26/297.08 ----------------------------- 1011.26/297.08 1) 'empty' failed due to the following reason: 1011.26/297.08 1011.26/297.08 Empty strict component of the problem is NOT empty. 1011.26/297.08 1011.26/297.08 2) 'With Problem ...' failed due to the following reason: 1011.26/297.08 1011.26/297.08 Empty strict component of the problem is NOT empty. 1011.26/297.08 1011.26/297.08 1011.26/297.08 1011.26/297.08 1011.26/297.08 2) 'With Problem ...' failed due to the following reason: 1011.26/297.08 1011.26/297.08 None of the processors succeeded. 1011.26/297.08 1011.26/297.08 Details of failed attempt(s): 1011.26/297.08 ----------------------------- 1011.26/297.08 1) 'empty' failed due to the following reason: 1011.26/297.08 1011.26/297.08 Empty strict component of the problem is NOT empty. 1011.26/297.08 1011.26/297.08 2) 'With Problem ...' failed due to the following reason: 1011.26/297.08 1011.26/297.08 Empty strict component of the problem is NOT empty. 1011.26/297.08 1011.26/297.08 1011.26/297.08 1011.26/297.08 1011.26/297.08 1011.26/297.08 3) 'Best' failed due to the following reason: 1011.26/297.08 1011.26/297.08 None of the processors succeeded. 1011.26/297.08 1011.26/297.08 Details of failed attempt(s): 1011.26/297.08 ----------------------------- 1011.26/297.08 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1011.26/297.08 following reason: 1011.26/297.08 1011.26/297.08 The input cannot be shown compatible 1011.26/297.08 1011.26/297.08 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1011.26/297.08 to the following reason: 1011.26/297.08 1011.26/297.08 The input cannot be shown compatible 1011.26/297.08 1011.26/297.08 1011.26/297.08 1011.26/297.08 1011.26/297.08 1011.26/297.08 Arrrr.. 1012.45/298.06 EOF