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