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]
Weak rule e8 calls a strict rule