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