0.002 * [progress]: [Phase 1 of 3] Setting up.
0.003 * * * [progress]: [1/2] Preparing points
0.005 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.006 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.079 * * * * [points]: Setting MPFR precision to 64
0.084 * * * * [points]: Setting MPFR precision to 320
0.086 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.089 * * * * [points]: Setting MPFR precision to 64
0.093 * * * * [points]: Setting MPFR precision to 320
0.095 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.097 * * * * [points]: Setting MPFR precision to 64
0.100 * * * * [points]: Setting MPFR precision to 320
0.103 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.105 * * * * [points]: Setting MPFR precision to 64
0.111 * * * * [points]: Setting MPFR precision to 320
0.116 * * * * [points]: Computing exacts for 256 points
0.117 * * * * [points]: Setting MPFR precision to 64
0.172 * * * * [points]: Setting MPFR precision to 320
0.203 * * * * [points]: Filtering points with unrepresentable outputs
0.205 * * * * [points]: Sampled 256 points with exact outputs
0.205 * * * [progress]: [2/2] Setting up program.
0.268 * [progress]: [Phase 2 of 3] Improving.
0.269 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
0.271 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.273 * * [simplify]: iters left: 5 (10 enodes)
0.382 * * [simplify]: iters left: 4 (31 enodes)
0.390 * * [simplify]: iters left: 3 (65 enodes)
0.405 * * [simplify]: iters left: 2 (207 enodes)
0.512 * * [simplify]: Extracting #0: cost 1 inf + 0
0.512 * * [simplify]: Extracting #1: cost 20 inf + 0
0.513 * * [simplify]: Extracting #2: cost 89 inf + 1
0.514 * * [simplify]: Extracting #3: cost 168 inf + 83
0.516 * * [simplify]: Extracting #4: cost 225 inf + 14445
0.524 * * [simplify]: Extracting #5: cost 184 inf + 98236
0.545 * * [simplify]: Extracting #6: cost 61 inf + 344560
0.563 * * [simplify]: Extracting #7: cost 0 inf + 437130
0.582 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
0.583 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
0.604 * * [progress]: iteration 1 / 4
0.604 * * * [progress]: picking best candidate
0.626 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
0.626 * * * [progress]: localizing error
0.838 * * * [progress]: generating rewritten candidates
0.839 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.842 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
0.842 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
0.845 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
0.849 * * * [progress]: generating series expansions
0.849 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.850 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
0.850 * * * * [progress]: [ 3 / 4 ] generating series at (2)
0.850 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
0.850 * * * [progress]: simplifying candidates
0.850 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (neg.p16 b_2) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
0.850 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
0.850 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
0.850 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
0.850 * * [simplify]: iters left: 5 (11 enodes)
0.853 * * [simplify]: iters left: 4 (35 enodes)
0.860 * * [simplify]: iters left: 3 (100 enodes)
0.885 * * [simplify]: iters left: 2 (360 enodes)
1.169 * * [simplify]: Extracting #0: cost 1 inf + 0
1.169 * * [simplify]: Extracting #1: cost 48 inf + 0
1.169 * * [simplify]: Extracting #2: cost 223 inf + 0
1.172 * * [simplify]: Extracting #3: cost 352 inf + 43275
1.196 * * [simplify]: Extracting #4: cost 318 inf + 335486
1.267 * * [simplify]: Extracting #5: cost 88 inf + 853833
1.359 * * [simplify]: Extracting #6: cost 1 inf + 996140
1.445 * * [simplify]: Extracting #7: cost 0 inf + 998783
1.525 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2))))
1.525 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))
1.526 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c))))) a))>
1.526 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
1.526 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1.526 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.526 * * [simplify]: iters left: 5 (10 enodes)
1.528 * * [simplify]: iters left: 4 (31 enodes)
1.533 * * [simplify]: iters left: 3 (65 enodes)
1.545 * * [simplify]: iters left: 2 (207 enodes)
1.631 * * [simplify]: Extracting #0: cost 1 inf + 0
1.631 * * [simplify]: Extracting #1: cost 20 inf + 0
1.632 * * [simplify]: Extracting #2: cost 89 inf + 1
1.633 * * [simplify]: Extracting #3: cost 168 inf + 83
1.635 * * [simplify]: Extracting #4: cost 225 inf + 14445
1.641 * * [simplify]: Extracting #5: cost 184 inf + 98236
1.665 * * [simplify]: Extracting #6: cost 61 inf + 344560
1.698 * * [simplify]: Extracting #7: cost 0 inf + 437130
1.725 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.725 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
1.725 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1.725 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.725 * * [simplify]: iters left: 5 (10 enodes)
1.727 * * [simplify]: iters left: 4 (31 enodes)
1.732 * * [simplify]: iters left: 3 (65 enodes)
1.745 * * [simplify]: iters left: 2 (207 enodes)
1.859 * * [simplify]: Extracting #0: cost 1 inf + 0
1.859 * * [simplify]: Extracting #1: cost 20 inf + 0
1.859 * * [simplify]: Extracting #2: cost 89 inf + 1
1.860 * * [simplify]: Extracting #3: cost 168 inf + 83
1.862 * * [simplify]: Extracting #4: cost 225 inf + 14445
1.869 * * [simplify]: Extracting #5: cost 184 inf + 98236
1.893 * * [simplify]: Extracting #6: cost 61 inf + 344560
1.927 * * [simplify]: Extracting #7: cost 0 inf + 437130
1.960 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.961 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
1.961 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1.961 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.961 * * [simplify]: iters left: 5 (10 enodes)
1.965 * * [simplify]: iters left: 4 (31 enodes)
1.976 * * [simplify]: iters left: 3 (65 enodes)
1.989 * * [simplify]: iters left: 2 (207 enodes)
2.062 * * [simplify]: Extracting #0: cost 1 inf + 0
2.063 * * [simplify]: Extracting #1: cost 20 inf + 0
2.063 * * [simplify]: Extracting #2: cost 89 inf + 1
2.064 * * [simplify]: Extracting #3: cost 168 inf + 83
2.066 * * [simplify]: Extracting #4: cost 225 inf + 14445
2.072 * * [simplify]: Extracting #5: cost 184 inf + 98236
2.096 * * [simplify]: Extracting #6: cost 61 inf + 344560
2.128 * * [simplify]: Extracting #7: cost 0 inf + 437130
2.154 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.154 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
2.154 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
2.154 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.155 * * [simplify]: iters left: 5 (10 enodes)
2.157 * * [simplify]: iters left: 4 (31 enodes)
2.162 * * [simplify]: iters left: 3 (65 enodes)
2.179 * * [simplify]: iters left: 2 (207 enodes)
2.282 * * [simplify]: Extracting #0: cost 1 inf + 0
2.282 * * [simplify]: Extracting #1: cost 20 inf + 0
2.282 * * [simplify]: Extracting #2: cost 89 inf + 1
2.283 * * [simplify]: Extracting #3: cost 168 inf + 83
2.284 * * [simplify]: Extracting #4: cost 225 inf + 14445
2.289 * * [simplify]: Extracting #5: cost 184 inf + 98236
2.302 * * [simplify]: Extracting #6: cost 61 inf + 344560
2.332 * * [simplify]: Extracting #7: cost 0 inf + 437130
2.367 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.367 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
2.367 * * * [progress]: adding candidates to table
2.542 * * [progress]: iteration 2 / 4
2.542 * * * [progress]: picking best candidate
2.591 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
2.591 * * * [progress]: localizing error
2.844 * * * [progress]: generating rewritten candidates
2.844 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
2.849 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
2.854 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2)
2.854 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2 1)
2.857 * * * [progress]: generating series expansions
2.857 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
2.857 * * * * [progress]: [ 2 / 4 ] generating series at (2)
2.857 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2)
2.857 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2 1)
2.857 * * * [progress]: simplifying candidates
2.857 * * * * [progress]: [ 1 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (neg.p16 b_2)))))>
2.857 * * * * [progress]: [ 2 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
2.857 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
2.857 * * [simplify]: iters left: 4 (9 enodes)
2.859 * * [simplify]: iters left: 3 (24 enodes)
2.863 * * [simplify]: iters left: 2 (47 enodes)
2.871 * * [simplify]: iters left: 1 (110 enodes)
2.898 * * [simplify]: Extracting #0: cost 1 inf + 0
2.898 * * [simplify]: Extracting #1: cost 6 inf + 0
2.898 * * [simplify]: Extracting #2: cost 10 inf + 1
2.899 * * [simplify]: Extracting #3: cost 23 inf + 403
2.899 * * [simplify]: Extracting #4: cost 60 inf + 1445
2.899 * * [simplify]: Extracting #5: cost 82 inf + 10995
2.904 * * [simplify]: Extracting #6: cost 72 inf + 62107
2.910 * * [simplify]: Extracting #7: cost 2 inf + 174263
2.916 * * [simplify]: Extracting #8: cost 0 inf + 178949
2.922 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
2.922 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
2.922 * * * * [progress]: [ 3 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c))))))))>
2.922 * * * * [progress]: [ 4 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
2.922 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
2.922 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
2.923 * * [simplify]: iters left: 6 (15 enodes)
2.926 * * [simplify]: iters left: 5 (47 enodes)
2.934 * * [simplify]: iters left: 4 (100 enodes)
2.953 * * [simplify]: iters left: 3 (250 enodes)
3.057 * * [simplify]: Extracting #0: cost 1 inf + 0
3.057 * * [simplify]: Extracting #1: cost 7 inf + 0
3.057 * * [simplify]: Extracting #2: cost 38 inf + 0
3.057 * * [simplify]: Extracting #3: cost 87 inf + 887
3.058 * * [simplify]: Extracting #4: cost 102 inf + 14607
3.061 * * [simplify]: Extracting #5: cost 76 inf + 73643
3.068 * * [simplify]: Extracting #6: cost 44 inf + 173054
3.077 * * [simplify]: Extracting #7: cost 1 inf + 240249
3.087 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.099 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
3.099 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
3.099 * * * * [progress]: [ 6 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
3.100 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
3.100 * * [simplify]: iters left: 6 (15 enodes)
3.103 * * [simplify]: iters left: 5 (47 enodes)
3.114 * * [simplify]: iters left: 4 (100 enodes)
3.133 * * [simplify]: iters left: 3 (250 enodes)
3.301 * * [simplify]: Extracting #0: cost 1 inf + 0
3.301 * * [simplify]: Extracting #1: cost 7 inf + 0
3.302 * * [simplify]: Extracting #2: cost 38 inf + 0
3.302 * * [simplify]: Extracting #3: cost 87 inf + 887
3.304 * * [simplify]: Extracting #4: cost 102 inf + 14607
3.311 * * [simplify]: Extracting #5: cost 76 inf + 73643
3.325 * * [simplify]: Extracting #6: cost 44 inf + 173054
3.342 * * [simplify]: Extracting #7: cost 1 inf + 240249
3.361 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.380 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
3.380 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
3.380 * * * * [progress]: [ 7 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
3.381 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
3.381 * * [simplify]: iters left: 6 (15 enodes)
3.387 * * [simplify]: iters left: 5 (47 enodes)
3.406 * * [simplify]: iters left: 4 (100 enodes)
3.425 * * [simplify]: iters left: 3 (250 enodes)
3.593 * * [simplify]: Extracting #0: cost 1 inf + 0
3.593 * * [simplify]: Extracting #1: cost 7 inf + 0
3.593 * * [simplify]: Extracting #2: cost 38 inf + 0
3.594 * * [simplify]: Extracting #3: cost 87 inf + 887
3.596 * * [simplify]: Extracting #4: cost 102 inf + 14607
3.602 * * [simplify]: Extracting #5: cost 76 inf + 73643
3.608 * * [simplify]: Extracting #6: cost 44 inf + 173054
3.617 * * [simplify]: Extracting #7: cost 1 inf + 240249
3.628 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.646 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
3.646 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
3.646 * * * * [progress]: [ 8 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
3.647 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
3.647 * * [simplify]: iters left: 6 (15 enodes)
3.653 * * [simplify]: iters left: 5 (47 enodes)
3.670 * * [simplify]: iters left: 4 (100 enodes)
3.695 * * [simplify]: iters left: 3 (250 enodes)
3.824 * * [simplify]: Extracting #0: cost 1 inf + 0
3.824 * * [simplify]: Extracting #1: cost 7 inf + 0
3.824 * * [simplify]: Extracting #2: cost 38 inf + 0
3.825 * * [simplify]: Extracting #3: cost 87 inf + 887
3.826 * * [simplify]: Extracting #4: cost 102 inf + 14607
3.829 * * [simplify]: Extracting #5: cost 76 inf + 73643
3.838 * * [simplify]: Extracting #6: cost 44 inf + 173054
3.856 * * [simplify]: Extracting #7: cost 1 inf + 240249
3.868 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.877 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
3.878 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
3.878 * * * [progress]: adding candidates to table
4.178 * * [progress]: iteration 3 / 4
4.178 * * * [progress]: picking best candidate
4.221 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
4.221 * * * [progress]: localizing error
4.568 * * * [progress]: generating rewritten candidates
4.568 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2)
4.573 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
4.577 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2)
4.577 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
4.584 * * * [progress]: generating series expansions
4.584 * * * * [progress]: [ 1 / 4 ] generating series at (2 2)
4.584 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
4.584 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2)
4.584 * * * * [progress]: [ 4 / 4 ] generating series at (2)
4.584 * * * [progress]: simplifying candidates
4.584 * * * * [progress]: [ 1 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (neg.p16 b_2))))>
4.584 * * * * [progress]: [ 2 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)))>
4.584 * [simplify]: Simplifying (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2))))
4.585 * * [simplify]: iters left: 4 (9 enodes)
4.589 * * [simplify]: iters left: 3 (24 enodes)
4.597 * * [simplify]: iters left: 2 (53 enodes)
4.618 * * [simplify]: iters left: 1 (140 enodes)
4.743 * * [simplify]: Extracting #0: cost 1 inf + 0
4.743 * * [simplify]: Extracting #1: cost 24 inf + 0
4.743 * * [simplify]: Extracting #2: cost 70 inf + 0
4.744 * * [simplify]: Extracting #3: cost 62 inf + 3454
4.745 * * [simplify]: Extracting #4: cost 19 inf + 33897
4.749 * * [simplify]: Extracting #5: cost 0 inf + 53655
4.752 * [simplify]: Simplified to (+.p16 (*.p16 c a) (real->posit16 0.0))
4.752 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)))
4.752 * * * * [progress]: [ 3 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
4.753 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.753 * * [simplify]: iters left: 4 (9 enodes)
4.754 * * [simplify]: iters left: 3 (24 enodes)
4.758 * * [simplify]: iters left: 2 (47 enodes)
4.766 * * [simplify]: iters left: 1 (110 enodes)
4.794 * * [simplify]: Extracting #0: cost 1 inf + 0
4.794 * * [simplify]: Extracting #1: cost 6 inf + 0
4.794 * * [simplify]: Extracting #2: cost 10 inf + 1
4.794 * * [simplify]: Extracting #3: cost 23 inf + 403
4.794 * * [simplify]: Extracting #4: cost 60 inf + 1445
4.795 * * [simplify]: Extracting #5: cost 82 inf + 10995
4.799 * * [simplify]: Extracting #6: cost 72 inf + 62107
4.804 * * [simplify]: Extracting #7: cost 2 inf + 174263
4.810 * * [simplify]: Extracting #8: cost 0 inf + 178949
4.816 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
4.816 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
4.816 * * * * [progress]: [ 4 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
4.817 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.817 * * [simplify]: iters left: 4 (9 enodes)
4.818 * * [simplify]: iters left: 3 (24 enodes)
4.822 * * [simplify]: iters left: 2 (47 enodes)
4.830 * * [simplify]: iters left: 1 (110 enodes)
4.856 * * [simplify]: Extracting #0: cost 1 inf + 0
4.856 * * [simplify]: Extracting #1: cost 6 inf + 0
4.856 * * [simplify]: Extracting #2: cost 10 inf + 1
4.856 * * [simplify]: Extracting #3: cost 23 inf + 403
4.856 * * [simplify]: Extracting #4: cost 60 inf + 1445
4.857 * * [simplify]: Extracting #5: cost 82 inf + 10995
4.859 * * [simplify]: Extracting #6: cost 72 inf + 62107
4.864 * * [simplify]: Extracting #7: cost 2 inf + 174263
4.872 * * [simplify]: Extracting #8: cost 0 inf + 178949
4.878 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
4.878 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
4.878 * * * * [progress]: [ 5 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
4.878 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.879 * * [simplify]: iters left: 4 (9 enodes)
4.881 * * [simplify]: iters left: 3 (24 enodes)
4.884 * * [simplify]: iters left: 2 (47 enodes)
4.892 * * [simplify]: iters left: 1 (110 enodes)
4.918 * * [simplify]: Extracting #0: cost 1 inf + 0
4.919 * * [simplify]: Extracting #1: cost 6 inf + 0
4.919 * * [simplify]: Extracting #2: cost 10 inf + 1
4.919 * * [simplify]: Extracting #3: cost 23 inf + 403
4.919 * * [simplify]: Extracting #4: cost 60 inf + 1445
4.919 * * [simplify]: Extracting #5: cost 82 inf + 10995
4.921 * * [simplify]: Extracting #6: cost 72 inf + 62107
4.927 * * [simplify]: Extracting #7: cost 2 inf + 174263
4.933 * * [simplify]: Extracting #8: cost 0 inf + 178949
4.939 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
4.939 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
4.939 * * * * [progress]: [ 6 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
4.939 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.940 * * [simplify]: iters left: 4 (9 enodes)
4.942 * * [simplify]: iters left: 3 (24 enodes)
4.946 * * [simplify]: iters left: 2 (47 enodes)
4.963 * * [simplify]: iters left: 1 (110 enodes)
5.020 * * [simplify]: Extracting #0: cost 1 inf + 0
5.020 * * [simplify]: Extracting #1: cost 6 inf + 0
5.020 * * [simplify]: Extracting #2: cost 10 inf + 1
5.020 * * [simplify]: Extracting #3: cost 23 inf + 403
5.020 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.021 * * [simplify]: Extracting #5: cost 82 inf + 10995
5.025 * * [simplify]: Extracting #6: cost 72 inf + 62107
5.036 * * [simplify]: Extracting #7: cost 2 inf + 174263
5.048 * * [simplify]: Extracting #8: cost 0 inf + 178949
5.061 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.061 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
5.061 * * * [progress]: adding candidates to table
5.220 * * [progress]: iteration 4 / 4
5.220 * * * [progress]: picking best candidate
5.258 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
5.258 * * * [progress]: localizing error
5.736 * * * [progress]: generating rewritten candidates
5.736 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2 2 1)
5.753 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 2)
5.758 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
5.763 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2)
5.764 * * * [progress]: generating series expansions
5.764 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2 2 1)
5.765 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 2)
5.765 * * * * [progress]: [ 3 / 4 ] generating series at (2)
5.765 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2)
5.765 * * * [progress]: simplifying candidates
5.765 * * * * [progress]: [ 1 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))))>
5.765 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
5.765 * * [simplify]: iters left: 2 (6 enodes)
5.766 * * [simplify]: iters left: 1 (14 enodes)
5.768 * * [simplify]: Extracting #0: cost 1 inf + 0
5.768 * * [simplify]: Extracting #1: cost 3 inf + 0
5.768 * * [simplify]: Extracting #2: cost 6 inf + 0
5.768 * * [simplify]: Extracting #3: cost 2 inf + 325
5.768 * * [simplify]: Extracting #4: cost 0 inf + 1329
5.768 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
5.768 * [simplify]: Simplified (2 2 2 2 1 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))))
5.769 * * * * [progress]: [ 2 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 a c) (*.p16 a c)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))>
5.769 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 a c) (*.p16 a c))))
5.769 * * [simplify]: iters left: 4 (10 enodes)
5.771 * * [simplify]: iters left: 3 (43 enodes)
5.779 * * [simplify]: iters left: 2 (121 enodes)
5.839 * * [simplify]: iters left: 1 (456 enodes)
6.297 * * [simplify]: Extracting #0: cost 1 inf + 0
6.297 * * [simplify]: Extracting #1: cost 46 inf + 0
6.298 * * [simplify]: Extracting #2: cost 270 inf + 0
6.303 * * [simplify]: Extracting #3: cost 402 inf + 62527
6.346 * * [simplify]: Extracting #4: cost 378 inf + 463702
6.458 * * [simplify]: Extracting #5: cost 11 inf + 1296655
6.557 * * [simplify]: Extracting #6: cost 0 inf + 1315117
6.664 * [simplify]: Simplified to (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))))
6.664 * [simplify]: Simplified (2 2 2 2 1 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))
6.664 * * * * [progress]: [ 3 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (neg.p16 b_2)))))>
6.664 * * * * [progress]: [ 4 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
6.664 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
6.664 * * [simplify]: iters left: 6 (13 enodes)
6.667 * * [simplify]: iters left: 5 (39 enodes)
6.674 * * [simplify]: iters left: 4 (84 enodes)
6.694 * * [simplify]: iters left: 3 (272 enodes)
6.889 * * [simplify]: Extracting #0: cost 1 inf + 0
6.889 * * [simplify]: Extracting #1: cost 6 inf + 0
6.889 * * [simplify]: Extracting #2: cost 10 inf + 1
6.890 * * [simplify]: Extracting #3: cost 65 inf + 804
6.891 * * [simplify]: Extracting #4: cost 230 inf + 1445
6.895 * * [simplify]: Extracting #5: cost 347 inf + 44545
6.918 * * [simplify]: Extracting #6: cost 220 inf + 258509
6.963 * * [simplify]: Extracting #7: cost 42 inf + 627336
7.013 * * [simplify]: Extracting #8: cost 4 inf + 723766
7.059 * * [simplify]: Extracting #9: cost 0 inf + 735179
7.464 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
7.464 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
7.464 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
7.464 * * * * [progress]: [ 6 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
7.464 * * * * [progress]: [ 7 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
7.464 * * * * [progress]: [ 8 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
7.464 * * * [progress]: adding candidates to table
7.684 * [progress]: [Phase 3 of 3] Extracting.
7.684 * * [regime]: Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>)
7.690 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
7.690 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>)
7.859 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>)
8.062 * * * * [regimes]: Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>)
8.233 * * * [regime]: Found split indices: #<option (#s(si 2 113) #s(si 6 256))>
8.235 * [binary-search]: Improving bounds with binary search for b_2 and (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>)
8.235 * [regimes]: Found splitpoints: (#s(sp 2 b_2 #<cpointer:posit16>) #s(sp 6 b_2 +nan.0)) , with alts (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>)
8.236 * [simplify]: Simplifying (if (<=.p16 b_2 (real->posit16 -0.071807861328125)) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))
8.237 * * [simplify]: iters left: 6 (21 enodes)
8.239 * * [simplify]: Extracting #0: cost 1 inf + 0
8.239 * * [simplify]: Extracting #1: cost 4 inf + 0
8.239 * * [simplify]: Extracting #2: cost 10 inf + 0
8.239 * * [simplify]: Extracting #3: cost 12 inf + 2
8.239 * * [simplify]: Extracting #4: cost 13 inf + 84
8.239 * * [simplify]: Extracting #5: cost 15 inf + 152
8.239 * * [simplify]: Extracting #6: cost 11 inf + 716
8.239 * * [simplify]: Extracting #7: cost 6 inf + 3848
8.240 * * [simplify]: Extracting #8: cost 3 inf + 6937
8.241 * * [simplify]: Extracting #9: cost 0 inf + 13357
8.241 * [simplify]: Simplified to (if (<=.p16 b_2 (real->posit16 -0.071807861328125)) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))
8.241 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
8.293 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
8.294 * * * * [points]: Setting MPFR precision to 64
8.296 * * * * [points]: Setting MPFR precision to 320
8.297 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
8.298 * * * * [points]: Setting MPFR precision to 64
8.302 * * * * [points]: Setting MPFR precision to 320
8.305 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
8.307 * * * * [points]: Setting MPFR precision to 64
8.315 * * * * [points]: Setting MPFR precision to 320
8.322 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
8.324 * * * * [points]: Setting MPFR precision to 64
8.338 * * * * [points]: Setting MPFR precision to 320
8.352 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
8.353 * * * * [points]: Setting MPFR precision to 64
8.369 * * * * [points]: Setting MPFR precision to 320
8.385 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
8.387 * * * * [points]: Setting MPFR precision to 64
8.443 * * * * [points]: Setting MPFR precision to 320
8.525 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
8.526 * * * * [points]: Setting MPFR precision to 64
8.588 * * * * [points]: Setting MPFR precision to 320
8.684 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
8.685 * * * * [points]: Setting MPFR precision to 64
8.845 * * * * [points]: Setting MPFR precision to 320
9.037 * * * * [points]: Computing exacts for 8000 points
9.038 * * * * [points]: Setting MPFR precision to 64
9.972 * * * * [points]: Setting MPFR precision to 320
10.768 * * * * [points]: Filtering points with unrepresentable outputs
11.146 * * * * [points]: Sampled 8000 points with exact outputs
14.964 * [regime-testing]: Baseline error score: 64.0
14.971 * [regime-testing]: Oracle error score: 64.0
14.984 * [regime-testing]: End program error score: 0.4473390316973186