Average Error: 1.8 → 0.5
Time: 2.3m
Precision: 64
Internal Precision: 384
\[\sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]
↓
\[\sqrt{\sqrt[3]{{\left(\frac{\left(b + a\right) + c}{\frac{2}{\frac{1}{2}}}\right)}^{3} \cdot \left(\left({\left(\left(a - b\right) + c\right)}^{3} \cdot {\left(\left(a - c\right) + b\right)}^{3}\right) \cdot {\left(\left(b - \left(a - c\right)\right) \cdot \left(\frac{1}{2} \cdot \frac{1}{2}\right)\right)}^{3}\right)}}\]

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

  1. Initial program 1.8

    \[\sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]

  2. Taylor expanded around 0 1.6

    \[\leadsto \sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \color{blue}{\left(\left(\frac{1}{2} \cdot b + \frac{1}{2} \cdot a\right) - \frac{1}{2} \cdot c\right)}}\]

  3. Applied simplify1.5

    \[\leadsto \color{blue}{\sqrt{\left(\left(\frac{a + \left(c + b\right)}{2} - a\right) \cdot \left(\frac{1}{2} \cdot \frac{a + \left(c + b\right)}{2}\right)\right) \cdot \left(\left(\frac{a + \left(c + b\right)}{2} - b\right) \cdot \left(a - \left(c - b\right)\right)\right)}}\]

  4. Taylor expanded around 0 1.1

    \[\leadsto \sqrt{\left(\left(\frac{a + \left(c + b\right)}{2} - a\right) \cdot \left(\frac{1}{2} \cdot \frac{a + \left(c + b\right)}{2}\right)\right) \cdot \left(\color{blue}{\left(\left(\frac{1}{2} \cdot c + \frac{1}{2} \cdot a\right) - \frac{1}{2} \cdot b\right)} \cdot \left(a - \left(c - b\right)\right)\right)}\]

  5. Applied simplify1.1

    \[\leadsto \color{blue}{\sqrt{\left(\frac{1}{2} \cdot \left(\frac{a + \left(c + b\right)}{2} - a\right)\right) \cdot \left(\left(\left(\frac{1}{2} \cdot \left(c + \left(a - b\right)\right)\right) \cdot \frac{a + \left(c + b\right)}{2}\right) \cdot \left(\left(a + b\right) - c\right)\right)}}\]

  6. Taylor expanded around 0 0.9

    \[\leadsto \sqrt{\left(\frac{1}{2} \cdot \color{blue}{\left(\left(\frac{1}{2} \cdot b + \frac{1}{2} \cdot c\right) - \frac{1}{2} \cdot a\right)}\right) \cdot \left(\left(\left(\frac{1}{2} \cdot \left(c + \left(a - b\right)\right)\right) \cdot \frac{a + \left(c + b\right)}{2}\right) \cdot \left(\left(a + b\right) - c\right)\right)}\]

  7. Applied simplify0.4

    \[\leadsto \color{blue}{\sqrt{\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\left(\left(b + \left(a - c\right)\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \frac{b + \left(a + c\right)}{\frac{2}{\frac{1}{2}}}\right)}}\]
  8. Using strategy rm

  9. Applied add-cbrt-cube0.4

    \[\leadsto \sqrt{\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\left(\left(b + \left(a - c\right)\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \frac{b + \left(a + c\right)}{\color{blue}{\sqrt[3]{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}}}\right)}\]

  10. Applied add-cbrt-cube0.5

    \[\leadsto \sqrt{\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\left(\left(b + \left(a - c\right)\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \frac{\color{blue}{\sqrt[3]{\left(\left(b + \left(a + c\right)\right) \cdot \left(b + \left(a + c\right)\right)\right) \cdot \left(b + \left(a + c\right)\right)}}}{\sqrt[3]{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}}\right)}\]

  11. Applied cbrt-undiv0.5

    \[\leadsto \sqrt{\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\left(\left(b + \left(a - c\right)\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \color{blue}{\sqrt[3]{\frac{\left(\left(b + \left(a + c\right)\right) \cdot \left(b + \left(a + c\right)\right)\right) \cdot \left(b + \left(a + c\right)\right)}{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}}}\right)}\]

  12. Applied add-cbrt-cube0.6

    \[\leadsto \sqrt{\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\left(\left(b + \left(a - c\right)\right) \cdot \color{blue}{\sqrt[3]{\left(\left(\left(a - b\right) + c\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \left(\left(a - b\right) + c\right)}}\right) \cdot \sqrt[3]{\frac{\left(\left(b + \left(a + c\right)\right) \cdot \left(b + \left(a + c\right)\right)\right) \cdot \left(b + \left(a + c\right)\right)}{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}}\right)}\]

  13. Applied add-cbrt-cube0.7

    \[\leadsto \sqrt{\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\left(\color{blue}{\sqrt[3]{\left(\left(b + \left(a - c\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(b + \left(a - c\right)\right)}} \cdot \sqrt[3]{\left(\left(\left(a - b\right) + c\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \left(\left(a - b\right) + c\right)}\right) \cdot \sqrt[3]{\frac{\left(\left(b + \left(a + c\right)\right) \cdot \left(b + \left(a + c\right)\right)\right) \cdot \left(b + \left(a + c\right)\right)}{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}}\right)}\]

  14. Applied cbrt-unprod0.6

    \[\leadsto \sqrt{\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\color{blue}{\sqrt[3]{\left(\left(\left(b + \left(a - c\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(\left(\left(\left(a - b\right) + c\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \left(\left(a - b\right) + c\right)\right)}} \cdot \sqrt[3]{\frac{\left(\left(b + \left(a + c\right)\right) \cdot \left(b + \left(a + c\right)\right)\right) \cdot \left(b + \left(a + c\right)\right)}{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}}\right)}\]

  15. Applied cbrt-unprod0.5

    \[\leadsto \sqrt{\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \color{blue}{\sqrt[3]{\left(\left(\left(\left(b + \left(a - c\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(\left(\left(\left(a - b\right) + c\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \left(\left(a - b\right) + c\right)\right)\right) \cdot \frac{\left(\left(b + \left(a + c\right)\right) \cdot \left(b + \left(a + c\right)\right)\right) \cdot \left(b + \left(a + c\right)\right)}{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}}}}\]

  16. Applied add-cbrt-cube0.6

    \[\leadsto \sqrt{\color{blue}{\sqrt[3]{\left(\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right)\right) \cdot \left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right)}} \cdot \sqrt[3]{\left(\left(\left(\left(b + \left(a - c\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(\left(\left(\left(a - b\right) + c\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \left(\left(a - b\right) + c\right)\right)\right) \cdot \frac{\left(\left(b + \left(a + c\right)\right) \cdot \left(b + \left(a + c\right)\right)\right) \cdot \left(b + \left(a + c\right)\right)}{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}}}\]

  17. Applied cbrt-unprod0.5

    \[\leadsto \sqrt{\color{blue}{\sqrt[3]{\left(\left(\left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right) \cdot \left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right)\right) \cdot \left(\left(\frac{1}{2} \cdot \frac{1}{2}\right) \cdot \left(c + \left(b - a\right)\right)\right)\right) \cdot \left(\left(\left(\left(\left(b + \left(a - c\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(b + \left(a - c\right)\right)\right) \cdot \left(\left(\left(\left(a - b\right) + c\right) \cdot \left(\left(a - b\right) + c\right)\right) \cdot \left(\left(a - b\right) + c\right)\right)\right) \cdot \frac{\left(\left(b + \left(a + c\right)\right) \cdot \left(b + \left(a + c\right)\right)\right) \cdot \left(b + \left(a + c\right)\right)}{\left(\frac{2}{\frac{1}{2}} \cdot \frac{2}{\frac{1}{2}}\right) \cdot \frac{2}{\frac{1}{2}}}\right)}}}\]

  18. Applied simplify0.5

    \[\leadsto \sqrt{\sqrt[3]{\color{blue}{{\left(\frac{\left(b + a\right) + c}{\frac{2}{\frac{1}{2}}}\right)}^{3} \cdot \left(\left({\left(\left(a - b\right) + c\right)}^{3} \cdot {\left(\left(a - c\right) + b\right)}^{3}\right) \cdot {\left(\left(b - \left(a - c\right)\right) \cdot \left(\frac{1}{2} \cdot \frac{1}{2}\right)\right)}^{3}\right)}}}\]

Runtime

Time bar (total: 2.3m)Debug log

herbie shell --seed '#(1743936871 1855164119 3668777427 1254258049 132811564 1366975197)' 
(FPCore (a b c)
  :name "triangle12"
  :pre (and (<= 1 a 9) (<= 1 b 9) (<= 1 c 9) (> (+ a b) (+ c 1e-12)) (> (+ a c) (+ b 1e-12)) (> (+ b c) (+ a 1e-12)))
  (sqrt (* (* (* (/ (+ (+ a b) c) 2) (- (/ (+ (+ a b) c) 2) a)) (- (/ (+ (+ a b) c) 2) b)) (- (/ (+ (+ a b) c) 2) c))))