MAYBE
Trs:
 {            not(not(x)) -> x,
          and(x, false()) -> false(),
     and(x, not(false())) -> x,
      implies(false(), y) -> not(false()),
  implies(not(x), not(y)) -> implies(y, and(x, y)),
      implies(x, false()) -> not(x)}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open