MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { implies(x, or(y, z)) -> or(y, implies(x, z)) , implies(not(x), y) -> or(x, y) , implies(not(x), or(y, z)) -> implies(y, or(x, z)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..