Input TRS:
    1: rec(rec(x)) -> sent(rec(x))
    2: rec(sent(x)) -> sent(rec(x))
    3: rec(no(x)) -> sent(rec(x))
    4: rec(bot()) -> up(sent(bot()))
    5: rec(up(x)) -> up(rec(x))
    6: sent(up(x)) -> up(sent(x))
    7: no(up(x)) -> up(no(x))
    8: top(rec(up(x))) -> top(check(rec(x)))
    9: top(sent(up(x))) -> top(check(rec(x)))
    10: top(no(up(x))) -> top(check(rec(x)))
    11: check(up(x)) -> up(check(x))
    12: check(sent(x)) -> sent(check(x))
    13: check(rec(x)) -> rec(check(x))
    14: check(no(x)) -> no(check(x))
    15: check(no(x)) -> no(x)
Number of strict rules: 15
Direct Order(PosReal,>,Poly) ... removes: 8 1 3 10
   top(x1)	weight: x1
    no(x1)	weight: (/ 42477 2) + x1
   bot()	weight: 0
 check(x1)	weight: x1
   rec(x1)	weight: (/ 20313 2) + x1
  sent(x1)	weight: (/ 1 4) + x1
    up(x1)	weight: (/ 40625 4) + x1
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... removes: 7
   top(x1)	weight: x1
    no(x1)	weight: (/ 1 4) + 2 * x1
   bot()	weight: 0
 check(x1)	weight: x1
   rec(x1)	weight: 10451 + x1
  sent(x1)	weight: (/ 1 4) + x1
    up(x1)	weight: (/ 41803 4) + x1
Number of strict rules: 10
Direct Order(PosReal,>,Poly) ... removes: 15 14
   top(x1)	weight: x1
    no(x1)	weight: (/ 1 4) + x1
   bot()	weight: 0
 check(x1)	weight: 2 * x1
   rec(x1)	weight: x1
  sent(x1)	weight: x1
    up(x1)	weight: 2 * x1
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #rec(sent(x)) -> #sent(rec(x))
   #2: #rec(sent(x)) -> #rec(x)
   #3: #sent(up(x)) -> #sent(x)
   #4: #check(rec(x)) -> #rec(check(x))
   #5: #check(rec(x)) -> #check(x)
   #6: #top(sent(up(x))) -> #top(check(rec(x)))
   #7: #top(sent(up(x))) -> #check(rec(x))
   #8: #top(sent(up(x))) -> #rec(x)
   #9: #check(up(x)) -> #check(x)
   #10: #check(sent(x)) -> #sent(check(x))
   #11: #check(sent(x)) -> #check(x)
   #12: #rec(up(x)) -> #rec(x)
   #13: #rec(bot()) -> #sent(bot())
Number of SCCs: 4, DPs: 7, edges: 15
	SCC { #3 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   top(x1)	weight: 0
    no(x1)	weight: 0
#check(x1)	weight: 0
   bot()	weight: 0
#sent(x1)	weight: x1
 #top(x1)	weight: 0
 check(x1)	weight: 0
   rec(x1)	weight: 0
 #rec(x1)	weight: 0
  sent(x1)	weight: 0
    up(x1)	weight: (/ 1 2) + x1
    Usable rules: { }
    Removed DPs: #3
Number of SCCs: 3, DPs: 6, edges: 14
	SCC { #6 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... succeeded.
   top(x1)	weight: 0; 0
    no(x1)	weight: 0; 0
#check(x1)	weight: 0; 0
   bot()	weight: (/ 1 8); (/ 1 4)
#sent(x1)	weight: 0; 0
 #top(x1)	weight: x1_1 + x1_2; x1_1 + x1_2
 check(x1)	weight: (/ 1 8) + x1_1; 0
   rec(x1)	weight: (/ 1 8) + x1_1 + x1_2; x1_2
 #rec(x1)	weight: 0; 0
  sent(x1)	weight: (/ 3 8) + x1_1; x1_2
    up(x1)	weight: x1_1; x1_2
    Usable rules: { 2 4..6 11..13 }
    Removed DPs: #6
Number of SCCs: 2, DPs: 5, edges: 13
	SCC { #2 #12 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   top(x1)	weight: 0
    no(x1)	weight: 0
#check(x1)	weight: 0
   bot()	weight: 0
#sent(x1)	weight: 0
 #top(x1)	weight: 0
 check(x1)	weight: (/ 1 4)
   rec(x1)	weight: (/ 1 2)
 #rec(x1)	weight: x1
  sent(x1)	weight: (/ 1 2) + x1
    up(x1)	weight: (/ 1 4) + x1
    Usable rules: { }
    Removed DPs: #2 #12
Number of SCCs: 1, DPs: 3, edges: 9
	SCC { #5 #9 #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   top(x1)	weight: 0
    no(x1)	weight: 0
#check(x1)	weight: x1
   bot()	weight: 0
#sent(x1)	weight: 0
 #top(x1)	weight: 0
 check(x1)	weight: (/ 1 4)
   rec(x1)	weight: (/ 1 4) + x1
 #rec(x1)	weight: 0
  sent(x1)	weight: x1
    up(x1)	weight: (/ 1 2) + x1
    Usable rules: { }
    Removed DPs: #5 #9
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   top(x1)	weight: 0
    no(x1)	weight: 0
#check(x1)	weight: x1
   bot()	weight: 0
#sent(x1)	weight: 0
 #top(x1)	weight: 0
 check(x1)	weight: (/ 1 4)
   rec(x1)	weight: (/ 1 2)
 #rec(x1)	weight: 0
  sent(x1)	weight: (/ 1 4) + x1
    up(x1)	weight: (/ 1 2)
    Usable rules: { }
    Removed DPs: #11
Number of SCCs: 0, DPs: 0, edges: 0
YES