Simplified1.5
\[\leadsto \color{blue}{\mathsf{fma}\left(-0.16666666666666666, \left(\frac{{c}^{4}}{{b}^{6}} \cdot 6.328125\right) \cdot \frac{{a}^{3}}{b}, \mathsf{fma}\left(-0.5625, \left(a \cdot a\right) \cdot \frac{{c}^{3}}{{b}^{5}}, \mathsf{fma}\left(-0.375, a \cdot \frac{c \cdot c}{{b}^{3}}, \frac{c}{\frac{b}{-0.5}}\right)\right)\right)}
\]
Proof
(fma.f64 -1/6 (*.f64 (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) 405/64) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) (Rewrite<= metadata-eval (+.f64 81/16 81/64))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (*.f64 (/.f64 (pow.f64 c 4) (pow.f64 b 6)) (+.f64 81/16 (Rewrite<= metadata-eval (*.f64 -9/8 -9/8)))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -9/8 -9/8) (/.f64 (pow.f64 c 4) (pow.f64 b 6))))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -9/8 -9/8) (/.f64 (pow.f64 c (Rewrite<= metadata-eval (*.f64 2 2))) (pow.f64 b 6)))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -9/8 -9/8) (/.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 c 2) (pow.f64 c 2))) (pow.f64 b 6)))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -9/8 -9/8) (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (pow.f64 b (Rewrite<= metadata-eval (*.f64 2 3)))))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -9/8 -9/8) (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 b 3) (pow.f64 b 3)))))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (*.f64 (*.f64 -9/8 -9/8) (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (pow.f64 c 2) (pow.f64 b 3)) (/.f64 (pow.f64 c 2) (pow.f64 b 3)))))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3)))))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (*.f64 (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (Rewrite<= unpow2_binary64 (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) (/.f64 (pow.f64 a 3) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 a 3) b) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2)))) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (fma.f64 -9/16 (*.f64 (*.f64 a a) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 a 2)) (/.f64 (pow.f64 c 3) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (pow.f64 a 2))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (fma.f64 -3/8 (*.f64 a (/.f64 (*.f64 c c) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (fma.f64 -3/8 (*.f64 a (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (fma.f64 -3/8 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 c 2) (pow.f64 b 3)) a)) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (fma.f64 -3/8 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (/.f64 c (/.f64 b -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c -1/2) b))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 c b) -1/2))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (Rewrite<= *-commutative_binary64 (*.f64 -1/2 (/.f64 c b)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -1/2 (/.f64 c b)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 a 3) (+.f64 (*.f64 81/16 (/.f64 (pow.f64 c 4) (pow.f64 b 6))) (pow.f64 (*.f64 -9/8 (/.f64 (pow.f64 c 2) (pow.f64 b 3))) 2))) b)) (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 0 points decrease in error