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]
Number of Rules: 8
Direct POLO(Sum) ... removes: 1 3 5 7 6 e1
	I(new) = x1
	I(top) = x1
	I(bot) = 0
	I(queue) = x1 + x2
	I(check) = x1
	I(ok) = x1
	I(old) = x1 + 1
Number of Rules: 3
Direct POLO(Sum) ...Direct Mat2b ... removes: e8
	I(new) = [1,0;1,1] * x1
	I(top) = x1
	I(bot) = [0;1]
	I(queue) = x1 + x2 + [0;1]
	I(check) = x1 + [0;1]
	I(ok) = x1 + [0;1]
	I(old) = [1,1;1,1] * x1 + [1;1]
Number of Rules: 3
Direct POLO(Sum) ...Direct Mat2b ... 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)))	[relative]
   #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
  SCC { #1..4 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.