MAYBE 1034.50/297.04 MAYBE 1034.50/297.04 1034.50/297.04 We are left with following problem, upon which TcT provides the 1034.50/297.04 certificate MAYBE. 1034.50/297.04 1034.50/297.04 Strict Trs: 1034.50/297.04 { isEmpty(empty()) -> true() 1034.50/297.04 , isEmpty(node(l, r)) -> false() 1034.50/297.04 , left(empty()) -> empty() 1034.50/297.04 , left(node(l, r)) -> l 1034.50/297.04 , right(empty()) -> empty() 1034.50/297.04 , right(node(l, r)) -> r 1034.50/297.04 , inc(0()) -> s(0()) 1034.50/297.04 , inc(s(x)) -> s(inc(x)) 1034.50/297.04 , count(n, x) -> 1034.50/297.04 if(isEmpty(n), 1034.50/297.04 isEmpty(left(n)), 1034.50/297.04 right(n), 1034.50/297.04 node(left(left(n)), node(right(left(n)), right(n))), 1034.50/297.04 x, 1034.50/297.04 inc(x)) 1034.50/297.04 , if(true(), b, n, m, x, y) -> x 1034.50/297.04 , if(false(), true(), n, m, x, y) -> count(n, y) 1034.50/297.04 , if(false(), false(), n, m, x, y) -> count(m, x) 1034.50/297.04 , nrOfNodes(n) -> count(n, 0()) } 1034.50/297.04 Obligation: 1034.50/297.04 innermost runtime complexity 1034.50/297.04 Answer: 1034.50/297.04 MAYBE 1034.50/297.04 1034.50/297.04 None of the processors succeeded. 1034.50/297.04 1034.50/297.04 Details of failed attempt(s): 1034.50/297.04 ----------------------------- 1034.50/297.04 1) 'empty' failed due to the following reason: 1034.50/297.04 1034.50/297.04 Empty strict component of the problem is NOT empty. 1034.50/297.04 1034.50/297.04 2) 'Best' failed due to the following reason: 1034.50/297.04 1034.50/297.04 None of the processors succeeded. 1034.50/297.04 1034.50/297.04 Details of failed attempt(s): 1034.50/297.04 ----------------------------- 1034.50/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1034.50/297.04 following reason: 1034.50/297.04 1034.50/297.04 Computation stopped due to timeout after 297.0 seconds. 1034.50/297.04 1034.50/297.04 2) 'Best' failed due to the following reason: 1034.50/297.04 1034.50/297.04 None of the processors succeeded. 1034.50/297.04 1034.50/297.04 Details of failed attempt(s): 1034.50/297.04 ----------------------------- 1034.50/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1034.50/297.04 seconds)' failed due to the following reason: 1034.50/297.04 1034.50/297.04 Computation stopped due to timeout after 148.0 seconds. 1034.50/297.04 1034.50/297.04 2) 'Best' failed due to the following reason: 1034.50/297.04 1034.50/297.04 None of the processors succeeded. 1034.50/297.04 1034.50/297.04 Details of failed attempt(s): 1034.50/297.04 ----------------------------- 1034.50/297.04 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1034.50/297.04 to the following reason: 1034.50/297.04 1034.50/297.04 The input cannot be shown compatible 1034.50/297.04 1034.50/297.04 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1034.50/297.04 following reason: 1034.50/297.04 1034.50/297.04 The input cannot be shown compatible 1034.50/297.04 1034.50/297.04 1034.50/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1034.50/297.04 failed due to the following reason: 1034.50/297.04 1034.50/297.04 None of the processors succeeded. 1034.50/297.04 1034.50/297.04 Details of failed attempt(s): 1034.50/297.04 ----------------------------- 1034.50/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1034.50/297.04 failed due to the following reason: 1034.50/297.04 1034.50/297.04 match-boundness of the problem could not be verified. 1034.50/297.04 1034.50/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1034.50/297.04 failed due to the following reason: 1034.50/297.04 1034.50/297.04 match-boundness of the problem could not be verified. 1034.50/297.04 1034.50/297.04 1034.50/297.04 1034.50/297.04 1034.50/297.04 1034.50/297.04 Arrrr.. 1035.18/297.60 EOF