Input TRS:
    1: Tl(O(x),y) -> Tr(check(x),y)
    2: Tl(O(x),y) -> Tr(x,check(y))
    3: Tl(N(x),y) -> Tr(check(x),y)
    4: Tl(N(x),y) -> Tr(x,check(y))
    5: Tr(x,O(y)) -> Tl(check(x),y)
    6: Tr(x,O(y)) -> Tl(x,check(y))
    7: Tr(x,N(y)) -> Tl(check(x),y)
    8: Tr(x,N(y)) -> Tl(x,check(y))
    9: Tl(B(),y) -> Tr(check(B()),y)
    10: Tl(B(),y) -> Tr(B(),check(y))
    11: Tr(x,B()) -> Tl(check(x),B())
    12: Tr(x,B()) -> Tl(x,check(B()))
   e1: Tl(O(x),y) ->= Tl(check(x),y)	[relative]
   e2: Tl(O(x),y) ->= Tl(x,check(y))	[relative]
   e3: Tl(N(x),y) ->= Tl(check(x),y)	[relative]
   e4: Tl(N(x),y) ->= Tl(x,check(y))	[relative]
   e5: Tr(x,O(y)) ->= Tr(check(x),y)	[relative]
   e6: Tr(x,O(y)) ->= Tr(x,check(y))	[relative]
   e7: Tr(x,N(y)) ->= Tr(check(x),y)	[relative]
   e8: Tr(x,N(y)) ->= Tr(x,check(y))	[relative]
   e9: B() ->= N(B())	[relative]
   e10: check(O(x)) ->= O(x)	[relative]
   e11: check(O(x)) ->= O(check(x))	[relative]
   e12: check(N(x)) ->= N(check(x))	[relative]
Number of Rules: 12
Direct Mat3b ... removes: 1 5 6 2 e6 e2 e5 e1
	I(Tl) = [1,0,0;0,0,0;1,0,0] * x1 + [1,0,0;0,0,0;0,0,0] * x2
	I(O) = [1,0,0;0,0,0;0,0,0] * x1 + [1;1;1]
	I(B) = [0;0;0]
	I(check) = [1,0,0;0,0,1;0,1,0] * x1 + [0;1;1]
	I(Tr) = [1,0,0;0,0,0;1,0,0] * x1 + [1,0,0;0,0,0;0,0,0] * x2
	I(N) = [1,0,0;0,0,1;0,1,0] * x1
Number of Rules: 8
Direct Mat3b ... removes: 9
	I(Tl) = [1,1,1;1,0,0;0,0,0] * x1 + [1,0,0;0,0,0;0,0,0] * x2
	I(O) = [1,0,0;0,0,0;0,0,0] * x1 + [1;0;0]
	I(B) = [1;1;1]
	I(check) = [1,0,0;0,0,0;0,0,0] * x1
	I(Tr) = [1,1,1;1,0,0;0,0,0] * x1 + [1,0,0;0,0,0;0,0,0] * x2
	I(N) = [1,0,0;0,0,1;0,1,0] * x1
Number of Rules: 7
Direct Mat3b ... removes: 12
	I(Tl) = [1,0,0;1,0,0;0,0,0] * x1 + [1,0,1;0,0,0;0,0,0] * x2 + [2;0;0]
	I(O) = [1,0,1;0,1,0;0,0,0] * x1 + [1;1;0]
	I(B) = [1;2;1]
	I(check) = [1,0,0;0,1,0;0,0,0] * x1 + [0;1;0]
	I(Tr) = [1,0,0;1,0,0;0,0,0] * x1 + [1,0,1;0,0,0;0,0,0] * x2 + [2;0;0]
	I(N) = [1,0,0;0,0,1;0,0,1] * x1 + [0;1;0]
Number of Rules: 6
Direct Mat3b ... failed.