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]
Number of Rules: 4
Direct POLO(Sum) ... removes: 1 3 e7 e9 e6 e3
	I(RAo) = x1 + 1
	I(RIo) = x1 + 2
	I(W) = 0
	I(top) = x1
	I(WIn) = x1
	I(PR) = 0
	I(WAo) = x1 + 1
	I(system) = x1 + x2 + x3 + x4 + x5
	I(Ww) = 0
	I(WIo) = x1 + 2
	I(check) = x1
	I(ok) = x1
	I(Rw) = 0
	I(R) = 0
	I(WAn) = x1
	I(RIn) = x1
	I(PW) = 0
	I(RAn) = x1
Number of Rules: 2
Direct POLO(Sum) ...Direct Mat2b ... failed.
Dependency Pairs:
   #1: # check(RAn(x)) -> # RAn(check(x))	[relative]
   #2: # check(RAn(x)) -> # check(x)	[relative]
   #3: # check(system(v1,v2,v3,v4,v5)) -> # check(v5)	[relative]
   #4: # top(ok(system(R(),W(),x,WIn(y),PW()))) -> # top(check(system(R(),WAn(W()),x,y,PR())))	[relative]
   #5: # top(ok(system(R(),W(),x,WIn(y),PW()))) -> # check(system(R(),WAn(W()),x,y,PR()))	[relative]
   #6: # top(ok(system(R(),W(),x,WIn(y),PW()))) -> # WAn(W())	[relative]
   #7: # check(system(v1,v2,v3,v4,v5)) -> # check(v2)	[relative]
   #8: # check(system(v1,v2,v3,v4,v5)) -> # check(v1)	[relative]
   #9: # check(WAo(x)) -> # check(x)	[relative]
   #10: # check(RIo(x)) -> # check(x)	[relative]
   #11: # check(WIn(x)) -> # check(x)	[relative]
   #12: # check(RAo(x)) -> # check(x)	[relative]
   #13: # check(WAn(x)) -> # WAn(check(x))	[relative]
   #14: # check(WAn(x)) -> # check(x)	[relative]
   #15: # top(ok(system(r,W(),RIn(x),y,PR()))) -> # top(check(system(RAn(r),W(),x,y,PW())))	[relative]
   #16: # top(ok(system(r,W(),RIn(x),y,PR()))) -> # check(system(RAn(r),W(),x,y,PW()))	[relative]
   #17: # top(ok(system(r,W(),RIn(x),y,PR()))) -> # RAn(r)	[relative]
   #18: # check(system(v1,v2,v3,v4,v5)) -> # check(v3)	[relative]
   #19: # check(system(v1,v2,v3,v4,v5)) -> # check(v4)	[relative]
   #20: # check(RIn(x)) -> # check(x)	[relative]
   #21: # check(WIo(x)) -> # check(x)	[relative]
   #22: # top(ok(system(r,W(),RIn(x),Ww(),p))) -> # top(check(system(RAn(r),W(),x,Ww(),p)))	[relative]
   #23: # top(ok(system(r,W(),RIn(x),Ww(),p))) -> # check(system(RAn(r),W(),x,Ww(),p))	[relative]
   #24: # top(ok(system(r,W(),RIn(x),Ww(),p))) -> # RAn(r)	[relative]
   #25: # RAn(ok(x)) -> # RAn(x)	[relative]
   #26: # top(ok(system(R(),W(),Rw(),WIn(y),p))) -> # top(check(system(R(),WAn(W()),Rw(),y,p)))	[relative]
   #27: # top(ok(system(R(),W(),Rw(),WIn(y),p))) -> # check(system(R(),WAn(W()),Rw(),y,p))	[relative]
   #28: # top(ok(system(R(),W(),Rw(),WIn(y),p))) -> # WAn(W())	[relative]
   #29: # WAn(ok(x)) -> # WAn(x)	[relative]
Number of SCCs: 4
  SCC { #25 }
    POLO(Sum)... removes: #25
	I(RAo) = max(x1, 0)
	I(RIo) = max(x1 + 1, 0)
	I(W) = 0
	I(WIn) = max(x1, 0)
	I(top) = 0
	I(PR) = 1
	I(WAo) = max(x1, 0)
	I(# check) = max(x1 - 1, 0)
	I(# WAn) = 0
	I(# RAn) = max(x1 - 2, 0)
	I(system) = max(x1 + x2 + x3 + x4 + x5, 0)
	I(Ww) = 0
	I(WIo) = max(x1, 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 + 4, 0)
	I(RIn) = max(x1, 0)
	I(PW) = 1
	I(RAn) = max(x1 + 2, 0)
Number of SCCs: 3
  SCC { #29 }
    POLO(Sum)... removes: #29
	I(RAo) = max(x1, 0)
	I(RIo) = max(x1 + 1, 0)
	I(W) = 0
	I(WIn) = max(x1, 0)
	I(top) = 0
	I(PR) = 1
	I(WAo) = max(x1, 0)
	I(# check) = max(x1 - 1, 0)
	I(# WAn) = max(x1 + 1, 0)
	I(# RAn) = max(x1 - 2, 0)
	I(system) = max(x1 + x2 + x3 + x4 + x5, 0)
	I(Ww) = 0
	I(WIo) = max(x1, 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 + 4, 0)
	I(RIn) = max(x1, 0)
	I(PW) = 1
	I(RAn) = max(x1 + 2, 0)
Number of SCCs: 2
  SCC { #4 #15 #22 #26 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.