Average Error: 4.2 → 3.3
Time: 57.2s
Precision: 64
\[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x\]
↓
\[\frac{x \cdot \left(\left(1 + 0.1049934947 \cdot \left(x \cdot x\right)\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0072644182 + \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971\right) + x \cdot \left(x \cdot 0.0005064034\right)\right)\right) + 0.0424060604\right)\right)}{\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(0.0694555761 \cdot \left(x \cdot x\right) + 0.2909738639\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0001789971 \cdot \left(\left(x \cdot x\right) \cdot 2\right) + 0.0008327945\right) + 0.0140005442\right)\right) + \left(0.7715471019 \cdot \left(x \cdot x\right) + 1\right)}\]
\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x
↓
\frac{x \cdot \left(\left(1 + 0.1049934947 \cdot \left(x \cdot x\right)\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0072644182 + \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971\right) + x \cdot \left(x \cdot 0.0005064034\right)\right)\right) + 0.0424060604\right)\right)}{\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(0.0694555761 \cdot \left(x \cdot x\right) + 0.2909738639\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0001789971 \cdot \left(\left(x \cdot x\right) \cdot 2\right) + 0.0008327945\right) + 0.0140005442\right)\right) + \left(0.7715471019 \cdot \left(x \cdot x\right) + 1\right)}
double f(double x) {
        double r6714462 = 1.0;
        double r6714463 = /* ERROR: no posit support in C */;
        double r6714464 = 0.1049934947;
        double r6714465 = /* ERROR: no posit support in C */;
        double r6714466 = x;
        double r6714467 = r6714466 * r6714466;
        double r6714468 = r6714465 * r6714467;
        double r6714469 = r6714463 + r6714468;
        double r6714470 = 0.0424060604;
        double r6714471 = /* ERROR: no posit support in C */;
        double r6714472 = r6714467 * r6714467;
        double r6714473 = r6714471 * r6714472;
        double r6714474 = r6714469 + r6714473;
        double r6714475 = 0.0072644182;
        double r6714476 = /* ERROR: no posit support in C */;
        double r6714477 = r6714472 * r6714467;
        double r6714478 = r6714476 * r6714477;
        double r6714479 = r6714474 + r6714478;
        double r6714480 = 0.0005064034;
        double r6714481 = /* ERROR: no posit support in C */;
        double r6714482 = r6714477 * r6714467;
        double r6714483 = r6714481 * r6714482;
        double r6714484 = r6714479 + r6714483;
        double r6714485 = 0.0001789971;
        double r6714486 = /* ERROR: no posit support in C */;
        double r6714487 = r6714482 * r6714467;
        double r6714488 = r6714486 * r6714487;
        double r6714489 = r6714484 + r6714488;
        double r6714490 = 0.7715471019;
        double r6714491 = /* ERROR: no posit support in C */;
        double r6714492 = r6714491 * r6714467;
        double r6714493 = r6714463 + r6714492;
        double r6714494 = 0.2909738639;
        double r6714495 = /* ERROR: no posit support in C */;
        double r6714496 = r6714495 * r6714472;
        double r6714497 = r6714493 + r6714496;
        double r6714498 = 0.0694555761;
        double r6714499 = /* ERROR: no posit support in C */;
        double r6714500 = r6714499 * r6714477;
        double r6714501 = r6714497 + r6714500;
        double r6714502 = 0.0140005442;
        double r6714503 = /* ERROR: no posit support in C */;
        double r6714504 = r6714503 * r6714482;
        double r6714505 = r6714501 + r6714504;
        double r6714506 = 0.0008327945;
        double r6714507 = /* ERROR: no posit support in C */;
        double r6714508 = r6714507 * r6714487;
        double r6714509 = r6714505 + r6714508;
        double r6714510 = 2.0;
        double r6714511 = /* ERROR: no posit support in C */;
        double r6714512 = r6714511 * r6714486;
        double r6714513 = r6714487 * r6714467;
        double r6714514 = r6714512 * r6714513;
        double r6714515 = r6714509 + r6714514;
        double r6714516 = r6714489 / r6714515;
        double r6714517 = r6714516 * r6714466;
        return r6714517;
}
↓
double f(double x) {
        double r6714518 = x;
        double r6714519 = 1.0;
        double r6714520 = 0.1049934947;
        double r6714521 = r6714518 * r6714518;
        double r6714522 = r6714520 * r6714521;
        double r6714523 = r6714519 + r6714522;
        double r6714524 = r6714521 * r6714521;
        double r6714525 = 0.0072644182;
        double r6714526 = 0.0001789971;
        double r6714527 = r6714521 * r6714526;
        double r6714528 = r6714521 * r6714527;
        double r6714529 = 0.0005064034;
        double r6714530 = r6714518 * r6714529;
        double r6714531 = r6714518 * r6714530;
        double r6714532 = r6714528 + r6714531;
        double r6714533 = r6714525 + r6714532;
        double r6714534 = r6714521 * r6714533;
        double r6714535 = 0.0424060604;
        double r6714536 = r6714534 + r6714535;
        double r6714537 = r6714524 * r6714536;
        double r6714538 = r6714523 + r6714537;
        double r6714539 = r6714518 * r6714538;
        double r6714540 = 0.0694555761;
        double r6714541 = r6714540 * r6714521;
        double r6714542 = 0.2909738639;
        double r6714543 = r6714541 + r6714542;
        double r6714544 = 2.0;
        double r6714545 = r6714521 * r6714544;
        double r6714546 = r6714526 * r6714545;
        double r6714547 = 0.0008327945;
        double r6714548 = r6714546 + r6714547;
        double r6714549 = r6714521 * r6714548;
        double r6714550 = 0.0140005442;
        double r6714551 = r6714549 + r6714550;
        double r6714552 = r6714524 * r6714551;
        double r6714553 = r6714543 + r6714552;
        double r6714554 = r6714524 * r6714553;
        double r6714555 = 0.7715471019;
        double r6714556 = r6714555 * r6714521;
        double r6714557 = r6714556 + r6714519;
        double r6714558 = r6714554 + r6714557;
        double r6714559 = r6714539 / r6714558;
        return r6714559;
}

Error

Bits error versus x

Derivation

  1. Initial program 4.2

    \[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x\]

  2. Simplified3.6

    \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}{\left(0.0005064034\right)}\right)\right)}{\left(\frac{\left(0.0424060604\right)}{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\right)}\right)}\right)\right)}{\left(1\right)}\right)}{\left(\left(x \cdot x\right) \cdot \left(0.1049934947\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(0.0001789971\right) \cdot \left(\left(2\right) \cdot \left(x \cdot x\right)\right)\right)}{\left(0.0008327945\right)}\right)\right)}{\left(0.0140005442\right)}\right)\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)\right)}\right)}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}\right)}\right)}\right) \cdot x}\]

  3. Simplified3.3

    \[\leadsto \color{blue}{\frac{\left(x \cdot \left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0072644182\right)}{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0001789971\right)\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0005064034\right)\right)}\right)}\right)\right)}{\left(0.0424060604\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0694555761\right) \cdot \left(x \cdot x\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(0.0001789971\right) \cdot \left(\left(x \cdot x\right) \cdot \left(2\right)\right)\right)}{\left(0.0008327945\right)}\right)\right)}{\left(0.0140005442\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}{\left(1\right)}\right)}\right)}}\]
  4. Using strategy rm

  5. Applied associate-*l*3.3

    \[\leadsto \frac{\left(x \cdot \left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0072644182\right)}{\left(\frac{\color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)\right)}}{\left(\left(x \cdot x\right) \cdot \left(0.0005064034\right)\right)}\right)}\right)\right)}{\left(0.0424060604\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0694555761\right) \cdot \left(x \cdot x\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(0.0001789971\right) \cdot \left(\left(x \cdot x\right) \cdot \left(2\right)\right)\right)}{\left(0.0008327945\right)}\right)\right)}{\left(0.0140005442\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}{\left(1\right)}\right)}\right)}\]
  6. Using strategy rm

  7. Applied associate-*l*3.3

    \[\leadsto \frac{\left(x \cdot \left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0072644182\right)}{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)\right)}{\color{blue}{\left(x \cdot \left(x \cdot \left(0.0005064034\right)\right)\right)}}\right)}\right)\right)}{\left(0.0424060604\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0694555761\right) \cdot \left(x \cdot x\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(0.0001789971\right) \cdot \left(\left(x \cdot x\right) \cdot \left(2\right)\right)\right)}{\left(0.0008327945\right)}\right)\right)}{\left(0.0140005442\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}{\left(1\right)}\right)}\right)}\]

  8. Final simplification3.3

    \[\leadsto \frac{x \cdot \left(\left(1 + 0.1049934947 \cdot \left(x \cdot x\right)\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0072644182 + \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971\right) + x \cdot \left(x \cdot 0.0005064034\right)\right)\right) + 0.0424060604\right)\right)}{\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(0.0694555761 \cdot \left(x \cdot x\right) + 0.2909738639\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(0.0001789971 \cdot \left(\left(x \cdot x\right) \cdot 2\right) + 0.0008327945\right) + 0.0140005442\right)\right) + \left(0.7715471019 \cdot \left(x \cdot x\right) + 1\right)}\]

Reproduce

herbie shell --seed 2019133 
(FPCore (x)
  :name "Jmat.Real.dawson"
  (*.p16 (/.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0072644182) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.7715471019) (*.p16 x x))) (*.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0694555761) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x))))) x))