YES
Time: 0.067934
TRS:
 {      .(x, 1()) -> x,
        .(x, i x) -> 1(),
  .(y, .(i y, z)) -> z,
    .(.(x, y), z) -> .(x, .(y, z)),
        .(1(), x) -> x,
        .(i x, x) -> 1(),
  .(i y, .(y, z)) -> z,
        i .(x, y) -> .(i y, i x),
            i 1() -> 1(),
            i i x -> x}
 DP:
  DP:
   {.#(.(x, y), z) -> .#(x, .(y, z)),
    .#(.(x, y), z) -> .#(y, z),
        i# .(x, y) -> .#(i y, i x),
        i# .(x, y) -> i# x,
        i# .(x, y) -> i# y}
  TRS:
  {      .(x, 1()) -> x,
         .(x, i x) -> 1(),
   .(y, .(i y, z)) -> z,
     .(.(x, y), z) -> .(x, .(y, z)),
         .(1(), x) -> x,
         .(i x, x) -> 1(),
   .(i y, .(y, z)) -> z,
         i .(x, y) -> .(i y, i x),
             i 1() -> 1(),
             i i x -> x}
  UR:
   {      .(x, 1()) -> x,
          .(x, i x) -> 1(),
    .(y, .(i y, z)) -> z,
      .(.(x, y), z) -> .(x, .(y, z)),
          .(1(), x) -> x,
          .(i x, x) -> 1(),
    .(i y, .(y, z)) -> z,
          i .(x, y) -> .(i y, i x),
              i 1() -> 1(),
              i i x -> x}
   EDG:
    {(.#(.(x, y), z) -> .#(x, .(y, z)), .#(.(x, y), z) -> .#(y, z))
     (.#(.(x, y), z) -> .#(x, .(y, z)), .#(.(x, y), z) -> .#(x, .(y, z)))
     (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)))
     (i# .(x, y) -> i# x, 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# y, i# .(x, y) -> .#(i y, i x))
     (i# .(x, y) -> i# y, i# .(x, y) -> i# x)
     (i# .(x, y) -> i# y, i# .(x, y) -> i# y)
     (.#(.(x, y), z) -> .#(y, z), .#(.(x, y), z) -> .#(x, .(y, z)))
     (.#(.(x, y), z) -> .#(y, z), .#(.(x, y), z) -> .#(y, z))}
    STATUS:
     arrows: 0.520000
     SCCS (2):
      Scc:
       {i# .(x, y) -> i# x,
        i# .(x, y) -> i# y}
      Scc:
       {.#(.(x, y), z) -> .#(x, .(y, z)),
        .#(.(x, y), z) -> .#(y, z)}
      
      SCC (2):
       Strict:
        {i# .(x, y) -> i# x,
         i# .(x, y) -> i# y}
       Weak:
       {      .(x, 1()) -> x,
              .(x, i x) -> 1(),
        .(y, .(i y, z)) -> z,
          .(.(x, y), z) -> .(x, .(y, z)),
              .(1(), x) -> x,
              .(i x, x) -> 1(),
        .(i y, .(y, z)) -> z,
              i .(x, y) -> .(i y, i x),
                  i 1() -> 1(),
                  i i x -> x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [.](x0, x1) = x0 + x1 + 1,
         
         [i](x0) = 0,
         
         [1] = 1,
         
         [i#](x0) = x0
        Strict:
         i# .(x, y) -> i# y
         1 + 1x + 1y >= 0 + 1y
         i# .(x, y) -> i# x
         1 + 1x + 1y >= 0 + 1x
        Weak:
         i i x -> x
         0 + 0x >= 1x
         i 1() -> 1()
         0 >= 1
         i .(x, y) -> .(i y, i x)
         0 + 0x + 0y >= 1 + 0x + 0y
         .(i y, .(y, z)) -> z
         2 + 1z + 1y >= 1z
         .(i x, x) -> 1()
         1 + 1x >= 1
         .(1(), x) -> x
         2 + 1x >= 1x
         .(.(x, y), z) -> .(x, .(y, z))
         2 + 1x + 1z + 1y >= 2 + 1x + 1z + 1y
         .(y, .(i y, z)) -> z
         2 + 1z + 1y >= 1z
         .(x, i x) -> 1()
         1 + 1x >= 1
         .(x, 1()) -> x
         2 + 1x >= 1x
       Qed
     
     SCC (2):
      Strict:
       {.#(.(x, y), z) -> .#(x, .(y, z)),
        .#(.(x, y), z) -> .#(y, z)}
      Weak:
      {      .(x, 1()) -> x,
             .(x, i x) -> 1(),
       .(y, .(i y, z)) -> z,
         .(.(x, y), z) -> .(x, .(y, z)),
             .(1(), x) -> x,
             .(i x, x) -> 1(),
       .(i y, .(y, z)) -> z,
             i .(x, y) -> .(i y, i x),
                 i 1() -> 1(),
                 i i x -> x}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [.](x0, x1) = x0 + x1 + 1,
        
        [i](x0) = x0,
        
        [1] = 1,
        
        [.#](x0, x1) = x0 + x1
       Strict:
        .#(.(x, y), z) -> .#(y, z)
        1 + 1x + 1z + 1y >= 0 + 1z + 1y
        .#(.(x, y), z) -> .#(x, .(y, z))
        1 + 1x + 1z + 1y >= 1 + 1x + 1z + 1y
       Weak:
        i i x -> x
        0 + 1x >= 1x
        i 1() -> 1()
        1 >= 1
        i .(x, y) -> .(i y, i x)
        1 + 1x + 1y >= 1 + 1x + 1y
        .(i y, .(y, z)) -> z
        2 + 1z + 2y >= 1z
        .(i x, x) -> 1()
        1 + 2x >= 1
        .(1(), x) -> x
        2 + 1x >= 1x
        .(.(x, y), z) -> .(x, .(y, z))
        2 + 1x + 1z + 1y >= 2 + 1x + 1z + 1y
        .(y, .(i y, z)) -> z
        2 + 1z + 2y >= 1z
        .(x, i x) -> 1()
        1 + 2x >= 1
        .(x, 1()) -> x
        2 + 1x >= 1x
      SCCS (1):
       Scc:
        {.#(.(x, y), z) -> .#(x, .(y, z))}
       
       SCC (1):
        Strict:
         {.#(.(x, y), z) -> .#(x, .(y, z))}
        Weak:
        {      .(x, 1()) -> x,
               .(x, i x) -> 1(),
         .(y, .(i y, z)) -> z,
           .(.(x, y), z) -> .(x, .(y, z)),
               .(1(), x) -> x,
               .(i x, x) -> 1(),
         .(i y, .(y, z)) -> z,
               i .(x, y) -> .(i y, i x),
                   i 1() -> 1(),
                   i i x -> x}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [.](x0, x1) = x0 + x1 + 1,
          
          [i](x0) = x0 + 1,
          
          [1] = 1,
          
          [.#](x0, x1) = x0 + 1
         Strict:
          .#(.(x, y), z) -> .#(x, .(y, z))
          2 + 1x + 0z + 1y >= 1 + 1x + 0z + 0y
         Weak:
          i i x -> x
          2 + 1x >= 1x
          i 1() -> 1()
          2 >= 1
          i .(x, y) -> .(i y, i x)
          2 + 1x + 1y >= 3 + 1x + 1y
          .(i y, .(y, z)) -> z
          3 + 1z + 2y >= 1z
          .(i x, x) -> 1()
          2 + 2x >= 1
          .(1(), x) -> x
          2 + 1x >= 1x
          .(.(x, y), z) -> .(x, .(y, z))
          2 + 1x + 1z + 1y >= 2 + 1x + 1z + 1y
          .(y, .(i y, z)) -> z
          3 + 1z + 2y >= 1z
          .(x, i x) -> 1()
          2 + 2x >= 1
          .(x, 1()) -> x
          2 + 1x >= 1x
        Qed