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)))
   e1: top(ok(queue(old(x),y))) ->= top(check(queue(x,y)))	[relative]
   e2: top(ok(queue(new(x),y))) ->= top(check(queue(x,y)))	[relative]
   e3: bot() ->= new(bot())	[relative]
   e4: check(old(x)) ->= ok(old(x))	[relative]
   e5: check(new(x)) ->= new(check(x))	[relative]
   e6: check(queue(x,y)) ->= queue(check(x),y)	[relative]
   e7: check(queue(x,y)) ->= queue(x,check(y))	[relative]
   e8: old(ok(x)) ->= ok(old(x))	[relative]
   e9: new(ok(x)) ->= ok(new(x))	[relative]
   e10: queue(ok(x),y) ->= ok(queue(x,y))	[relative]
   e11: queue(x,ok(y)) ->= ok(queue(x,y))	[relative]
Dependency Pairs:
   #1: # top(ok(queue(new(x),bot()))) -> # top(check(queue(x,bot())))
   #2: # top(ok(queue(old(x),new(y)))) -> # top(check(queue(x,y)))
   #3: # top(ok(queue(new(x),y))) -> # top(check(queue(x,y)))	[relative]
   #4: # top(ok(queue(new(x),old(y)))) -> # top(check(queue(x,y)))
   #5: # top(ok(queue(old(x),y))) -> # top(check(queue(x,y)))	[relative]
   #6: # top(ok(queue(old(x),old(y)))) -> # top(check(queue(x,y)))
   #7: # top(ok(queue(bot(),old(x)))) -> # top(check(queue(bot(),x)))
   #8: # top(ok(queue(old(x),bot()))) -> # top(check(queue(x,bot())))
   #9: # top(ok(queue(new(x),new(y)))) -> # top(check(queue(x,y)))
   #10: # top(ok(queue(bot(),new(x)))) -> # top(check(queue(bot(),x)))
Number of SCCs: 1
  SCC { #1..10 }
    POLO(Sum)... removes: #2 #4 #5 #6 #7 #8
	I(new) = max(x1, 0)
	I(top) = 0
	I(bot) = 1
	I(queue) = max(x1 + x2 + 1, 0)
	I(check) = max(x1 + 3, 0)
	I(ok) = max(x1 + 3, 0)
	I(# top) = max(x1 - 5, 0)
	I(old) = max(x1 + 2, 0)
Number of SCCs: 1
  SCC { #1 #3 #9 #10 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.