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(system(r,W(),RIo(x),Ww(),p))) ->= top(check(system(RAo(r),W(),x,Ww(),p)))	[relative]
   e4: top(ok(system(r,W(),RIn(x),Ww(),p))) ->= top(check(system(RAn(r),W(),x,Ww(),p)))	[relative]
   e5: top(ok(system(R(),W(),Rw(),WIn(y),p))) ->= top(check(system(R(),WAn(W()),Rw(),y,p)))	[relative]
   e6: top(ok(system(R(),W(),Rw(),WIo(y),p))) ->= top(check(system(R(),WAo(W()),Rw(),y,p)))	[relative]
   e7: top(ok(system(r,W(),RIo(x),y,PR()))) ->= top(check(system(RAo(r),W(),x,y,PW())))	[relative]
   e8: top(ok(system(r,W(),RIn(x),y,PR()))) ->= top(check(system(RAn(r),W(),x,y,PW())))	[relative]
   e9: top(ok(system(R(),W(),x,WIo(y),PW()))) ->= top(check(system(R(),WAo(W()),x,y,PR())))	[relative]
   e10: top(ok(system(R(),W(),x,WIn(y),PW()))) ->= top(check(system(R(),WAn(W()),x,y,PR())))	[relative]
   e11: check(RIo(x)) ->= ok(RIo(x))	[relative]
   e12: check(RAo(x)) ->= RAo(check(x))	[relative]
   e13: check(RAn(x)) ->= RAn(check(x))	[relative]
   e14: check(WAo(x)) ->= WAo(check(x))	[relative]
   e15: check(WAn(x)) ->= WAn(check(x))	[relative]
   e16: check(RIo(x)) ->= RIo(check(x))	[relative]
   e17: check(RIn(x)) ->= RIn(check(x))	[relative]
   e18: check(WIo(x)) ->= WIo(check(x))	[relative]
   e19: check(WIn(x)) ->= WIn(check(x))	[relative]
   e20: check(system(v1,v2,v3,v4,v5)) ->= system(check(v1),v2,v3,v4,v5)	[relative]
   e21: check(system(v1,v2,v3,v4,v5)) ->= system(v1,check(v2),v3,v4,v5)	[relative]
   e22: check(system(v1,v2,v3,v4,v5)) ->= system(v1,v2,check(v3),v4,v5)	[relative]
   e23: check(system(v1,v2,v3,v4,v5)) ->= system(v1,v2,v3,check(v4),v5)	[relative]
   e24: check(system(v1,v2,v3,v4,v5)) ->= system(v1,v2,v3,v4,check(v5))	[relative]
   e25: RAo(ok(x)) ->= ok(RAo(x))	[relative]
   e26: RAn(ok(x)) ->= ok(RAn(x))	[relative]
   e27: WAo(ok(x)) ->= ok(WAo(x))	[relative]
   e28: WAn(ok(x)) ->= ok(WAn(x))	[relative]
   e29: RIo(ok(x)) ->= ok(RIo(x))	[relative]
   e30: RIn(ok(x)) ->= ok(RIn(x))	[relative]
   e31: WIo(ok(x)) ->= ok(WIo(x))	[relative]
   e32: WIn(ok(x)) ->= ok(WIn(x))	[relative]
   e33: system(ok(v1),v2,v3,v4,v5) ->= ok(system(v1,v2,v3,v4,v5))	[relative]
   e34: system(v1,ok(v2),v3,v4,v5) ->= ok(system(v1,v2,v3,v4,v5))	[relative]
   e35: system(v1,v2,ok(v3),v4,v5) ->= ok(system(v1,v2,v3,v4,v5))	[relative]
   e36: system(v1,v2,v3,ok(v4),v5) ->= ok(system(v1,v2,v3,v4,v5))	[relative]
   e37: system(v1,v2,v3,v4,ok(v5)) ->= ok(system(v1,v2,v3,v4,v5))	[relative]
Dependency Pairs:
   #1: # check(system(v1,v2,v3,v4,v5)) -> # check(v1)	[relative]
   #2: # top(ok(system(r,W(),RIo(x),y,PR()))) -> # top(check(system(RAo(r),W(),x,y,PW())))	[relative]
   #3: # top(ok(system(r,W(),RIo(x),y,PR()))) -> # check(system(RAo(r),W(),x,y,PW()))	[relative]
   #4: # top(ok(system(r,W(),RIo(x),y,PR()))) -> # RAo(r)	[relative]
   #5: # check(WAn(x)) -> # WAn(check(x))	[relative]
   #6: # check(WAn(x)) -> # check(x)	[relative]
   #7: # top(ok(system(R(),W(),x,WIo(y),PW()))) -> # top(check(system(R(),WAo(W()),x,y,PR())))	[relative]
   #8: # top(ok(system(R(),W(),x,WIo(y),PW()))) -> # check(system(R(),WAo(W()),x,y,PR()))	[relative]
   #9: # top(ok(system(R(),W(),x,WIo(y),PW()))) -> # WAo(W())	[relative]
   #10: # top(ok(system(R(),W(),x,WIn(y),PW()))) -> # top(check(system(R(),WAn(W()),x,y,PR())))	[relative]
   #11: # top(ok(system(R(),W(),x,WIn(y),PW()))) -> # check(system(R(),WAn(W()),x,y,PR()))	[relative]
   #12: # top(ok(system(R(),W(),x,WIn(y),PW()))) -> # WAn(W())	[relative]
   #13: # WAn(ok(x)) -> # WAn(x)	[relative]
   #14: # check(system(v1,v2,v3,v4,v5)) -> # check(v4)	[relative]
   #15: # WAo(ok(x)) -> # WAo(x)	[relative]
   #16: # top(ok(system(R(),W(),Rw(),WIo(y),p))) -> # top(check(system(R(),WAo(W()),Rw(),y,p)))	[relative]
   #17: # top(ok(system(R(),W(),Rw(),WIo(y),p))) -> # check(system(R(),WAo(W()),Rw(),y,p))	[relative]
   #18: # top(ok(system(R(),W(),Rw(),WIo(y),p))) -> # WAo(W())	[relative]
   #19: # check(RIn(x)) -> # check(x)	[relative]
   #20: # top(ok(system(R(),W(),Rw(),WIn(y),p))) -> # top(check(system(R(),WAn(W()),Rw(),y,p)))	[relative]
   #21: # top(ok(system(R(),W(),Rw(),WIn(y),p))) -> # check(system(R(),WAn(W()),Rw(),y,p))	[relative]
   #22: # top(ok(system(R(),W(),Rw(),WIn(y),p))) -> # WAn(W())	[relative]
   #23: # check(RAn(x)) -> # RAn(check(x))	[relative]
   #24: # check(RAn(x)) -> # check(x)	[relative]
   #25: # RAn(ok(x)) -> # RAn(x)	[relative]
   #26: # top(ok(system(r,W(),RIn(x),y,PR()))) -> # top(check(system(RAn(r),W(),x,y,PW())))	[relative]
   #27: # top(ok(system(r,W(),RIn(x),y,PR()))) -> # check(system(RAn(r),W(),x,y,PW()))	[relative]
   #28: # top(ok(system(r,W(),RIn(x),y,PR()))) -> # RAn(r)	[relative]
   #29: # check(system(v1,v2,v3,v4,v5)) -> # check(v3)	[relative]
   #30: # RAo(ok(x)) -> # RAo(x)	[relative]
   #31: # check(WIo(x)) -> # check(x)	[relative]
   #32: # check(system(v1,v2,v3,v4,v5)) -> # check(v5)	[relative]
   #33: # top(ok(system(r,W(),RIo(x),Ww(),p))) -> # top(check(system(RAo(r),W(),x,Ww(),p)))	[relative]
   #34: # top(ok(system(r,W(),RIo(x),Ww(),p))) -> # check(system(RAo(r),W(),x,Ww(),p))	[relative]
   #35: # top(ok(system(r,W(),RIo(x),Ww(),p))) -> # RAo(r)	[relative]
   #36: # check(WIn(x)) -> # check(x)	[relative]
   #37: # top(ok(system(r,W(),RIn(x),Ww(),p))) -> # top(check(system(RAn(r),W(),x,Ww(),p)))	[relative]
   #38: # top(ok(system(r,W(),RIn(x),Ww(),p))) -> # check(system(RAn(r),W(),x,Ww(),p))	[relative]
   #39: # top(ok(system(r,W(),RIn(x),Ww(),p))) -> # RAn(r)	[relative]
   #40: # check(WAo(x)) -> # WAo(check(x))	[relative]
   #41: # check(WAo(x)) -> # check(x)	[relative]
   #42: # check(RAo(x)) -> # RAo(check(x))	[relative]
   #43: # check(RAo(x)) -> # check(x)	[relative]
   #44: # check(system(v1,v2,v3,v4,v5)) -> # check(v2)	[relative]
   #45: # check(RIo(x)) -> # check(x)	[relative]
Number of SCCs: 6
  SCC { #13 }
    POLO(Sum)... removes: #13
	I(# RAo) = max(x1 - 1, 0)
	I(# WAo) = 0
	I(RAo) = max(x1 + 1, 0)
	I(RIo) = max(x1 + 1, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 0
	I(PR) = 1
	I(WAo) = max(x1 + 3, 0)
	I(# check) = 0
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = 0
	I(system) = max(x1 + x2 + x3 + x4 + x5 + 1, 0)
	I(Ww) = 1
	I(WIo) = max(x1 + 3, 0)
	I(check) = max(x1 + 2, 0)
	I(ok) = max(x1 + 2, 0)
	I(Rw) = 1
	I(# top) = 0
	I(R) = 1
	I(WAn) = max(x1 + 1, 0)
	I(RIn) = max(x1, 0)
	I(PW) = 1
	I(RAn) = max(x1 + 1, 0)
Number of SCCs: 5
  SCC { #25 }
    POLO(Sum)... removes: #25
	I(# RAo) = max(x1 - 1, 0)
	I(# WAo) = 0
	I(RAo) = max(x1 + 1, 0)
	I(RIo) = max(x1 + 1, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 0
	I(PR) = 1
	I(WAo) = max(x1 + 3, 0)
	I(# check) = 0
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(system) = max(x1 + x2 + x3 + x4 + x5 + 1, 0)
	I(Ww) = 1
	I(WIo) = max(x1 + 3, 0)
	I(check) = max(x1 + 2, 0)
	I(ok) = max(x1 + 2, 0)
	I(Rw) = 1
	I(# top) = 0
	I(R) = 1
	I(WAn) = max(x1 + 1, 0)
	I(RIn) = max(x1, 0)
	I(PW) = 1
	I(RAn) = max(x1 + 1, 0)
Number of SCCs: 4
  SCC { #15 }
    POLO(Sum)... removes: #15
	I(# RAo) = max(x1 - 1, 0)
	I(# WAo) = max(x1 + 1, 0)
	I(RAo) = max(x1 + 1, 0)
	I(RIo) = max(x1 + 1, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 0
	I(PR) = 1
	I(WAo) = max(x1 + 3, 0)
	I(# check) = 0
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(system) = max(x1 + x2 + x3 + x4 + x5 + 1, 0)
	I(Ww) = 1
	I(WIo) = max(x1 + 3, 0)
	I(check) = max(x1 + 2, 0)
	I(ok) = max(x1 + 2, 0)
	I(Rw) = 1
	I(# top) = 0
	I(R) = 1
	I(WAn) = max(x1 + 1, 0)
	I(RIn) = max(x1, 0)
	I(PW) = 1
	I(RAn) = max(x1 + 1, 0)
Number of SCCs: 3
  SCC { #30 }
    POLO(Sum)... removes: #30
	I(# RAo) = max(x1 - 1, 0)
	I(# WAo) = max(x1 + 1, 0)
	I(RAo) = max(x1 + 1, 0)
	I(RIo) = max(x1 + 1, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 0
	I(PR) = 1
	I(WAo) = max(x1 + 3, 0)
	I(# check) = 0
	I(# WAn) = max(x1 - 1, 0)
	I(# RAn) = max(x1 + 1, 0)
	I(system) = max(x1 + x2 + x3 + x4 + x5 + 1, 0)
	I(Ww) = 1
	I(WIo) = max(x1 + 3, 0)
	I(check) = max(x1 + 2, 0)
	I(ok) = max(x1 + 2, 0)
	I(Rw) = 1
	I(# top) = 0
	I(R) = 1
	I(WAn) = max(x1 + 1, 0)
	I(RIn) = max(x1, 0)
	I(PW) = 1
	I(RAn) = max(x1 + 1, 0)
Number of SCCs: 2
  SCC { #1 #6 #14 #19 #24 #29 #31 #32 #36 #41 #43..45 }
    POLO(Sum)... removes: #1 #6 #14 #24 #29 #31 #32 #41 #43 #44 #45
	I(# RAo) = max(x1 - 1, 0)
	I(# WAo) = max(x1 + 1, 0)
	I(RAo) = max(x1 + 2, 0)
	I(RIo) = max(x1 + 2, 0)
	I(W) = 1
	I(WIn) = max(x1, 0)
	I(top) = 0
	I(PR) = 1
	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(system) = max(x1 + x2 + x3 + x4 + x5 + 2, 0)
	I(Ww) = 1
	I(WIo) = max(x1 + 4, 0)
	I(check) = max(x1 + 3, 0)
	I(ok) = max(x1 + 3, 0)
	I(Rw) = 1
	I(# top) = 0
	I(R) = 1
	I(WAn) = max(x1 + 2, 0)
	I(RIn) = max(x1, 0)
	I(PW) = 1
	I(RAn) = max(x1 + 2, 0)
Number of SCCs: 2
  SCC { #19 #36 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.