MAYBE

'Pop* with parameter subtitution (timeout of 60.0 seconds)'
-----------------------------------------------------------
Answer:           MAYBE
Input Problem:    innermost relative runtime-complexity with respect to
  Strict Rules:
    {T(ok(sys(x, P(d, b), R(b), y))) ->
     T(check(sys(x, bot(), R(not(b)), y)))}
  Weak Rules:
    {  T(ok(sys(S(b, c(d, ds)), bot(), y, z))) ->
       T(check(sys(S(b, c(d, ds)), P(d, b), y, z)))
     , T(ok(sys(S(b, c(d, ds)), x, y, F(b)))) ->
       T(check(sys(S(not(b), ds), x, y, bot())))
     , T(ok(sys(x, y, R(b), bot()))) ->
       T(check(sys(x, y, R(b), F(not(b)))))
     , not(1()) -> 0()
     , not(0()) -> 1()
     , nils() -> c(new(), nils())
     , p(d, b) -> bot()
     , f(b) -> bot()
     , check(old()) -> ok(old())
     , check(f(v1)) -> f(check(v1))
     , f(ok(v1)) -> ok(f(v1))
     , check(p(v1, v2())) -> p(v1, check(v2()))
     , check(p(v1, v2())) -> p(check(v1), v2())
     , p(v1, ok(v2())) -> ok(p(v1, v2()))
     , p(ok(v1), v2()) -> ok(p(v1, v2()))
     , check(R(v1)) -> R(check(v1))
     , R(ok(v1)) -> ok(R(v1))
     , check(not(v1)) -> not(check(v1))
     , not(ok(v1)) -> ok(not(v1))
     , check(F(v1)) -> F(check(v1))
     , F(ok(v1)) -> ok(F(v1))
     , check(P(v1, v2())) -> P(v1, check(v2()))
     , check(P(v1, v2())) -> P(check(v1), v2())
     , P(v1, ok(v2())) -> ok(P(v1, v2()))
     , P(ok(v1), v2()) -> ok(P(v1, v2()))
     , check(c(v1, v2())) -> c(v1, check(v2()))
     , check(c(v1, v2())) -> c(check(v1), v2())
     , c(v1, ok(v2())) -> ok(c(v1, v2()))
     , c(ok(v1), v2()) -> ok(c(v1, v2()))
     , check(S(v1, v2())) -> S(v1, check(v2()))
     , check(S(v1, v2())) -> S(check(v1), v2())
     , S(v1, ok(v2())) -> ok(S(v1, v2()))
     , S(ok(v1), v2()) -> ok(S(v1, v2()))
     , check(sys(v1, v2(), v3(), v4)) -> sys(v1, v2(), v3(), check(v4))
     , check(sys(v1, v2(), v3(), v4)) -> sys(v1, v2(), check(v3()), v4)
     , check(sys(v1, v2(), v3(), v4)) -> sys(v1, check(v2()), v3(), v4)
     , check(sys(v1, v2(), v3(), v4)) -> sys(check(v1), v2(), v3(), v4)
     , sys(v1, v2(), v3(), ok(v4)) -> ok(sys(v1, v2(), v3(), v4))
     , sys(v1, v2(), ok(v3()), v4) -> ok(sys(v1, v2(), v3(), v4))
     , sys(v1, ok(v2()), v3(), v4) -> ok(sys(v1, v2(), v3(), v4))
     , sys(ok(v1), v2(), v3(), v4) -> ok(sys(v1, v2(), v3(), v4))}

Proof Output:    
  The input cannot be shown compatible