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)
  EDG 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)
   graph:
    i#(:(x,y)) -> :#(y,x) -> :#(:(x,y),z) -> i#(y)
    i#(:(x,y)) -> :#(y,x) -> :#(:(x,y),z) -> :#(z,i(y))
    i#(:(x,y)) -> :#(y,x) -> :#(:(x,y),z) -> :#(x,:(z,i(y)))
    i#(:(x,y)) -> :#(y,x) -> :#(e(),x) -> i#(x)
    i#(:(x,y)) -> :#(y,x) -> :#(x,:(y,i(x))) -> i#(y)
    i#(:(x,y)) -> :#(y,x) -> :#(x,:(y,:(i(x),z))) -> i#(z)
    i#(:(x,y)) -> :#(y,x) -> :#(x,:(y,:(i(x),z))) -> :#(i(z),y)
    i#(:(x,y)) -> :#(y,x) -> :#(i(x),:(y,x)) -> i#(y)
    i#(:(x,y)) -> :#(y,x) -> :#(i(x),:(y,:(x,z))) -> i#(z)
    i#(:(x,y)) -> :#(y,x) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y)
    :#(i(x),:(y,:(x,z))) -> i#(z) -> i#(:(x,y)) -> :#(y,x)
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(:(x,y),z) -> i#(y)
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) ->
    :#(:(x,y),z) -> :#(z,i(y))
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) ->
    :#(:(x,y),z) -> :#(x,:(z,i(y)))
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(e(),x) -> i#(x)
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) ->
    :#(x,:(y,i(x))) -> i#(y)
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) ->
    :#(x,:(y,:(i(x),z))) -> i#(z)
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) ->
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y)
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) ->
    :#(i(x),:(y,x)) -> i#(y)
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) ->
    :#(i(x),:(y,:(x,z))) -> i#(z)
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y) ->
    :#(i(x),:(y,:(x,z))) -> :#(i(z),y)
    :#(i(x),:(y,x)) -> i#(y) -> i#(:(x,y)) -> :#(y,x)
    :#(e(),x) -> i#(x) -> i#(:(x,y)) -> :#(y,x)
    :#(:(x,y),z) -> i#(y) -> i#(:(x,y)) -> :#(y,x)
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(:(x,y),z) -> i#(y)
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(:(x,y),z) -> :#(z,i(y))
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(:(x,y),z) -> :#(x,:(z,i(y)))
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(e(),x) -> i#(x)
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(x,:(y,i(x))) -> i#(y)
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(x,:(y,:(i(x),z))) -> i#(z)
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(x,:(y,:(i(x),z))) -> :#(i(z),y)
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(i(x),:(y,x)) -> i#(y)
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(i(x),:(y,:(x,z))) -> i#(z)
    :#(:(x,y),z) -> :#(z,i(y)) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y)
    :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(:(x,y),z) -> i#(y)
    :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(:(x,y),z) -> :#(z,i(y))
    :#(:(x,y),z) -> :#(x,:(z,i(y))) ->
    :#(:(x,y),z) -> :#(x,:(z,i(y)))
    :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(e(),x) -> i#(x)
    :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(x,:(y,i(x))) -> i#(y)
    :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(x,:(y,:(i(x),z))) -> i#(z)
    :#(:(x,y),z) -> :#(x,:(z,i(y))) ->
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y)
    :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(i(x),:(y,x)) -> i#(y)
    :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(i(x),:(y,:(x,z))) -> i#(z)
    :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y)
    :#(x,:(y,i(x))) -> i#(y) -> i#(:(x,y)) -> :#(y,x)
    :#(x,:(y,:(i(x),z))) -> i#(z) -> i#(:(x,y)) -> :#(y,x)
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(:(x,y),z) -> i#(y)
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) ->
    :#(:(x,y),z) -> :#(z,i(y))
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) ->
    :#(:(x,y),z) -> :#(x,:(z,i(y)))
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(e(),x) -> i#(x)
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) ->
    :#(x,:(y,i(x))) -> i#(y)
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) ->
    :#(x,:(y,:(i(x),z))) -> i#(z)
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) ->
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y)
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) ->
    :#(i(x),:(y,x)) -> i#(y)
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) ->
    :#(i(x),:(y,:(x,z))) -> i#(z)
    :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [i#](x0) = x0,
     
     [:#](x0, x1) = x0 + x1,
     
     [i](x0) = x0,
     
     [e] = 0,
     
     [:](x0, x1) = x0 + x1 + 1
    orientation:
     i#(:(x,y)) = x + y + 1 >= x + y = :#(y,x)
     
     :#(:(x,y),z) = x + y + z + 1 >= y = i#(y)
     
     :#(:(x,y),z) = x + y + z + 1 >= y + z = :#(z,i(y))
     
     :#(:(x,y),z) = x + y + z + 1 >= x + y + z + 1 = :#(x,:(z,i(y)))
     
     :#(e(),x) = x >= x = i#(x)
     
     :#(x,:(y,i(x))) = 2x + y + 1 >= y = i#(y)
     
     :#(x,:(y,:(i(x),z))) = 2x + y + z + 2 >= z = i#(z)
     
     :#(x,:(y,:(i(x),z))) = 2x + y + z + 2 >= y + z = :#(i(z),y)
     
     :#(i(x),:(y,x)) = 2x + y + 1 >= y = i#(y)
     
     :#(i(x),:(y,:(x,z))) = 2x + y + z + 2 >= z = i#(z)
     
     :#(i(x),:(y,:(x,z))) = 2x + y + z + 2 >= y + z = :#(i(z),y)
     
     :(x,x) = 2x + 1 >= 0 = e()
     
     :(x,e()) = x + 1 >= x = x
     
     i(:(x,y)) = x + y + 1 >= x + y + 1 = :(y,x)
     
     :(:(x,y),z) = x + y + z + 2 >= x + y + z + 2 = :(x,:(z,i(y)))
     
     :(e(),x) = x + 1 >= x = i(x)
     
     i(i(x)) = x >= x = x
     
     i(e()) = 0 >= 0 = e()
     
     :(x,:(y,i(x))) = 2x + y + 2 >= y = i(y)
     
     :(x,:(y,:(i(x),z))) = 2x + y + z + 3 >= y + z + 1 = :(i(z),y)
     
     :(i(x),:(y,x)) = 2x + y + 2 >= y = i(y)
     
     :(i(x),:(y,:(x,z))) = 2x + y + z + 3 >= y + z + 1 = :(i(z),y)
    problem:
     DPs:
      :#(:(x,y),z) -> :#(x,:(z,i(y)))
      :#(e(),x) -> i#(x)
     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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [i#](x0) = 0,
      
      [:#](x0, x1) = 1,
      
      [i](x0) = x0,
      
      [e] = 0,
      
      [:](x0, x1) = x0 + x1
     orientation:
      :#(:(x,y),z) = 1 >= 1 = :#(x,:(z,i(y)))
      
      :#(e(),x) = 1 >= 0 = i#(x)
      
      :(x,x) = 2x >= 0 = e()
      
      :(x,e()) = x >= x = x
      
      i(:(x,y)) = x + y >= x + y = :(y,x)
      
      :(:(x,y),z) = x + y + z >= x + y + z = :(x,:(z,i(y)))
      
      :(e(),x) = x >= x = i(x)
      
      i(i(x)) = x >= x = x
      
      i(e()) = 0 >= 0 = e()
      
      :(x,:(y,i(x))) = 2x + y >= y = i(y)
      
      :(x,:(y,:(i(x),z))) = 2x + y + z >= y + z = :(i(z),y)
      
      :(i(x),:(y,x)) = 2x + y >= y = i(y)
      
      :(i(x),:(y,:(x,z))) = 2x + y + z >= y + z = :(i(z),y)
     problem:
      DPs:
       :#(:(x,y),z) -> :#(x,:(z,i(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)
     Subterm Criterion Processor:
      simple projection:
       pi(:#) = 0
      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