YES
TRS:
 {              if(x, y, y) -> y,
  if(if(x, y, z), u(), v()) -> if(x, if(y, u(), v()), if(z, u(), v())),
           if(true(), x, y) -> x,
          if(false(), x, y) -> y}
 RUF:
  Strict:
   {              if(x, y, y) -> y,
    if(if(x, y, z), u(), v()) -> if(x, if(y, u(), v()), if(z, u(), v()))}
  Weak:
   {}
  DP:
   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(x, y, y) -> y,
    if(if(x, y, z), u(), v()) -> if(x, if(y, u(), v()), if(z, u(), v()))}
   EDG:
    {(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#(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#(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#(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#(z, 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#(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()))}
    SCCS:
     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:
      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(x, y, y) -> y,
       if(if(x, y, z), u(), v()) -> if(x, if(y, u(), v()), if(z, u(), v()))}
      SPSC:
       Simple Projection:
        pi(if#) = 0
       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#(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#(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#(z, u(), v()))}
        SCCS:
         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#(z, u(), v())}
         SCC:
          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#(z, u(), v())}
          Weak:
          {              if(x, y, y) -> y,
           if(if(x, y, z), u(), v()) -> if(x, if(y, u(), v()), if(z, u(), v()))}
          SPSC:
           Simple Projection:
            pi(if#) = 0
           Strict:
            {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()))}
            SCCS:
             Scc:
              {if#(if(x, y, z), u(), v()) -> if#(z, u(), v())}
             SCC:
              Strict:
               {if#(if(x, y, z), u(), v()) -> if#(z, u(), v())}
              Weak:
              {              if(x, y, y) -> y,
               if(if(x, y, z), u(), v()) -> if(x, if(y, u(), v()), if(z, u(), v()))}
              SPSC:
               Simple Projection:
                pi(if#) = 0
               Strict:
                {}
               Qed