Input TRS:
    1: del(.(x,.(y,z))) -> f(=(x,y),x,y,z)
    2: f(true(),x,y,z) -> del(.(y,z))
    3: f(false(),x,y,z) -> .(x,del(.(y,z)))
    4: =(nil(),nil()) -> true()
    5: =(.(x,y),nil()) -> false()
    6: =(nil(),.(y,z)) -> false()
    7: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v()))
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... failed.
Freezing del
1: del❆1_.(x,.(y,z)) -> f(=(x,y),x,y,z)
2: f(true(),x,y,z) -> del❆1_.(y,z)
3: f(false(),x,y,z) -> .(x,del❆1_.(y,z))
4: =(nil(),nil()) -> true()
5: =(.(x,y),nil()) -> false()
6: =(nil(),.(y,z)) -> false()
7: =(.(x,y),.(u(),v())) -> and(=(x,u()),=(y,v()))
8: del(.(_1,_2)) ->= del❆1_.(_1,_2)
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #f(true(),x,y,z) -> #del❆1_.(y,z)
   #2: #=(.(x,y),.(u(),v())) -> #=(x,u())
   #3: #=(.(x,y),.(u(),v())) -> #=(y,v())
   #4: #f(false(),x,y,z) -> #del❆1_.(y,z)
   #5: #del❆1_.(x,.(y,z)) -> #f(=(x,y),x,y,z)
   #6: #del❆1_.(x,.(y,z)) -> #=(x,y)
   #7: #del(.(_1,_2)) ->? #del❆1_.(_1,_2)
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #1 #4 #5 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #del(x1)	weight: 0
     v()	weight: 0
     u()	weight: 0
   and(x1,x2)	weight: 0
#del❆1_.(x1,x2)	weight: x2
 false()	weight: 0
  true()	weight: 0
     f(x1,x2,x3,x4)	weight: 0
   del(x1)	weight: 0
     =(x1,x2)	weight: (/ 1 2) + x2
   nil()	weight: 0
   #f(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x4
     .(x1,x2)	weight: (/ 3 2) + x1 + x2
   #=(x1,x2)	weight: 0
del❆1_.(x1,x2)	weight: 0
    Usable rules: { 4..7 }
    Removed DPs: #1 #4 #5
Number of SCCs: 0, DPs: 0, edges: 0
YES