Average Error: 0.3 → 0.3
Time: 2.3m
Precision: 64
$1 \le a \le 9 \land 1 \le b \le 9 \land 1 \le c \le 9 \land a + b \gt c + 9.999999999999999547481118258862586856139 \cdot 10^{-7} \land a + c \gt b + 9.999999999999999547481118258862586856139 \cdot 10^{-7} \land b + c \gt a + 9.999999999999999547481118258862586856139 \cdot 10^{-7} \land a \lt c \land b \lt c$
$\begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot \left(c + \left(a - b\right)\right)}}{4}\\ \end{array}$
$\begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(c + \left(b - a\right)\right) \cdot \left(\left(a + \left(c - b\right)\right) \cdot \left(\left(c + \left(a + b\right)\right) \cdot \left(a - \left(c - b\right)\right)\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(a - b\right) \cdot \frac{\left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right) \cdot \left(\left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right) \cdot \left({\left(a + b\right)}^{3} + {c}^{3}\right)\right)}{\left(b - \left(c - a\right)\right) \cdot \left(\left(\left(\left(a + b\right) \cdot \left(a + b\right) - c \cdot \left(a + b\right)\right) + c \cdot c\right) \cdot \left(\left(c - a\right) + b\right)\right)} + c \cdot \left(\left(\left(b - \left(c - a\right)\right) \cdot \left(c + \left(a + b\right)\right)\right) \cdot \left(\left(c - a\right) + b\right)\right)}}{4}\\ \end{array}$
\begin{array}{l}
\mathbf{if}\;a \lt b:\\
\;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\

\mathbf{else}:\\
\;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot \left(c + \left(a - b\right)\right)}}{4}\\

\end{array}
\begin{array}{l}
\mathbf{if}\;a \lt b:\\
\;\;\;\;\frac{\sqrt{\left(c + \left(b - a\right)\right) \cdot \left(\left(a + \left(c - b\right)\right) \cdot \left(\left(c + \left(a + b\right)\right) \cdot \left(a - \left(c - b\right)\right)\right)\right)}}{4}\\

\mathbf{else}:\\
\;\;\;\;\frac{\sqrt{\left(a - b\right) \cdot \frac{\left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right) \cdot \left(\left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right) \cdot \left({\left(a + b\right)}^{3} + {c}^{3}\right)\right)}{\left(b - \left(c - a\right)\right) \cdot \left(\left(\left(\left(a + b\right) \cdot \left(a + b\right) - c \cdot \left(a + b\right)\right) + c \cdot c\right) \cdot \left(\left(c - a\right) + b\right)\right)} + c \cdot \left(\left(\left(b - \left(c - a\right)\right) \cdot \left(c + \left(a + b\right)\right)\right) \cdot \left(\left(c - a\right) + b\right)\right)}}{4}\\

\end{array}
double f(double a, double b, double c) {
double r29763505 = a;
double r29763506 = b;
bool r29763507 = r29763505 < r29763506;
double r29763508 = c;
double r29763509 = r29763506 + r29763505;
double r29763510 = r29763508 + r29763509;
double r29763511 = r29763508 - r29763506;
double r29763512 = r29763505 - r29763511;
double r29763513 = r29763510 * r29763512;
double r29763514 = r29763505 + r29763511;
double r29763515 = r29763513 * r29763514;
double r29763516 = r29763506 - r29763505;
double r29763517 = r29763508 + r29763516;
double r29763518 = r29763515 * r29763517;
double r29763519 = sqrt(r29763518);
double r29763520 = 4.0;
double r29763521 = r29763519 / r29763520;
double r29763522 = r29763505 + r29763506;
double r29763523 = r29763508 + r29763522;
double r29763524 = r29763508 - r29763505;
double r29763525 = r29763506 - r29763524;
double r29763526 = r29763523 * r29763525;
double r29763527 = r29763506 + r29763524;
double r29763528 = r29763526 * r29763527;
double r29763529 = r29763505 - r29763506;
double r29763530 = r29763508 + r29763529;
double r29763531 = r29763528 * r29763530;
double r29763532 = sqrt(r29763531);
double r29763533 = r29763532 / r29763520;
double r29763534 = r29763507 ? r29763521 : r29763533;
return r29763534;
}


double f(double a, double b, double c) {
double r29763535 = a;
double r29763536 = b;
bool r29763537 = r29763535 < r29763536;
double r29763538 = c;
double r29763539 = r29763536 - r29763535;
double r29763540 = r29763538 + r29763539;
double r29763541 = r29763538 - r29763536;
double r29763542 = r29763535 + r29763541;
double r29763543 = r29763535 + r29763536;
double r29763544 = r29763538 + r29763543;
double r29763545 = r29763535 - r29763541;
double r29763546 = r29763544 * r29763545;
double r29763547 = r29763542 * r29763546;
double r29763548 = r29763540 * r29763547;
double r29763549 = sqrt(r29763548);
double r29763550 = 4.0;
double r29763551 = r29763549 / r29763550;
double r29763552 = r29763535 - r29763536;
double r29763553 = r29763536 * r29763536;
double r29763554 = r29763538 - r29763535;
double r29763555 = r29763554 * r29763554;
double r29763556 = r29763553 - r29763555;
double r29763557 = 3.0;
double r29763558 = pow(r29763543, r29763557);
double r29763559 = pow(r29763538, r29763557);
double r29763560 = r29763558 + r29763559;
double r29763561 = r29763556 * r29763560;
double r29763562 = r29763556 * r29763561;
double r29763563 = r29763536 - r29763554;
double r29763564 = r29763543 * r29763543;
double r29763565 = r29763538 * r29763543;
double r29763566 = r29763564 - r29763565;
double r29763567 = r29763538 * r29763538;
double r29763568 = r29763566 + r29763567;
double r29763569 = r29763554 + r29763536;
double r29763570 = r29763568 * r29763569;
double r29763571 = r29763563 * r29763570;
double r29763572 = r29763562 / r29763571;
double r29763573 = r29763552 * r29763572;
double r29763574 = r29763563 * r29763544;
double r29763575 = r29763574 * r29763569;
double r29763576 = r29763538 * r29763575;
double r29763577 = r29763573 + r29763576;
double r29763578 = sqrt(r29763577);
double r29763579 = r29763578 / r29763550;
double r29763580 = r29763537 ? r29763551 : r29763579;
return r29763580;
}



# Try it out

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Initial program 0.3

$\begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot \left(c + \left(a - b\right)\right)}}{4}\\ \end{array}$
2. Using strategy rm
3. Applied distribute-lft-in0.3

$\leadsto \begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot c + \left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot \left(a - b\right)}}{4}\\ \end{array}$
4. Using strategy rm
5. Applied flip-+0.3

$\leadsto \begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot c + \left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \frac{b \cdot b - \left(c - a\right) \cdot \left(c - a\right)}{b - \left(c - a\right)}\right) \cdot \left(a - b\right)}}{4}\\ \end{array}$
6. Applied flip--0.3

$\leadsto \begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot c + \left(\left(\left(c + \left(a + b\right)\right) \cdot \frac{b \cdot b - \left(c - a\right) \cdot \left(c - a\right)}{b + \left(c - a\right)}\right) \cdot \frac{b \cdot b - \left(c - a\right) \cdot \left(c - a\right)}{b - \left(c - a\right)}\right) \cdot \left(a - b\right)}}{4}\\ \end{array}$
7. Applied flip3-+0.3

$\leadsto \begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot c + \left(\left(\frac{{c}^{3} + {\left(a + b\right)}^{3}}{c \cdot c + \left(\left(a + b\right) \cdot \left(a + b\right) - c \cdot \left(a + b\right)\right)} \cdot \frac{b \cdot b - \left(c - a\right) \cdot \left(c - a\right)}{b + \left(c - a\right)}\right) \cdot \frac{b \cdot b - \left(c - a\right) \cdot \left(c - a\right)}{b - \left(c - a\right)}\right) \cdot \left(a - b\right)}}{4}\\ \end{array}$
8. Applied frac-times0.3

$\leadsto \begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot c + \left(\frac{\left({c}^{3} + {\left(a + b\right)}^{3}\right) \cdot \left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right)}{\left(c \cdot c + \left(\left(a + b\right) \cdot \left(a + b\right) - c \cdot \left(a + b\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)} \cdot \frac{b \cdot b - \left(c - a\right) \cdot \left(c - a\right)}{b - \left(c - a\right)}\right) \cdot \left(a - b\right)}}{4}\\ \end{array}$
9. Applied frac-times0.3

$\leadsto \begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(b + a\right)\right) \cdot \left(a - \left(c - b\right)\right)\right) \cdot \left(a + \left(c - b\right)\right)\right) \cdot \left(c + \left(b - a\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(\left(\left(c + \left(a + b\right)\right) \cdot \left(b - \left(c - a\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot c + \frac{\left(\left({c}^{3} + {\left(a + b\right)}^{3}\right) \cdot \left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right)\right) \cdot \left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right)}{\left(\left(c \cdot c + \left(\left(a + b\right) \cdot \left(a + b\right) - c \cdot \left(a + b\right)\right)\right) \cdot \left(b + \left(c - a\right)\right)\right) \cdot \left(b - \left(c - a\right)\right)} \cdot \left(a - b\right)}}{4}\\ \end{array}$
10. Final simplification0.3

$\leadsto \begin{array}{l} \mathbf{if}\;a \lt b:\\ \;\;\;\;\frac{\sqrt{\left(c + \left(b - a\right)\right) \cdot \left(\left(a + \left(c - b\right)\right) \cdot \left(\left(c + \left(a + b\right)\right) \cdot \left(a - \left(c - b\right)\right)\right)\right)}}{4}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(a - b\right) \cdot \frac{\left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right) \cdot \left(\left(b \cdot b - \left(c - a\right) \cdot \left(c - a\right)\right) \cdot \left({\left(a + b\right)}^{3} + {c}^{3}\right)\right)}{\left(b - \left(c - a\right)\right) \cdot \left(\left(\left(\left(a + b\right) \cdot \left(a + b\right) - c \cdot \left(a + b\right)\right) + c \cdot c\right) \cdot \left(\left(c - a\right) + b\right)\right)} + c \cdot \left(\left(\left(b - \left(c - a\right)\right) \cdot \left(c + \left(a + b\right)\right)\right) \cdot \left(\left(c - a\right) + b\right)\right)}}{4}\\ \end{array}$

# Reproduce

herbie shell --seed 1
(FPCore (a b c)
:name "triangleSorted"
:pre (and (<= 1.0 a 9.0) (<= 1.0 b 9.0) (<= 1.0 c 9.0) (> (+ a b) (+ c 1e-06)) (> (+ a c) (+ b 1e-06)) (> (+ b c) (+ a 1e-06)) (< a c) (< b c))
(if (< a b) (/ (sqrt (* (* (* (+ c (+ b a)) (- a (- c b))) (+ a (- c b))) (+ c (- b a)))) 4.0) (/ (sqrt (* (* (* (+ c (+ a b)) (- b (- c a))) (+ b (- c a))) (+ c (- a b)))) 4.0)))