MAYBE
Time: 0.002201
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)}
  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)}
      Open