Average Error: 0.6 → 0.4
Time: 40.6s
Precision: 64
$4 \le x1 \le \frac{159}{25} \land 4 \le x2 \le \frac{159}{25} \land 4 \le x3 \le \frac{159}{25} \land 4 \le x4 \le \frac{159}{25} \land 4 \le x5 \le \frac{159}{25} \land 4 \le x6 \le \frac{159}{25}$
$\left(\left(\left(x2 \cdot x5 + x3 \cdot x6\right) - x2 \cdot x3\right) - x5 \cdot x6\right) + x1 \cdot \left(\left(\left(\left(\left(\left(-x1\right) + x2\right) + x3\right) - x4\right) + x5\right) + x6\right)$
$x6 \cdot x1 + \log \left(e^{\left(x6 - x2\right) \cdot x3 + \left(x2 \cdot x5 - \left(x5 \cdot x6 - \left(\left(\left(x3 - x4\right) + \left(x2 - x1\right)\right) + x5\right) \cdot x1\right)\right)}\right)$
\left(\left(\left(x2 \cdot x5 + x3 \cdot x6\right) - x2 \cdot x3\right) - x5 \cdot x6\right) + x1 \cdot \left(\left(\left(\left(\left(\left(-x1\right) + x2\right) + x3\right) - x4\right) + x5\right) + x6\right)
x6 \cdot x1 + \log \left(e^{\left(x6 - x2\right) \cdot x3 + \left(x2 \cdot x5 - \left(x5 \cdot x6 - \left(\left(\left(x3 - x4\right) + \left(x2 - x1\right)\right) + x5\right) \cdot x1\right)\right)}\right)
double f(double x1, double x2, double x3, double x4, double x5, double x6) {
double r52952461 = x2;
double r52952462 = x5;
double r52952463 = r52952461 * r52952462;
double r52952464 = x3;
double r52952465 = x6;
double r52952466 = r52952464 * r52952465;
double r52952467 = r52952463 + r52952466;
double r52952468 = r52952461 * r52952464;
double r52952469 = r52952467 - r52952468;
double r52952470 = r52952462 * r52952465;
double r52952471 = r52952469 - r52952470;
double r52952472 = x1;
double r52952473 = -r52952472;
double r52952474 = r52952473 + r52952461;
double r52952475 = r52952474 + r52952464;
double r52952476 = x4;
double r52952477 = r52952475 - r52952476;
double r52952478 = r52952477 + r52952462;
double r52952479 = r52952478 + r52952465;
double r52952480 = r52952472 * r52952479;
double r52952481 = r52952471 + r52952480;
return r52952481;
}


double f(double x1, double x2, double x3, double x4, double x5, double x6) {
double r52952482 = x6;
double r52952483 = x1;
double r52952484 = r52952482 * r52952483;
double r52952485 = x2;
double r52952486 = r52952482 - r52952485;
double r52952487 = x3;
double r52952488 = r52952486 * r52952487;
double r52952489 = x5;
double r52952490 = r52952485 * r52952489;
double r52952491 = r52952489 * r52952482;
double r52952492 = x4;
double r52952493 = r52952487 - r52952492;
double r52952494 = r52952485 - r52952483;
double r52952495 = r52952493 + r52952494;
double r52952496 = r52952495 + r52952489;
double r52952497 = r52952496 * r52952483;
double r52952498 = r52952491 - r52952497;
double r52952499 = r52952490 - r52952498;
double r52952500 = r52952488 + r52952499;
double r52952501 = exp(r52952500);
double r52952502 = log(r52952501);
double r52952503 = r52952484 + r52952502;
return r52952503;
}



# Try it out

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Initial program 0.6

$\left(\left(\left(x2 \cdot x5 + x3 \cdot x6\right) - x2 \cdot x3\right) - x5 \cdot x6\right) + x1 \cdot \left(\left(\left(\left(\left(\left(-x1\right) + x2\right) + x3\right) - x4\right) + x5\right) + x6\right)$
2. Using strategy rm
3. Applied distribute-rgt-in0.5

$\leadsto \left(\left(\left(x2 \cdot x5 + x3 \cdot x6\right) - x2 \cdot x3\right) - x5 \cdot x6\right) + \color{blue}{\left(\left(\left(\left(\left(\left(-x1\right) + x2\right) + x3\right) - x4\right) + x5\right) \cdot x1 + x6 \cdot x1\right)}$
4. Applied associate-+r+0.5

$\leadsto \color{blue}{\left(\left(\left(\left(x2 \cdot x5 + x3 \cdot x6\right) - x2 \cdot x3\right) - x5 \cdot x6\right) + \left(\left(\left(\left(\left(-x1\right) + x2\right) + x3\right) - x4\right) + x5\right) \cdot x1\right) + x6 \cdot x1}$
5. Simplified0.3

$\leadsto \color{blue}{\left(\left(\left(x5 \cdot x2 + x3 \cdot \left(x6 - x2\right)\right) - x5 \cdot x6\right) + x1 \cdot \left(\left(\left(x2 - x1\right) + x3\right) - \left(x4 - x5\right)\right)\right)} + x6 \cdot x1$
6. Using strategy rm

$\leadsto \left(\left(\left(x5 \cdot x2 + x3 \cdot \left(x6 - x2\right)\right) - x5 \cdot x6\right) + \color{blue}{\log \left(e^{x1 \cdot \left(\left(\left(x2 - x1\right) + x3\right) - \left(x4 - x5\right)\right)}\right)}\right) + x6 \cdot x1$

$\leadsto \left(\left(\left(x5 \cdot x2 + x3 \cdot \left(x6 - x2\right)\right) - \color{blue}{\log \left(e^{x5 \cdot x6}\right)}\right) + \log \left(e^{x1 \cdot \left(\left(\left(x2 - x1\right) + x3\right) - \left(x4 - x5\right)\right)}\right)\right) + x6 \cdot x1$

$\leadsto \left(\left(\left(x5 \cdot x2 + \color{blue}{\log \left(e^{x3 \cdot \left(x6 - x2\right)}\right)}\right) - \log \left(e^{x5 \cdot x6}\right)\right) + \log \left(e^{x1 \cdot \left(\left(\left(x2 - x1\right) + x3\right) - \left(x4 - x5\right)\right)}\right)\right) + x6 \cdot x1$

$\leadsto \left(\left(\left(\color{blue}{\log \left(e^{x5 \cdot x2}\right)} + \log \left(e^{x3 \cdot \left(x6 - x2\right)}\right)\right) - \log \left(e^{x5 \cdot x6}\right)\right) + \log \left(e^{x1 \cdot \left(\left(\left(x2 - x1\right) + x3\right) - \left(x4 - x5\right)\right)}\right)\right) + x6 \cdot x1$
11. Applied sum-log0.3

$\leadsto \left(\left(\color{blue}{\log \left(e^{x5 \cdot x2} \cdot e^{x3 \cdot \left(x6 - x2\right)}\right)} - \log \left(e^{x5 \cdot x6}\right)\right) + \log \left(e^{x1 \cdot \left(\left(\left(x2 - x1\right) + x3\right) - \left(x4 - x5\right)\right)}\right)\right) + x6 \cdot x1$
12. Applied diff-log0.3

$\leadsto \left(\color{blue}{\log \left(\frac{e^{x5 \cdot x2} \cdot e^{x3 \cdot \left(x6 - x2\right)}}{e^{x5 \cdot x6}}\right)} + \log \left(e^{x1 \cdot \left(\left(\left(x2 - x1\right) + x3\right) - \left(x4 - x5\right)\right)}\right)\right) + x6 \cdot x1$
13. Applied sum-log0.3

$\leadsto \color{blue}{\log \left(\frac{e^{x5 \cdot x2} \cdot e^{x3 \cdot \left(x6 - x2\right)}}{e^{x5 \cdot x6}} \cdot e^{x1 \cdot \left(\left(\left(x2 - x1\right) + x3\right) - \left(x4 - x5\right)\right)}\right)} + x6 \cdot x1$
14. Simplified0.4

$\leadsto \log \color{blue}{\left(e^{\left(x6 - x2\right) \cdot x3 + \left(x2 \cdot x5 - \left(x6 \cdot x5 - x1 \cdot \left(x5 + \left(\left(x2 - x1\right) + \left(x3 - x4\right)\right)\right)\right)\right)}\right)} + x6 \cdot x1$
15. Final simplification0.4

$\leadsto x6 \cdot x1 + \log \left(e^{\left(x6 - x2\right) \cdot x3 + \left(x2 \cdot x5 - \left(x5 \cdot x6 - \left(\left(\left(x3 - x4\right) + \left(x2 - x1\right)\right) + x5\right) \cdot x1\right)\right)}\right)$

# Reproduce

herbie shell --seed 1
(FPCore (x1 x2 x3 x4 x5 x6)
:name "kepler0"
:pre (and (<= 4 x1 159/25) (<= 4 x2 159/25) (<= 4 x3 159/25) (<= 4 x4 159/25) (<= 4 x5 159/25) (<= 4 x6 159/25))
(+ (- (- (+ (* x2 x5) (* x3 x6)) (* x2 x3)) (* x5 x6)) (* x1 (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6))))