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