Input TRS:
    1: R(x,RT()) -> RT()
    2: W(x,WT()) -> WT()
   e1: RB() ->= R(New(),RB())	[relative]
   e2: WB() ->= W(New(),WB())	[relative]
   e3: top(ok(sys(read(r1,R(t,r2)),write(WT(),WB()),p))) ->= top(check(sys(read(R(t,r1),r2),write(WT(),WB()),p)))	[relative]
   e4: top(ok(sys(read(RT(),RB()),write(WT(),W(t,w1)),p))) ->= top(check(sys(read(RT(),RB()),write(W(t,WT()),w1),p)))	[relative]
   e5: top(ok(sys(read(r1,R(t,r2)),write(WT(),w1),PR()))) ->= top(check(sys(read(R(t,r1),r2),write(WT(),w1),PW())))	[relative]
   e6: top(ok(sys(read(RT(),r2),write(WT(),W(t,w1)),PW()))) ->= top(check(sys(read(RT(),r2),write(W(t,WT()),w1),PR())))	[relative]
   e7: check(Old()) ->= ok(Old())	[relative]
   e8: check(R(x,y)) ->= R(check(x),y)	[relative]
   e9: check(R(x,y)) ->= R(x,check(y))	[relative]
   e10: check(W(x,y)) ->= W(check(x),y)	[relative]
   e11: check(W(x,y)) ->= W(x,check(y))	[relative]
   e12: check(read(x,y)) ->= read(check(x),y)	[relative]
   e13: check(read(x,y)) ->= read(x,check(y))	[relative]
   e14: check(write(x,y)) ->= write(check(x),y)	[relative]
   e15: check(write(x,y)) ->= write(x,check(y))	[relative]
   e16: check(sys(x,y,z)) ->= sys(check(x),y,z)	[relative]
   e17: check(sys(x,y,z)) ->= sys(x,check(y),z)	[relative]
   e18: check(sys(x,y,z)) ->= sys(x,y,check(z))	[relative]
   e19: R(ok(x),y) ->= ok(R(x,y))	[relative]
   e20: R(x,ok(y)) ->= ok(R(x,y))	[relative]
   e21: W(ok(x),y) ->= ok(W(x,y))	[relative]
   e22: W(x,ok(y)) ->= ok(W(x,y))	[relative]
   e23: read(ok(x),y) ->= ok(read(x,y))	[relative]
   e24: read(x,ok(y)) ->= ok(read(x,y))	[relative]
   e25: write(ok(x),y) ->= ok(write(x,y))	[relative]
   e26: write(x,ok(y)) ->= ok(write(x,y))	[relative]
   e27: sys(ok(x),y,z) ->= ok(sys(x,y,z))	[relative]
   e28: sys(x,ok(y),z) ->= ok(sys(x,y,z))	[relative]
   e29: sys(x,y,ok(z)) ->= ok(sys(x,y,z))	[relative]
Number of Rules: 2
Direct POLO(Sum) ...Direct Mat2b ... failed.
Dependency Pairs:
   #1: # W(ok(x),y) -> # W(x,y)	[relative]
   #2: # check(R(x,y)) -> # R(x,check(y))	[relative]
   #3: # check(R(x,y)) -> # check(y)	[relative]
   #4: # check(read(x,y)) -> # check(y)	[relative]
   #5: # top(ok(sys(read(r1,R(t,r2)),write(WT(),w1),PR()))) -> # top(check(sys(read(R(t,r1),r2),write(WT(),w1),PW())))	[relative]
   #6: # top(ok(sys(read(r1,R(t,r2)),write(WT(),w1),PR()))) -> # check(sys(read(R(t,r1),r2),write(WT(),w1),PW()))	[relative]
   #7: # top(ok(sys(read(r1,R(t,r2)),write(WT(),w1),PR()))) -> # R(t,r1)	[relative]
   #8: # check(sys(x,y,z)) -> # check(x)	[relative]
   #9: # top(ok(sys(read(RT(),RB()),write(WT(),W(t,w1)),p))) -> # top(check(sys(read(RT(),RB()),write(W(t,WT()),w1),p)))	[relative]
   #10: # top(ok(sys(read(RT(),RB()),write(WT(),W(t,w1)),p))) -> # check(sys(read(RT(),RB()),write(W(t,WT()),w1),p))	[relative]
   #11: # top(ok(sys(read(RT(),RB()),write(WT(),W(t,w1)),p))) -> # W(t,WT())	[relative]
   #12: # check(W(x,y)) -> # W(x,check(y))	[relative]
   #13: # check(W(x,y)) -> # check(y)	[relative]
   #14: # W(x,ok(y)) -> # W(x,y)	[relative]
   #15: # check(R(x,y)) -> # R(check(x),y)	[relative]
   #16: # check(R(x,y)) -> # check(x)	[relative]
   #17: # check(read(x,y)) -> # check(x)	[relative]
   #18: # WB() -> # W(New(),WB())	[relative]
   #19: # WB() -> # WB()	[relative]
   #20: # check(write(x,y)) -> # check(x)	[relative]
   #21: # check(sys(x,y,z)) -> # check(y)	[relative]
   #22: # check(sys(x,y,z)) -> # check(z)	[relative]
   #23: # check(write(x,y)) -> # check(y)	[relative]
   #24: # RB() -> # R(New(),RB())	[relative]
   #25: # RB() -> # RB()	[relative]
   #26: # R(x,ok(y)) -> # R(x,y)	[relative]
   #27: # top(ok(sys(read(r1,R(t,r2)),write(WT(),WB()),p))) -> # top(check(sys(read(R(t,r1),r2),write(WT(),WB()),p)))	[relative]
   #28: # top(ok(sys(read(r1,R(t,r2)),write(WT(),WB()),p))) -> # check(sys(read(R(t,r1),r2),write(WT(),WB()),p))	[relative]
   #29: # top(ok(sys(read(r1,R(t,r2)),write(WT(),WB()),p))) -> # R(t,r1)	[relative]
   #30: # check(W(x,y)) -> # W(check(x),y)	[relative]
   #31: # check(W(x,y)) -> # check(x)	[relative]
   #32: # top(ok(sys(read(RT(),r2),write(WT(),W(t,w1)),PW()))) -> # top(check(sys(read(RT(),r2),write(W(t,WT()),w1),PR())))	[relative]
   #33: # top(ok(sys(read(RT(),r2),write(WT(),W(t,w1)),PW()))) -> # check(sys(read(RT(),r2),write(W(t,WT()),w1),PR()))	[relative]
   #34: # top(ok(sys(read(RT(),r2),write(WT(),W(t,w1)),PW()))) -> # W(t,WT())	[relative]
   #35: # R(ok(x),y) -> # R(x,y)	[relative]
Number of SCCs: 6
  SCC { #19 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.