Simplified1.0
\[\leadsto \mathsf{copysign}\left(\color{blue}{\mathsf{fma}\left(\frac{-0.125}{1 + x} + \frac{-0.125}{{\left(1 + x\right)}^{2}}, {x}^{4}, \mathsf{fma}\left(0.5, \frac{x \cdot x}{1 + x}, \mathsf{log1p}\left(x\right)\right)\right)}, x\right)
\]
Proof
(fma.f64 (+.f64 (/.f64 -1/8 (+.f64 1 x)) (/.f64 -1/8 (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 3 -1/24)) (+.f64 1 x)) (/.f64 -1/8 (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (/.f64 (*.f64 3 -1/24) (+.f64 1 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 x) (sqrt.f64 x))))) (/.f64 -1/8 (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 69 points increase in error, 6 points decrease in error
(fma.f64 (+.f64 (/.f64 (*.f64 3 -1/24) (+.f64 1 (Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (sqrt.f64 x) (sqrt.f64 x)))))) (/.f64 -1/8 (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (/.f64 (*.f64 3 -1/24) (+.f64 1 (fabs.f64 (Rewrite=> rem-square-sqrt_binary64 x)))) (/.f64 -1/8 (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 6 points increase in error, 69 points decrease in error
(fma.f64 (+.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 3 (+.f64 1 (fabs.f64 x))) -1/24)) (/.f64 -1/8 (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 2 points decrease in error
(fma.f64 (+.f64 (*.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 3 1)) (+.f64 1 (fabs.f64 x))) -1/24) (/.f64 -1/8 (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (*.f64 (Rewrite<= associate-*r/_binary64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x))))) -1/24) (/.f64 -1/8 (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 2 points increase in error, 4 points decrease in error
(fma.f64 (+.f64 (*.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) -1/24) (/.f64 (Rewrite<= metadata-eval (*.f64 3 -1/24)) (pow.f64 (+.f64 1 x) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (*.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) -1/24) (/.f64 (*.f64 3 -1/24) (pow.f64 (+.f64 1 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 x) (sqrt.f64 x)))) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 65 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (*.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) -1/24) (/.f64 (*.f64 3 -1/24) (pow.f64 (+.f64 1 (Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (sqrt.f64 x) (sqrt.f64 x))))) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (*.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) -1/24) (/.f64 (*.f64 3 -1/24) (pow.f64 (+.f64 1 (fabs.f64 (Rewrite=> rem-square-sqrt_binary64 x))) 2))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 65 points decrease in error
(fma.f64 (+.f64 (*.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) -1/24) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 3 (pow.f64 (+.f64 1 (fabs.f64 x)) 2)) -1/24))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (*.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) -1/24) (*.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 3 1)) (pow.f64 (+.f64 1 (fabs.f64 x)) 2)) -1/24)) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (+.f64 (*.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) -1/24) (*.f64 (Rewrite<= associate-*r/_binary64 (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2)))) -1/24)) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2)))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (*.f64 x x) (+.f64 1 x)) (log1p.f64 x))): 1 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) (+.f64 1 x)) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 x) (sqrt.f64 x))))) (log1p.f64 x))): 65 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (sqrt.f64 x) (sqrt.f64 x)))))) (log1p.f64 x))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (fabs.f64 (Rewrite=> rem-square-sqrt_binary64 x)))) (log1p.f64 x))): 0 points increase in error, 65 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (fabs.f64 x))) (log1p.f64 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 x) (sqrt.f64 x)))))): 110 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (fabs.f64 x))) (log1p.f64 (Rewrite<= fabs-sqr_binary64 (fabs.f64 (*.f64 (sqrt.f64 x) (sqrt.f64 x))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (fabs.f64 x))) (log1p.f64 (fabs.f64 (Rewrite=> rem-square-sqrt_binary64 x))))): 0 points increase in error, 123 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (fma.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (fabs.f64 x))) (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 (fabs.f64 x)))))): 77 points increase in error, 64 points decrease in error
(fma.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (fabs.f64 x)))) (log.f64 (+.f64 1 (fabs.f64 x)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 -1/24 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2))))) (pow.f64 x 4)) (+.f64 (*.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (fabs.f64 x)))) (log.f64 (+.f64 1 (fabs.f64 x)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1/24 (*.f64 (+.f64 (*.f64 3 (/.f64 1 (+.f64 1 (fabs.f64 x)))) (*.f64 3 (/.f64 1 (pow.f64 (+.f64 1 (fabs.f64 x)) 2)))) (pow.f64 x 4)))) (+.f64 (*.f64 1/2 (/.f64 (pow.f64 x 2) (+.f64 1 (fabs.f64 x)))) (log.f64 (+.f64 1 (fabs.f64 x))))): 2 points increase in error, 6 points decrease in error