Simplified27.7
\[\leadsto \color{blue}{\mathsf{fma}\left(j, k \cdot -27, \mathsf{fma}\left(t, \mathsf{fma}\left(x, y \cdot \left(18 \cdot z\right), a \cdot -4\right), \mathsf{fma}\left(b, c, i \cdot \left(x \cdot -4\right)\right)\right)\right)}
\]
Proof
(fma.f64 j (*.f64 k -27) (fma.f64 t (fma.f64 x (*.f64 y (*.f64 18 z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (*.f64 k (Rewrite<= metadata-eval (neg.f64 27))) (fma.f64 t (fma.f64 x (*.f64 y (*.f64 18 z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 k 27))) (fma.f64 t (fma.f64 x (*.f64 y (*.f64 18 z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 27 k))) (fma.f64 t (fma.f64 x (*.f64 y (*.f64 18 z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (fma.f64 x (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y 18) z)) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 1 points increase in error, 3 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (fma.f64 x (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 18 y)) z) (*.f64 a -4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (fma.f64 x (*.f64 (*.f64 18 y) z) (*.f64 a (Rewrite<= metadata-eval (neg.f64 4)))) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (fma.f64 x (*.f64 (*.f64 18 y) z) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4)))) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 x (*.f64 (*.f64 18 y) z)) (*.f64 a 4))) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 0 points increase in error, 1 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x (*.f64 18 y)) z)) (*.f64 a 4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 13 points increase in error, 12 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x 18) y)) z) (*.f64 a 4)) (fma.f64 b c (*.f64 i (*.f64 x -4))))): 5 points increase in error, 1 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (fma.f64 b c (*.f64 i (*.f64 x (Rewrite<= metadata-eval (neg.f64 4))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (fma.f64 b c (*.f64 i (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 x 4))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (fma.f64 b c (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 x 4)) i))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (fma.f64 b c (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 (*.f64 x 4) i)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (fma.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4)) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b c) (*.f64 (*.f64 x 4) i))))): 0 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (-.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) (*.f64 a 4))) (-.f64 (*.f64 b c) (*.f64 (*.f64 x 4) i))))): 1 points increase in error, 0 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (+.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t))) (-.f64 (*.f64 b c) (*.f64 (*.f64 x 4) i)))): 1 points increase in error, 1 points decrease in error
(fma.f64 j (neg.f64 (*.f64 27 k)) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 j (neg.f64 (*.f64 27 k))) (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)))): 2 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 j (*.f64 27 k)))) (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 j 27) k))) (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i))): 7 points increase in error, 7 points decrease in error
(+.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 (*.f64 j 27)) k)) (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)) (*.f64 (neg.f64 (*.f64 j 27)) k))): 0 points increase in error, 0 points decrease in error
(Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)) (*.f64 (*.f64 j 27) k))): 0 points increase in error, 0 points decrease in error