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