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