MAYBE

'Pop* with parameter subtitution (timeout of 60.0 seconds)'
-----------------------------------------------------------
Answer:           MAYBE
Input Problem:    innermost relative runtime-complexity with respect to
  Strict Rules:
    {  top(ok(left(car(x, y), z))) -> top(check(right(y, z)))
     , top(ok(right(x, car(y, z)))) -> top(check(left(x, z)))
     , top(ok(left(bot(), x))) -> top(check(right(bot(), x)))
     , top(ok(right(x, bot()))) -> top(check(left(x, bot())))}
  Weak Rules:
    {  top(ok(left(car(x, y), z))) -> top(check(left(y, z)))
     , top(ok(right(x, car(y, z)))) -> top(check(right(x, z)))
     , bot() -> car(new(), bot())
     , check(old()) -> ok(old())
     , check(car(x, y)) -> car(check(x), y)
     , check(car(x, y)) -> car(x, check(y))
     , check(left(x, y)) -> left(check(x), y)
     , check(left(x, y)) -> left(x, check(y))
     , check(right(x, y)) -> right(check(x), y)
     , check(right(x, y)) -> right(x, check(y))
     , car(ok(x), y) -> ok(car(x, y))
     , car(x, ok(y)) -> ok(car(x, y))
     , left(ok(x), y) -> ok(left(x, y))
     , left(x, ok(y)) -> ok(left(x, y))
     , right(ok(x), y) -> ok(right(x, y))
     , right(x, ok(y)) -> ok(right(x, y))}

Proof Output:    
  The input cannot be shown compatible