YES(?,PRIMREC) We are left with following problem, upon which TcT provides the certificate YES(?,PRIMREC). Strict Trs: { add(0(), x) -> x , add(s(x), y) -> s(add(x, y)) , mult(0(), x) -> 0() , mult(s(x), y) -> add(y, mult(x, y)) } Obligation: innermost runtime complexity Answer: YES(?,PRIMREC) The input was oriented with the instance of'multiset path order' as induced by the precedence add > s, 0 > add, 0 > s, mult > add, mult > s, 0 ~ mult . Hurray, we answered YES(?,PRIMREC)