MAYBE

Problem:
 del(.(x,.(y,z))) -> f(=(x,y),x,y,z)
 f(true(),x,y,z) -> del(.(y,z))
 f(false(),x,y,z) -> .(x,del(.(y,z)))
 =(nil(),nil()) -> true()
 =(.(x,y),nil()) -> false()
 =(nil(),.(y,z)) -> false()
 =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v()))

Proof:
 DP Processor:
  DPs:
   del#(.(x,.(y,z))) -> =#(x,y)
   del#(.(x,.(y,z))) -> f#(=(x,y),x,y,z)
   f#(true(),x,y,z) -> del#(.(y,z))
   f#(false(),x,y,z) -> del#(.(y,z))
   =#(.(x,y),.(u(),v())) -> =#(y,v())
   =#(.(x,y),.(u(),v())) -> =#(x,u())
  TRS:
   del(.(x,.(y,z))) -> f(=(x,y),x,y,z)
   f(true(),x,y,z) -> del(.(y,z))
   f(false(),x,y,z) -> .(x,del(.(y,z)))
   =(nil(),nil()) -> true()
   =(.(x,y),nil()) -> false()
   =(nil(),.(y,z)) -> false()
   =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v()))
  Usable Rule Processor:
   DPs:
    del#(.(x,.(y,z))) -> =#(x,y)
    del#(.(x,.(y,z))) -> f#(=(x,y),x,y,z)
    f#(true(),x,y,z) -> del#(.(y,z))
    f#(false(),x,y,z) -> del#(.(y,z))
    =#(.(x,y),.(u(),v())) -> =#(y,v())
    =#(.(x,y),.(u(),v())) -> =#(x,u())
   TRS:
    f13(x,y) -> x
    f13(x,y) -> y
    =(nil(),nil()) -> true()
    =(.(x,y),nil()) -> false()
    =(nil(),.(y,z)) -> false()
    =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v()))
   CDG Processor:
    DPs:
     del#(.(x,.(y,z))) -> =#(x,y)
     del#(.(x,.(y,z))) -> f#(=(x,y),x,y,z)
     f#(true(),x,y,z) -> del#(.(y,z))
     f#(false(),x,y,z) -> del#(.(y,z))
     =#(.(x,y),.(u(),v())) -> =#(y,v())
     =#(.(x,y),.(u(),v())) -> =#(x,u())
    TRS:
     f13(x,y) -> x
     f13(x,y) -> y
     =(nil(),nil()) -> true()
     =(.(x,y),nil()) -> false()
     =(nil(),.(y,z)) -> false()
     =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v()))
    graph:
     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))) -> =#(x,y)
     f#(true(),x,y,z) -> del#(.(y,z)) ->
     del#(.(x,.(y,z))) -> f#(=(x,y),x,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#(false(),x,y,z) -> del#(.(y,z))
     del#(.(x,.(y,z))) -> =#(x,y) -> =#(.(x,y),.(u(),v())) -> =#(y,v())
     del#(.(x,.(y,z))) -> =#(x,y) -> =#(.(x,y),.(u(),v())) -> =#(x,u())
    Restore Modifier:
     DPs:
      del#(.(x,.(y,z))) -> =#(x,y)
      del#(.(x,.(y,z))) -> f#(=(x,y),x,y,z)
      f#(true(),x,y,z) -> del#(.(y,z))
      f#(false(),x,y,z) -> del#(.(y,z))
      =#(.(x,y),.(u(),v())) -> =#(y,v())
      =#(.(x,y),.(u(),v())) -> =#(x,u())
     TRS:
      del(.(x,.(y,z))) -> f(=(x,y),x,y,z)
      f(true(),x,y,z) -> del(.(y,z))
      f(false(),x,y,z) -> .(x,del(.(y,z)))
      =(nil(),nil()) -> true()
      =(.(x,y),nil()) -> false()
      =(nil(),.(y,z)) -> false()
      =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v()))
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 8/36
      DPs:
       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))
      TRS:
       del(.(x,.(y,z))) -> f(=(x,y),x,y,z)
       f(true(),x,y,z) -> del(.(y,z))
       f(false(),x,y,z) -> .(x,del(.(y,z)))
       =(nil(),nil()) -> true()
       =(.(x,y),nil()) -> false()
       =(nil(),.(y,z)) -> false()
       =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v()))
      Open