TRS: { implies(not(x), y) -> or(x, y), implies(not(x), or(y, z)) -> implies(y, or(x, z)), implies(x, or(y, z)) -> or(y, implies(x, z))} Fail