YES
TRS:
 {               :(x, x) -> e(),
               :(x, e()) -> x,
  :(x, :(y, :(i(x), z))) -> :(i(z), y),
        :(x, :(y, i(x))) -> i(y),
               :(e(), x) -> i(x),
           :(:(x, y), z) -> :(x, :(z, i(y))),
        :(i(x), :(y, x)) -> i(y),
  :(i(x), :(y, :(x, z))) -> :(i(z), y),
                  i(e()) -> e(),
              i(:(x, y)) -> :(y, x),
                 i(i(x)) -> x}
 DP:
  Strict:
   {:#(x, :(y, :(i(x), z))) -> :#(i(z), y),
    :#(x, :(y, :(i(x), z))) -> i#(z),
          :#(x, :(y, i(x))) -> i#(y),
                 :#(e(), x) -> i#(x),
             :#(:(x, y), z) -> :#(x, :(z, i(y))),
             :#(:(x, y), z) -> :#(z, i(y)),
             :#(:(x, y), z) -> i#(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)) -> :#(y, x)}
  Weak:
  {               :(x, x) -> e(),
                :(x, e()) -> x,
   :(x, :(y, :(i(x), z))) -> :(i(z), y),
         :(x, :(y, i(x))) -> i(y),
                :(e(), x) -> i(x),
            :(:(x, y), z) -> :(x, :(z, i(y))),
         :(i(x), :(y, x)) -> i(y),
   :(i(x), :(y, :(x, z))) -> :(i(z), y),
                   i(e()) -> e(),
               i(:(x, y)) -> :(y, x),
                  i(i(x)) -> x}
  EDG:
   {(:#(:(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) -> :#(z, i(y)), :#(i(x), :(y, x)) -> i#(y))
    (:#(:(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, i(x))) -> i#(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))
    (:#(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))
    (:#(x, :(y, :(i(x), z))) -> :#(i(z), y), :#(i(x), :(y, x)) -> i#(y))
    (:#(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))
    (:#(i(x), :(y, :(x, z))) -> :#(i(z), y), :#(x, :(y, :(i(x), z))) -> :#(i(z), 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))) -> i#(y))
    (:#(i(x), :(y, :(x, z))) -> :#(i(z), y), :#(e(), x) -> i#(x))
    (:#(i(x), :(y, :(x, z))) -> :#(i(z), y), :#(:(x, y), z) -> :#(x, :(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) -> i#(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), y))
    (:#(i(x), :(y, :(x, z))) -> :#(i(z), y), :#(i(x), :(y, :(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))), :#(x, :(y, :(i(x), z))) -> i#(z))
    (:#(:(x, y), z) -> :#(x, :(z, i(y))), :#(x, :(y, i(x))) -> i#(y))
    (:#(:(x, y), z) -> :#(x, :(z, i(y))), :#(e(), x) -> i#(x))
    (:#(:(x, y), z) -> :#(x, :(z, i(y))), :#(:(x, y), z) -> :#(x, :(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) -> i#(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), y))
    (:#(:(x, y), z) -> :#(x, :(z, i(y))), :#(i(x), :(y, :(x, z))) -> i#(z))
    (:#(x, :(y, :(i(x), z))) -> i#(z), i#(:(x, y)) -> :#(y, x))
    (:#(:(x, y), z) -> i#(y), i#(:(x, y)) -> :#(y, x))
    (:#(e(), x) -> i#(x), i#(:(x, y)) -> :#(y, x))
    (i#(:(x, y)) -> :#(y, x), :#(x, :(y, :(i(x), z))) -> :#(i(z), y))
    (i#(:(x, y)) -> :#(y, x), :#(x, :(y, :(i(x), z))) -> i#(z))
    (i#(:(x, y)) -> :#(y, x), :#(x, :(y, i(x))) -> i#(y))
    (i#(:(x, y)) -> :#(y, x), :#(e(), x) -> i#(x))
    (i#(:(x, y)) -> :#(y, x), :#(:(x, y), z) -> :#(x, :(z, i(y))))
    (i#(:(x, y)) -> :#(y, x), :#(:(x, y), z) -> :#(z, i(y)))
    (i#(:(x, y)) -> :#(y, x), :#(:(x, y), z) -> i#(y))
    (i#(:(x, y)) -> :#(y, x), :#(i(x), :(y, x)) -> i#(y))
    (i#(:(x, y)) -> :#(y, x), :#(i(x), :(y, :(x, z))) -> :#(i(z), y))
    (i#(:(x, y)) -> :#(y, x), :#(i(x), :(y, :(x, z))) -> i#(z))}
   SCCS:
    Scc:
     {:#(x, :(y, :(i(x), z))) -> :#(i(z), y),
      :#(x, :(y, :(i(x), z))) -> i#(z),
            :#(x, :(y, i(x))) -> i#(y),
                   :#(e(), x) -> i#(x),
               :#(:(x, y), z) -> :#(x, :(z, i(y))),
               :#(:(x, y), z) -> :#(z, i(y)),
               :#(:(x, y), z) -> i#(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)) -> :#(y, x)}
    SCC:
     Strict:
      {:#(x, :(y, :(i(x), z))) -> :#(i(z), y),
       :#(x, :(y, :(i(x), z))) -> i#(z),
             :#(x, :(y, i(x))) -> i#(y),
                    :#(e(), x) -> i#(x),
                :#(:(x, y), z) -> :#(x, :(z, i(y))),
                :#(:(x, y), z) -> :#(z, i(y)),
                :#(:(x, y), z) -> i#(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)) -> :#(y, x)}
     Weak:
     {               :(x, x) -> e(),
                   :(x, e()) -> x,
      :(x, :(y, :(i(x), z))) -> :(i(z), y),
            :(x, :(y, i(x))) -> i(y),
                   :(e(), x) -> i(x),
               :(:(x, y), z) -> :(x, :(z, i(y))),
            :(i(x), :(y, x)) -> i(y),
      :(i(x), :(y, :(x, z))) -> :(i(z), y),
                      i(e()) -> e(),
                  i(:(x, y)) -> :(y, x),
                     i(i(x)) -> x}
     POLY:
      Argument Filtering:
       pi(i#) = [0], pi(i) = 0, pi(:#) = [0,1], pi(:) = [0,1], pi(e) = []
      Usable Rules:
       {}
      Interpretation:
       [:#](x0, x1) = x0 + x1 + 1,
       [i#](x0) = x0 + 1,
       [:](x0, x1) = x0 + x1 + 1,
       [e] = 0
      Strict:
       {    :#(e(), x) -> i#(x),
        :#(:(x, y), z) -> :#(x, :(z, i(y)))}
      Weak:
       {               :(x, x) -> e(),
                     :(x, e()) -> x,
        :(x, :(y, :(i(x), z))) -> :(i(z), y),
              :(x, :(y, i(x))) -> i(y),
                     :(e(), x) -> i(x),
                 :(:(x, y), z) -> :(x, :(z, i(y))),
              :(i(x), :(y, x)) -> i(y),
        :(i(x), :(y, :(x, z))) -> :(i(z), y),
                        i(e()) -> e(),
                    i(:(x, y)) -> :(y, x),
                       i(i(x)) -> x}
      EDG:
       {(:#(:(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))}
       SCCS:
        Scc:
         {:#(:(x, y), z) -> :#(x, :(z, i(y)))}
        SCC:
         Strict:
          {:#(:(x, y), z) -> :#(x, :(z, i(y)))}
         Weak:
         {               :(x, x) -> e(),
                       :(x, e()) -> x,
          :(x, :(y, :(i(x), z))) -> :(i(z), y),
                :(x, :(y, i(x))) -> i(y),
                       :(e(), x) -> i(x),
                   :(:(x, y), z) -> :(x, :(z, i(y))),
                :(i(x), :(y, x)) -> i(y),
          :(i(x), :(y, :(x, z))) -> :(i(z), y),
                          i(e()) -> e(),
                      i(:(x, y)) -> :(y, x),
                         i(i(x)) -> x}
         SPSC:
          Simple Projection:
           pi(:#) = 0
          Strict:
           {}
          Qed