YES
Time: 0.000458
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}
 DP:
  DP:
   {}
  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}
  Qed