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]
Dependency Pairs:
   #1: # check(sys_w(x,y)) -> # check(x)	[relative]
   #2: # top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) -> # top(check(sys_w(read(R(),Rw()),write(WAn(W()),y))))	[relative]
   #3: # top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) -> # check(sys_w(read(R(),Rw()),write(WAn(W()),y)))	[relative]
   #4: # top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) -> # WAn(W())	[relative]
   #5: # top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) -> # top(check(sys_w(read(R(),Rw()),write(WAo(W()),y))))	[relative]
   #6: # top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) -> # check(sys_w(read(R(),Rw()),write(WAo(W()),y)))	[relative]
   #7: # top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) -> # WAo(W())	[relative]
   #8: # top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) -> # top(check(sys_w(read(RAn(r),x),write(W(),y))))	[relative]
   #9: # top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) -> # check(sys_w(read(RAn(r),x),write(W(),y)))	[relative]
   #10: # top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) -> # RAn(r)	[relative]
   #11: # top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) -> # top(check(sys_r(read(R(),Rw()),write(WAo(W()),y))))	[relative]
   #12: # top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) -> # check(sys_r(read(R(),Rw()),write(WAo(W()),y)))	[relative]
   #13: # top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) -> # WAo(W())	[relative]
   #14: # check(RAn(x)) -> # RAn(check(x))	[relative]
   #15: # check(RAn(x)) -> # check(x)	[relative]
   #16: # RAo(ok(x)) -> # RAo(x)	[relative]
   #17: # top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) -> # top(check(sys_w(read(RAo(r),x),write(W(),y))))	[relative]
   #18: # top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) -> # check(sys_w(read(RAo(r),x),write(W(),y)))	[relative]
   #19: # top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) -> # RAo(r)	[relative]
   #20: # check(RIn(x)) -> # check(x)	[relative]
   #21: # top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) -> # top(check(sys_w(read(RAn(r),x),write(W(),Ww()))))	[relative]
   #22: # top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) -> # check(sys_w(read(RAn(r),x),write(W(),Ww())))	[relative]
   #23: # top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) -> # RAn(r)	[relative]
   #24: # check(sys_w(x,y)) -> # check(y)	[relative]
   #25: # check(WAn(x)) -> # WAn(check(x))	[relative]
   #26: # check(WAn(x)) -> # check(x)	[relative]
   #27: # top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) -> # top(check(sys_w(read(RAo(r),x),write(W(),Ww()))))	[relative]
   #28: # top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) -> # check(sys_w(read(RAo(r),x),write(W(),Ww())))	[relative]
   #29: # top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) -> # RAo(r)	[relative]
   #30: # top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) -> # top(check(sys_r(read(R(),Rw()),write(WAn(W()),y))))	[relative]
   #31: # top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) -> # check(sys_r(read(R(),Rw()),write(WAn(W()),y)))	[relative]
   #32: # top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) -> # WAn(W())	[relative]
   #33: # WAn(ok(x)) -> # WAn(x)	[relative]
   #34: # RAn(ok(x)) -> # RAn(x)	[relative]
   #35: # check(RIo(x)) -> # check(x)	[relative]
   #36: # check(WIn(x)) -> # check(x)	[relative]
   #37: # check(WIo(x)) -> # check(x)	[relative]
   #38: # WAo(ok(x)) -> # WAo(x)	[relative]
   #39: # check(sys_r(x,y)) -> # check(x)	[relative]
   #40: # top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) -> # top(check(sys_r(read(RAn(r),x),write(W(),Ww()))))	[relative]
   #41: # top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) -> # check(sys_r(read(RAn(r),x),write(W(),Ww())))	[relative]
   #42: # top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) -> # RAn(r)	[relative]
   #43: # check(WAo(x)) -> # WAo(check(x))	[relative]
   #44: # check(WAo(x)) -> # check(x)	[relative]
   #45: # check(sys_r(x,y)) -> # check(y)	[relative]
   #46: # check(RAo(x)) -> # RAo(check(x))	[relative]
   #47: # check(RAo(x)) -> # check(x)	[relative]
   #48: # top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) -> # top(check(sys_r(read(R(),x),write(WAo(W()),y))))	[relative]
   #49: # top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) -> # check(sys_r(read(R(),x),write(WAo(W()),y)))	[relative]
   #50: # top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) -> # WAo(W())	[relative]
   #51: # top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) -> # top(check(sys_r(read(R(),x),write(WAn(W()),y))))	[relative]
   #52: # top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) -> # check(sys_r(read(R(),x),write(WAn(W()),y)))	[relative]
   #53: # top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) -> # WAn(W())	[relative]
   #54: # top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) -> # top(check(sys_r(read(RAo(r),x),write(W(),Ww()))))	[relative]
   #55: # top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) -> # check(sys_r(read(RAo(r),x),write(W(),Ww())))	[relative]
   #56: # top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) -> # RAo(r)	[relative]
Number of SCCs: 6
  SCC { #34 }
    POLO(Sum)... removes: #34
	I(# RAo) = 0
	I(sys_w) = max(x1 + x2 + 6, 0)
	I(# WAo) = 0
	I(RAo) = max(x1 + 1, 0)
	I(RIo) = max(x1 + 16, 0)
	I(read) = max(x2 + 11, 0)
	I(W) = 10
	I(WIn) = max(x1, 0)
	I(top) = max(x1 - 24, 0)
	I(WAo) = max(x1 + 4, 0)
	I(# check) = max(x1 - 1, 0)
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(Ww) = 1
	I(WIo) = max(x1 + 1, 0)
	I(check) = max(x1 + 7, 0)
	I(ok) = max(x1 + 7, 0)
	I(Rw) = 1
	I(# top) = 0
	I(R) = 3
	I(WAn) = max(x1 + 13, 0)
	I(RIn) = max(x1, 0)
	I(write) = max(x1 - 26, 0)
	I(RAn) = max(x1 + 1, 0)
	I(sys_r) = max(x1 + x2 + 6, 0)
Number of SCCs: 5
  SCC { #33 }
    POLO(Sum)... removes: #33
	I(# RAo) = 0
	I(sys_w) = max(x1 + x2 + 6, 0)
	I(# WAo) = 0
	I(RAo) = max(x1 + 1, 0)
	I(RIo) = max(x1 + 16, 0)
	I(read) = max(x2 + 11, 0)
	I(W) = 10
	I(WIn) = max(x1, 0)
	I(top) = max(x1 - 24, 0)
	I(WAo) = max(x1 + 4, 0)
	I(# check) = max(x1 - 1, 0)
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(Ww) = 1
	I(WIo) = max(x1 + 1, 0)
	I(check) = max(x1 + 7, 0)
	I(ok) = max(x1 + 7, 0)
	I(Rw) = 1
	I(# top) = 0
	I(R) = 3
	I(WAn) = max(x1 + 13, 0)
	I(RIn) = max(x1, 0)
	I(write) = max(x1 - 26, 0)
	I(RAn) = max(x1 + 1, 0)
	I(sys_r) = max(x1 + x2 + 6, 0)
Number of SCCs: 4
  SCC { #38 }
    POLO(Sum)... removes: #38
	I(# RAo) = 0
	I(sys_w) = max(x1 + x2 + 2, 0)
	I(# WAo) = max(x1 + 1, 0)
	I(RAo) = max(x1 + 3, 0)
	I(RIo) = max(x1 - 1, 0)
	I(read) = max(x1 + x2 - 9, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 1
	I(WAo) = max(x1 + 1, 0)
	I(# check) = max(x1 - 1, 0)
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(Ww) = 21
	I(WIo) = max(x1 + 9, 0)
	I(check) = max(x1 + 8, 0)
	I(ok) = max(x1 + 7, 0)
	I(Rw) = 23
	I(# top) = 0
	I(R) = 0
	I(WAn) = max(x1 + 1, 0)
	I(RIn) = max(x1, 0)
	I(write) = max(x2 - 23, 0)
	I(RAn) = max(x1 + 5, 0)
	I(sys_r) = max(x1 + x2 + 6, 0)
Number of SCCs: 3
  SCC { #16 }
    POLO(Sum)... removes: #16
	I(# RAo) = max(x1 + 1, 0)
	I(sys_w) = max(x1 + x2 + 1, 0)
	I(# WAo) = max(x1 + 1, 0)
	I(RAo) = max(x1 + 2, 0)
	I(RIo) = max(x1 - 4, 0)
	I(read) = max(x1 + x2 - 9, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 1
	I(WAo) = max(x1 + 7, 0)
	I(# check) = max(x1 - 1, 0)
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(Ww) = 22
	I(WIo) = max(x1 + 13, 0)
	I(check) = max(x1 + 12, 0)
	I(ok) = max(x1 + 8, 0)
	I(Rw) = 23
	I(# top) = 0
	I(R) = 0
	I(WAn) = max(x1 + 1, 0)
	I(RIn) = max(x1, 0)
	I(write) = max(x2 - 23, 0)
	I(RAn) = max(x1 + 3, 0)
	I(sys_r) = max(x1 + x2 + 7, 0)
Number of SCCs: 2
  SCC { #1 #15 #20 #24 #26 #35..37 #39 #44 #45 #47 }
    POLO(Sum)... removes: #1 #15 #24 #26 #37 #39 #44 #45 #47
	I(# RAo) = max(x1 + 1, 0)
	I(sys_w) = max(x1 + x2 + 2, 0)
	I(# WAo) = max(x1 + 1, 0)
	I(RAo) = max(x1 + 3, 0)
	I(RIo) = max(x1, 0)
	I(read) = max(x1 + x2 - 10, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 1
	I(WAo) = max(x1 + 7, 0)
	I(# check) = max(x1 - 1, 0)
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(Ww) = 12
	I(WIo) = max(x1 + 13, 0)
	I(check) = max(x1 + 11, 0)
	I(ok) = max(x1 + 8, 0)
	I(Rw) = 14
	I(# top) = 0
	I(R) = 0
	I(WAn) = max(x1 + 2, 0)
	I(RIn) = max(x1, 0)
	I(write) = max(x2 - 14, 0)
	I(RAn) = max(x1 + 5, 0)
	I(sys_r) = max(x1 + x2 + 7, 0)
Number of SCCs: 2
  SCC { #20 #35 #36 }
    POLO(Sum)... removes: #35
	I(# RAo) = max(x1 + 1, 0)
	I(sys_w) = max(x1 + x2 + 2, 0)
	I(# WAo) = max(x1 + 1, 0)
	I(RAo) = max(x1 + 6, 0)
	I(RIo) = max(x1 + 2, 0)
	I(read) = max(x1 + x2 - 21, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 1
	I(WAo) = max(x1 + 16, 0)
	I(# check) = max(x1 - 1, 0)
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(Ww) = 12
	I(WIo) = max(x1 + 29, 0)
	I(check) = max(x1 + 26, 0)
	I(ok) = max(x1 + 17, 0)
	I(Rw) = 16
	I(# top) = 0
	I(R) = 0
	I(WAn) = max(x1 + 1, 0)
	I(RIn) = max(x1, 0)
	I(write) = max(x2 - 14, 0)
	I(RAn) = max(x1 + 8, 0)
	I(sys_r) = max(x1 + x2 + 15, 0)
Number of SCCs: 2
  SCC { #20 #36 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.