Gyroid sphere

Percentage Accurate: 35.9% → 99.4%

Time: 18.1s

Alternatives: 7

Speedup: 14.7×

• unsoundness detected in the egraph

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

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: 35.9% 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

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: 99.4% accurate, 0.5× speedup

Math

\[\begin{array}{l} t_0 := {\left(z \cdot 30\right)}^{2}\\ t_1 := {\left(y \cdot 30\right)}^{2}\\ \mathbf{if}\;\mathsf{max}\left(\sqrt{\left({\left(x \cdot 30\right)}^{2} + t\_1\right) + t\_0} - 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) \leq -0.1:\\ \;\;\;\;\mathsf{max}\left(\sqrt{\left({\left(0 \cdot 30\right)}^{2} + t\_1\right) + t\_0} - 25, \left|\sin \left(30 \cdot 0\right) + \frac{0.25 \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z - 0\right) \cdot 30\right)\right)\right) - \left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z + 0\right) \cdot 30\right)\right)\right)\right)}{\sin \left(-30 \cdot 0\right) \cdot \cos \left(-30 \cdot z\right)}\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)\right) - 25, \left|\sin \left(30 \cdot z\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right| - 0.2\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (let* ((t_0 (pow (* z 30.0) 2.0)) (t_1 (pow (* y 30.0) 2.0)))
  (if (<=
       (fmax
        (- (sqrt (+ (+ (pow (* x 30.0) 2.0) t_1) t_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))
       -0.1)
    (fmax
     (- (sqrt (+ (+ (pow (* 0.0 30.0) 2.0) t_1) t_0)) 25.0)
     (-
      (fabs
       (+
        (sin (* 30.0 0.0))
        (/
         (*
          0.25
          (-
           (- 0.5 (* 0.5 (cos (* 2.0 (* (- z 0.0) 30.0)))))
           (- 0.5 (* 0.5 (cos (* 2.0 (* (+ z 0.0) 30.0)))))))
         (* (sin (* -30.0 0.0)) (cos (* -30.0 z))))))
      0.2))
    (fmax
     (- (hypot (* z 30.0) (hypot (* y 30.0) (* 30.0 x))) 25.0)
     (-
      (fabs
       (+ (sin (* 30.0 z)) (* (cos (* 30.0 z)) (sin (* 30.0 y)))))
      0.2)))))

C

double code(double x, double y, double z) {
	double t_0 = pow((z * 30.0), 2.0);
	double t_1 = pow((y * 30.0), 2.0);
	double tmp;
	if (fmax((sqrt(((pow((x * 30.0), 2.0) + t_1) + t_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)) <= -0.1) {
		tmp = fmax((sqrt(((pow((0.0 * 30.0), 2.0) + t_1) + t_0)) - 25.0), (fabs((sin((30.0 * 0.0)) + ((0.25 * ((0.5 - (0.5 * cos((2.0 * ((z - 0.0) * 30.0))))) - (0.5 - (0.5 * cos((2.0 * ((z + 0.0) * 30.0))))))) / (sin((-30.0 * 0.0)) * cos((-30.0 * z)))))) - 0.2));
	} else {
		tmp = fmax((hypot((z * 30.0), hypot((y * 30.0), (30.0 * x))) - 25.0), (fabs((sin((30.0 * z)) + (cos((30.0 * z)) * sin((30.0 * y))))) - 0.2));
	}
	return tmp;
}

Java

public static double code(double x, double y, double z) {
	double t_0 = Math.pow((z * 30.0), 2.0);
	double t_1 = Math.pow((y * 30.0), 2.0);
	double tmp;
	if (fmax((Math.sqrt(((Math.pow((x * 30.0), 2.0) + t_1) + t_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)) <= -0.1) {
		tmp = fmax((Math.sqrt(((Math.pow((0.0 * 30.0), 2.0) + t_1) + t_0)) - 25.0), (Math.abs((Math.sin((30.0 * 0.0)) + ((0.25 * ((0.5 - (0.5 * Math.cos((2.0 * ((z - 0.0) * 30.0))))) - (0.5 - (0.5 * Math.cos((2.0 * ((z + 0.0) * 30.0))))))) / (Math.sin((-30.0 * 0.0)) * Math.cos((-30.0 * z)))))) - 0.2));
	} else {
		tmp = fmax((Math.hypot((z * 30.0), Math.hypot((y * 30.0), (30.0 * x))) - 25.0), (Math.abs((Math.sin((30.0 * z)) + (Math.cos((30.0 * z)) * Math.sin((30.0 * y))))) - 0.2));
	}
	return tmp;
}

Python

def code(x, y, z):
	t_0 = math.pow((z * 30.0), 2.0)
	t_1 = math.pow((y * 30.0), 2.0)
	tmp = 0
	if fmax((math.sqrt(((math.pow((x * 30.0), 2.0) + t_1) + t_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)) <= -0.1:
		tmp = fmax((math.sqrt(((math.pow((0.0 * 30.0), 2.0) + t_1) + t_0)) - 25.0), (math.fabs((math.sin((30.0 * 0.0)) + ((0.25 * ((0.5 - (0.5 * math.cos((2.0 * ((z - 0.0) * 30.0))))) - (0.5 - (0.5 * math.cos((2.0 * ((z + 0.0) * 30.0))))))) / (math.sin((-30.0 * 0.0)) * math.cos((-30.0 * z)))))) - 0.2))
	else:
		tmp = fmax((math.hypot((z * 30.0), math.hypot((y * 30.0), (30.0 * x))) - 25.0), (math.fabs((math.sin((30.0 * z)) + (math.cos((30.0 * z)) * math.sin((30.0 * y))))) - 0.2))
	return tmp

Julia

function code(x, y, z)
	t_0 = Float64(z * 30.0) ^ 2.0
	t_1 = Float64(y * 30.0) ^ 2.0
	tmp = 0.0
	if (fmax(Float64(sqrt(Float64(Float64((Float64(x * 30.0) ^ 2.0) + t_1) + t_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)) <= -0.1)
		tmp = fmax(Float64(sqrt(Float64(Float64((Float64(0.0 * 30.0) ^ 2.0) + t_1) + t_0)) - 25.0), Float64(abs(Float64(sin(Float64(30.0 * 0.0)) + Float64(Float64(0.25 * Float64(Float64(0.5 - Float64(0.5 * cos(Float64(2.0 * Float64(Float64(z - 0.0) * 30.0))))) - Float64(0.5 - Float64(0.5 * cos(Float64(2.0 * Float64(Float64(z + 0.0) * 30.0))))))) / Float64(sin(Float64(-30.0 * 0.0)) * cos(Float64(-30.0 * z)))))) - 0.2));
	else
		tmp = fmax(Float64(hypot(Float64(z * 30.0), hypot(Float64(y * 30.0), Float64(30.0 * x))) - 25.0), Float64(abs(Float64(sin(Float64(30.0 * z)) + Float64(cos(Float64(30.0 * z)) * sin(Float64(30.0 * y))))) - 0.2));
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z)
	t_0 = (z * 30.0) ^ 2.0;
	t_1 = (y * 30.0) ^ 2.0;
	tmp = 0.0;
	if (max((sqrt(((((x * 30.0) ^ 2.0) + t_1) + t_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)) <= -0.1)
		tmp = max((sqrt(((((0.0 * 30.0) ^ 2.0) + t_1) + t_0)) - 25.0), (abs((sin((30.0 * 0.0)) + ((0.25 * ((0.5 - (0.5 * cos((2.0 * ((z - 0.0) * 30.0))))) - (0.5 - (0.5 * cos((2.0 * ((z + 0.0) * 30.0))))))) / (sin((-30.0 * 0.0)) * cos((-30.0 * z)))))) - 0.2));
	else
		tmp = max((hypot((z * 30.0), hypot((y * 30.0), (30.0 * x))) - 25.0), (abs((sin((30.0 * z)) + (cos((30.0 * z)) * sin((30.0 * y))))) - 0.2));
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[Power[N[(z * 30.0), $MachinePrecision], 2.0], $MachinePrecision]}, Block[{t$95$1 = N[Power[N[(y * 30.0), $MachinePrecision], 2.0], $MachinePrecision]}, If[LessEqual[N[Max[N[(N[Sqrt[N[(N[(N[Power[N[(x * 30.0), $MachinePrecision], 2.0], $MachinePrecision] + t$95$1), $MachinePrecision] + t$95$0), $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], -0.1], N[Max[N[(N[Sqrt[N[(N[(N[Power[N[(0.0 * 30.0), $MachinePrecision], 2.0], $MachinePrecision] + t$95$1), $MachinePrecision] + t$95$0), $MachinePrecision]], $MachinePrecision] - 25.0), $MachinePrecision], N[(N[Abs[N[(N[Sin[N[(30.0 * 0.0), $MachinePrecision]], $MachinePrecision] + N[(N[(0.25 * N[(N[(0.5 - N[(0.5 * N[Cos[N[(2.0 * N[(N[(z - 0.0), $MachinePrecision] * 30.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(0.5 - N[(0.5 * N[Cos[N[(2.0 * N[(N[(z + 0.0), $MachinePrecision] * 30.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[Sin[N[(-30.0 * 0.0), $MachinePrecision]], $MachinePrecision] * N[Cos[N[(-30.0 * z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], N[Max[N[(N[Sqrt[N[(z * 30.0), $MachinePrecision] ^ 2 + N[Sqrt[N[(y * 30.0), $MachinePrecision] ^ 2 + N[(30.0 * x), $MachinePrecision] ^ 2], $MachinePrecision] ^ 2], $MachinePrecision] - 25.0), $MachinePrecision], N[(N[Abs[N[(N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision] + N[(N[Cos[N[(30.0 * z), $MachinePrecision]], $MachinePrecision] * N[Sin[N[(30.0 * y), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]]]]

Derivation

1. Split input into 2 regimes

2. if (fmax.f64 (-.f64 (sqrt.f64 (+.f64 (+.f64 (pow.f64 (*.f64 x #s(literal 30 binary64)) #s(literal 2 binary64)) (pow.f64 (*.f64 y #s(literal 30 binary64)) #s(literal 2 binary64))) (pow.f64 (*.f64 z #s(literal 30 binary64)) #s(literal 2 binary64)))) #s(literal 25 binary64)) (-.f64 (fabs.f64 (+.f64 (+.f64 (*.f64 (sin.f64 (*.f64 x #s(literal 30 binary64))) (cos.f64 (*.f64 y #s(literal 30 binary64)))) (*.f64 (sin.f64 (*.f64 y #s(literal 30 binary64))) (cos.f64 (*.f64 z #s(literal 30 binary64))))) (*.f64 (sin.f64 (*.f64 z #s(literal 30 binary64))) (cos.f64 (*.f64 x #s(literal 30 binary64)))))) #s(literal 1/5 binary64))) < -0.10000000000000001

   1. Initial program 35.9%

      \[\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 y 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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \color{blue}{\left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \color{blue}{\sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \color{blue}{\left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(\color{blue}{30} \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 35.9%

         \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - 0.2\right) \]

   4. Applied rewrites 35.9%

      \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\right) \]

   6. Applied rewrites 35.9%

      \[\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 x\right) + \frac{0.25 \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z - x\right) \cdot 30\right)\right)\right) - \left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z + x\right) \cdot 30\right)\right)\right)\right)}{\color{blue}{\sin \left(-30 \cdot x\right) \cdot \cos \left(-30 \cdot z\right)}}\right| - 0.2\right) \]

   7. Taylor expanded in undef-var around zero

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

   9. Applied rewrites 25.8%

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

   10. Taylor expanded in undef-var around zero

       \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(0 \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot 0\right) + \frac{0.25 \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z - x\right) \cdot 30\right)\right)\right) - \left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z + x\right) \cdot 30\right)\right)\right)\right)}{\sin \left(-30 \cdot x\right) \cdot \cos \left(-30 \cdot z\right)}\right| - 0.2\right) \]
   11. Step-by-step derivation

   12. Applied rewrites 25.4%

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

   13. Taylor expanded in undef-var around zero

       \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(0 \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot 0\right) + \frac{0.25 \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z - 0\right) \cdot 30\right)\right)\right) - \left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z + x\right) \cdot 30\right)\right)\right)\right)}{\sin \left(-30 \cdot x\right) \cdot \cos \left(-30 \cdot z\right)}\right| - 0.2\right) \]
   14. Step-by-step derivation

   15. Applied rewrites 25.6%

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

   16. Taylor expanded in undef-var around zero

       \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(0 \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot 0\right) + \frac{0.25 \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z - 0\right) \cdot 30\right)\right)\right) - \left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z + 0\right) \cdot 30\right)\right)\right)\right)}{\sin \left(-30 \cdot x\right) \cdot \cos \left(-30 \cdot z\right)}\right| - 0.2\right) \]
   17. Step-by-step derivation

   18. Applied rewrites 25.4%

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

   19. Taylor expanded in undef-var around zero

       \[\leadsto \mathsf{max}\left(\sqrt{\left({\left(0 \cdot 30\right)}^{2} + {\left(y \cdot 30\right)}^{2}\right) + {\left(z \cdot 30\right)}^{2}} - 25, \left|\sin \left(30 \cdot 0\right) + \frac{0.25 \cdot \left(\left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z - 0\right) \cdot 30\right)\right)\right) - \left(0.5 - 0.5 \cdot \cos \left(2 \cdot \left(\left(z + 0\right) \cdot 30\right)\right)\right)\right)}{\sin \left(-30 \cdot 0\right) \cdot \cos \left(-30 \cdot z\right)}\right| - 0.2\right) \]
   20. Step-by-step derivation

   21. Applied rewrites 35.8%

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

   if -0.10000000000000001 < (fmax.f64 (-.f64 (sqrt.f64 (+.f64 (+.f64 (pow.f64 (*.f64 x #s(literal 30 binary64)) #s(literal 2 binary64)) (pow.f64 (*.f64 y #s(literal 30 binary64)) #s(literal 2 binary64))) (pow.f64 (*.f64 z #s(literal 30 binary64)) #s(literal 2 binary64)))) #s(literal 25 binary64)) (-.f64 (fabs.f64 (+.f64 (+.f64 (*.f64 (sin.f64 (*.f64 x #s(literal 30 binary64))) (cos.f64 (*.f64 y #s(literal 30 binary64)))) (*.f64 (sin.f64 (*.f64 y #s(literal 30 binary64))) (cos.f64 (*.f64 z #s(literal 30 binary64))))) (*.f64 (sin.f64 (*.f64 z #s(literal 30 binary64))) (cos.f64 (*.f64 x #s(literal 30 binary64)))))) #s(literal 1/5 binary64)))

   1. Initial program 35.9%

      \[\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) \]

   3. Applied rewrites 49.3%

      \[\leadsto \mathsf{max}\left(\color{blue}{\mathsf{hypot}\left(z \cdot 30, \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right)} - 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) \]
   4. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      2. lift-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      3. *-commutative N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

      4. sqrt-prod N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      5. metadata-eval N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\color{blue}{900}}\right) - 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| - \frac{1}{5}\right) \]

      6. sqrt-unprod N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

      7. metadata-eval N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot \color{blue}{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      8. fabs-mul N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      9. *-commutative N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

      10. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

      11. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      12. sqr-neg-rev N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      13. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right|}}\right) - 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| - \frac{1}{5}\right) \]

      14. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      15. sqr-neg-rev N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      16. sqrt-unprod N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      17. rem-square-sqrt N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      18. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   5. Applied rewrites 89.2%

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)}\right) - 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) \]

   6. Taylor expanded in x around 0

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

      1. lower-+.f64 N/A

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

      2. lower-sin.f64 N/A

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

      3. lower-*.f64 N/A

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

      4. lower-*.f64 N/A

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

      5. lower-cos.f64 N/A

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

      6. lower-*.f64 N/A

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

      7. lower-sin.f64 N/A

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

      8. lower-*.f64 89.2%

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

   8. Applied rewrites 89.2%

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

Alternative 2: 93.6% accurate, 0.5× speedup

Math

\[\begin{array}{l} t_0 := \sin \left(30 \cdot \left(y - z\right)\right) \cdot 0.5\\ t_1 := \sin \left(30 \cdot \left(z + y\right)\right) \cdot 0.5\\ t_2 := \sin \left(30 \cdot z\right)\\ \mathbf{if}\;\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) \leq -0.1:\\ \;\;\;\;\mathsf{max}\left(-30 \cdot z - 25, \left|t\_2 + \frac{\frac{1}{{t\_0}^{-2}} - \frac{1}{{t\_1}^{-2}}}{t\_0 - t\_1}\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)\right) - 25, \left|t\_2 + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right| - 0.2\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (let* ((t_0 (* (sin (* 30.0 (- y z))) 0.5))
       (t_1 (* (sin (* 30.0 (+ z y))) 0.5))
       (t_2 (sin (* 30.0 z))))
  (if (<=
       (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))
       -0.1)
    (fmax
     (- (* -30.0 z) 25.0)
     (-
      (fabs
       (+
        t_2
        (/
         (- (/ 1.0 (pow t_0 -2.0)) (/ 1.0 (pow t_1 -2.0)))
         (- t_0 t_1))))
      0.2))
    (fmax
     (- (hypot (* z 30.0) (hypot (* y 30.0) (* 30.0 x))) 25.0)
     (- (fabs (+ t_2 (* (cos (* 30.0 z)) (sin (* 30.0 y))))) 0.2)))))

C

double code(double x, double y, double z) {
	double t_0 = sin((30.0 * (y - z))) * 0.5;
	double t_1 = sin((30.0 * (z + y))) * 0.5;
	double t_2 = sin((30.0 * z));
	double tmp;
	if (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)) <= -0.1) {
		tmp = fmax(((-30.0 * z) - 25.0), (fabs((t_2 + (((1.0 / pow(t_0, -2.0)) - (1.0 / pow(t_1, -2.0))) / (t_0 - t_1)))) - 0.2));
	} else {
		tmp = fmax((hypot((z * 30.0), hypot((y * 30.0), (30.0 * x))) - 25.0), (fabs((t_2 + (cos((30.0 * z)) * sin((30.0 * y))))) - 0.2));
	}
	return tmp;
}

Java

public static double code(double x, double y, double z) {
	double t_0 = Math.sin((30.0 * (y - z))) * 0.5;
	double t_1 = Math.sin((30.0 * (z + y))) * 0.5;
	double t_2 = Math.sin((30.0 * z));
	double tmp;
	if (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)) <= -0.1) {
		tmp = fmax(((-30.0 * z) - 25.0), (Math.abs((t_2 + (((1.0 / Math.pow(t_0, -2.0)) - (1.0 / Math.pow(t_1, -2.0))) / (t_0 - t_1)))) - 0.2));
	} else {
		tmp = fmax((Math.hypot((z * 30.0), Math.hypot((y * 30.0), (30.0 * x))) - 25.0), (Math.abs((t_2 + (Math.cos((30.0 * z)) * Math.sin((30.0 * y))))) - 0.2));
	}
	return tmp;
}

Python

def code(x, y, z):
	t_0 = math.sin((30.0 * (y - z))) * 0.5
	t_1 = math.sin((30.0 * (z + y))) * 0.5
	t_2 = math.sin((30.0 * z))
	tmp = 0
	if 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)) <= -0.1:
		tmp = fmax(((-30.0 * z) - 25.0), (math.fabs((t_2 + (((1.0 / math.pow(t_0, -2.0)) - (1.0 / math.pow(t_1, -2.0))) / (t_0 - t_1)))) - 0.2))
	else:
		tmp = fmax((math.hypot((z * 30.0), math.hypot((y * 30.0), (30.0 * x))) - 25.0), (math.fabs((t_2 + (math.cos((30.0 * z)) * math.sin((30.0 * y))))) - 0.2))
	return tmp

Julia

function code(x, y, z)
	t_0 = Float64(sin(Float64(30.0 * Float64(y - z))) * 0.5)
	t_1 = Float64(sin(Float64(30.0 * Float64(z + y))) * 0.5)
	t_2 = sin(Float64(30.0 * z))
	tmp = 0.0
	if (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)) <= -0.1)
		tmp = fmax(Float64(Float64(-30.0 * z) - 25.0), Float64(abs(Float64(t_2 + Float64(Float64(Float64(1.0 / (t_0 ^ -2.0)) - Float64(1.0 / (t_1 ^ -2.0))) / Float64(t_0 - t_1)))) - 0.2));
	else
		tmp = fmax(Float64(hypot(Float64(z * 30.0), hypot(Float64(y * 30.0), Float64(30.0 * x))) - 25.0), Float64(abs(Float64(t_2 + Float64(cos(Float64(30.0 * z)) * sin(Float64(30.0 * y))))) - 0.2));
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z)
	t_0 = sin((30.0 * (y - z))) * 0.5;
	t_1 = sin((30.0 * (z + y))) * 0.5;
	t_2 = sin((30.0 * z));
	tmp = 0.0;
	if (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)) <= -0.1)
		tmp = max(((-30.0 * z) - 25.0), (abs((t_2 + (((1.0 / (t_0 ^ -2.0)) - (1.0 / (t_1 ^ -2.0))) / (t_0 - t_1)))) - 0.2));
	else
		tmp = max((hypot((z * 30.0), hypot((y * 30.0), (30.0 * x))) - 25.0), (abs((t_2 + (cos((30.0 * z)) * sin((30.0 * y))))) - 0.2));
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[(N[Sin[N[(30.0 * N[(y - z), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * 0.5), $MachinePrecision]}, Block[{t$95$1 = N[(N[Sin[N[(30.0 * N[(z + y), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * 0.5), $MachinePrecision]}, Block[{t$95$2 = N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[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], -0.1], N[Max[N[(N[(-30.0 * z), $MachinePrecision] - 25.0), $MachinePrecision], N[(N[Abs[N[(t$95$2 + N[(N[(N[(1.0 / N[Power[t$95$0, -2.0], $MachinePrecision]), $MachinePrecision] - N[(1.0 / N[Power[t$95$1, -2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(t$95$0 - t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], N[Max[N[(N[Sqrt[N[(z * 30.0), $MachinePrecision] ^ 2 + N[Sqrt[N[(y * 30.0), $MachinePrecision] ^ 2 + N[(30.0 * x), $MachinePrecision] ^ 2], $MachinePrecision] ^ 2], $MachinePrecision] - 25.0), $MachinePrecision], N[(N[Abs[N[(t$95$2 + N[(N[Cos[N[(30.0 * z), $MachinePrecision]], $MachinePrecision] * N[Sin[N[(30.0 * y), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]]]]]

Derivation

1. Split input into 2 regimes

2. if (fmax.f64 (-.f64 (sqrt.f64 (+.f64 (+.f64 (pow.f64 (*.f64 x #s(literal 30 binary64)) #s(literal 2 binary64)) (pow.f64 (*.f64 y #s(literal 30 binary64)) #s(literal 2 binary64))) (pow.f64 (*.f64 z #s(literal 30 binary64)) #s(literal 2 binary64)))) #s(literal 25 binary64)) (-.f64 (fabs.f64 (+.f64 (+.f64 (*.f64 (sin.f64 (*.f64 x #s(literal 30 binary64))) (cos.f64 (*.f64 y #s(literal 30 binary64)))) (*.f64 (sin.f64 (*.f64 y #s(literal 30 binary64))) (cos.f64 (*.f64 z #s(literal 30 binary64))))) (*.f64 (sin.f64 (*.f64 z #s(literal 30 binary64))) (cos.f64 (*.f64 x #s(literal 30 binary64)))))) #s(literal 1/5 binary64))) < -0.10000000000000001

   1. Initial program 35.9%

      \[\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 -inf

      \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot z} - 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) \]
   3. Step-by-step derivation

      1. lower-*.f64 19.7%

         \[\leadsto \mathsf{max}\left(-30 \cdot \color{blue}{z} - 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) \]

   4. Applied rewrites 19.7%

      \[\leadsto \mathsf{max}\left(\color{blue}{-30 \cdot z} - 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) \]

   5. Taylor expanded in x around 0

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

      1. lower-+.f64 N/A

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

      2. lower-sin.f64 N/A

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

      3. lower-*.f64 N/A

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

      4. lower-*.f64 N/A

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

      5. lower-cos.f64 N/A

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

      6. lower-*.f64 N/A

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

      7. lower-sin.f64 N/A

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

      8. lower-*.f64 19.3%

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

   7. Applied rewrites 19.3%

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

   9. Applied rewrites 22.7%

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

   if -0.10000000000000001 < (fmax.f64 (-.f64 (sqrt.f64 (+.f64 (+.f64 (pow.f64 (*.f64 x #s(literal 30 binary64)) #s(literal 2 binary64)) (pow.f64 (*.f64 y #s(literal 30 binary64)) #s(literal 2 binary64))) (pow.f64 (*.f64 z #s(literal 30 binary64)) #s(literal 2 binary64)))) #s(literal 25 binary64)) (-.f64 (fabs.f64 (+.f64 (+.f64 (*.f64 (sin.f64 (*.f64 x #s(literal 30 binary64))) (cos.f64 (*.f64 y #s(literal 30 binary64)))) (*.f64 (sin.f64 (*.f64 y #s(literal 30 binary64))) (cos.f64 (*.f64 z #s(literal 30 binary64))))) (*.f64 (sin.f64 (*.f64 z #s(literal 30 binary64))) (cos.f64 (*.f64 x #s(literal 30 binary64)))))) #s(literal 1/5 binary64)))

   1. Initial program 35.9%

      \[\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) \]

   3. Applied rewrites 49.3%

      \[\leadsto \mathsf{max}\left(\color{blue}{\mathsf{hypot}\left(z \cdot 30, \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right)} - 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) \]
   4. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      2. lift-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      3. *-commutative N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

      4. sqrt-prod N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      5. metadata-eval N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\color{blue}{900}}\right) - 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| - \frac{1}{5}\right) \]

      6. sqrt-unprod N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

      7. metadata-eval N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot \color{blue}{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      8. fabs-mul N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      9. *-commutative N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

      10. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

      11. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      12. sqr-neg-rev N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      13. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right|}}\right) - 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| - \frac{1}{5}\right) \]

      14. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      15. sqr-neg-rev N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      16. sqrt-unprod N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      17. rem-square-sqrt N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      18. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   5. Applied rewrites 89.2%

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)}\right) - 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) \]

   6. Taylor expanded in x around 0

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

      1. lower-+.f64 N/A

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

      2. lower-sin.f64 N/A

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

      3. lower-*.f64 N/A

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

      4. lower-*.f64 N/A

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

      5. lower-cos.f64 N/A

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

      6. lower-*.f64 N/A

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

      7. lower-sin.f64 N/A

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

      8. lower-*.f64 89.2%

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

   8. Applied rewrites 89.2%

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

Alternative 3: 91.5% accurate, 0.6× speedup

Math

\[\begin{array}{l} t_0 := \sin \left(z \cdot 30\right)\\ \mathbf{if}\;\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) + t\_0 \cdot \cos \left(x \cdot 30\right)\right| - 0.2\right) \leq -0.1:\\ \;\;\;\;\mathsf{max}\left(-30 \cdot y - 25, \left|\frac{\mathsf{fma}\left(\left(x \cdot x\right) \cdot x, 27000, \left(\left(1 - \cos \left(z \cdot 60\right)\right) \cdot 0.5\right) \cdot t\_0\right)}{\mathsf{fma}\left(900 \cdot x, x, t\_0 \cdot \mathsf{fma}\left(-30, x, t\_0\right)\right)}\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)\right) - 25, \left|\sin \left(30 \cdot z\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)\right| - 0.2\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (let* ((t_0 (sin (* z 30.0))))
  (if (<=
       (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))))
           (* t_0 (cos (* x 30.0)))))
         0.2))
       -0.1)
    (fmax
     (- (* -30.0 y) 25.0)
     (-
      (fabs
       (/
        (fma
         (* (* x x) x)
         27000.0
         (* (* (- 1.0 (cos (* z 60.0))) 0.5) t_0))
        (fma (* 900.0 x) x (* t_0 (fma -30.0 x t_0)))))
      0.2))
    (fmax
     (- (hypot (* z 30.0) (hypot (* y 30.0) (* 30.0 x))) 25.0)
     (-
      (fabs
       (+ (sin (* 30.0 z)) (* (cos (* 30.0 z)) (sin (* 30.0 y)))))
      0.2)))))

C

double code(double x, double y, double z) {
	double t_0 = sin((z * 30.0));
	double tmp;
	if (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)))) + (t_0 * cos((x * 30.0))))) - 0.2)) <= -0.1) {
		tmp = fmax(((-30.0 * y) - 25.0), (fabs((fma(((x * x) * x), 27000.0, (((1.0 - cos((z * 60.0))) * 0.5) * t_0)) / fma((900.0 * x), x, (t_0 * fma(-30.0, x, t_0))))) - 0.2));
	} else {
		tmp = fmax((hypot((z * 30.0), hypot((y * 30.0), (30.0 * x))) - 25.0), (fabs((sin((30.0 * z)) + (cos((30.0 * z)) * sin((30.0 * y))))) - 0.2));
	}
	return tmp;
}

Julia

function code(x, y, z)
	t_0 = sin(Float64(z * 30.0))
	tmp = 0.0
	if (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(t_0 * cos(Float64(x * 30.0))))) - 0.2)) <= -0.1)
		tmp = fmax(Float64(Float64(-30.0 * y) - 25.0), Float64(abs(Float64(fma(Float64(Float64(x * x) * x), 27000.0, Float64(Float64(Float64(1.0 - cos(Float64(z * 60.0))) * 0.5) * t_0)) / fma(Float64(900.0 * x), x, Float64(t_0 * fma(-30.0, x, t_0))))) - 0.2));
	else
		tmp = fmax(Float64(hypot(Float64(z * 30.0), hypot(Float64(y * 30.0), Float64(30.0 * x))) - 25.0), Float64(abs(Float64(sin(Float64(30.0 * z)) + Float64(cos(Float64(30.0 * z)) * sin(Float64(30.0 * y))))) - 0.2));
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[Sin[N[(z * 30.0), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[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[(t$95$0 * N[Cos[N[(x * 30.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], -0.1], N[Max[N[(N[(-30.0 * y), $MachinePrecision] - 25.0), $MachinePrecision], N[(N[Abs[N[(N[(N[(N[(x * x), $MachinePrecision] * x), $MachinePrecision] * 27000.0 + N[(N[(N[(1.0 - N[Cos[N[(z * 60.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision] * t$95$0), $MachinePrecision]), $MachinePrecision] / N[(N[(900.0 * x), $MachinePrecision] * x + N[(t$95$0 * N[(-30.0 * x + t$95$0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision], N[Max[N[(N[Sqrt[N[(z * 30.0), $MachinePrecision] ^ 2 + N[Sqrt[N[(y * 30.0), $MachinePrecision] ^ 2 + N[(30.0 * x), $MachinePrecision] ^ 2], $MachinePrecision] ^ 2], $MachinePrecision] - 25.0), $MachinePrecision], N[(N[Abs[N[(N[Sin[N[(30.0 * z), $MachinePrecision]], $MachinePrecision] + N[(N[Cos[N[(30.0 * z), $MachinePrecision]], $MachinePrecision] * N[Sin[N[(30.0 * y), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - 0.2), $MachinePrecision]], $MachinePrecision]]]

Derivation

1. Split input into 2 regimes

2. if (fmax.f64 (-.f64 (sqrt.f64 (+.f64 (+.f64 (pow.f64 (*.f64 x #s(literal 30 binary64)) #s(literal 2 binary64)) (pow.f64 (*.f64 y #s(literal 30 binary64)) #s(literal 2 binary64))) (pow.f64 (*.f64 z #s(literal 30 binary64)) #s(literal 2 binary64)))) #s(literal 25 binary64)) (-.f64 (fabs.f64 (+.f64 (+.f64 (*.f64 (sin.f64 (*.f64 x #s(literal 30 binary64))) (cos.f64 (*.f64 y #s(literal 30 binary64)))) (*.f64 (sin.f64 (*.f64 y #s(literal 30 binary64))) (cos.f64 (*.f64 z #s(literal 30 binary64))))) (*.f64 (sin.f64 (*.f64 z #s(literal 30 binary64))) (cos.f64 (*.f64 x #s(literal 30 binary64)))))) #s(literal 1/5 binary64))) < -0.10000000000000001

   1. Initial program 35.9%

      \[\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 y 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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \color{blue}{\left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \color{blue}{\sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \color{blue}{\left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(\color{blue}{30} \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 35.9%

         \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - 0.2\right) \]

   4. Applied rewrites 35.9%

      \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\right) \]

   5. 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|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]
   6. 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) + 30 \cdot \color{blue}{x}\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) + 30 \cdot x\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) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 35.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 z\right) + 30 \cdot x\right| - 0.2\right) \]

   7. Applied rewrites 35.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 z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

   8. Taylor expanded in y around -inf

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

      1. lower-*.f64 46.9%

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

   10. Applied rewrites 46.9%

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

   12. Applied rewrites 25.1%

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

   if -0.10000000000000001 < (fmax.f64 (-.f64 (sqrt.f64 (+.f64 (+.f64 (pow.f64 (*.f64 x #s(literal 30 binary64)) #s(literal 2 binary64)) (pow.f64 (*.f64 y #s(literal 30 binary64)) #s(literal 2 binary64))) (pow.f64 (*.f64 z #s(literal 30 binary64)) #s(literal 2 binary64)))) #s(literal 25 binary64)) (-.f64 (fabs.f64 (+.f64 (+.f64 (*.f64 (sin.f64 (*.f64 x #s(literal 30 binary64))) (cos.f64 (*.f64 y #s(literal 30 binary64)))) (*.f64 (sin.f64 (*.f64 y #s(literal 30 binary64))) (cos.f64 (*.f64 z #s(literal 30 binary64))))) (*.f64 (sin.f64 (*.f64 z #s(literal 30 binary64))) (cos.f64 (*.f64 x #s(literal 30 binary64)))))) #s(literal 1/5 binary64)))

   1. Initial program 35.9%

      \[\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) \]

   3. Applied rewrites 49.3%

      \[\leadsto \mathsf{max}\left(\color{blue}{\mathsf{hypot}\left(z \cdot 30, \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right)} - 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) \]
   4. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      2. lift-*.f64 N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      3. *-commutative N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

      4. sqrt-prod N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      5. metadata-eval N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\color{blue}{900}}\right) - 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| - \frac{1}{5}\right) \]

      6. sqrt-unprod N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

      7. metadata-eval N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot \color{blue}{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      8. fabs-mul N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900\right|}}\right) - 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| - \frac{1}{5}\right) \]

      9. *-commutative N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

      10. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

      11. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      12. sqr-neg-rev N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      13. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right|}}\right) - 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| - \frac{1}{5}\right) \]

      14. rem-sqrt-square N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      15. sqr-neg-rev N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      16. sqrt-unprod N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}}\right) - 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| - \frac{1}{5}\right) \]

      17. rem-square-sqrt N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

      18. lift-*.f64 N/A

          \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   5. Applied rewrites 89.2%

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)}\right) - 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) \]

   6. Taylor expanded in x around 0

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

      1. lower-+.f64 N/A

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

      2. lower-sin.f64 N/A

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

      3. lower-*.f64 N/A

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

      4. lower-*.f64 N/A

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

      5. lower-cos.f64 N/A

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

      6. lower-*.f64 N/A

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

      7. lower-sin.f64 N/A

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

      8. lower-*.f64 89.2%

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

   8. Applied rewrites 89.2%

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

Alternative 4: 89.2% accurate, 1.9× speedup

Math

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

FPCore

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

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Derivation

1. Initial program 35.9%

   \[\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) \]

3. Applied rewrites 49.3%

   \[\leadsto \mathsf{max}\left(\color{blue}{\mathsf{hypot}\left(z \cdot 30, \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right)} - 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) \]
4. Step-by-step derivation

   1. lift-sqrt.f64 N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   2. lift-*.f64 N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   3. *-commutative N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

   4. sqrt-prod N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

   5. metadata-eval N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\color{blue}{900}}\right) - 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| - \frac{1}{5}\right) \]

   6. sqrt-unprod N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

   7. metadata-eval N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot \color{blue}{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

   8. fabs-mul N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900\right|}}\right) - 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| - \frac{1}{5}\right) \]

   9. *-commutative N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

   10. lift-*.f64 N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

   11. rem-sqrt-square N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   12. sqr-neg-rev N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   13. rem-sqrt-square N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right|}}\right) - 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| - \frac{1}{5}\right) \]

   14. rem-sqrt-square N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   15. sqr-neg-rev N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   16. sqrt-unprod N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   17. rem-square-sqrt N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   18. lift-*.f64 N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

5. Applied rewrites 89.2%

   \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)}\right) - 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) \]

6. Taylor expanded in x around 0

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

   1. lower-+.f64 N/A

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

   2. lower-sin.f64 N/A

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

   3. lower-*.f64 N/A

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

   4. lower-*.f64 N/A

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

   5. lower-cos.f64 N/A

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

   6. lower-*.f64 N/A

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

   7. lower-sin.f64 N/A

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

   8. lower-*.f64 89.2%

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

8. Applied rewrites 89.2%

   \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)\right) - 25, \left|\color{blue}{\sin \left(30 \cdot z\right) + \cos \left(30 \cdot z\right) \cdot \sin \left(30 \cdot y\right)}\right| - 0.2\right) \]
9. Add Preprocessing

Alternative 5: 88.9% accurate, 3.4× speedup

Math

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

FPCore

(FPCore (x y z)
  :precision binary64
  (fmax
 (- (hypot (* z 30.0) (hypot (* y 30.0) (* 30.0 x))) 25.0)
 (- (fabs (+ (sin (* 30.0 y)) (* 30.0 z))) 0.2)))

C

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

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

Derivation

1. Initial program 35.9%

   \[\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) \]

3. Applied rewrites 49.3%

   \[\leadsto \mathsf{max}\left(\color{blue}{\mathsf{hypot}\left(z \cdot 30, \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right)} - 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) \]
4. Step-by-step derivation

   1. lift-sqrt.f64 N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   2. lift-*.f64 N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   3. *-commutative N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

   4. sqrt-prod N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

   5. metadata-eval N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right|} \cdot \sqrt{\color{blue}{900}}\right) - 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| - \frac{1}{5}\right) \]

   6. sqrt-unprod N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot 900}}\right) - 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| - \frac{1}{5}\right) \]

   7. metadata-eval N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\mathsf{fma}\left(y, y, x \cdot x\right)\right| \cdot \color{blue}{\left|900\right|}}\right) - 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| - \frac{1}{5}\right) \]

   8. fabs-mul N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{fma}\left(y, y, x \cdot x\right) \cdot 900\right|}}\right) - 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| - \frac{1}{5}\right) \]

   9. *-commutative N/A

      \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

   10. lift-*.f64 N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\left|\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}\right|}\right) - 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| - \frac{1}{5}\right) \]

   11. rem-sqrt-square N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   12. sqr-neg-rev N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   13. rem-sqrt-square N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\left|\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right|}}\right) - 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| - \frac{1}{5}\right) \]

   14. rem-sqrt-square N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{\left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right) \cdot \left(\mathsf{neg}\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   15. sqr-neg-rev N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\sqrt{\color{blue}{\left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right) \cdot \left(900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   16. sqrt-unprod N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{\sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \sqrt{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}}\right) - 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| - \frac{1}{5}\right) \]

   17. rem-square-sqrt N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

   18. lift-*.f64 N/A

       \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \sqrt{\color{blue}{900 \cdot \mathsf{fma}\left(y, y, x \cdot x\right)}}\right) - 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| - \frac{1}{5}\right) \]

5. Applied rewrites 89.2%

   \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(z \cdot 30, \color{blue}{\mathsf{hypot}\left(y \cdot 30, 30 \cdot x\right)}\right) - 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) \]

6. Taylor expanded in x around 0

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

   1. lower-+.f64 N/A

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

   2. lower-sin.f64 N/A

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

   3. lower-*.f64 N/A

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

   4. lower-*.f64 N/A

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

   5. lower-cos.f64 N/A

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

   6. lower-*.f64 N/A

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

   7. lower-sin.f64 N/A

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

   8. lower-*.f64 89.2%

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

8. Applied rewrites 89.2%

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

9. Taylor expanded in z around 0

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

    1. lower-+.f64 N/A

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

    2. lower-sin.f64 N/A

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

    3. lower-*.f64 N/A

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

    4. lower-*.f64 88.9%

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

11. Applied rewrites 88.9%

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

Alternative 6: 78.5% accurate, 0.8× speedup

Math

\[\begin{array}{l} \mathbf{if}\;\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) \leq 2 \cdot 10^{+141}:\\ \;\;\;\;\mathsf{max}\left(\mathsf{hypot}\left(\sqrt{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot 30, z \cdot 30\right) - 25, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - 0.2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{max}\left(-30 \cdot y - 25, \left|\mathsf{fma}\left(30, x, 30 \cdot z\right)\right| - 0.2\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (if (<=
     (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))
     2e+141)
  (fmax
   (- (hypot (* (sqrt (fma y y (* x x))) 30.0) (* z 30.0)) 25.0)
   (- (fabs (+ (sin (* 30.0 z)) (* 30.0 x))) 0.2))
  (fmax (- (* -30.0 y) 25.0) (- (fabs (fma 30.0 x (* 30.0 z))) 0.2))))

C

double code(double x, double y, double z) {
	double tmp;
	if (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)) <= 2e+141) {
		tmp = fmax((hypot((sqrt(fma(y, y, (x * x))) * 30.0), (z * 30.0)) - 25.0), (fabs((sin((30.0 * z)) + (30.0 * x))) - 0.2));
	} else {
		tmp = fmax(((-30.0 * y) - 25.0), (fabs(fma(30.0, x, (30.0 * z))) - 0.2));
	}
	return tmp;
}

Julia

function code(x, y, z)
	tmp = 0.0
	if (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)) <= 2e+141)
		tmp = fmax(Float64(hypot(Float64(sqrt(fma(y, y, Float64(x * x))) * 30.0), Float64(z * 30.0)) - 25.0), Float64(abs(Float64(sin(Float64(30.0 * z)) + Float64(30.0 * x))) - 0.2));
	else
		tmp = fmax(Float64(Float64(-30.0 * y) - 25.0), Float64(abs(fma(30.0, x, Float64(30.0 * z))) - 0.2));
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := If[LessEqual[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], 2e+141], N[Max[N[(N[Sqrt[N[(N[Sqrt[N[(y * y + N[(x * x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * 30.0), $MachinePrecision] ^ 2 + N[(z * 30.0), $MachinePrecision] ^ 2], $MachinePrecision] - 25.0), $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[(N[(-30.0 * y), $MachinePrecision] - 25.0), $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 (fmax.f64 (-.f64 (sqrt.f64 (+.f64 (+.f64 (pow.f64 (*.f64 x #s(literal 30 binary64)) #s(literal 2 binary64)) (pow.f64 (*.f64 y #s(literal 30 binary64)) #s(literal 2 binary64))) (pow.f64 (*.f64 z #s(literal 30 binary64)) #s(literal 2 binary64)))) #s(literal 25 binary64)) (-.f64 (fabs.f64 (+.f64 (+.f64 (*.f64 (sin.f64 (*.f64 x #s(literal 30 binary64))) (cos.f64 (*.f64 y #s(literal 30 binary64)))) (*.f64 (sin.f64 (*.f64 y #s(literal 30 binary64))) (cos.f64 (*.f64 z #s(literal 30 binary64))))) (*.f64 (sin.f64 (*.f64 z #s(literal 30 binary64))) (cos.f64 (*.f64 x #s(literal 30 binary64)))))) #s(literal 1/5 binary64))) < 2e141

   1. Initial program 35.9%

      \[\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 y 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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \color{blue}{\left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \color{blue}{\sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \color{blue}{\left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(\color{blue}{30} \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 35.9%

         \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - 0.2\right) \]

   4. Applied rewrites 35.9%

      \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\right) \]

   6. Applied rewrites 49.5%

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

   7. Taylor expanded in x around 0

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

      1. lower-+.f64 N/A

         \[\leadsto \mathsf{max}\left(\mathsf{hypot}\left(\sqrt{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot 30, z \cdot 30\right) - 25, \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(\mathsf{hypot}\left(\sqrt{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot 30, z \cdot 30\right) - 25, \left|\sin \left(30 \cdot z\right) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      3. lower-*.f64 N/A

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

      4. lower-*.f64 49.3%

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

   9. Applied rewrites 49.3%

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

   if 2e141 < (fmax.f64 (-.f64 (sqrt.f64 (+.f64 (+.f64 (pow.f64 (*.f64 x #s(literal 30 binary64)) #s(literal 2 binary64)) (pow.f64 (*.f64 y #s(literal 30 binary64)) #s(literal 2 binary64))) (pow.f64 (*.f64 z #s(literal 30 binary64)) #s(literal 2 binary64)))) #s(literal 25 binary64)) (-.f64 (fabs.f64 (+.f64 (+.f64 (*.f64 (sin.f64 (*.f64 x #s(literal 30 binary64))) (cos.f64 (*.f64 y #s(literal 30 binary64)))) (*.f64 (sin.f64 (*.f64 y #s(literal 30 binary64))) (cos.f64 (*.f64 z #s(literal 30 binary64))))) (*.f64 (sin.f64 (*.f64 z #s(literal 30 binary64))) (cos.f64 (*.f64 x #s(literal 30 binary64)))))) #s(literal 1/5 binary64)))

   1. Initial program 35.9%

      \[\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 y 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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \color{blue}{\left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \color{blue}{\sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \color{blue}{\left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(\color{blue}{30} \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - \frac{1}{5}\right) \]

      8. lower-*.f64 35.9%

         \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - 0.2\right) \]

   4. Applied rewrites 35.9%

      \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\right) \]

   5. 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|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]
   6. 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) + 30 \cdot \color{blue}{x}\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) + 30 \cdot x\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) + 30 \cdot x\right| - \frac{1}{5}\right) \]

      4. lower-*.f64 35.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 z\right) + 30 \cdot x\right| - 0.2\right) \]

   7. Applied rewrites 35.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 z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

   8. Taylor expanded in y around -inf

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

      1. lower-*.f64 46.9%

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

   10. Applied rewrites 46.9%

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

   11. Taylor expanded in z around 0

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

       1. lower-fma.f64 N/A

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

       2. lower-*.f64 73.9%

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

   13. Applied rewrites 73.9%

       \[\leadsto \mathsf{max}\left(-30 \cdot y - 25, \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: 73.9% accurate, 14.7× speedup

Math

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

FPCore

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

C

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

Julia

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

Wolfram

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

Derivation

1. Initial program 35.9%

   \[\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 y 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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\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 x\right) + \color{blue}{\cos \left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \color{blue}{\left(30 \cdot x\right)} \cdot \sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \color{blue}{\sin \left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \color{blue}{\left(30 \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(\color{blue}{30} \cdot z\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - \frac{1}{5}\right) \]

   8. lower-*.f64 35.9%

      \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)\right| - 0.2\right) \]

4. Applied rewrites 35.9%

   \[\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 x\right) + \cos \left(30 \cdot x\right) \cdot \sin \left(30 \cdot z\right)}\right| - 0.2\right) \]

5. 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|\sin \left(30 \cdot z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]
6. 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) + 30 \cdot \color{blue}{x}\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) + 30 \cdot x\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) + 30 \cdot x\right| - \frac{1}{5}\right) \]

   4. lower-*.f64 35.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 z\right) + 30 \cdot x\right| - 0.2\right) \]

7. Applied rewrites 35.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 z\right) + \color{blue}{30 \cdot x}\right| - 0.2\right) \]

8. Taylor expanded in y around -inf

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

   1. lower-*.f64 46.9%

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

10. Applied rewrites 46.9%

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

11. Taylor expanded in z around 0

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

    1. lower-fma.f64 N/A

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

    2. lower-*.f64 73.9%

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

13. Applied rewrites 73.9%

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

Reproduce

herbie shell --seed 2025322 
(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)))