YES

Problem:
 .(1(),x) -> x
 .(x,1()) -> x
 .(i(x),x) -> 1()
 .(x,i(x)) -> 1()
 i(1()) -> 1()
 i(i(x)) -> x
 .(i(y),.(y,z)) -> z
 .(y,.(i(y),z)) -> z
 .(.(x,y),z) -> .(x,.(y,z))
 i(.(x,y)) -> .(i(y),i(x))

Proof:
 DP Processor:
  DPs:
   .#(.(x,y),z) -> .#(y,z)
   .#(.(x,y),z) -> .#(x,.(y,z))
   i#(.(x,y)) -> i#(x)
   i#(.(x,y)) -> i#(y)
   i#(.(x,y)) -> .#(i(y),i(x))
  TRS:
   .(1(),x) -> x
   .(x,1()) -> x
   .(i(x),x) -> 1()
   .(x,i(x)) -> 1()
   i(1()) -> 1()
   i(i(x)) -> x
   .(i(y),.(y,z)) -> z
   .(y,.(i(y),z)) -> z
   .(.(x,y),z) -> .(x,.(y,z))
   i(.(x,y)) -> .(i(y),i(x))
  CDG Processor:
   DPs:
    .#(.(x,y),z) -> .#(y,z)
    .#(.(x,y),z) -> .#(x,.(y,z))
    i#(.(x,y)) -> i#(x)
    i#(.(x,y)) -> i#(y)
    i#(.(x,y)) -> .#(i(y),i(x))
   TRS:
    .(1(),x) -> x
    .(x,1()) -> x
    .(i(x),x) -> 1()
    .(x,i(x)) -> 1()
    i(1()) -> 1()
    i(i(x)) -> x
    .(i(y),.(y,z)) -> z
    .(y,.(i(y),z)) -> z
    .(.(x,y),z) -> .(x,.(y,z))
    i(.(x,y)) -> .(i(y),i(x))
   graph:
    i#(.(x,y)) -> i#(y) -> i#(.(x,y)) -> i#(x)
    i#(.(x,y)) -> i#(y) -> i#(.(x,y)) -> i#(y)
    i#(.(x,y)) -> i#(y) -> i#(.(x,y)) -> .#(i(y),i(x))
    i#(.(x,y)) -> i#(x) -> i#(.(x,y)) -> i#(x)
    i#(.(x,y)) -> i#(x) -> i#(.(x,y)) -> i#(y)
    i#(.(x,y)) -> i#(x) -> i#(.(x,y)) -> .#(i(y),i(x))
    i#(.(x,y)) -> .#(i(y),i(x)) -> .#(.(x,y),z) -> .#(y,z)
    i#(.(x,y)) -> .#(i(y),i(x)) -> .#(.(x,y),z) -> .#(x,.(y,z))
    .#(.(x,y),z) -> .#(y,z) -> .#(.(x,y),z) -> .#(y,z)
    .#(.(x,y),z) -> .#(y,z) -> .#(.(x,y),z) -> .#(x,.(y,z))
    .#(.(x,y),z) -> .#(x,.(y,z)) -> .#(.(x,y),z) -> .#(y,z)
    .#(.(x,y),z) -> .#(x,.(y,z)) -> .#(.(x,y),z) -> .#(x,.(y,z))
   Restore Modifier:
    DPs:
     .#(.(x,y),z) -> .#(y,z)
     .#(.(x,y),z) -> .#(x,.(y,z))
     i#(.(x,y)) -> i#(x)
     i#(.(x,y)) -> i#(y)
     i#(.(x,y)) -> .#(i(y),i(x))
    TRS:
     .(1(),x) -> x
     .(x,1()) -> x
     .(i(x),x) -> 1()
     .(x,i(x)) -> 1()
     i(1()) -> 1()
     i(i(x)) -> x
     .(i(y),.(y,z)) -> z
     .(y,.(i(y),z)) -> z
     .(.(x,y),z) -> .(x,.(y,z))
     i(.(x,y)) -> .(i(y),i(x))
    SCC Processor:
     #sccs: 2
     #rules: 4
     #arcs: 12/25
     DPs:
      i#(.(x,y)) -> i#(y)
      i#(.(x,y)) -> i#(x)
     TRS:
      .(1(),x) -> x
      .(x,1()) -> x
      .(i(x),x) -> 1()
      .(x,i(x)) -> 1()
      i(1()) -> 1()
      i(i(x)) -> x
      .(i(y),.(y,z)) -> z
      .(y,.(i(y),z)) -> z
      .(.(x,y),z) -> .(x,.(y,z))
      i(.(x,y)) -> .(i(y),i(x))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [i#](x0) = x0 + 1,
       
       [i](x0) = x0,
       
       [.](x0, x1) = x0 + x1 + 1,
       
       [1] = 0
      orientation:
       i#(.(x,y)) = x + y + 2 >= y + 1 = i#(y)
       
       i#(.(x,y)) = x + y + 2 >= x + 1 = i#(x)
       
       .(1(),x) = x + 1 >= x = x
       
       .(x,1()) = x + 1 >= x = x
       
       .(i(x),x) = 2x + 1 >= 0 = 1()
       
       .(x,i(x)) = 2x + 1 >= 0 = 1()
       
       i(1()) = 0 >= 0 = 1()
       
       i(i(x)) = x >= x = x
       
       .(i(y),.(y,z)) = 2y + z + 2 >= z = z
       
       .(y,.(i(y),z)) = 2y + z + 2 >= z = z
       
       .(.(x,y),z) = x + y + z + 2 >= x + y + z + 2 = .(x,.(y,z))
       
       i(.(x,y)) = x + y + 1 >= x + y + 1 = .(i(y),i(x))
      problem:
       DPs:
        
       TRS:
        .(1(),x) -> x
        .(x,1()) -> x
        .(i(x),x) -> 1()
        .(x,i(x)) -> 1()
        i(1()) -> 1()
        i(i(x)) -> x
        .(i(y),.(y,z)) -> z
        .(y,.(i(y),z)) -> z
        .(.(x,y),z) -> .(x,.(y,z))
        i(.(x,y)) -> .(i(y),i(x))
      Qed
     
     DPs:
      .#(.(x,y),z) -> .#(x,.(y,z))
      .#(.(x,y),z) -> .#(y,z)
     TRS:
      .(1(),x) -> x
      .(x,1()) -> x
      .(i(x),x) -> 1()
      .(x,i(x)) -> 1()
      i(1()) -> 1()
      i(i(x)) -> x
      .(i(y),.(y,z)) -> z
      .(y,.(i(y),z)) -> z
      .(.(x,y),z) -> .(x,.(y,z))
      i(.(x,y)) -> .(i(y),i(x))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [.#](x0, x1) = x0 + x1 + 1,
       
       [i](x0) = x0,
       
       [.](x0, x1) = x0 + x1 + 1,
       
       [1] = 1
      orientation:
       .#(.(x,y),z) = x + y + z + 2 >= x + y + z + 2 = .#(x,.(y,z))
       
       .#(.(x,y),z) = x + y + z + 2 >= y + z + 1 = .#(y,z)
       
       .(1(),x) = x + 2 >= x = x
       
       .(x,1()) = x + 2 >= x = x
       
       .(i(x),x) = 2x + 1 >= 1 = 1()
       
       .(x,i(x)) = 2x + 1 >= 1 = 1()
       
       i(1()) = 1 >= 1 = 1()
       
       i(i(x)) = x >= x = x
       
       .(i(y),.(y,z)) = 2y + z + 2 >= z = z
       
       .(y,.(i(y),z)) = 2y + z + 2 >= z = z
       
       .(.(x,y),z) = x + y + z + 2 >= x + y + z + 2 = .(x,.(y,z))
       
       i(.(x,y)) = x + y + 1 >= x + y + 1 = .(i(y),i(x))
      problem:
       DPs:
        .#(.(x,y),z) -> .#(x,.(y,z))
       TRS:
        .(1(),x) -> x
        .(x,1()) -> x
        .(i(x),x) -> 1()
        .(x,i(x)) -> 1()
        i(1()) -> 1()
        i(i(x)) -> x
        .(i(y),.(y,z)) -> z
        .(y,.(i(y),z)) -> z
        .(.(x,y),z) -> .(x,.(y,z))
        i(.(x,y)) -> .(i(y),i(x))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [.#](x0, x1) = x0,
        
        [i](x0) = x0,
        
        [.](x0, x1) = x0 + x1 + 1,
        
        [1] = 1
       orientation:
        .#(.(x,y),z) = x + y + 1 >= x = .#(x,.(y,z))
        
        .(1(),x) = x + 2 >= x = x
        
        .(x,1()) = x + 2 >= x = x
        
        .(i(x),x) = 2x + 1 >= 1 = 1()
        
        .(x,i(x)) = 2x + 1 >= 1 = 1()
        
        i(1()) = 1 >= 1 = 1()
        
        i(i(x)) = x >= x = x
        
        .(i(y),.(y,z)) = 2y + z + 2 >= z = z
        
        .(y,.(i(y),z)) = 2y + z + 2 >= z = z
        
        .(.(x,y),z) = x + y + z + 2 >= x + y + z + 2 = .(x,.(y,z))
        
        i(.(x,y)) = x + y + 1 >= x + y + 1 = .(i(y),i(x))
       problem:
        DPs:
         
        TRS:
         .(1(),x) -> x
         .(x,1()) -> x
         .(i(x),x) -> 1()
         .(x,i(x)) -> 1()
         i(1()) -> 1()
         i(i(x)) -> x
         .(i(y),.(y,z)) -> z
         .(y,.(i(y),z)) -> z
         .(.(x,y),z) -> .(x,.(y,z))
         i(.(x,y)) -> .(i(y),i(x))
       Qed