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