from dreal import * # pip3 install dreal.
x = Variable("x")
# To use dReal, we flip the inequality and verify that the slope being less
# that mu is unsatisfiable (over the finite domain). I then found the largest
# mu that returns "none" (== unsatisfiable). Larger values provide a witness
# that can verify satisfiability.
mu = 0.175
result = CheckSatisfiability(
And(
Or(And(-1e6 <= x, x <= -1e-6), And(1e-6 <= x, x <= 1e6)),
0.5 * (2 * x + 6 * sin(x) * cos(x)) ** 2 <= mu * (x**2 + 3 * sin(x) ** 2),
),
1e-6,
)
print(result)