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