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