MAYBE 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: MAYBE Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { R(x, RT()) -> RT() , W(x, WT()) -> WT()} Weak Rules: { RB() -> R(New(), RB()) , WB() -> W(New(), WB()) , top(ok(sys(read(r1, R(t, r2)), write(WT(), WB()), p))) -> top(check(sys(read(R(t, r1), r2), write(WT(), WB()), p))) , top(ok(sys(read(RT(), RB()), write(WT(), W(t, w1)), p))) -> top(check(sys(read(RT(), RB()), write(W(t, WT()), w1), p))) , top(ok(sys(read(r1, R(t, r2)), write(WT(), w1), PR()))) -> top(check(sys(read(R(t, r1), r2), write(WT(), w1), PW()))) , top(ok(sys(read(RT(), r2), write(WT(), W(t, w1)), PW()))) -> top(check(sys(read(RT(), r2), write(W(t, WT()), w1), PR()))) , check(Old()) -> ok(Old()) , check(R(x, y)) -> R(check(x), y) , check(R(x, y)) -> R(x, check(y)) , check(W(x, y)) -> W(check(x), y) , check(W(x, y)) -> W(x, check(y)) , check(read(x, y)) -> read(check(x), y) , check(read(x, y)) -> read(x, check(y)) , check(write(x, y)) -> write(check(x), y) , check(write(x, y)) -> write(x, check(y)) , check(sys(x, y, z)) -> sys(check(x), y, z) , check(sys(x, y, z)) -> sys(x, check(y), z) , check(sys(x, y, z)) -> sys(x, y, check(z)) , R(ok(x), y) -> ok(R(x, y)) , R(x, ok(y)) -> ok(R(x, y)) , W(ok(x), y) -> ok(W(x, y)) , W(x, ok(y)) -> ok(W(x, y)) , read(ok(x), y) -> ok(read(x, y)) , read(x, ok(y)) -> ok(read(x, y)) , write(ok(x), y) -> ok(write(x, y)) , write(x, ok(y)) -> ok(write(x, y)) , sys(ok(x), y, z) -> ok(sys(x, y, z)) , sys(x, ok(y), z) -> ok(sys(x, y, z)) , sys(x, y, ok(z)) -> ok(sys(x, y, z))} Proof Output: The input cannot be shown compatible