Simplified1.8
\[\leadsto \color{blue}{\mathsf{fma}\left(y, z, \mathsf{fma}\left(a, \mathsf{fma}\left(z, b, t\right), x\right)\right)}
\]
Proof
(fma.f64 y z (fma.f64 a (fma.f64 z b t) x)): 0 points increase in error, 0 points decrease in error
(fma.f64 y z (fma.f64 a (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z b) t)) x)): 0 points increase in error, 1 points decrease in error
(fma.f64 y z (fma.f64 a (Rewrite<= +-commutative_binary64 (+.f64 t (*.f64 z b))) x)): 0 points increase in error, 0 points decrease in error
(fma.f64 y z (Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (+.f64 t (*.f64 z b))) x))): 1 points increase in error, 0 points decrease in error
(fma.f64 y z (+.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 a t) (*.f64 a (*.f64 z b)))) x)): 0 points increase in error, 0 points decrease in error
(fma.f64 y z (+.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 t a)) (*.f64 a (*.f64 z b))) x)): 0 points increase in error, 0 points decrease in error
(fma.f64 y z (+.f64 (+.f64 (*.f64 t a) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a z) b))) x)): 11 points increase in error, 15 points decrease in error
(fma.f64 y z (Rewrite<= +-commutative_binary64 (+.f64 x (+.f64 (*.f64 t a) (*.f64 (*.f64 a z) b))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 y z) (+.f64 x (+.f64 (*.f64 t a) (*.f64 (*.f64 a z) b))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 y z) x) (+.f64 (*.f64 t a) (*.f64 (*.f64 a z) b)))): 0 points increase in error, 1 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 y z))) (+.f64 (*.f64 t a) (*.f64 (*.f64 a z) b))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 x (*.f64 y z)) (*.f64 t a)) (*.f64 (*.f64 a z) b))): 0 points increase in error, 0 points decrease in error