MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, r)) -> false() , left(empty()) -> empty() , left(node(l, r)) -> l , right(empty()) -> empty() , right(node(l, r)) -> r , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , count(n, x) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) , if(true(), b, n, m, x, y) -> x , if(false(), true(), n, m, x, y) -> count(n, y) , if(false(), false(), n, m, x, y) -> count(m, x) , nrOfNodes(n) -> count(n, 0()) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { isEmpty^#(empty()) -> c_1() , isEmpty^#(node(l, r)) -> c_2() , left^#(empty()) -> c_3() , left^#(node(l, r)) -> c_4(l) , right^#(empty()) -> c_5() , right^#(node(l, r)) -> c_6(r) , inc^#(0()) -> c_7() , inc^#(s(x)) -> c_8(inc^#(x)) , count^#(n, x) -> c_9(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))) , if^#(true(), b, n, m, x, y) -> c_10(x) , if^#(false(), true(), n, m, x, y) -> c_11(count^#(n, y)) , if^#(false(), false(), n, m, x, y) -> c_12(count^#(m, x)) , nrOfNodes^#(n) -> c_13(count^#(n, 0())) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isEmpty^#(empty()) -> c_1() , isEmpty^#(node(l, r)) -> c_2() , left^#(empty()) -> c_3() , left^#(node(l, r)) -> c_4(l) , right^#(empty()) -> c_5() , right^#(node(l, r)) -> c_6(r) , inc^#(0()) -> c_7() , inc^#(s(x)) -> c_8(inc^#(x)) , count^#(n, x) -> c_9(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))) , if^#(true(), b, n, m, x, y) -> c_10(x) , if^#(false(), true(), n, m, x, y) -> c_11(count^#(n, y)) , if^#(false(), false(), n, m, x, y) -> c_12(count^#(m, x)) , nrOfNodes^#(n) -> c_13(count^#(n, 0())) } Strict Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, r)) -> false() , left(empty()) -> empty() , left(node(l, r)) -> l , right(empty()) -> empty() , right(node(l, r)) -> r , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , count(n, x) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) , if(true(), b, n, m, x, y) -> x , if(false(), true(), n, m, x, y) -> count(n, y) , if(false(), false(), n, m, x, y) -> count(m, x) , nrOfNodes(n) -> count(n, 0()) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,5,7} by applications of Pre({1,2,3,5,7}) = {4,6,8,10}. Here rules are labeled as follows: DPs: { 1: isEmpty^#(empty()) -> c_1() , 2: isEmpty^#(node(l, r)) -> c_2() , 3: left^#(empty()) -> c_3() , 4: left^#(node(l, r)) -> c_4(l) , 5: right^#(empty()) -> c_5() , 6: right^#(node(l, r)) -> c_6(r) , 7: inc^#(0()) -> c_7() , 8: inc^#(s(x)) -> c_8(inc^#(x)) , 9: count^#(n, x) -> c_9(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))) , 10: if^#(true(), b, n, m, x, y) -> c_10(x) , 11: if^#(false(), true(), n, m, x, y) -> c_11(count^#(n, y)) , 12: if^#(false(), false(), n, m, x, y) -> c_12(count^#(m, x)) , 13: nrOfNodes^#(n) -> c_13(count^#(n, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { left^#(node(l, r)) -> c_4(l) , right^#(node(l, r)) -> c_6(r) , inc^#(s(x)) -> c_8(inc^#(x)) , count^#(n, x) -> c_9(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))) , if^#(true(), b, n, m, x, y) -> c_10(x) , if^#(false(), true(), n, m, x, y) -> c_11(count^#(n, y)) , if^#(false(), false(), n, m, x, y) -> c_12(count^#(m, x)) , nrOfNodes^#(n) -> c_13(count^#(n, 0())) } Strict Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, r)) -> false() , left(empty()) -> empty() , left(node(l, r)) -> l , right(empty()) -> empty() , right(node(l, r)) -> r , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , count(n, x) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) , if(true(), b, n, m, x, y) -> x , if(false(), true(), n, m, x, y) -> count(n, y) , if(false(), false(), n, m, x, y) -> count(m, x) , nrOfNodes(n) -> count(n, 0()) } Weak DPs: { isEmpty^#(empty()) -> c_1() , isEmpty^#(node(l, r)) -> c_2() , left^#(empty()) -> c_3() , right^#(empty()) -> c_5() , inc^#(0()) -> c_7() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..