TIMEOUT
MAYBE
Trs:
 {implies(not(x), or(y, z)) -> implies(y, or(x, z)),
         implies(not(x), y) -> or(x, y),
       implies(x, or(y, z)) -> or(y, implies(x, z))}
 Open