(VAR p r v1 v2 v3 v4 v5 x y )
(RULES 
        RAo(R) -> R
        RAn(R) -> R
        WAo(W) -> W
        WAn(W) -> W
        Rw ->= RIn(Rw)
        Ww ->= WIn(Ww)
        top(ok(system(r,W,RIo(x),Ww,p))) ->= top(check(system(RAo(r),W,x,Ww,p)))
        top(ok(system(r,W,RIn(x),Ww,p))) ->= top(check(system(RAn(r),W,x,Ww,p)))
        top(ok(system(R,W,Rw,WIn(y),p))) ->= top(check(system(R,WAn(W),Rw,y,p)))
        top(ok(system(R,W,Rw,WIo(y),p))) ->= top(check(system(R,WAo(W),Rw,y,p)))
        top(ok(system(r,W,RIo(x),y,PR))) ->= top(check(system(RAo(r),W,x,y,PW)))
        top(ok(system(r,W,RIn(x),y,PR))) ->= top(check(system(RAn(r),W,x,y,PW)))
        top(ok(system(R,W,x,WIo(y),PW))) ->= top(check(system(R,WAo(W),x,y,PR)))
        top(ok(system(R,W,x,WIn(y),PW))) ->= top(check(system(R,WAn(W),x,y,PR)))
        check(RIo(x)) ->= ok(RIo(x))
        check(RAo(x)) ->= RAo(check(x))
        check(RAn(x)) ->= RAn(check(x))
        check(WAo(x)) ->= WAo(check(x))
        check(WAn(x)) ->= WAn(check(x))
        check(RIo(x)) ->= RIo(check(x))
        check(RIn(x)) ->= RIn(check(x))
        check(WIo(x)) ->= WIo(check(x))
        check(WIn(x)) ->= WIn(check(x))
        check(system(v1,v2,v3,v4,v5)) ->= system(check(v1),v2,v3,v4,v5)
        check(system(v1,v2,v3,v4,v5)) ->= system(v1,check(v2),v3,v4,v5)
        check(system(v1,v2,v3,v4,v5)) ->= system(v1,v2,check(v3),v4,v5)
        check(system(v1,v2,v3,v4,v5)) ->= system(v1,v2,v3,check(v4),v5)
        check(system(v1,v2,v3,v4,v5)) ->= system(v1,v2,v3,v4,check(v5))
        RAo(ok(x)) ->= ok(RAo(x))
        RAn(ok(x)) ->= ok(RAn(x))
        WAo(ok(x)) ->= ok(WAo(x))
        WAn(ok(x)) ->= ok(WAn(x))
        RIo(ok(x)) ->= ok(RIo(x))
        RIn(ok(x)) ->= ok(RIn(x))
        WIo(ok(x)) ->= ok(WIo(x))
        WIn(ok(x)) ->= ok(WIn(x))
        system(ok(v1),v2,v3,v4,v5) ->= ok(system(v1,v2,v3,v4,v5))
        system(v1,ok(v2),v3,v4,v5) ->= ok(system(v1,v2,v3,v4,v5))
        system(v1,v2,ok(v3),v4,v5) ->= ok(system(v1,v2,v3,v4,v5))
        system(v1,v2,v3,ok(v4),v5) ->= ok(system(v1,v2,v3,v4,v5))
        system(v1,v2,v3,v4,ok(v5)) ->= ok(system(v1,v2,v3,v4,v5))
)