YES
Time: 0.025779
TRS:
 {     f(true(), x, y, z) -> del .(y, z),
      f(false(), x, y, z) -> .(x, del .(y, z)),
  =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
        =(.(x, y), nil()) -> false(),
        =(nil(), .(y, z)) -> false(),
          =(nil(), nil()) -> true(),
        del .(x, .(y, z)) -> f(=(x, y), x, y, z)}
 DP:
  DP:
   {     f#(true(), x, y, z) -> del# .(y, z),
        f#(false(), x, y, z) -> del# .(y, z),
    =#(.(x, y), .(u(), v())) -> =#(x, u()),
    =#(.(x, y), .(u(), v())) -> =#(y, v()),
          del# .(x, .(y, z)) -> f#(=(x, y), x, y, z),
          del# .(x, .(y, z)) -> =#(x, y)}
  TRS:
  {     f(true(), x, y, z) -> del .(y, z),
       f(false(), x, y, z) -> .(x, del .(y, z)),
   =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
         =(.(x, y), nil()) -> false(),
         =(nil(), .(y, z)) -> false(),
           =(nil(), nil()) -> true(),
         del .(x, .(y, z)) -> f(=(x, y), x, y, z)}
  UR:
   {=(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
          =(.(x, y), nil()) -> false(),
          =(nil(), .(y, z)) -> false(),
            =(nil(), nil()) -> true(),
                    a(w, v) -> w,
                    a(w, v) -> v}
   EDG:
    {(del# .(x, .(y, z)) -> =#(x, y), =#(.(x, y), .(u(), v())) -> =#(y, v()))
     (del# .(x, .(y, z)) -> =#(x, y), =#(.(x, y), .(u(), v())) -> =#(x, u()))
     (f#(false(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> =#(x, y))
     (f#(false(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> f#(=(x, y), x, y, z))
     (f#(true(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> f#(=(x, y), x, y, z))
     (f#(true(), x, y, z) -> del# .(y, z), del# .(x, .(y, z)) -> =#(x, y))
     (del# .(x, .(y, z)) -> f#(=(x, y), x, y, z), f#(true(), x, y, z) -> del# .(y, z))
     (del# .(x, .(y, z)) -> f#(=(x, y), x, y, z), f#(false(), x, y, z) -> del# .(y, z))}
    STATUS:
     arrows: 0.777778
     SCCS (1):
      Scc:
       { f#(true(), x, y, z) -> del# .(y, z),
        f#(false(), x, y, z) -> del# .(y, z),
          del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)}
      
      SCC (3):
       Strict:
        { f#(true(), x, y, z) -> del# .(y, z),
         f#(false(), x, y, z) -> del# .(y, z),
           del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)}
       Weak:
       {     f(true(), x, y, z) -> del .(y, z),
            f(false(), x, y, z) -> .(x, del .(y, z)),
        =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
              =(.(x, y), nil()) -> false(),
              =(nil(), .(y, z)) -> false(),
                =(nil(), nil()) -> true(),
              del .(x, .(y, z)) -> f(=(x, y), x, y, z)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1, x2, x3) = 0,
         
         [=](x0, x1) = x0,
         
         [.](x0, x1) = x0 + x1,
         
         [and](x0, x1) = x0 + x1,
         
         [del](x0) = 0,
         
         [true] = 1,
         
         [false] = 0,
         
         [nil] = 1,
         
         [u] = 1,
         
         [v] = 1,
         
         [f#](x0, x1, x2, x3) = x0 + x1 + x2,
         
         [del#](x0) = x0
        Strict:
         del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)
         0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
         f#(false(), x, y, z) -> del# .(y, z)
         0 + 0x + 1y + 1z >= 0 + 1y + 1z
         f#(true(), x, y, z) -> del# .(y, z)
         1 + 0x + 1y + 1z >= 0 + 1y + 1z
        Weak:
         del .(x, .(y, z)) -> f(=(x, y), x, y, z)
         0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
         =(nil(), nil()) -> true()
         1 >= 1
         =(nil(), .(y, z)) -> false()
         1 + 0y + 0z >= 0
         =(.(x, y), nil()) -> false()
         0 + 1x + 1y >= 0
         =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v()))
         0 + 1x + 1y >= 0 + 1x + 1y
         f(false(), x, y, z) -> .(x, del .(y, z))
         0 + 0x + 0y + 0z >= 0 + 1x + 0y + 0z
         f(true(), x, y, z) -> del .(y, z)
         0 + 0x + 0y + 0z >= 0 + 0y + 0z
       SCCS (1):
        Scc:
         {f#(false(), x, y, z) -> del# .(y, z),
            del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)}
        
        SCC (2):
         Strict:
          {f#(false(), x, y, z) -> del# .(y, z),
             del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)}
         Weak:
         {     f(true(), x, y, z) -> del .(y, z),
              f(false(), x, y, z) -> .(x, del .(y, z)),
          =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())),
                =(.(x, y), nil()) -> false(),
                =(nil(), .(y, z)) -> false(),
                  =(nil(), nil()) -> true(),
                del .(x, .(y, z)) -> f(=(x, y), x, y, z)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [f](x0, x1, x2, x3) = 0,
           
           [=](x0, x1) = 0,
           
           [.](x0, x1) = x0 + 1,
           
           [and](x0, x1) = 0,
           
           [del](x0) = x0 + 1,
           
           [true] = 0,
           
           [false] = 0,
           
           [nil] = 0,
           
           [u] = 0,
           
           [v] = 1,
           
           [f#](x0, x1, x2, x3) = x0 + 1,
           
           [del#](x0) = x0
          Strict:
           del# .(x, .(y, z)) -> f#(=(x, y), x, y, z)
           2 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z
           f#(false(), x, y, z) -> del# .(y, z)
           1 + 0x + 0y + 1z >= 1 + 0y + 1z
          Weak:
           del .(x, .(y, z)) -> f(=(x, y), x, y, z)
           3 + 0x + 0y + 1z >= 0 + 0x + 0y + 0z
           =(nil(), nil()) -> true()
           0 >= 0
           =(nil(), .(y, z)) -> false()
           0 + 0y + 0z >= 0
           =(.(x, y), nil()) -> false()
           0 + 0x + 0y >= 0
           =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v()))
           0 + 0x + 0y >= 0 + 0x + 0y
           f(false(), x, y, z) -> .(x, del .(y, z))
           0 + 0x + 0y + 0z >= 3 + 0x + 0y + 1z
           f(true(), x, y, z) -> del .(y, z)
           0 + 0x + 0y + 0z >= 2 + 0y + 1z
         SCCS (0):