Input TRS:
    1: *(|0|(),x) -> |0|()
    2: *(|1|(),x) -> x
    3: *(|2|(),|2|()) -> .(|1|(),|0|())
    4: *(|3|(),x) -> .(x,*(min(),x))
    5: *(min(),min()) -> |1|()
    6: *(|2|(),min()) -> .(min(),|2|())
    7: *(.(x,y),z) -> .(*(x,z),*(y,z))
    8: *(+(y,z),x) -> +(*(x,y),*(x,z))
    9: +(|0|(),x) -> x
    10: +(x,x) -> *(|2|(),x)
    11: +(|1|(),|2|()) -> |3|()
    12: +(|1|(),min()) -> |0|()
    13: +(|2|(),min()) -> |1|()
    14: +(|3|(),x) -> .(|1|(),+(min(),x))
    15: +(.(x,y),z) -> .(x,+(y,z))
    16: +(*(|2|(),x),x) -> *(|3|(),x)
    17: +(*(min(),x),x) -> |0|()
    18: +(*(|2|(),v),*(min(),v)) -> v
    19: .(min(),|3|()) -> min()
    20: .(x,min()) -> .(+(min(),x),|3|())
    21: .(|0|(),x) -> x
    22: .(x,.(y,z)) -> .(+(x,y),z)
Number of strict rules: 22
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #*(|2|(),min()) -> #.(min(),|2|())
   #2: #+(|3|(),x) -> #.(|1|(),+(min(),x))
   #3: #+(|3|(),x) -> #+(min(),x)
   #4: #.(x,min()) -> #.(+(min(),x),|3|())
   #5: #.(x,min()) -> #+(min(),x)
   #6: #*(.(x,y),z) -> #.(*(x,z),*(y,z))
   #7: #*(.(x,y),z) -> #*(x,z)
   #8: #*(.(x,y),z) -> #*(y,z)
   #9: #+(x,x) -> #*(|2|(),x)
   #10: #.(x,.(y,z)) -> #.(+(x,y),z)
   #11: #.(x,.(y,z)) -> #+(x,y)
   #12: #+(*(|2|(),x),x) -> #*(|3|(),x)
   #13: #*(|2|(),|2|()) -> #.(|1|(),|0|())
   #14: #*(+(y,z),x) -> #+(*(x,y),*(x,z))
   #15: #*(+(y,z),x) -> #*(x,y)
   #16: #*(+(y,z),x) -> #*(x,z)
   #17: #+(.(x,y),z) -> #.(x,+(y,z))
   #18: #+(.(x,y),z) -> #+(y,z)
   #19: #*(|3|(),x) -> #.(x,*(min(),x))
   #20: #*(|3|(),x) -> #*(min(),x)
Number of SCCs: 2, DPs: 9, edges: 28
	SCC { #7 #8 #15 #16 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
   #.(x1,x2)	weight: 0
   #*(x1,x2)	weight: x1 + x2
   |1|()	weight: 0
   |3|()	weight: 0
     .(x1,x2)	weight: (/ 1 2) + x1 + x2
   min()	weight: 0
   |2|()	weight: 0
     +(x1,x2)	weight: (/ 1 2) + x1 + x2
   #+(x1,x2)	weight: 0
     *(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #7 #8 #15 #16
Number of SCCs: 1, DPs: 5, edges: 12
	SCC { #2 #10 #11 #17 #18 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE