Gyroid sphere

Percentage Accurate: 47.0% → 89.3%

Time: 6.3s

Alternatives: 7

Speedup: 10.8×

Specification

Math

\[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

FPCore

(FPCore (x y z)
 :precision binary64
 (fmax
  (-
   (sqrt
    (+ (+ (pow (* x 30.0) 2.0) (pow (* y 30.0) 2.0)) (pow (* z 30.0) 2.0)))
   25.0)
  (-
   (fabs
    (+
     (+
      (* (sin (* x 30.0)) (cos (* y 30.0)))
      (* (sin (* y 30.0)) (cos (* z 30.0))))
     (* (sin (* z 30.0)) (cos (* x 30.0)))))
   0.2)))

C

double code(double x, double y, double z) {
	return fmax((sqrt(((pow((x * 30.0), 2.0) + pow((y * 30.0), 2.0)) + pow((z * 30.0), 2.0))) - 25.0), (fabs((((sin((x * 30.0)) * cos((y * 30.0))) + (sin((y * 30.0)) * cos((z * 30.0)))) + (sin((z * 30.0)) * cos((x * 30.0))))) - 0.2));
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = fmax((sqrt(((((x * 30.0d0) ** 2.0d0) + ((y * 30.0d0) ** 2.0d0)) + ((z * 30.0d0) ** 2.0d0))) - 25.0d0), (abs((((sin((x * 30.0d0)) * cos((y * 30.0d0))) + (sin((y * 30.0d0)) * cos((z * 30.0d0)))) + (sin((z * 30.0d0)) * cos((x * 30.0d0))))) - 0.2d0))
end function

Java

public static double code(double x, double y, double z) {
	return fmax((Math.sqrt(((Math.pow((x * 30.0), 2.0) + Math.pow((y * 30.0), 2.0)) + Math.pow((z * 30.0), 2.0))) - 25.0), (Math.abs((((Math.sin((x * 30.0)) * Math.cos((y * 30.0))) + (Math.sin((y * 30.0)) * Math.cos((z * 30.0)))) + (Math.sin((z * 30.0)) * Math.cos((x * 30.0))))) - 0.2));
}

Python

def code(x, y, z):
	return fmax((math.sqrt(((math.pow((x * 30.0), 2.0) + math.pow((y * 30.0), 2.0)) + math.pow((z * 30.0), 2.0))) - 25.0), (math.fabs((((math.sin((x * 30.0)) * math.cos((y * 30.0))) + (math.sin((y * 30.0)) * math.cos((z * 30.0)))) + (math.sin((z * 30.0)) * math.cos((x * 30.0))))) - 0.2))

Julia

function code(x, y, z)
	return fmax(Float64(sqrt(Float64(Float64((Float64(x * 30.0) ^ 2.0) + (Float64(y * 30.0) ^ 2.0)) + (Float64(z * 30.0) ^ 2.0))) - 25.0), Float64(abs(Float64(Float64(Float64(sin(Float64(x * 30.0)) * cos(Float64(y * 30.0))) + Float64(sin(Float64(y * 30.0)) * cos(Float64(z * 30.0)))) + Float64(sin(Float64(z * 30.0)) * cos(Float64(x * 30.0))))) - 0.2))
end

MATLAB

function tmp = code(x, y, z)
	tmp = max((sqrt(((((x * 30.0) ^ 2.0) + ((y * 30.0) ^ 2.0)) + ((z * 30.0) ^ 2.0))) - 25.0), (abs((((sin((x * 30.0)) * cos((y * 30.0))) + (sin((y * 30.0)) * cos((z * 30.0)))) + (sin((z * 30.0)) * cos((x * 30.0))))) - 0.2));
end

Wolfram

code[x_, y_, z_] := N[Max[N[(N[Sqrt[N[(N[(N[Power[N[(x * 30.0), $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[(y * 30.0), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision] + N[Power[N[(z * 30.0), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 25.0), $MachinePrecision], N[(N[Abs[N[(N[(N[(N[Sin[N[(x * 30.0), $MachinePrecision]], $MachinePrecision] * N[Cos[N[(y * 30.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] + N[(N[Sin[N[(y * 30.0), $MachinePrecision]], $MachinePrecision] * N[Cos[N[(z * 30.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sin[N[(z * 30.0), $MachinePrecision]], $MachinePrecision] * N[Cos[N[(x * 30.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]

Initial Program: 47.0% accurate, 1.0× speedup

Math

\[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

FPCore

(FPCore (x y z)
 :precision binary64
 (fmax
  (-
   (sqrt
    (+ (+ (pow (* x 30.0) 2.0) (pow (* y 30.0) 2.0)) (pow (* z 30.0) 2.0)))
   25.0)
  (-
   (fabs
    (+
     (+
      (* (sin (* x 30.0)) (cos (* y 30.0)))
      (* (sin (* y 30.0)) (cos (* z 30.0))))
     (* (sin (* z 30.0)) (cos (* x 30.0)))))
   0.2)))

C

double code(double x, double y, double z) {
	return fmax((sqrt(((pow((x * 30.0), 2.0) + pow((y * 30.0), 2.0)) + pow((z * 30.0), 2.0))) - 25.0), (fabs((((sin((x * 30.0)) * cos((y * 30.0))) + (sin((y * 30.0)) * cos((z * 30.0)))) + (sin((z * 30.0)) * cos((x * 30.0))))) - 0.2));
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = fmax((sqrt(((((x * 30.0d0) ** 2.0d0) + ((y * 30.0d0) ** 2.0d0)) + ((z * 30.0d0) ** 2.0d0))) - 25.0d0), (abs((((sin((x * 30.0d0)) * cos((y * 30.0d0))) + (sin((y * 30.0d0)) * cos((z * 30.0d0)))) + (sin((z * 30.0d0)) * cos((x * 30.0d0))))) - 0.2d0))
end function

Java

public static double code(double x, double y, double z) {
	return fmax((Math.sqrt(((Math.pow((x * 30.0), 2.0) + Math.pow((y * 30.0), 2.0)) + Math.pow((z * 30.0), 2.0))) - 25.0), (Math.abs((((Math.sin((x * 30.0)) * Math.cos((y * 30.0))) + (Math.sin((y * 30.0)) * Math.cos((z * 30.0)))) + (Math.sin((z * 30.0)) * Math.cos((x * 30.0))))) - 0.2));
}

Python

def code(x, y, z):
	return fmax((math.sqrt(((math.pow((x * 30.0), 2.0) + math.pow((y * 30.0), 2.0)) + math.pow((z * 30.0), 2.0))) - 25.0), (math.fabs((((math.sin((x * 30.0)) * math.cos((y * 30.0))) + (math.sin((y * 30.0)) * math.cos((z * 30.0)))) + (math.sin((z * 30.0)) * math.cos((x * 30.0))))) - 0.2))

Julia

function code(x, y, z)
	return fmax(Float64(sqrt(Float64(Float64((Float64(x * 30.0) ^ 2.0) + (Float64(y * 30.0) ^ 2.0)) + (Float64(z * 30.0) ^ 2.0))) - 25.0), Float64(abs(Float64(Float64(Float64(sin(Float64(x * 30.0)) * cos(Float64(y * 30.0))) + Float64(sin(Float64(y * 30.0)) * cos(Float64(z * 30.0)))) + Float64(sin(Float64(z * 30.0)) * cos(Float64(x * 30.0))))) - 0.2))
end

MATLAB

function tmp = code(x, y, z)
	tmp = max((sqrt(((((x * 30.0) ^ 2.0) + ((y * 30.0) ^ 2.0)) + ((z * 30.0) ^ 2.0))) - 25.0), (abs((((sin((x * 30.0)) * cos((y * 30.0))) + (sin((y * 30.0)) * cos((z * 30.0)))) + (sin((z * 30.0)) * cos((x * 30.0))))) - 0.2));
end

Wolfram

code[x_, y_, z_] := N[Max[N[(N[Sqrt[N[(N[(N[Power[N[(x * 30.0), $MachinePrecision], 2.0], $MachinePrecision] + N[Power[N[(y * 30.0), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision] + N[Power[N[(z * 30.0), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 25.0), $MachinePrecision], N[(N[Abs[N[(N[(N[(N[Sin[N[(x * 30.0), $MachinePrecision]], $MachinePrecision] * N[Cos[N[(y * 30.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] + N[(N[Sin[N[(y * 30.0), $MachinePrecision]], $MachinePrecision] * N[Cos[N[(z * 30.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sin[N[(z * 30.0), $MachinePrecision]], $MachinePrecision] * N[Cos[N[(x * 30.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]

Alternative 1: 89.3% accurate, 2.7× speedup

Math

\[\begin{array}{l} t_0 := \sin \left(30 \cdot z\right)\\ \mathbf{if}\;z \leq -125000:\\ \;\;\;\;\mathsf{max}\left(-30 \cdot z, \left|t\_0 + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|t\_0 + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\mathsf{fma}\left(-30, z, \pi \cdot 0.5\right)\right)\right)\right)\right| - 0.2\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (let* ((t_0 (sin (* 30.0 z))))
   (if (<= z -125000.0)
     (fmax
      (* -30.0 z)
      (- (fabs (+ t_0 (fma 30.0 x (* 30.0 (* y (cos (* 30.0 z))))))) 0.2))
     (fmax
      (* z (- 30.0 (* 25.0 (/ 1.0 z))))
      (-
       (fabs
        (+ t_0 (fma 30.0 x (* 30.0 (* y (sin (fma -30.0 z (* PI 0.5))))))))
       0.2)))))

C

double code(double x, double y, double z) {
	double t_0 = sin((30.0 * z));
	double tmp;
	if (z <= -125000.0) {
		tmp = fmax((-30.0 * z), (fabs((t_0 + fma(30.0, x, (30.0 * (y * cos((30.0 * z))))))) - 0.2));
	} else {
		tmp = fmax((z * (30.0 - (25.0 * (1.0 / z)))), (fabs((t_0 + fma(30.0, x, (30.0 * (y * sin(fma(-30.0, z, (((double) M_PI) * 0.5)))))))) - 0.2));
	}
	return tmp;
}

Julia

function code(x, y, z)
	t_0 = sin(Float64(30.0 * z))
	tmp = 0.0
	if (z <= -125000.0)
		tmp = fmax(Float64(-30.0 * z), Float64(abs(Float64(t_0 + fma(30.0, x, Float64(30.0 * Float64(y * cos(Float64(30.0 * z))))))) - 0.2));
	else
		tmp = fmax(Float64(z * Float64(30.0 - Float64(25.0 * Float64(1.0 / z)))), Float64(abs(Float64(t_0 + fma(30.0, x, Float64(30.0 * Float64(y * sin(fma(-30.0, z, Float64(pi * 0.5)))))))) - 0.2));
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[z, -125000.0], N[Max[N[(-30.0 * z), $MachinePrecision], N[(N[Abs[N[(t$95$0 + N[(30.0 * x + N[(30.0 * N[(y * N[Cos[N[(30.0 * z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], N[Max[N[(z * N[(30.0 - N[(25.0 * N[(1.0 / z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Abs[N[(t$95$0 + N[(30.0 * x + N[(30.0 * N[(y * N[Sin[N[(-30.0 * z + N[(Pi * 0.5), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]]]

Derivation

1. Split input into 2 regimes

2. if z < -125000

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \left(30 \cdot x + \color{blue}{30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)}\right)\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 75.9

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   10. Applied rewrites 75.9%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x}, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   11. Taylor expanded in z around -inf

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-*.f64 63.3

          \[\leadsto \mathsf{max}\left(-30 \cdot \color{blue}{z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   13. Applied rewrites 63.3%

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   if -125000 < z

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \left(30 \cdot x + \color{blue}{30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)}\right)\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 75.9

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   10. Applied rewrites 75.9%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x}, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]
   11. Step-by-step derivation

       1. lift-cos.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

       2. cos-neg-rev N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(\mathsf{neg}\left(30 \cdot z\right)\right)\right)\right)\right| - \frac{1}{5}\right) \]

       3. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(\mathsf{neg}\left(30 \cdot z\right)\right)\right)\right)\right| - \frac{1}{5}\right) \]

       4. *-commutative N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(\mathsf{neg}\left(z \cdot 30\right)\right)\right)\right)\right| - \frac{1}{5}\right) \]

       5. sin-+PI/2-rev N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\left(\mathsf{neg}\left(z \cdot 30\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right)\right| - \frac{1}{5}\right) \]

       6. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\left(\mathsf{neg}\left(z \cdot 30\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right)\right| - \frac{1}{5}\right) \]

       7. *-commutative N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\left(\mathsf{neg}\left(30 \cdot z\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right)\right| - \frac{1}{5}\right) \]

       8. distribute-lft-neg-in N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\left(\mathsf{neg}\left(30\right)\right) \cdot z + \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right)\right| - \frac{1}{5}\right) \]

       9. lower-fma.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\mathsf{fma}\left(\mathsf{neg}\left(30\right), z, \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right)\right)\right| - \frac{1}{5}\right) \]

       10. metadata-eval N/A

           \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\mathsf{fma}\left(-30, z, \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right)\right)\right| - \frac{1}{5}\right) \]

       11. mult-flip N/A

           \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\mathsf{fma}\left(-30, z, \mathsf{PI}\left(\right) \cdot \frac{1}{2}\right)\right)\right)\right)\right| - \frac{1}{5}\right) \]

       12. metadata-eval N/A

           \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\mathsf{fma}\left(-30, z, \mathsf{PI}\left(\right) \cdot \frac{1}{2}\right)\right)\right)\right)\right| - \frac{1}{5}\right) \]

       13. lower-*.f64 N/A

           \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\mathsf{fma}\left(-30, z, \mathsf{PI}\left(\right) \cdot \frac{1}{2}\right)\right)\right)\right)\right| - \frac{1}{5}\right) \]

       14. lower-PI.f64 75.8

           \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\mathsf{fma}\left(-30, z, \pi \cdot 0.5\right)\right)\right)\right)\right| - 0.2\right) \]

   12. Applied rewrites 75.8%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \sin \left(\mathsf{fma}\left(-30, z, \pi \cdot 0.5\right)\right)\right)\right)\right| - 0.2\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 2: 89.3% accurate, 2.8× speedup

Math

\[\begin{array}{l} t_0 := \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\\ \mathbf{if}\;z \leq -125000:\\ \;\;\;\;\mathsf{max}\left(-30 \cdot z, t\_0\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), t\_0\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (let* ((t_0
         (-
          (fabs
           (+ (sin (* 30.0 z)) (fma 30.0 x (* 30.0 (* y (cos (* 30.0 z)))))))
          0.2)))
   (if (<= z -125000.0)
     (fmax (* -30.0 z) t_0)
     (fmax (* z (- 30.0 (* 25.0 (/ 1.0 z)))) t_0))))

C

double code(double x, double y, double z) {
	double t_0 = fabs((sin((30.0 * z)) + fma(30.0, x, (30.0 * (y * cos((30.0 * z))))))) - 0.2;
	double tmp;
	if (z <= -125000.0) {
		tmp = fmax((-30.0 * z), t_0);
	} else {
		tmp = fmax((z * (30.0 - (25.0 * (1.0 / z)))), t_0);
	}
	return tmp;
}

Julia

function code(x, y, z)
	t_0 = Float64(abs(Float64(sin(Float64(30.0 * z)) + fma(30.0, x, Float64(30.0 * Float64(y * cos(Float64(30.0 * z))))))) - 0.2)
	tmp = 0.0
	if (z <= -125000.0)
		tmp = fmax(Float64(-30.0 * z), t_0);
	else
		tmp = fmax(Float64(z * Float64(30.0 - Float64(25.0 * Float64(1.0 / z)))), t_0);
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[(N[Abs[N[(N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision] + N[(30.0 * x + N[(30.0 * N[(y * N[Cos[N[(30.0 * z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]}, If[LessEqual[z, -125000.0], N[Max[N[(-30.0 * z), $MachinePrecision], t$95$0], $MachinePrecision], N[Max[N[(z * N[(30.0 - N[(25.0 * N[(1.0 / z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$0], $MachinePrecision]]]

Derivation

1. Split input into 2 regimes

2. if z < -125000

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \left(30 \cdot x + \color{blue}{30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)}\right)\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 75.9

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   10. Applied rewrites 75.9%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x}, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   11. Taylor expanded in z around -inf

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-*.f64 63.3

          \[\leadsto \mathsf{max}\left(-30 \cdot \color{blue}{z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   13. Applied rewrites 63.3%

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   if -125000 < z

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \left(30 \cdot x + \color{blue}{30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)}\right)\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 75.9

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   10. Applied rewrites 75.9%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x}, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 3: 88.0% accurate, 3.0× speedup

Math

\[\begin{array}{l} t_0 := \sin \left(30 \cdot z\right)\\ \mathbf{if}\;z \leq -1.2 \cdot 10^{-5}:\\ \;\;\;\;\mathsf{max}\left(-30 \cdot z, \left|t\_0 + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right)\\ \mathbf{elif}\;z \leq 7.8 \cdot 10^{-22}:\\ \;\;\;\;\mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|t\_0 + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(\mathsf{fma}\left(z, 30, \frac{-25}{z} \cdot z\right), \left|t\_0 + 30 \cdot x\right| - 0.2\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (let* ((t_0 (sin (* 30.0 z))))
   (if (<= z -1.2e-5)
     (fmax
      (* -30.0 z)
      (- (fabs (+ t_0 (fma 30.0 x (* 30.0 (* y (cos (* 30.0 z))))))) 0.2))
     (if (<= z 7.8e-22)
       (fmax
        (* z (- 30.0 (* 25.0 (/ 1.0 z))))
        (-
         (fabs
          (+ t_0 (fma 30.0 x (fma -13500.0 (* y (pow z 2.0)) (* 30.0 y)))))
         0.2))
       (fmax
        (fma z 30.0 (* (/ -25.0 z) z))
        (- (fabs (+ t_0 (* 30.0 x))) 0.2))))))

C

double code(double x, double y, double z) {
	double t_0 = sin((30.0 * z));
	double tmp;
	if (z <= -1.2e-5) {
		tmp = fmax((-30.0 * z), (fabs((t_0 + fma(30.0, x, (30.0 * (y * cos((30.0 * z))))))) - 0.2));
	} else if (z <= 7.8e-22) {
		tmp = fmax((z * (30.0 - (25.0 * (1.0 / z)))), (fabs((t_0 + fma(30.0, x, fma(-13500.0, (y * pow(z, 2.0)), (30.0 * y))))) - 0.2));
	} else {
		tmp = fmax(fma(z, 30.0, ((-25.0 / z) * z)), (fabs((t_0 + (30.0 * x))) - 0.2));
	}
	return tmp;
}

Julia

function code(x, y, z)
	t_0 = sin(Float64(30.0 * z))
	tmp = 0.0
	if (z <= -1.2e-5)
		tmp = fmax(Float64(-30.0 * z), Float64(abs(Float64(t_0 + fma(30.0, x, Float64(30.0 * Float64(y * cos(Float64(30.0 * z))))))) - 0.2));
	elseif (z <= 7.8e-22)
		tmp = fmax(Float64(z * Float64(30.0 - Float64(25.0 * Float64(1.0 / z)))), Float64(abs(Float64(t_0 + fma(30.0, x, fma(-13500.0, Float64(y * (z ^ 2.0)), Float64(30.0 * y))))) - 0.2));
	else
		tmp = fmax(fma(z, 30.0, Float64(Float64(-25.0 / z) * z)), Float64(abs(Float64(t_0 + Float64(30.0 * x))) - 0.2));
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[z, -1.2e-5], N[Max[N[(-30.0 * z), $MachinePrecision], N[(N[Abs[N[(t$95$0 + N[(30.0 * x + N[(30.0 * N[(y * N[Cos[N[(30.0 * z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], If[LessEqual[z, 7.8e-22], N[Max[N[(z * N[(30.0 - N[(25.0 * N[(1.0 / z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Abs[N[(t$95$0 + N[(30.0 * x + N[(-13500.0 * N[(y * N[Power[z, 2.0], $MachinePrecision]), $MachinePrecision] + N[(30.0 * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], N[Max[N[(z * 30.0 + N[(N[(-25.0 / z), $MachinePrecision] * z), $MachinePrecision]), $MachinePrecision], N[(N[Abs[N[(t$95$0 + N[(30.0 * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]]]]

Derivation

1. Split input into 3 regimes

2. if z < -1.2e-5

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \left(30 \cdot x + \color{blue}{30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)}\right)\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 75.9

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   10. Applied rewrites 75.9%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x}, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   11. Taylor expanded in z around -inf

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-*.f64 63.3

          \[\leadsto \mathsf{max}\left(-30 \cdot \color{blue}{z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   13. Applied rewrites 63.3%

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot z}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   if -1.2e-5 < z < 7.79999999999999996e-22

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \left(30 \cdot x + \color{blue}{30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)}\right)\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 75.9

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   10. Applied rewrites 75.9%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x}, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   11. Taylor expanded in z around 0

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, -13500 \cdot \left(y \cdot {z}^{2}\right) + 30 \cdot y\right)\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-fma.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

       2. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

       3. lower-pow.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

       4. lower-*.f64 59.4

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - 0.2\right) \]

   13. Applied rewrites 59.4%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - 0.2\right) \]

   if 7.79999999999999996e-22 < z

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot \color{blue}{x}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 57.2

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   10. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]
   11. Step-by-step derivation

       1. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       2. lift--.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       3. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       4. fp-cancel-sub-sign-inv N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + \color{blue}{\left(\mathsf{neg}\left(25\right)\right) \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       5. metadata-eval N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + -25 \cdot \frac{\color{blue}{1}}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       6. lift-/.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + -25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       7. mult-flip N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + \frac{-25}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       8. lift-/.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + \frac{-25}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       9. distribute-rgt-out N/A

          \[\leadsto \mathsf{max}\left(30 \cdot z + \color{blue}{\frac{-25}{z} \cdot z}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       10. *-commutative N/A

           \[\leadsto \mathsf{max}\left(z \cdot 30 + \color{blue}{\frac{-25}{z}} \cdot z, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       11. lift-*.f64 N/A

           \[\leadsto \mathsf{max}\left(z \cdot 30 + \frac{-25}{z} \cdot \color{blue}{z}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       12. lift-fma.f64 57.2

           \[\leadsto \mathsf{max}\left(\mathsf{fma}\left(z, \color{blue}{30}, \frac{-25}{z} \cdot z\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   12. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(\mathsf{fma}\left(z, \color{blue}{30}, \frac{-25}{z} \cdot z\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 4: 87.4% accurate, 3.1× speedup

Math

\[\begin{array}{l} t_0 := \sin \left(30 \cdot z\right)\\ t_1 := \left|t\_0 + 30 \cdot x\right| - 0.2\\ t_2 := 25 \cdot \frac{1}{z}\\ \mathbf{if}\;z \leq -125000:\\ \;\;\;\;\mathsf{max}\left(-1 \cdot \left(z \cdot \left(30 + t\_2\right)\right), t\_1\right)\\ \mathbf{elif}\;z \leq 7.8 \cdot 10^{-22}:\\ \;\;\;\;\mathsf{max}\left(z \cdot \left(30 - t\_2\right), \left|t\_0 + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(\mathsf{fma}\left(z, 30, \frac{-25}{z} \cdot z\right), t\_1\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (let* ((t_0 (sin (* 30.0 z)))
        (t_1 (- (fabs (+ t_0 (* 30.0 x))) 0.2))
        (t_2 (* 25.0 (/ 1.0 z))))
   (if (<= z -125000.0)
     (fmax (* -1.0 (* z (+ 30.0 t_2))) t_1)
     (if (<= z 7.8e-22)
       (fmax
        (* z (- 30.0 t_2))
        (-
         (fabs
          (+ t_0 (fma 30.0 x (fma -13500.0 (* y (pow z 2.0)) (* 30.0 y)))))
         0.2))
       (fmax (fma z 30.0 (* (/ -25.0 z) z)) t_1)))))

C

double code(double x, double y, double z) {
	double t_0 = sin((30.0 * z));
	double t_1 = fabs((t_0 + (30.0 * x))) - 0.2;
	double t_2 = 25.0 * (1.0 / z);
	double tmp;
	if (z <= -125000.0) {
		tmp = fmax((-1.0 * (z * (30.0 + t_2))), t_1);
	} else if (z <= 7.8e-22) {
		tmp = fmax((z * (30.0 - t_2)), (fabs((t_0 + fma(30.0, x, fma(-13500.0, (y * pow(z, 2.0)), (30.0 * y))))) - 0.2));
	} else {
		tmp = fmax(fma(z, 30.0, ((-25.0 / z) * z)), t_1);
	}
	return tmp;
}

Julia

function code(x, y, z)
	t_0 = sin(Float64(30.0 * z))
	t_1 = Float64(abs(Float64(t_0 + Float64(30.0 * x))) - 0.2)
	t_2 = Float64(25.0 * Float64(1.0 / z))
	tmp = 0.0
	if (z <= -125000.0)
		tmp = fmax(Float64(-1.0 * Float64(z * Float64(30.0 + t_2))), t_1);
	elseif (z <= 7.8e-22)
		tmp = fmax(Float64(z * Float64(30.0 - t_2)), Float64(abs(Float64(t_0 + fma(30.0, x, fma(-13500.0, Float64(y * (z ^ 2.0)), Float64(30.0 * y))))) - 0.2));
	else
		tmp = fmax(fma(z, 30.0, Float64(Float64(-25.0 / z) * z)), t_1);
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[(N[Abs[N[(t$95$0 + N[(30.0 * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]}, Block[{t$95$2 = N[(25.0 * N[(1.0 / z), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[z, -125000.0], N[Max[N[(-1.0 * N[(z * N[(30.0 + t$95$2), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1], $MachinePrecision], If[LessEqual[z, 7.8e-22], N[Max[N[(z * N[(30.0 - t$95$2), $MachinePrecision]), $MachinePrecision], N[(N[Abs[N[(t$95$0 + N[(30.0 * x + N[(-13500.0 * N[(y * N[Power[z, 2.0], $MachinePrecision]), $MachinePrecision] + N[(30.0 * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], N[Max[N[(z * 30.0 + N[(N[(-25.0 / z), $MachinePrecision] * z), $MachinePrecision]), $MachinePrecision], t$95$1], $MachinePrecision]]]]]]

Derivation

1. Split input into 3 regimes

2. if z < -125000

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot \color{blue}{x}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 57.2

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   10. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

   11. Taylor expanded in z around -inf

       \[\leadsto \mathsf{max}\left(\color{blue}{-1 \cdot \left(z \cdot \left(30 + 25 \cdot \frac{1}{z}\right)\right)}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(-1 \cdot \color{blue}{\left(z \cdot \left(30 + 25 \cdot \frac{1}{z}\right)\right)}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       2. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(-1 \cdot \left(z \cdot \color{blue}{\left(30 + 25 \cdot \frac{1}{z}\right)}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       3. lower-+.f64 N/A

          \[\leadsto \mathsf{max}\left(-1 \cdot \left(z \cdot \left(30 + \color{blue}{25 \cdot \frac{1}{z}}\right)\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       4. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(-1 \cdot \left(z \cdot \left(30 + 25 \cdot \color{blue}{\frac{1}{z}}\right)\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       5. lower-/.f64 57.0

          \[\leadsto \mathsf{max}\left(-1 \cdot \left(z \cdot \left(30 + 25 \cdot \frac{1}{\color{blue}{z}}\right)\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   13. Applied rewrites 57.0%

       \[\leadsto \mathsf{max}\left(\color{blue}{-1 \cdot \left(z \cdot \left(30 + 25 \cdot \frac{1}{z}\right)\right)}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   if -125000 < z < 7.79999999999999996e-22

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \left(30 \cdot x + \color{blue}{30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)}\right)\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 75.9

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   10. Applied rewrites 75.9%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x}, 30 \cdot \left(y \cdot \cos \left(30 \cdot z\right)\right)\right)\right| - 0.2\right) \]

   11. Taylor expanded in z around 0

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, -13500 \cdot \left(y \cdot {z}^{2}\right) + 30 \cdot y\right)\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-fma.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

       2. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

       3. lower-pow.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

       4. lower-*.f64 59.4

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - 0.2\right) \]

   13. Applied rewrites 59.4%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x, \mathsf{fma}\left(-13500, y \cdot {z}^{2}, 30 \cdot y\right)\right)\right| - 0.2\right) \]

   if 7.79999999999999996e-22 < z

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot \color{blue}{x}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 57.2

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   10. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]
   11. Step-by-step derivation

       1. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       2. lift--.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       3. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       4. fp-cancel-sub-sign-inv N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + \color{blue}{\left(\mathsf{neg}\left(25\right)\right) \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       5. metadata-eval N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + -25 \cdot \frac{\color{blue}{1}}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       6. lift-/.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + -25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       7. mult-flip N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + \frac{-25}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       8. lift-/.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 + \frac{-25}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       9. distribute-rgt-out N/A

          \[\leadsto \mathsf{max}\left(30 \cdot z + \color{blue}{\frac{-25}{z} \cdot z}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       10. *-commutative N/A

           \[\leadsto \mathsf{max}\left(z \cdot 30 + \color{blue}{\frac{-25}{z}} \cdot z, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       11. lift-*.f64 N/A

           \[\leadsto \mathsf{max}\left(z \cdot 30 + \frac{-25}{z} \cdot \color{blue}{z}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

       12. lift-fma.f64 57.2

           \[\leadsto \mathsf{max}\left(\mathsf{fma}\left(z, \color{blue}{30}, \frac{-25}{z} \cdot z\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   12. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(\mathsf{fma}\left(z, \color{blue}{30}, \frac{-25}{z} \cdot z\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 5: 84.7% accurate, 4.8× speedup

Math

\[\begin{array}{l} \mathbf{if}\;y \leq -2.4 \cdot 10^{+141}:\\ \;\;\;\;\mathsf{max}\left(-30 \cdot y, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right)\\ \mathbf{elif}\;y \leq 3.7 \cdot 10^{+105}:\\ \;\;\;\;\mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right)\right| - 0.2\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (if (<= y -2.4e+141)
   (fmax (* -30.0 y) (- (fabs (+ (sin (* 30.0 z)) (* 30.0 x))) 0.2))
   (if (<= y 3.7e+105)
     (fmax
      (* z (- 30.0 (* 25.0 (/ 1.0 z))))
      (- (fabs (fma 30.0 x (* 30.0 z))) 0.2))
     (fmax
      (* y (- 30.0 (* 25.0 (/ 1.0 y))))
      (- (fabs (sin (* 30.0 y))) 0.2)))))

C

double code(double x, double y, double z) {
	double tmp;
	if (y <= -2.4e+141) {
		tmp = fmax((-30.0 * y), (fabs((sin((30.0 * z)) + (30.0 * x))) - 0.2));
	} else if (y <= 3.7e+105) {
		tmp = fmax((z * (30.0 - (25.0 * (1.0 / z)))), (fabs(fma(30.0, x, (30.0 * z))) - 0.2));
	} else {
		tmp = fmax((y * (30.0 - (25.0 * (1.0 / y)))), (fabs(sin((30.0 * y))) - 0.2));
	}
	return tmp;
}

Julia

function code(x, y, z)
	tmp = 0.0
	if (y <= -2.4e+141)
		tmp = fmax(Float64(-30.0 * y), Float64(abs(Float64(sin(Float64(30.0 * z)) + Float64(30.0 * x))) - 0.2));
	elseif (y <= 3.7e+105)
		tmp = fmax(Float64(z * Float64(30.0 - Float64(25.0 * Float64(1.0 / z)))), Float64(abs(fma(30.0, x, Float64(30.0 * z))) - 0.2));
	else
		tmp = fmax(Float64(y * Float64(30.0 - Float64(25.0 * Float64(1.0 / y)))), Float64(abs(sin(Float64(30.0 * y))) - 0.2));
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := If[LessEqual[y, -2.4e+141], N[Max[N[(-30.0 * y), $MachinePrecision], N[(N[Abs[N[(N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision] + N[(30.0 * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], If[LessEqual[y, 3.7e+105], N[Max[N[(z * N[(30.0 - N[(25.0 * N[(1.0 / z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Abs[N[(30.0 * x + N[(30.0 * z), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], N[Max[N[(y * N[(30.0 - N[(25.0 * N[(1.0 / y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Abs[N[Sin[N[(30.0 * y), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]]]

Derivation

1. Split input into 3 regimes

2. if y < -2.39999999999999997e141

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot \color{blue}{x}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 57.2

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   10. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

   11. Taylor expanded in y around -inf

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot y}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-*.f64 45.1

          \[\leadsto \mathsf{max}\left(-30 \cdot \color{blue}{y}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   13. Applied rewrites 45.1%

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot y}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   if -2.39999999999999997e141 < y < 3.69999999999999985e105

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot \color{blue}{x}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 57.2

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   10. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

   11. Taylor expanded in z around 0

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|30 \cdot x + 30 \cdot \color{blue}{z}\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-fma.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - \frac{1}{5}\right) \]

       2. lower-*.f64 70.3

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right) \]

   13. Applied rewrites 70.3%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right) \]

   if 3.69999999999999985e105 < y

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in z around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot y\right) + \color{blue}{\cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot y\right) + \color{blue}{\cos \left(30 \cdot y\right)} \cdot \sin \left(30 \cdot x\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot y\right) + \cos \color{blue}{\left(30 \cdot y\right)} \cdot \sin \left(30 \cdot x\right)\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \color{blue}{\sin \left(30 \cdot x\right)}\right| - \frac{1}{5}\right) \]

      5. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \color{blue}{\left(30 \cdot x\right)}\right| - \frac{1}{5}\right) \]

      6. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(\color{blue}{30} \cdot x\right)\right| - \frac{1}{5}\right) \]

      7. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 46.6

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.6%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)}\right| - 0.2\right) \]

   5. Taylor expanded in y around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{y \cdot \left(30 - 25 \cdot \frac{1}{y}\right)}, \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(y \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{y}\right)}, \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(y \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{y}}\right), \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{y}}\right), \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 29.5

         \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{y}}\right), \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)\right| - 0.2\right) \]

   7. Applied rewrites 29.5%

      \[\leadsto \mathsf{max}\left(\color{blue}{y \cdot \left(30 - 25 \cdot \frac{1}{y}\right)}, \left|\sin \left(30 \cdot y\right) + \cos \left(30 \cdot y\right) \cdot \sin \left(30 \cdot x\right)\right| - 0.2\right) \]

   8. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right) + 30 \cdot \color{blue}{\left(x \cdot \cos \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right) + 30 \cdot \left(x \cdot \color{blue}{\cos \left(30 \cdot y\right)}\right)\right| - \frac{1}{5}\right) \]

      2. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right) + 30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right) + 30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 48.5

         \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right) + 30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   10. Applied rewrites 48.5%

       \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right) + 30 \cdot \color{blue}{\left(x \cdot \cos \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   11. Taylor expanded in x around 0

       \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right)\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right)\right| - \frac{1}{5}\right) \]

       2. lower-*.f64 28.4

          \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right)\right| - 0.2\right) \]

   13. Applied rewrites 28.4%

       \[\leadsto \mathsf{max}\left(y \cdot \left(30 - 25 \cdot \frac{1}{y}\right), \left|\sin \left(30 \cdot y\right)\right| - 0.2\right) \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 6: 78.3% accurate, 5.4× speedup

Math

\[\begin{array}{l} \mathbf{if}\;y \leq -2.4 \cdot 10^{+141}:\\ \;\;\;\;\mathsf{max}\left(-30 \cdot y, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (if (<= y -2.4e+141)
   (fmax (* -30.0 y) (- (fabs (+ (sin (* 30.0 z)) (* 30.0 x))) 0.2))
   (fmax
    (* z (- 30.0 (* 25.0 (/ 1.0 z))))
    (- (fabs (fma 30.0 x (* 30.0 z))) 0.2))))

C

double code(double x, double y, double z) {
	double tmp;
	if (y <= -2.4e+141) {
		tmp = fmax((-30.0 * y), (fabs((sin((30.0 * z)) + (30.0 * x))) - 0.2));
	} else {
		tmp = fmax((z * (30.0 - (25.0 * (1.0 / z)))), (fabs(fma(30.0, x, (30.0 * z))) - 0.2));
	}
	return tmp;
}

Julia

function code(x, y, z)
	tmp = 0.0
	if (y <= -2.4e+141)
		tmp = fmax(Float64(-30.0 * y), Float64(abs(Float64(sin(Float64(30.0 * z)) + Float64(30.0 * x))) - 0.2));
	else
		tmp = fmax(Float64(z * Float64(30.0 - Float64(25.0 * Float64(1.0 / z)))), Float64(abs(fma(30.0, x, Float64(30.0 * z))) - 0.2));
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := If[LessEqual[y, -2.4e+141], N[Max[N[(-30.0 * y), $MachinePrecision], N[(N[Abs[N[(N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision] + N[(30.0 * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], N[Max[N[(z * N[(30.0 - N[(25.0 * N[(1.0 / z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Abs[N[(30.0 * x + N[(30.0 * z), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if y < -2.39999999999999997e141

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot \color{blue}{x}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 57.2

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   10. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

   11. Taylor expanded in y around -inf

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot y}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-*.f64 45.1

          \[\leadsto \mathsf{max}\left(-30 \cdot \color{blue}{y}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   13. Applied rewrites 45.1%

       \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot y}, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   if -2.39999999999999997e141 < y

   1. Initial program 47.0%

      \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

   2. Taylor expanded in x around 0

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
   3. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-fma.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      6. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      7. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      9. lower-cos.f64 N/A

         \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      10. lower-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      12. lower-*.f64 46.5

          \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   4. Applied rewrites 46.5%

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      2. lower--.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

      4. lower-/.f64 50.0

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   7. Applied rewrites 50.0%

      \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

   8. Taylor expanded in y around 0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - \frac{1}{5}\right) \]
   9. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot \color{blue}{x}\right| - \frac{1}{5}\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 57.2

         \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

   10. Applied rewrites 57.2%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

   11. Taylor expanded in z around 0

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|30 \cdot x + 30 \cdot \color{blue}{z}\right| - \frac{1}{5}\right) \]
   12. Step-by-step derivation

       1. lower-fma.f64 N/A

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - \frac{1}{5}\right) \]

       2. lower-*.f64 70.3

          \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right) \]

   13. Applied rewrites 70.3%

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 7: 70.3% accurate, 10.8× speedup

Math

\[\mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right) \]

FPCore

(FPCore (x y z)
 :precision binary64
 (fmax
  (* z (- 30.0 (* 25.0 (/ 1.0 z))))
  (- (fabs (fma 30.0 x (* 30.0 z))) 0.2)))

C

double code(double x, double y, double z) {
	return fmax((z * (30.0 - (25.0 * (1.0 / z)))), (fabs(fma(30.0, x, (30.0 * z))) - 0.2));
}

Julia

function code(x, y, z)
	return fmax(Float64(z * Float64(30.0 - Float64(25.0 * Float64(1.0 / z)))), Float64(abs(fma(30.0, x, Float64(30.0 * z))) - 0.2))
end

Wolfram

code[x_, y_, z_] := N[Max[N[(z * N[(30.0 - N[(25.0 * N[(1.0 / z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[Abs[N[(30.0 * x + N[(30.0 * z), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]

Derivation

1. Initial program 47.0%

   \[\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\left(\sin \left(x \cdot 30\right) \cdot \cos \left(y \cdot 30\right) + \sin \left(y \cdot 30\right) \cdot \cos \left(z \cdot 30\right)\right) + \sin \left(z \cdot 30\right) \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \]

2. Taylor expanded in x around 0

   \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]
3. Step-by-step derivation

   1. lower-+.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \color{blue}{\left(30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - \frac{1}{5}\right) \]

   2. lower-sin.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30 \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right)} + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   3. lower-*.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \left(\color{blue}{30} \cdot \left(x \cdot \cos \left(30 \cdot y\right)\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   4. lower-fma.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, \color{blue}{x \cdot \cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   5. lower-*.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \color{blue}{\cos \left(30 \cdot y\right)}, \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   6. lower-cos.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   7. lower-*.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   8. lower-*.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   9. lower-cos.f64 N/A

      \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   10. lower-*.f64 N/A

       \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   11. lower-sin.f64 N/A

       \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   12. lower-*.f64 46.5

       \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

4. Applied rewrites 46.5%

   \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)}\right| - 0.2\right) \]

5. Taylor expanded in z around inf

   \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]
6. Step-by-step derivation

   1. lower-*.f64 N/A

      \[\leadsto \mathsf{max}\left(z \cdot \color{blue}{\left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   2. lower--.f64 N/A

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - \color{blue}{25 \cdot \frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   3. lower-*.f64 N/A

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \color{blue}{\frac{1}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - \frac{1}{5}\right) \]

   4. lower-/.f64 50.0

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{\color{blue}{z}}\right), \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

7. Applied rewrites 50.0%

   \[\leadsto \mathsf{max}\left(\color{blue}{z \cdot \left(30 - 25 \cdot \frac{1}{z}\right)}, \left|\sin \left(30 \cdot z\right) + \mathsf{fma}\left(30, x \cdot \cos \left(30 \cdot y\right), \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right)\right| - 0.2\right) \]

8. Taylor expanded in y around 0

   \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - \frac{1}{5}\right) \]
9. Step-by-step derivation

   1. lower-+.f64 N/A

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot \color{blue}{x}\right| - \frac{1}{5}\right) \]

   2. lower-sin.f64 N/A

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

   3. lower-*.f64 N/A

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

   4. lower-*.f64 57.2

      \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right) \]

10. Applied rewrites 57.2%

    \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

11. Taylor expanded in z around 0

    \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|30 \cdot x + 30 \cdot \color{blue}{z}\right| - \frac{1}{5}\right) \]
12. Step-by-step derivation

    1. lower-fma.f64 N/A

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - \frac{1}{5}\right) \]

    2. lower-*.f64 70.3

       \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right) \]

13. Applied rewrites 70.3%

    \[\leadsto \mathsf{max}\left(z \cdot \left(30 - 25 \cdot \frac{1}{z}\right), \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right) \]
14. Add Preprocessing

Reproduce

herbie shell --seed 2025167 
(FPCore (x y z)
  :name "Gyroid sphere"
  :precision binary64
  (fmax (- (sqrt (+ (+ (pow (* x 30.0) 2.0) (pow (* y 30.0) 2.0)) (pow (* z 30.0) 2.0))) 25.0) (- (fabs (+ (+ (* (sin (* x 30.0)) (cos (* y 30.0))) (* (sin (* y 30.0)) (cos (* z 30.0)))) (* (sin (* z 30.0)) (cos (* x 30.0))))) 0.2)))