YES

TRS:

  :(x,x) -> e()
  :(x,e()) -> x
  i(:(x,y)) -> :(y,x)
  :(:(x,y),z) -> :(x,:(z,i(y)))
  :(e(),x) -> i(x)
  i(i(x)) -> x
  i(e()) -> e()
  :(x,:(y,i(x))) -> i(y)
  :(x,:(y,:(i(x),z))) -> :(i(z),y)
  :(i(x),:(y,x)) -> i(y)
  :(i(x),:(y,:(x,z))) -> :(i(z),y)

linear polynomial interpretations on N:

  :_A(x1,x2) = x1 + x2 + 2
  :#_A(x1,x2) = x1 + x2 + 2
  e_A = 1
  e#_A = 1
  i_A(x1) = x1
  i#_A(x1) = x1

precedence:

  : = i > e