Input TRS:
    1: RAo(R()) -> R()
    2: RAn(R()) -> R()
    3: WAo(W()) -> W()
    4: WAn(W()) -> W()
    5: Rw() ->= RIn(Rw())
    6: Ww() ->= WIn(Ww())
    7: top(ok(sys_r(read(r,RIo(x)),write(W(),Ww())))) ->= top(check(sys_r(read(RAo(r),x),write(W(),Ww()))))
    8: top(ok(sys_w(read(r,RIo(x)),write(W(),Ww())))) ->= top(check(sys_w(read(RAo(r),x),write(W(),Ww()))))
    9: top(ok(sys_r(read(r,RIn(x)),write(W(),Ww())))) ->= top(check(sys_r(read(RAn(r),x),write(W(),Ww()))))
    10: top(ok(sys_w(read(r,RIn(x)),write(W(),Ww())))) ->= top(check(sys_w(read(RAn(r),x),write(W(),Ww()))))
    11: top(ok(sys_r(read(R(),Rw()),write(W(),WIn(y))))) ->= top(check(sys_r(read(R(),Rw()),write(WAn(W()),y))))
    12: top(ok(sys_w(read(R(),Rw()),write(W(),WIn(y))))) ->= top(check(sys_w(read(R(),Rw()),write(WAn(W()),y))))
    13: top(ok(sys_r(read(R(),Rw()),write(W(),WIo(y))))) ->= top(check(sys_r(read(R(),Rw()),write(WAo(W()),y))))
    14: top(ok(sys_w(read(R(),Rw()),write(W(),WIo(y))))) ->= top(check(sys_w(read(R(),Rw()),write(WAo(W()),y))))
    15: top(ok(sys_r(read(r,RIo(x)),write(W(),y)))) ->= top(check(sys_w(read(RAo(r),x),write(W(),y))))
    16: top(ok(sys_r(read(r,RIn(x)),write(W(),y)))) ->= top(check(sys_w(read(RAn(r),x),write(W(),y))))
    17: top(ok(sys_w(read(R(),x),write(W(),WIo(y))))) ->= top(check(sys_r(read(R(),x),write(WAo(W()),y))))
    18: top(ok(sys_w(read(R(),x),write(W(),WIn(y))))) ->= top(check(sys_r(read(R(),x),write(WAn(W()),y))))
    19: check(RIo(x)) ->= ok(RIo(x))
    20: check(RAo(x)) ->= RAo(check(x))
    21: check(RAn(x)) ->= RAn(check(x))
    22: check(WAo(x)) ->= WAo(check(x))
    23: check(WAn(x)) ->= WAn(check(x))
    24: check(RIo(x)) ->= RIo(check(x))
    25: check(RIn(x)) ->= RIn(check(x))
    26: check(WIo(x)) ->= WIo(check(x))
    27: check(WIn(x)) ->= WIn(check(x))
    28: check(sys_r(x,y)) ->= sys_r(check(x),y)
    29: check(sys_r(x,y)) ->= sys_r(x,check(y))
    30: check(sys_w(x,y)) ->= sys_w(check(x),y)
    31: check(sys_w(x,y)) ->= sys_w(x,check(y))
    32: RAo(ok(x)) ->= ok(RAo(x))
    33: RAn(ok(x)) ->= ok(RAn(x))
    34: WAo(ok(x)) ->= ok(WAo(x))
    35: WAn(ok(x)) ->= ok(WAn(x))
    36: RIn(ok(x)) ->= ok(RIn(x))
    37: WIo(ok(x)) ->= ok(WIo(x))
    38: WIn(ok(x)) ->= ok(WIn(x))
    39: sys_r(ok(x),y) ->= ok(sys_r(x,y))
    40: sys_r(x,ok(y)) ->= ok(sys_r(x,y))
    41: sys_w(ok(x),y) ->= ok(sys_w(x,y))
    42: sys_w(x,ok(y)) ->= ok(sys_w(x,y))
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 15 8 1 3 17 7 14 13
 sys_w(x1,x2)	weight: (/ 322081 32) + x2 + x1
   RAo(x1)	weight: (/ 1 32) + x1
   RIo(x1)	weight: (/ 1 16) + x1
  read(x1,x2)	weight: (/ 1 32) + x2 + x1
     W()	weight: (/ 1 32)
   WIn(x1)	weight: x1
   top(x1)	weight: x1
   WAo(x1)	weight: (/ 1 32) + x1
    Ww()	weight: (/ 1 32)
   WIo(x1)	weight: (/ 1 16) + x1
 check(x1)	weight: x1
    ok(x1)	weight: x1
    Rw()	weight: (/ 1 32)
     R()	weight: (/ 1 32)
   WAn(x1)	weight: x1
   RIn(x1)	weight: x1
 write(x1,x2)	weight: x2 + x1
   RAn(x1)	weight: x1
 sys_r(x1,x2)	weight: (/ 322081 32) + x2 + x1
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ...