Quantifiers and Powers

[philzook58]

I know that powers are a dicey thing to start playing with, but I was wondering if there is insight into what I can look at to understand why the first two queries do not work but the last one does. Logically, I believe they are all equivalent. Is a different solver being inferred perhaps?

from z3 import *
print(get_version_string())
x = Real("x")
s = Solver()
s.add(Not(ForAll([x], Implies(x >= 0, x**0.5 >= 0))))
print(s.check())

s = Solver()
s.add(Exists([x], Not(Implies(x >= 0, x**0.5 >= 0))))
print(s.check())

s = Solver()
s.add(Not(Implies(x >= 0, x**0.5 >= 0)))
print(s.check())

4.13.0
unknown
unknown
unsat