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