YES

Problem:
 :(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)

Proof:
 DP Processor:
  DPs:
   i#(:(x,y)) -> :#(y,x)
   :#(:(x,y),z) -> i#(y)
   :#(:(x,y),z) -> :#(z,i(y))
   :#(:(x,y),z) -> :#(x,:(z,i(y)))
   :#(e(),x) -> i#(x)
   :#(x,:(y,i(x))) -> i#(y)
   :#(x,:(y,:(i(x),z))) -> i#(z)
   :#(x,:(y,:(i(x),z))) -> :#(i(z),y)
   :#(i(x),:(y,x)) -> i#(y)
   :#(i(x),:(y,:(x,z))) -> i#(z)
   :#(i(x),:(y,:(x,z))) -> :#(i(z),y)
  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)
  KBO Processor:
   argument filtering:
    pi(:) = [0,1]
    pi(e) = []
    pi(i) = [0]
    pi(:#) = [0,1]
    pi(i#) = 0
   usable rules:
    :(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)
   weight function:
    w0 = 1
    w(i#) = w(e) = 1
    w(:#) = w(i) = w(:) = 0
   precedence:
    i > : > i# ~ :# ~ e
   problem:
    DPs:
     
    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)
   Qed