MAYBE

'Pop* with parameter subtitution (timeout of 60.0 seconds)'
-----------------------------------------------------------
Answer:           MAYBE
Input Problem:    innermost relative runtime-complexity with respect to
  Strict Rules:
    {  RAo(R()) -> R()
     , RAn(R()) -> R()
     , WAo(W()) -> W()
     , WAn(W()) -> W()}
  Weak Rules:
    {  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))}

Proof Output:    
  The input cannot be shown compatible