MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { f(0(x1)) -> s(0(x1)) , f(s(x1)) -> d(f(p(s(x1)))) , d(0(x1)) -> 0(x1) , d(s(x1)) -> s(s(d(p(s(x1))))) , p(s(x1)) -> x1 } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { f^#(0(x1)) -> c_1() , f^#(s(x1)) -> c_2(d^#(f(p(s(x1)))), f^#(p(s(x1))), p^#(s(x1))) , d^#(0(x1)) -> c_3() , d^#(s(x1)) -> c_4(d^#(p(s(x1))), p^#(s(x1))) , p^#(s(x1)) -> c_5() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f^#(0(x1)) -> c_1() , f^#(s(x1)) -> c_2(d^#(f(p(s(x1)))), f^#(p(s(x1))), p^#(s(x1))) , d^#(0(x1)) -> c_3() , d^#(s(x1)) -> c_4(d^#(p(s(x1))), p^#(s(x1))) , p^#(s(x1)) -> c_5() } Weak Trs: { f(0(x1)) -> s(0(x1)) , f(s(x1)) -> d(f(p(s(x1)))) , d(0(x1)) -> 0(x1) , d(s(x1)) -> s(s(d(p(s(x1))))) , p(s(x1)) -> x1 } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3,5} by applications of Pre({1,3,5}) = {2,4}. Here rules are labeled as follows: DPs: { 1: f^#(0(x1)) -> c_1() , 2: f^#(s(x1)) -> c_2(d^#(f(p(s(x1)))), f^#(p(s(x1))), p^#(s(x1))) , 3: d^#(0(x1)) -> c_3() , 4: d^#(s(x1)) -> c_4(d^#(p(s(x1))), p^#(s(x1))) , 5: p^#(s(x1)) -> c_5() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f^#(s(x1)) -> c_2(d^#(f(p(s(x1)))), f^#(p(s(x1))), p^#(s(x1))) , d^#(s(x1)) -> c_4(d^#(p(s(x1))), p^#(s(x1))) } Weak DPs: { f^#(0(x1)) -> c_1() , d^#(0(x1)) -> c_3() , p^#(s(x1)) -> c_5() } Weak Trs: { f(0(x1)) -> s(0(x1)) , f(s(x1)) -> d(f(p(s(x1)))) , d(0(x1)) -> 0(x1) , d(s(x1)) -> s(s(d(p(s(x1))))) , p(s(x1)) -> x1 } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { f^#(0(x1)) -> c_1() , d^#(0(x1)) -> c_3() , p^#(s(x1)) -> c_5() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f^#(s(x1)) -> c_2(d^#(f(p(s(x1)))), f^#(p(s(x1))), p^#(s(x1))) , d^#(s(x1)) -> c_4(d^#(p(s(x1))), p^#(s(x1))) } Weak Trs: { f(0(x1)) -> s(0(x1)) , f(s(x1)) -> d(f(p(s(x1)))) , d(0(x1)) -> 0(x1) , d(s(x1)) -> s(s(d(p(s(x1))))) , p(s(x1)) -> x1 } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { f^#(s(x1)) -> c_2(d^#(f(p(s(x1)))), f^#(p(s(x1))), p^#(s(x1))) , d^#(s(x1)) -> c_4(d^#(p(s(x1))), p^#(s(x1))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f^#(s(x1)) -> c_1(d^#(f(p(s(x1)))), f^#(p(s(x1)))) , d^#(s(x1)) -> c_2(d^#(p(s(x1)))) } Weak Trs: { f(0(x1)) -> s(0(x1)) , f(s(x1)) -> d(f(p(s(x1)))) , d(0(x1)) -> 0(x1) , d(s(x1)) -> s(s(d(p(s(x1))))) , p(s(x1)) -> x1 } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..