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 The input cannot be shown compatible Arrrr..