Simplified51.9
\[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, C - A\right)}{B}\right)}{\pi}}
\]
Proof
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (hypot.f64 B (-.f64 C A))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 C A) (-.f64 C A)))))) B)) (PI.f64))): 91 points increase in error, 21 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 C A) (-.f64 C A))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= sqr-neg_binary64 (*.f64 (neg.f64 (-.f64 C A)) (neg.f64 (-.f64 C A))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 C A))) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 C) A)) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 C)) A) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 A (neg.f64 C))) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 A C)) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 C A))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 C) A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 C)) A))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= +-commutative_binary64 (+.f64 A (neg.f64 C))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= sub-neg_binary64 (-.f64 A C)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (PI.f64))): 1 points increase in error, 0 points decrease in error
Simplified1.3
\[\leadsto \color{blue}{\tan^{-1} \left(0.5 \cdot \frac{B}{A - C}\right) \cdot \frac{180}{\pi}}
\]
Proof
(*.f64 (atan.f64 (*.f64 1/2 (/.f64 B (-.f64 A C)))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (*.f64 1/2 (/.f64 B (Rewrite<= unsub-neg_binary64 (+.f64 A (neg.f64 C)))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (*.f64 1/2 (/.f64 B (+.f64 A (Rewrite<= mul-1-neg_binary64 (*.f64 -1 C)))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 1/2 B) (+.f64 A (*.f64 -1 C))))) (/.f64 180 (PI.f64))): 0 points increase in error, 2 points decrease in error
(*.f64 (atan.f64 (/.f64 (*.f64 1/2 B) (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 C) A)))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (*.f64 1/2 B) (+.f64 (*.f64 -1 C) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 A)))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (*.f64 1/2 B) (+.f64 (*.f64 -1 C) (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 A)))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (*.f64 1/2 B) (Rewrite=> unsub-neg_binary64 (-.f64 (*.f64 -1 C) (*.f64 -1 A))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (*.f64 1/2 B) (Rewrite=> distribute-lft-out--_binary64 (*.f64 -1 (-.f64 C A))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 1/2 -1) (/.f64 B (-.f64 C A))))) (/.f64 180 (PI.f64))): 2 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (*.f64 (Rewrite=> metadata-eval -1/2) (/.f64 B (-.f64 C A)))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (*.f64 -1/2 (/.f64 B (Rewrite=> sub-neg_binary64 (+.f64 C (neg.f64 A)))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (*.f64 -1/2 (/.f64 B (+.f64 C (Rewrite<= mul-1-neg_binary64 (*.f64 -1 A)))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (*.f64 -1/2 (/.f64 B (+.f64 C (Rewrite=> mul-1-neg_binary64 (neg.f64 A)))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (*.f64 -1/2 (/.f64 B (Rewrite<= sub-neg_binary64 (-.f64 C A))))) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 180 (PI.f64)) (atan.f64 (*.f64 -1/2 (/.f64 B (-.f64 C A)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 180 (/.f64 (PI.f64) (atan.f64 (*.f64 -1/2 (/.f64 B (-.f64 C A))))))): 25 points increase in error, 19 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (*.f64 -1/2 (/.f64 B (Rewrite=> sub-neg_binary64 (+.f64 C (neg.f64 A)))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (*.f64 -1/2 (/.f64 B (+.f64 C (Rewrite<= mul-1-neg_binary64 (*.f64 -1 A)))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 1/2 -1)) (/.f64 B (+.f64 C (*.f64 -1 A))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (*.f64 (/.f64 1/2 -1) (/.f64 B (+.f64 C (Rewrite=> mul-1-neg_binary64 (neg.f64 A)))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (*.f64 (/.f64 1/2 -1) (/.f64 B (Rewrite<= sub-neg_binary64 (-.f64 C A))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 1/2 B) (*.f64 -1 (-.f64 C A))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (/.f64 (*.f64 1/2 B) (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 C) (*.f64 -1 A))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (/.f64 (*.f64 1/2 B) (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 C) (neg.f64 (*.f64 -1 A)))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (/.f64 (*.f64 1/2 B) (+.f64 (*.f64 -1 C) (neg.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 A)))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (/.f64 (*.f64 1/2 B) (+.f64 (*.f64 -1 C) (Rewrite=> remove-double-neg_binary64 A)))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (/.f64 (*.f64 1/2 B) (Rewrite<= +-commutative_binary64 (+.f64 A (*.f64 -1 C))))))): 0 points increase in error, 0 points decrease in error
(/.f64 180 (/.f64 (PI.f64) (atan.f64 (Rewrite<= associate-*r/_binary64 (*.f64 1/2 (/.f64 B (+.f64 A (*.f64 -1 C)))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 180 (atan.f64 (*.f64 1/2 (/.f64 B (+.f64 A (*.f64 -1 C)))))) (PI.f64))): 29 points increase in error, 26 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 180 (/.f64 (atan.f64 (*.f64 1/2 (/.f64 B (+.f64 A (*.f64 -1 C))))) (PI.f64)))): 27 points increase in error, 29 points decrease in error