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