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 Mat2b ... removes: 1 3 5 7 6 e1
	I(new) = [1,1;0,1] * x1
	I(top) = [2,1;0,1] * x1
	I(bot) = [1;0]
	I(queue) = [1,0;0,0] * x1 + [1,0;1,1] * x2 + [1;1]
	I(check) = x1
	I(ok) = x1
	I(old) = [2,0;0,1] * x1 + [1;1]
Number of Rules: 3
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 Mat2b ... failed.