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]
Weak rule e2 calls a strict rule