Average Error: 0.1 → 0.2
Time: 13.8s
Precision: 64
$0 \le x1 \le 2 \land 0 \le x2 \le 3 \land -2 \cdot \left(\left(x1 \cdot x1\right) \cdot \left(x1 \cdot x1\right)\right) + 2 \ge x2$
$\left(-12 \cdot x1 - 7 \cdot x2\right) + x2 \cdot x2$
$\frac{\left(x2 \cdot x2 + -49\right) \cdot x2}{7 + x2} - 12 \cdot x1$
\left(-12 \cdot x1 - 7 \cdot x2\right) + x2 \cdot x2
\frac{\left(x2 \cdot x2 + -49\right) \cdot x2}{7 + x2} - 12 \cdot x1
double f(double x1, double x2) {
double r40095880 = -12.0;
double r40095881 = x1;
double r40095882 = r40095880 * r40095881;
double r40095883 = 7.0;
double r40095884 = x2;
double r40095885 = r40095883 * r40095884;
double r40095886 = r40095882 - r40095885;
double r40095887 = r40095884 * r40095884;
double r40095888 = r40095886 + r40095887;
return r40095888;
}


double f(double x1, double x2) {
double r40095889 = x2;
double r40095890 = r40095889 * r40095889;
double r40095891 = -49.0;
double r40095892 = r40095890 + r40095891;
double r40095893 = r40095892 * r40095889;
double r40095894 = 7.0;
double r40095895 = r40095894 + r40095889;
double r40095896 = r40095893 / r40095895;
double r40095897 = 12.0;
double r40095898 = x1;
double r40095899 = r40095897 * r40095898;
double r40095900 = r40095896 - r40095899;
return r40095900;
}



Try it out

Results

 In Out
Enter valid numbers for all inputs

Derivation

1. Initial program 0.1

$\left(-12 \cdot x1 - 7 \cdot x2\right) + x2 \cdot x2$
2. Simplified0.1

$\leadsto \color{blue}{\left(x2 - 7\right) \cdot x2 - x1 \cdot 12}$
3. Using strategy rm
4. Applied flip--0.1

$\leadsto \color{blue}{\frac{x2 \cdot x2 - 7 \cdot 7}{x2 + 7}} \cdot x2 - x1 \cdot 12$
5. Applied associate-*l/0.2

$\leadsto \color{blue}{\frac{\left(x2 \cdot x2 - 7 \cdot 7\right) \cdot x2}{x2 + 7}} - x1 \cdot 12$
6. Simplified0.2

$\leadsto \frac{\color{blue}{x2 \cdot \left(x2 \cdot x2 + -49\right)}}{x2 + 7} - x1 \cdot 12$
7. Final simplification0.2

$\leadsto \frac{\left(x2 \cdot x2 + -49\right) \cdot x2}{7 + x2} - 12 \cdot x1$

Reproduce

herbie shell --seed 1
(FPCore (x1 x2)
:name "floudas3"
:pre (and (<= 0 x1 2) (<= 0 x2 3) (>= (+ (* -2 (* (* x1 x1) (* x1 x1))) 2) x2))
(+ (- (* -12 x1) (* 7 x2)) (* x2 x2)))