\[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U\]
\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U
(FPCore (J l K U)
 :precision binary64
 (+ (* (* J (- (exp l) (exp (- l)))) (cos (/ K 2.0))) U))
double code(double J, double l, double K, double U) {
	return ((J * (exp(l) - exp(-l))) * cos(K / 2.0)) + U;
}

Reproduce

Please include this information when filing a bug report:

herbie shell --seed 2021060 
(FPCore (J l K U)
  :name "Maksimov and Kolovsky, Equation (4)"
  :precision binary64
  (+ (* (* J (- (exp l) (exp (- l)))) (cos (/ K 2.0))) U))

Backtrace

Failed to produce proof for (*.f64 (exp.f64 (*.f64 1/3 (+.f64 (log.f64 l) (log.f64 (*.f64 (cos.f64 (*.f64 1/2 K)) J))))) (cbrt.f64 2)) to (*.f64 (cbrt.f64 (*.f64 l (*.f64 (cos.f64 (*.f64 1/2 K)) J))) (cbrt.f64 2))LC
(unnamed)/data/pavpan/nightlies/herbie/egg-generate-proof/src/core/simplify.rkt1496
egraph-add-exprs/data/pavpan/nightlies/herbie/egg-generate-proof/egg-herbie/main.rkt1540
with-egraph/data/pavpan/nightlies/herbie/egg-generate-proof/egg-herbie/main.rkt740
(unnamed)/data/pavpan/nightlies/herbie/egg-generate-proof/src/core/simplify.rkt790
simplify!/data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt2360
run-iter!/data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt3600
for-loop/data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt3912
run-improve/data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt3770
(unnamed)/data/pavpan/nightlies/herbie/egg-generate-proof/src/sandbox.rkt546
run/opt/racket-7.9/share/pkgs/profile-lib/main.rkt392
profile-thunk/opt/racket-7.9/share/pkgs/profile-lib/main.rkt90
(unnamed)/opt/racket-7.9/collects/racket/engine.rkt4224