MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { del(.(x, .(y, z))) -> f(=(x, y), x, y, z) , f(true(), x, y, z) -> del(.(y, z)) , f(false(), x, y, z) -> .(x, del(.(y, z))) , =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) , =(.(x, y), nil()) -> false() , =(nil(), .(y, z)) -> false() , =(nil(), nil()) -> true() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..