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