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