Input TRS:
    1: top(ok(queue(old(x),bot()))) -> top(check(queue(x,bot())))
    2: top(ok(queue(new(x),bot()))) -> top(check(queue(x,bot())))
    3: top(ok(queue(bot(),old(x)))) -> top(check(queue(bot(),x)))
    4: top(ok(queue(bot(),new(x)))) -> top(check(queue(bot(),x)))
    5: top(ok(queue(old(x),old(y)))) -> top(check(queue(x,y)))
    6: top(ok(queue(old(x),new(y)))) -> top(check(queue(x,y)))
    7: top(ok(queue(new(x),old(y)))) -> top(check(queue(x,y)))
    8: top(ok(queue(new(x),new(y)))) -> top(check(queue(x,y)))
    9: top(ok(queue(old(x),y))) ->= top(check(queue(x,y)))
    10: top(ok(queue(new(x),y))) ->= top(check(queue(x,y)))
    11: bot() ->= new(bot())
    12: check(old(x)) ->= ok(old(x))
    13: check(new(x)) ->= new(check(x))
    14: check(queue(x,y)) ->= queue(check(x),y)
    15: check(queue(x,y)) ->= queue(x,check(y))
    16: old(ok(x)) ->= ok(old(x))
    17: new(ok(x)) ->= ok(new(x))
    18: queue(ok(x),y) ->= ok(queue(x,y))
    19: queue(x,ok(y)) ->= ok(queue(x,y))
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... removes: 1 3 5 7 9 6
   new(x1)	weight: x1
   top(x1)	weight: x1
   bot()	weight: (/ 1 8)
 queue(x1,x2)	weight: (/ 46825 8) + x2 + x1
 check(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 8) + x1
   old(x1)	weight: (/ 244897 8) + x1
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 16
   new(x1)	weight: x1
   top(x1)	weight: x1
   bot()	weight: (/ 261929 8)
 queue(x1,x2)	weight: (/ 222849 8) + x2 + x1
 check(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 8) + x1
   old(x1)	weight: (/ 1 8) + 2 * x1
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #top(ok(queue(new(x),bot()))) -> #top(check(queue(x,bot())))
   #2: #top(ok(queue(new(x),y))) ->? #top(check(queue(x,y)))
   #3: #top(ok(queue(new(x),new(y)))) -> #top(check(queue(x,y)))
   #4: #top(ok(queue(bot(),new(x)))) -> #top(check(queue(bot(),x)))
Number of SCCs: 1, DPs: 4, edges: 16
	SCC { #1..4 }
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