Input TRS:
    1: RAo(R()) -> R()
    2: RAn(R()) -> R()
    3: WAo(W()) -> W()
    4: WAn(W()) -> W()
   e1: Rw() ->= RIn(Rw())	[relative]
   e2: Ww() ->= WIn(Ww())	[relative]
   e3: top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) ->= top(check(sys_r(read(RAo(r),x),write(W(),Ww()))))	[relative]
   e4: top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) ->= top(check(sys_w(read(RAo(r),x),write(W(),Ww()))))	[relative]
   e5: top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) ->= top(check(sys_r(read(RAn(r),x),write(W(),Ww()))))	[relative]
   e6: top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) ->= top(check(sys_w(read(RAn(r),x),write(W(),Ww()))))	[relative]
   e7: top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) ->= top(check(sys_r(read(R(),Rw()),write(WAn(W()),y))))	[relative]
   e8: top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) ->= top(check(sys_w(read(R(),Rw()),write(WAn(W()),y))))	[relative]
   e9: top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) ->= top(check(sys_r(read(R(),Rw()),write(WAo(W()),y))))	[relative]
   e10: top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) ->= top(check(sys_w(read(R(),Rw()),write(WAo(W()),y))))	[relative]
   e11: top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) ->= top(check(sys_w(read(RAo(r),x),write(W(),y))))	[relative]
   e12: top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) ->= top(check(sys_w(read(RAn(r),x),write(W(),y))))	[relative]
   e13: top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) ->= top(check(sys_r(read(R(),x),write(WAo(W()),y))))	[relative]
   e14: top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) ->= top(check(sys_r(read(R(),x),write(WAn(W()),y))))	[relative]
   e15: check(RIo(x)) ->= ok(RIo(x))	[relative]
   e16: check(RAo(x)) ->= RAo(check(x))	[relative]
   e17: check(RAn(x)) ->= RAn(check(x))	[relative]
   e18: check(WAo(x)) ->= WAo(check(x))	[relative]
   e19: check(WAn(x)) ->= WAn(check(x))	[relative]
   e20: check(RIo(x)) ->= RIo(check(x))	[relative]
   e21: check(RIn(x)) ->= RIn(check(x))	[relative]
   e22: check(WIo(x)) ->= WIo(check(x))	[relative]
   e23: check(WIn(x)) ->= WIn(check(x))	[relative]
   e24: check(sys_r(x,y)) ->= sys_r(check(x),y)	[relative]
   e25: check(sys_r(x,y)) ->= sys_r(x,check(y))	[relative]
   e26: check(sys_w(x,y)) ->= sys_w(check(x),y)	[relative]
   e27: check(sys_w(x,y)) ->= sys_w(x,check(y))	[relative]
   e28: RAo(ok(x)) ->= ok(RAo(x))	[relative]
   e29: RAn(ok(x)) ->= ok(RAn(x))	[relative]
   e30: WAo(ok(x)) ->= ok(WAo(x))	[relative]
   e31: WAn(ok(x)) ->= ok(WAn(x))	[relative]
   e32: RIn(ok(x)) ->= ok(RIn(x))	[relative]
   e33: WIo(ok(x)) ->= ok(WIo(x))	[relative]
   e34: WIn(ok(x)) ->= ok(WIn(x))	[relative]
   e35: sys_r(ok(x),y) ->= ok(sys_r(x,y))	[relative]
   e36: sys_r(x,ok(y)) ->= ok(sys_r(x,y))	[relative]
   e37: sys_w(ok(x),y) ->= ok(sys_w(x,y))	[relative]
   e38: sys_w(x,ok(y)) ->= ok(sys_w(x,y))	[relative]
Number of Rules: 4
Direct Mat2b ... removes: 3 e13 e9 e11 e10 e3 e4
	I(sys_w) = [1,0;0,0] * x1 + [1,0;0,0] * x2 + [1;1]
	I(RAo) = [1,0;0,0] * x1
	I(RIo) = x1 + [1;0]
	I(read) = [1,1;0,1] * x1 + [1,0;0,0] * x2
	I(W) = [1;1]
	I(top) = [1,0;0,0] * x1
	I(WIn) = x1
	I(WAo) = [1,0;0,0] * x1 + [1;1]
	I(Ww) = [2;1]
	I(WIo) = x1 + [3;0]
	I(check) = [1,0;0,0] * x1 + [1;1]
	I(ok) = [1,0;0,0] * x1 + [1;0]
	I(Rw) = [1;1]
	I(R) = [1;0]
	I(WAn) = x1
	I(RIn) = x1
	I(write) = [2,1;0,0] * x1 + [1,1;0,1] * x2
	I(RAn) = x1
	I(sys_r) = [1,0;0,0] * x1 + [1,0;0,0] * x2 + [1;0]
Number of Rules: 3
Direct Mat2b ... removes: 1
	I(sys_w) = [1,0;0,0] * x1 + [1,0;0,0] * x2 + [1;1]
	I(RAo) = [1,0;0,0] * x1 + [1;1]
	I(RIo) = [1,0;0,0] * x1 + [2;1]
	I(read) = [1,1;0,1] * x1 + x2
	I(W) = [1;0]
	I(top) = x1
	I(WIn) = [1,0;0,0] * x1 + [0;1]
	I(WAo) = [1,0;0,0] * x1 + [1;1]
	I(Ww) = [1;1]
	I(WIo) = x1 + [1;0]
	I(check) = [1,0;0,0] * x1 + [1;1]
	I(ok) = [1,0;0,0] * x1 + [1;1]
	I(Rw) = [1;1]
	I(R) = [1;0]
	I(WAn) = [1,0;0,0] * x1 + [0;1]
	I(RIn) = [1,0;0,0] * x1 + [0;1]
	I(write) = [1,0;0,0] * x1 + [1,0;0,0] * x2 + [0;1]
	I(RAn) = x1
	I(sys_r) = [1,0;0,0] * x1 + [1,0;0,0] * x2 + [1;1]
Number of Rules: 2
Direct Mat2b ... removes: 4 2 e7 e12 e5
	I(sys_w) = [2,0;0,1] * x1 + x2 + [1;1]
	I(RAo) = x1 + [1;1]
	I(RIo) = x1 + [1;5]
	I(read) = [1,1;0,0] * x1 + [1,0;0,0] * x2 + [1;0]
	I(W) = [1;1]
	I(top) = [1,1;0,0] * x1
	I(WIn) = x1
	I(WAo) = x1 + [1;1]
	I(Ww) = [1;0]
	I(WIo) = [1,0;1,0] * x1 + [1;5]
	I(check) = x1
	I(ok) = [1,0;0,0] * x1 + [0;5]
	I(Rw) = [0;5]
	I(R) = [0;1]
	I(WAn) = x1 + [1;2]
	I(RIn) = [1,0;0,0] * x1 + [0;5]
	I(write) = [2,1;0,0] * x1 + [1,1;0,0] * x2
	I(RAn) = x1 + [1;1]
	I(sys_r) = [2,0;0,1] * x1 + x2 + [2;0]
Number of Rules: 0