YES(?,PRIMREC) We are left with following problem, upon which TcT provides the certificate YES(?,PRIMREC). Strict Trs: { or(x, true()) -> true() , or(true(), y) -> true() , or(false(), false()) -> false() , mem(x, nil()) -> false() , mem(x, set(y)) -> =(x, y) , mem(x, union(y, z)) -> or(mem(x, y), mem(x, z)) } Obligation: innermost runtime complexity Answer: YES(?,PRIMREC) The input was oriented with the instance of'multiset path order' as induced by the precedence mem > or, mem > true, mem > false, mem > =, nil > or, nil > true, nil > false, nil > =, set > or, set > true, set > false, set > =, union > or, union > true, union > false, union > =, or ~ true, or ~ false, or ~ =, true ~ false, true ~ =, false ~ =, mem ~ nil, mem ~ set, mem ~ union, nil ~ set, nil ~ union, set ~ union . Hurray, we answered YES(?,PRIMREC)