Average Error: 4.2 → 3.3
Time: 58.0s
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 r4364633 = 1.0;
        double r4364634 = /* ERROR: no posit support in C */;
        double r4364635 = 0.1049934947;
        double r4364636 = /* ERROR: no posit support in C */;
        double r4364637 = x;
        double r4364638 = r4364637 * r4364637;
        double r4364639 = r4364636 * r4364638;
        double r4364640 = r4364634 + r4364639;
        double r4364641 = 0.0424060604;
        double r4364642 = /* ERROR: no posit support in C */;
        double r4364643 = r4364638 * r4364638;
        double r4364644 = r4364642 * r4364643;
        double r4364645 = r4364640 + r4364644;
        double r4364646 = 0.0072644182;
        double r4364647 = /* ERROR: no posit support in C */;
        double r4364648 = r4364643 * r4364638;
        double r4364649 = r4364647 * r4364648;
        double r4364650 = r4364645 + r4364649;
        double r4364651 = 0.0005064034;
        double r4364652 = /* ERROR: no posit support in C */;
        double r4364653 = r4364648 * r4364638;
        double r4364654 = r4364652 * r4364653;
        double r4364655 = r4364650 + r4364654;
        double r4364656 = 0.0001789971;
        double r4364657 = /* ERROR: no posit support in C */;
        double r4364658 = r4364653 * r4364638;
        double r4364659 = r4364657 * r4364658;
        double r4364660 = r4364655 + r4364659;
        double r4364661 = 0.7715471019;
        double r4364662 = /* ERROR: no posit support in C */;
        double r4364663 = r4364662 * r4364638;
        double r4364664 = r4364634 + r4364663;
        double r4364665 = 0.2909738639;
        double r4364666 = /* ERROR: no posit support in C */;
        double r4364667 = r4364666 * r4364643;
        double r4364668 = r4364664 + r4364667;
        double r4364669 = 0.0694555761;
        double r4364670 = /* ERROR: no posit support in C */;
        double r4364671 = r4364670 * r4364648;
        double r4364672 = r4364668 + r4364671;
        double r4364673 = 0.0140005442;
        double r4364674 = /* ERROR: no posit support in C */;
        double r4364675 = r4364674 * r4364653;
        double r4364676 = r4364672 + r4364675;
        double r4364677 = 0.0008327945;
        double r4364678 = /* ERROR: no posit support in C */;
        double r4364679 = r4364678 * r4364658;
        double r4364680 = r4364676 + r4364679;
        double r4364681 = 2.0;
        double r4364682 = /* ERROR: no posit support in C */;
        double r4364683 = r4364682 * r4364657;
        double r4364684 = r4364658 * r4364638;
        double r4364685 = r4364683 * r4364684;
        double r4364686 = r4364680 + r4364685;
        double r4364687 = r4364660 / r4364686;
        double r4364688 = r4364687 * r4364637;
        return r4364688;
}

double f(double x) {
        double r4364689 = x;
        double r4364690 = 1.0;
        double r4364691 = 0.1049934947;
        double r4364692 = r4364689 * r4364689;
        double r4364693 = r4364691 * r4364692;
        double r4364694 = r4364690 + r4364693;
        double r4364695 = r4364692 * r4364692;
        double r4364696 = 0.0072644182;
        double r4364697 = 0.0001789971;
        double r4364698 = r4364692 * r4364697;
        double r4364699 = r4364692 * r4364698;
        double r4364700 = 0.0005064034;
        double r4364701 = r4364689 * r4364700;
        double r4364702 = r4364689 * r4364701;
        double r4364703 = r4364699 + r4364702;
        double r4364704 = r4364696 + r4364703;
        double r4364705 = r4364692 * r4364704;
        double r4364706 = 0.0424060604;
        double r4364707 = r4364705 + r4364706;
        double r4364708 = r4364695 * r4364707;
        double r4364709 = r4364694 + r4364708;
        double r4364710 = r4364689 * r4364709;
        double r4364711 = 0.0694555761;
        double r4364712 = r4364711 * r4364692;
        double r4364713 = 0.2909738639;
        double r4364714 = r4364712 + r4364713;
        double r4364715 = 2.0;
        double r4364716 = r4364692 * r4364715;
        double r4364717 = r4364697 * r4364716;
        double r4364718 = 0.0008327945;
        double r4364719 = r4364717 + r4364718;
        double r4364720 = r4364692 * r4364719;
        double r4364721 = 0.0140005442;
        double r4364722 = r4364720 + r4364721;
        double r4364723 = r4364695 * r4364722;
        double r4364724 = r4364714 + r4364723;
        double r4364725 = r4364695 * r4364724;
        double r4364726 = 0.7715471019;
        double r4364727 = r4364726 * r4364692;
        double r4364728 = r4364727 + r4364690;
        double r4364729 = r4364725 + r4364728;
        double r4364730 = r4364710 / r4364729;
        return r4364730;
}

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 +o rules:numerics
(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))