MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { add(true(), x, xs) -> add(and(isNat(x), isList(xs)), x, Cons(x, xs)) , and(x, false()) -> false() , and(true(), true()) -> true() , and(false(), x) -> false() , isNat(s(x)) -> isNat(x) , isNat(0()) -> true() , isList(Cons(x, xs)) -> isList(xs) , isList(nil()) -> true() , if(true(), x, y) -> x , if(false(), x, y) -> y } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..