MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a(d(x)) -> d(c(b(a(x)))) , a(c(x)) -> x , b(d(x)) -> x , b(c(x)) -> c(d(a(b(x)))) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { a^#(d(x)) -> c_1(b^#(a(x)), a^#(x)) , a^#(c(x)) -> c_2() , b^#(d(x)) -> c_3() , b^#(c(x)) -> c_4(a^#(b(x)), b^#(x)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a^#(d(x)) -> c_1(b^#(a(x)), a^#(x)) , a^#(c(x)) -> c_2() , b^#(d(x)) -> c_3() , b^#(c(x)) -> c_4(a^#(b(x)), b^#(x)) } Weak Trs: { a(d(x)) -> d(c(b(a(x)))) , a(c(x)) -> x , b(d(x)) -> x , b(c(x)) -> c(d(a(b(x)))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {2,3} by applications of Pre({2,3}) = {1,4}. Here rules are labeled as follows: DPs: { 1: a^#(d(x)) -> c_1(b^#(a(x)), a^#(x)) , 2: a^#(c(x)) -> c_2() , 3: b^#(d(x)) -> c_3() , 4: b^#(c(x)) -> c_4(a^#(b(x)), b^#(x)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a^#(d(x)) -> c_1(b^#(a(x)), a^#(x)) , b^#(c(x)) -> c_4(a^#(b(x)), b^#(x)) } Weak DPs: { a^#(c(x)) -> c_2() , b^#(d(x)) -> c_3() } Weak Trs: { a(d(x)) -> d(c(b(a(x)))) , a(c(x)) -> x , b(d(x)) -> x , b(c(x)) -> c(d(a(b(x)))) } 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. { a^#(c(x)) -> c_2() , b^#(d(x)) -> c_3() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a^#(d(x)) -> c_1(b^#(a(x)), a^#(x)) , b^#(c(x)) -> c_4(a^#(b(x)), b^#(x)) } Weak Trs: { a(d(x)) -> d(c(b(a(x)))) , a(c(x)) -> x , b(d(x)) -> x , b(c(x)) -> c(d(a(b(x)))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..