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))
  TDG 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(y),i(x))
    i#(.(x,y)) -> i#(y) -> i#(.(x,y)) -> i#(y)
    i#(.(x,y)) -> i#(y) -> i#(.(x,y)) -> i#(x)
    i#(.(x,y)) -> i#(x) -> i#(.(x,y)) -> .#(i(y),i(x))
    i#(.(x,y)) -> i#(x) -> i#(.(x,y)) -> i#(y)
    i#(.(x,y)) -> i#(x) -> i#(.(x,y)) -> i#(x)
    i#(.(x,y)) -> .#(i(y),i(x)) -> .#(.(x,y),z) -> .#(x,.(y,z))
    i#(.(x,y)) -> .#(i(y),i(x)) -> .#(.(x,y),z) -> .#(y,z)
    .#(.(x,y),z) -> .#(y,z) -> .#(.(x,y),z) -> .#(x,.(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) -> .#(x,.(y,z)) -> .#(.(x,y),z) -> .#(y,z)
   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))
    Subterm Criterion Processor:
     simple projection:
      pi(i#) = 0
     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) -> .#(y,z)
     .#(.(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))
    Subterm Criterion Processor:
     simple projection:
      pi(.#) = 0
     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