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;
}

Error

Bits error versus x1

Bits error versus x2

Bits error versus x3

Bits error versus x4

Bits error versus x5

Bits error versus x6

Try it out

Your Program's Arguments

Results

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
  7. Applied add-log-exp0.3

    \[\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\]
  8. Applied add-log-exp0.3

    \[\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\]
  9. Applied add-log-exp0.3

    \[\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\]
  10. Applied add-log-exp0.3

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