MAYBE 788.62/297.08 MAYBE 788.62/297.08 788.62/297.08 We are left with following problem, upon which TcT provides the 788.62/297.08 certificate MAYBE. 788.62/297.08 788.62/297.08 Strict Trs: 788.62/297.08 { le(0(), y) -> true() 788.62/297.08 , le(s(x), 0()) -> false() 788.62/297.08 , le(s(x), s(y)) -> le(x, y) 788.62/297.08 , inc(0()) -> 0() 788.62/297.08 , inc(s(x)) -> s(inc(x)) 788.62/297.08 , minus(x, 0()) -> x 788.62/297.08 , minus(0(), y) -> 0() 788.62/297.08 , minus(s(x), s(y)) -> minus(x, y) 788.62/297.08 , quot(0(), s(y)) -> 0() 788.62/297.08 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 788.62/297.08 , log(x) -> log2(x, 0()) 788.62/297.08 , log2(x, y) -> if(le(x, 0()), le(x, s(0())), x, inc(y)) 788.62/297.08 , if(true(), b, x, y) -> log_undefined() 788.62/297.08 , if(false(), b, x, y) -> if2(b, x, y) 788.62/297.08 , if2(true(), x, s(y)) -> y 788.62/297.08 , if2(false(), x, y) -> log2(quot(x, s(s(0()))), y) } 788.62/297.08 Obligation: 788.62/297.08 runtime complexity 788.62/297.08 Answer: 788.62/297.08 MAYBE 788.62/297.08 788.62/297.08 None of the processors succeeded. 788.62/297.08 788.62/297.08 Details of failed attempt(s): 788.62/297.08 ----------------------------- 788.62/297.08 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 788.62/297.08 following reason: 788.62/297.08 788.62/297.08 Computation stopped due to timeout after 297.0 seconds. 788.62/297.08 788.62/297.08 2) 'Best' failed due to the following reason: 788.62/297.08 788.62/297.08 None of the processors succeeded. 788.62/297.08 788.62/297.08 Details of failed attempt(s): 788.62/297.08 ----------------------------- 788.62/297.08 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 788.62/297.08 seconds)' failed due to the following reason: 788.62/297.08 788.62/297.08 Computation stopped due to timeout after 148.0 seconds. 788.62/297.08 788.62/297.08 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 788.62/297.08 failed due to the following reason: 788.62/297.08 788.62/297.08 None of the processors succeeded. 788.62/297.08 788.62/297.08 Details of failed attempt(s): 788.62/297.08 ----------------------------- 788.62/297.08 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 788.62/297.08 failed due to the following reason: 788.62/297.08 788.62/297.08 match-boundness of the problem could not be verified. 788.62/297.08 788.62/297.08 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 788.62/297.08 failed due to the following reason: 788.62/297.08 788.62/297.08 match-boundness of the problem could not be verified. 788.62/297.08 788.62/297.08 788.62/297.08 3) 'Best' failed due to the following reason: 788.62/297.08 788.62/297.08 None of the processors succeeded. 788.62/297.08 788.62/297.08 Details of failed attempt(s): 788.62/297.08 ----------------------------- 788.62/297.08 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 788.62/297.08 to the following reason: 788.62/297.08 788.62/297.08 The processor is inapplicable, reason: 788.62/297.08 Processor only applicable for innermost runtime complexity analysis 788.62/297.08 788.62/297.08 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 788.62/297.08 following reason: 788.62/297.08 788.62/297.08 The processor is inapplicable, reason: 788.62/297.08 Processor only applicable for innermost runtime complexity analysis 788.62/297.08 788.62/297.08 788.62/297.08 788.62/297.08 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 788.62/297.08 the following reason: 788.62/297.08 788.62/297.08 We add the following weak dependency pairs: 788.62/297.08 788.62/297.08 Strict DPs: 788.62/297.08 { le^#(0(), y) -> c_1() 788.62/297.08 , le^#(s(x), 0()) -> c_2() 788.62/297.08 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 788.62/297.08 , inc^#(0()) -> c_4() 788.62/297.08 , inc^#(s(x)) -> c_5(inc^#(x)) 788.62/297.08 , minus^#(x, 0()) -> c_6(x) 788.62/297.08 , minus^#(0(), y) -> c_7() 788.62/297.08 , minus^#(s(x), s(y)) -> c_8(minus^#(x, y)) 788.62/297.08 , quot^#(0(), s(y)) -> c_9() 788.62/297.08 , quot^#(s(x), s(y)) -> c_10(quot^#(minus(x, y), s(y))) 788.62/297.08 , log^#(x) -> c_11(log2^#(x, 0())) 788.62/297.08 , log2^#(x, y) -> c_12(if^#(le(x, 0()), le(x, s(0())), x, inc(y))) 788.62/297.08 , if^#(true(), b, x, y) -> c_13() 788.62/297.08 , if^#(false(), b, x, y) -> c_14(if2^#(b, x, y)) 788.62/297.08 , if2^#(true(), x, s(y)) -> c_15(y) 788.62/297.08 , if2^#(false(), x, y) -> c_16(log2^#(quot(x, s(s(0()))), y)) } 788.62/297.08 788.62/297.08 and mark the set of starting terms. 788.62/297.08 788.62/297.08 We are left with following problem, upon which TcT provides the 788.62/297.08 certificate MAYBE. 788.62/297.08 788.62/297.08 Strict DPs: 788.62/297.08 { le^#(0(), y) -> c_1() 788.62/297.08 , le^#(s(x), 0()) -> c_2() 788.62/297.08 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 788.62/297.08 , inc^#(0()) -> c_4() 788.62/297.08 , inc^#(s(x)) -> c_5(inc^#(x)) 788.62/297.08 , minus^#(x, 0()) -> c_6(x) 788.62/297.08 , minus^#(0(), y) -> c_7() 788.62/297.08 , minus^#(s(x), s(y)) -> c_8(minus^#(x, y)) 788.62/297.08 , quot^#(0(), s(y)) -> c_9() 788.62/297.08 , quot^#(s(x), s(y)) -> c_10(quot^#(minus(x, y), s(y))) 788.62/297.08 , log^#(x) -> c_11(log2^#(x, 0())) 788.62/297.08 , log2^#(x, y) -> c_12(if^#(le(x, 0()), le(x, s(0())), x, inc(y))) 788.62/297.08 , if^#(true(), b, x, y) -> c_13() 788.62/297.08 , if^#(false(), b, x, y) -> c_14(if2^#(b, x, y)) 788.62/297.08 , if2^#(true(), x, s(y)) -> c_15(y) 788.62/297.08 , if2^#(false(), x, y) -> c_16(log2^#(quot(x, s(s(0()))), y)) } 788.62/297.08 Strict Trs: 788.62/297.08 { le(0(), y) -> true() 788.62/297.08 , le(s(x), 0()) -> false() 788.62/297.08 , le(s(x), s(y)) -> le(x, y) 788.62/297.08 , inc(0()) -> 0() 788.62/297.08 , inc(s(x)) -> s(inc(x)) 788.62/297.08 , minus(x, 0()) -> x 788.62/297.08 , minus(0(), y) -> 0() 788.62/297.08 , minus(s(x), s(y)) -> minus(x, y) 788.62/297.08 , quot(0(), s(y)) -> 0() 788.62/297.08 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 788.62/297.08 , log(x) -> log2(x, 0()) 788.62/297.08 , log2(x, y) -> if(le(x, 0()), le(x, s(0())), x, inc(y)) 788.62/297.08 , if(true(), b, x, y) -> log_undefined() 788.62/297.08 , if(false(), b, x, y) -> if2(b, x, y) 788.62/297.08 , if2(true(), x, s(y)) -> y 788.62/297.08 , if2(false(), x, y) -> log2(quot(x, s(s(0()))), y) } 788.62/297.08 Obligation: 788.62/297.08 runtime complexity 788.62/297.08 Answer: 788.62/297.08 MAYBE 788.62/297.08 788.62/297.08 We estimate the number of application of {1,2,4,7,9,13} by 788.62/297.08 applications of Pre({1,2,4,7,9,13}) = {3,5,6,8,10,12,15}. Here 788.62/297.08 rules are labeled as follows: 788.62/297.08 788.62/297.08 DPs: 788.62/297.08 { 1: le^#(0(), y) -> c_1() 788.62/297.08 , 2: le^#(s(x), 0()) -> c_2() 788.62/297.08 , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y)) 788.62/297.08 , 4: inc^#(0()) -> c_4() 788.62/297.08 , 5: inc^#(s(x)) -> c_5(inc^#(x)) 788.62/297.08 , 6: minus^#(x, 0()) -> c_6(x) 788.62/297.08 , 7: minus^#(0(), y) -> c_7() 788.62/297.08 , 8: minus^#(s(x), s(y)) -> c_8(minus^#(x, y)) 788.62/297.08 , 9: quot^#(0(), s(y)) -> c_9() 788.62/297.08 , 10: quot^#(s(x), s(y)) -> c_10(quot^#(minus(x, y), s(y))) 788.62/297.08 , 11: log^#(x) -> c_11(log2^#(x, 0())) 788.62/297.08 , 12: log2^#(x, y) -> 788.62/297.08 c_12(if^#(le(x, 0()), le(x, s(0())), x, inc(y))) 788.62/297.08 , 13: if^#(true(), b, x, y) -> c_13() 788.62/297.08 , 14: if^#(false(), b, x, y) -> c_14(if2^#(b, x, y)) 788.62/297.08 , 15: if2^#(true(), x, s(y)) -> c_15(y) 788.62/297.08 , 16: if2^#(false(), x, y) -> c_16(log2^#(quot(x, s(s(0()))), y)) } 788.62/297.08 788.62/297.08 We are left with following problem, upon which TcT provides the 788.62/297.08 certificate MAYBE. 788.62/297.08 788.62/297.08 Strict DPs: 788.62/297.08 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 788.62/297.08 , inc^#(s(x)) -> c_5(inc^#(x)) 788.62/297.08 , minus^#(x, 0()) -> c_6(x) 788.62/297.08 , minus^#(s(x), s(y)) -> c_8(minus^#(x, y)) 788.62/297.08 , quot^#(s(x), s(y)) -> c_10(quot^#(minus(x, y), s(y))) 788.62/297.08 , log^#(x) -> c_11(log2^#(x, 0())) 788.62/297.08 , log2^#(x, y) -> c_12(if^#(le(x, 0()), le(x, s(0())), x, inc(y))) 788.62/297.08 , if^#(false(), b, x, y) -> c_14(if2^#(b, x, y)) 788.62/297.08 , if2^#(true(), x, s(y)) -> c_15(y) 788.62/297.08 , if2^#(false(), x, y) -> c_16(log2^#(quot(x, s(s(0()))), y)) } 788.62/297.08 Strict Trs: 788.62/297.08 { le(0(), y) -> true() 788.62/297.08 , le(s(x), 0()) -> false() 788.62/297.08 , le(s(x), s(y)) -> le(x, y) 788.62/297.08 , inc(0()) -> 0() 788.62/297.08 , inc(s(x)) -> s(inc(x)) 788.62/297.08 , minus(x, 0()) -> x 788.62/297.08 , minus(0(), y) -> 0() 788.62/297.08 , minus(s(x), s(y)) -> minus(x, y) 788.62/297.08 , quot(0(), s(y)) -> 0() 788.62/297.08 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 788.62/297.08 , log(x) -> log2(x, 0()) 788.62/297.08 , log2(x, y) -> if(le(x, 0()), le(x, s(0())), x, inc(y)) 788.62/297.08 , if(true(), b, x, y) -> log_undefined() 788.62/297.08 , if(false(), b, x, y) -> if2(b, x, y) 788.62/297.08 , if2(true(), x, s(y)) -> y 788.62/297.08 , if2(false(), x, y) -> log2(quot(x, s(s(0()))), y) } 788.62/297.08 Weak DPs: 788.62/297.08 { le^#(0(), y) -> c_1() 788.62/297.08 , le^#(s(x), 0()) -> c_2() 788.62/297.08 , inc^#(0()) -> c_4() 788.62/297.08 , minus^#(0(), y) -> c_7() 788.62/297.08 , quot^#(0(), s(y)) -> c_9() 788.62/297.08 , if^#(true(), b, x, y) -> c_13() } 788.62/297.08 Obligation: 788.62/297.08 runtime complexity 788.62/297.08 Answer: 788.62/297.08 MAYBE 788.62/297.08 788.62/297.08 Empty strict component of the problem is NOT empty. 788.62/297.08 788.62/297.08 788.62/297.08 Arrrr.. 789.08/297.41 EOF