MAYBE
MAYBE
TRS:
 {
          and(x, false()) -> false(),
     and(x, not(false())) -> x,
              not(not(x)) -> x,
      implies(x, false()) -> not(x),
      implies(false(), y) -> not(false()),
  implies(not(x), not(y)) -> implies(y, and(x, y))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
            and(x, false()) -> false(),
       and(x, not(false())) -> x,
                not(not(x)) -> x,
        implies(x, false()) -> not(x),
        implies(false(), y) -> not(false()),
    implies(not(x), not(y)) -> implies(y, and(x, y))
   }
  Fail