YES
Time: 0.000443
TRS:
 {      \(x, x) -> e(),
  \(x, .(x, y)) -> y,
      \(e(), x) -> x,
  \(/(x, y), x) -> y,
        /(x, x) -> e(),
      /(x, e()) -> x,
  /(x, \(y, x)) -> y,
  /(.(y, x), x) -> y,
      .(x, e()) -> x,
  .(x, \(x, y)) -> y,
      .(e(), x) -> x,
  .(/(y, x), x) -> y}
 RUF:
  Strict:
   {}
  Weak:
   {}
  Qed