YES
Time: 0.006003
TRS:
 {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))}
 DP:
  DP:
   {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)),
    if#(if(x, y, z), u, v) -> if#(y, u, v),
    if#(if(x, y, z), u, v) -> if#(z, u, v)}
  TRS:
  {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))}
  UR:
   {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v)),
                  a(w, t) -> w,
                  a(w, t) -> t}
   EDG:
    {(if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))
     (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v))
     (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
     (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
     (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(y, u, v))
     (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v))
     (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
     (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v))
     (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))}
    EDG:
     {(if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))
      (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v))
      (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
      (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
      (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(y, u, v))
      (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v))
      (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
      (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v))
      (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))}
     EDG:
      {(if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))
       (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v))
       (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
       (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
       (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(y, u, v))
       (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v))
       (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
       (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v))
       (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))}
      EDG:
       {(if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))
        (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v))
        (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
        (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
        (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(y, u, v))
        (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v))
        (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)))
        (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v))
        (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))}
       STATUS:
        arrows: 0.000000
        SCCS (1):
         Scc:
          {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)),
           if#(if(x, y, z), u, v) -> if#(y, u, v),
           if#(if(x, y, z), u, v) -> if#(z, u, v)}
         
         SCC (3):
          Strict:
           {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)),
            if#(if(x, y, z), u, v) -> if#(y, u, v),
            if#(if(x, y, z), u, v) -> if#(z, u, v)}
          Weak:
          {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [if](x0, x1, x2) = x0 + x1 + x2 + 1,
            
            [if#](x0, x1, x2) = x0
           Strict:
            if#(if(x, y, z), u, v) -> if#(z, u, v)
            1 + 1x + 1y + 0u + 0v + 1z >= 0 + 0u + 0v + 1z
            if#(if(x, y, z), u, v) -> if#(y, u, v)
            1 + 1x + 1y + 0u + 0v + 1z >= 0 + 1y + 0u + 0v
            if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v))
            1 + 1x + 1y + 0u + 0v + 1z >= 0 + 1x + 0y + 0u + 0v + 0z
           Weak:
            if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))
            2 + 1x + 1y + 1u + 1v + 1z >= 3 + 1x + 1y + 2u + 2v + 1z
          Qed