0.004 * [progress]: [Phase 1 of 3] Setting up.
0.006 * * * [progress]: [1/2] Preparing points
0.009 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.012 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.124 * * * * [points]: Setting MPFR precision to 64
0.128 * * * * [points]: Setting MPFR precision to 320
0.129 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.130 * * * * [points]: Setting MPFR precision to 64
0.132 * * * * [points]: Setting MPFR precision to 320
0.135 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.136 * * * * [points]: Setting MPFR precision to 64
0.139 * * * * [points]: Setting MPFR precision to 320
0.143 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.144 * * * * [points]: Setting MPFR precision to 64
0.152 * * * * [points]: Setting MPFR precision to 320
0.158 * * * * [points]: Computing exacts for 256 points
0.159 * * * * [points]: Setting MPFR precision to 64
0.178 * * * * [points]: Setting MPFR precision to 320
0.204 * * * * [points]: Filtering points with unrepresentable outputs
0.205 * * * * [points]: Sampled 256 points with exact outputs
0.205 * * * [progress]: [2/2] Setting up program.
0.217 * [progress]: [Phase 2 of 3] Improving.
0.217 * * * * [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.218 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.219 * * [simplify]: iters left: 5 (10 enodes)
0.225 * * [simplify]: iters left: 4 (31 enodes)
0.232 * * [simplify]: iters left: 3 (65 enodes)
0.247 * * [simplify]: iters left: 2 (207 enodes)
0.374 * * [simplify]: Extracting #0: cost 1 inf + 0
0.374 * * [simplify]: Extracting #1: cost 20 inf + 0
0.375 * * [simplify]: Extracting #2: cost 89 inf + 1
0.376 * * [simplify]: Extracting #3: cost 168 inf + 83
0.378 * * [simplify]: Extracting #4: cost 227 inf + 12401
0.385 * * [simplify]: Extracting #5: cost 180 inf + 98398
0.404 * * [simplify]: Extracting #6: cost 61 inf + 349602
0.427 * * [simplify]: Extracting #7: cost 2 inf + 436444
0.450 * * [simplify]: Extracting #8: cost 0 inf + 442330
0.471 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
0.471 * [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.483 * * [progress]: iteration 1 / 4
0.484 * * * [progress]: picking best candidate
0.493 * * * * [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.493 * * * [progress]: localizing error
0.721 * * * [progress]: generating rewritten candidates
0.721 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.728 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
0.728 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
0.747 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
0.755 * * * [progress]: generating series expansions
0.756 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.756 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
0.756 * * * * [progress]: [ 3 / 4 ] generating series at (2)
0.756 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
0.756 * * * [progress]: simplifying candidates
0.756 * * * * [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.756 * * * * [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.756 * * * * [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.757 * [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.757 * * [simplify]: iters left: 5 (11 enodes)
0.762 * * [simplify]: iters left: 4 (35 enodes)
0.773 * * [simplify]: iters left: 3 (100 enodes)
0.796 * * [simplify]: iters left: 2 (360 enodes)
1.100 * * [simplify]: Extracting #0: cost 1 inf + 0
1.100 * * [simplify]: Extracting #1: cost 48 inf + 0
1.101 * * [simplify]: Extracting #2: cost 223 inf + 0
1.106 * * [simplify]: Extracting #3: cost 348 inf + 45039
1.131 * * [simplify]: Extracting #4: cost 315 inf + 336131
1.197 * * [simplify]: Extracting #5: cost 84 inf + 852438
1.286 * * [simplify]: Extracting #6: cost 1 inf + 990774
1.342 * * [simplify]: Extracting #7: cost 0 inf + 992777
1.426 * [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.426 * [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.426 * * * * [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.426 * * * * [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.427 * * * * [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.427 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.427 * * [simplify]: iters left: 5 (10 enodes)
1.431 * * [simplify]: iters left: 4 (31 enodes)
1.439 * * [simplify]: iters left: 3 (65 enodes)
1.452 * * [simplify]: iters left: 2 (207 enodes)
1.536 * * [simplify]: Extracting #0: cost 1 inf + 0
1.536 * * [simplify]: Extracting #1: cost 20 inf + 0
1.536 * * [simplify]: Extracting #2: cost 89 inf + 1
1.536 * * [simplify]: Extracting #3: cost 168 inf + 83
1.537 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.541 * * [simplify]: Extracting #5: cost 180 inf + 98398
1.553 * * [simplify]: Extracting #6: cost 61 inf + 349602
1.569 * * [simplify]: Extracting #7: cost 2 inf + 436444
1.586 * * [simplify]: Extracting #8: cost 0 inf + 442330
1.605 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.605 * [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.605 * * * * [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.606 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.606 * * [simplify]: iters left: 5 (10 enodes)
1.608 * * [simplify]: iters left: 4 (31 enodes)
1.613 * * [simplify]: iters left: 3 (65 enodes)
1.626 * * [simplify]: iters left: 2 (207 enodes)
1.697 * * [simplify]: Extracting #0: cost 1 inf + 0
1.697 * * [simplify]: Extracting #1: cost 20 inf + 0
1.697 * * [simplify]: Extracting #2: cost 89 inf + 1
1.697 * * [simplify]: Extracting #3: cost 168 inf + 83
1.698 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.702 * * [simplify]: Extracting #5: cost 180 inf + 98398
1.713 * * [simplify]: Extracting #6: cost 61 inf + 349602
1.734 * * [simplify]: Extracting #7: cost 2 inf + 436444
1.766 * * [simplify]: Extracting #8: cost 0 inf + 442330
1.791 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.791 * [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.791 * * * * [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.791 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.791 * * [simplify]: iters left: 5 (10 enodes)
1.793 * * [simplify]: iters left: 4 (31 enodes)
1.799 * * [simplify]: iters left: 3 (65 enodes)
1.812 * * [simplify]: iters left: 2 (207 enodes)
1.923 * * [simplify]: Extracting #0: cost 1 inf + 0
1.923 * * [simplify]: Extracting #1: cost 20 inf + 0
1.923 * * [simplify]: Extracting #2: cost 89 inf + 1
1.924 * * [simplify]: Extracting #3: cost 168 inf + 83
1.926 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.932 * * [simplify]: Extracting #5: cost 180 inf + 98398
1.956 * * [simplify]: Extracting #6: cost 61 inf + 349602
1.980 * * [simplify]: Extracting #7: cost 2 inf + 436444
1.997 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.026 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.026 * [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.026 * * * * [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.026 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.027 * * [simplify]: iters left: 5 (10 enodes)
2.030 * * [simplify]: iters left: 4 (31 enodes)
2.041 * * [simplify]: iters left: 3 (65 enodes)
2.066 * * [simplify]: iters left: 2 (207 enodes)
2.175 * * [simplify]: Extracting #0: cost 1 inf + 0
2.175 * * [simplify]: Extracting #1: cost 20 inf + 0
2.175 * * [simplify]: Extracting #2: cost 89 inf + 1
2.176 * * [simplify]: Extracting #3: cost 168 inf + 83
2.177 * * [simplify]: Extracting #4: cost 227 inf + 12401
2.180 * * [simplify]: Extracting #5: cost 180 inf + 98398
2.192 * * [simplify]: Extracting #6: cost 61 inf + 349602
2.220 * * [simplify]: Extracting #7: cost 2 inf + 436444
2.249 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.268 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.268 * [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.268 * * * [progress]: adding candidates to table
2.426 * * [progress]: iteration 2 / 4
2.427 * * * [progress]: picking best candidate
2.461 * * * * [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.461 * * * [progress]: localizing error
2.855 * * * [progress]: generating rewritten candidates
2.855 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
2.862 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
2.868 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2)
2.868 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2 1)
2.874 * * * [progress]: generating series expansions
2.874 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
2.874 * * * * [progress]: [ 2 / 4 ] generating series at (2)
2.874 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2)
2.874 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2 1)
2.875 * * * [progress]: simplifying candidates
2.875 * * * * [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.875 * * * * [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.875 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
2.875 * * [simplify]: iters left: 4 (9 enodes)
2.879 * * [simplify]: iters left: 3 (24 enodes)
2.887 * * [simplify]: iters left: 2 (47 enodes)
2.903 * * [simplify]: iters left: 1 (110 enodes)
2.964 * * [simplify]: Extracting #0: cost 1 inf + 0
2.964 * * [simplify]: Extracting #1: cost 6 inf + 0
2.964 * * [simplify]: Extracting #2: cost 10 inf + 1
2.964 * * [simplify]: Extracting #3: cost 23 inf + 403
2.964 * * [simplify]: Extracting #4: cost 60 inf + 1445
2.965 * * [simplify]: Extracting #5: cost 79 inf + 13843
2.969 * * [simplify]: Extracting #6: cost 73 inf + 57826
2.978 * * [simplify]: Extracting #7: cost 3 inf + 171780
2.990 * * [simplify]: Extracting #8: cost 0 inf + 178629
3.001 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
3.001 * [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)))
3.002 * * * * [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))))))))>
3.002 * * * * [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))))))))>
3.002 * * * * [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)))))))>
3.002 * [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.002 * * [simplify]: iters left: 6 (15 enodes)
3.009 * * [simplify]: iters left: 5 (47 enodes)
3.024 * * [simplify]: iters left: 4 (100 enodes)
3.050 * * [simplify]: iters left: 3 (250 enodes)
3.251 * * [simplify]: Extracting #0: cost 1 inf + 0
3.252 * * [simplify]: Extracting #1: cost 7 inf + 0
3.253 * * [simplify]: Extracting #2: cost 38 inf + 0
3.254 * * [simplify]: Extracting #3: cost 89 inf + 404
3.255 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.263 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.278 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.295 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.312 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.330 * [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.330 * [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.330 * * * * [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.331 * [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.331 * * [simplify]: iters left: 6 (15 enodes)
3.337 * * [simplify]: iters left: 5 (47 enodes)
3.355 * * [simplify]: iters left: 4 (100 enodes)
3.394 * * [simplify]: iters left: 3 (250 enodes)
3.597 * * [simplify]: Extracting #0: cost 1 inf + 0
3.597 * * [simplify]: Extracting #1: cost 7 inf + 0
3.597 * * [simplify]: Extracting #2: cost 38 inf + 0
3.598 * * [simplify]: Extracting #3: cost 89 inf + 404
3.599 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.605 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.618 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.635 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.657 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.675 * [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.675 * [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.676 * * * * [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.676 * [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.676 * * [simplify]: iters left: 6 (15 enodes)
3.683 * * [simplify]: iters left: 5 (47 enodes)
3.700 * * [simplify]: iters left: 4 (100 enodes)
3.738 * * [simplify]: iters left: 3 (250 enodes)
3.947 * * [simplify]: Extracting #0: cost 1 inf + 0
3.948 * * [simplify]: Extracting #1: cost 7 inf + 0
3.948 * * [simplify]: Extracting #2: cost 38 inf + 0
3.948 * * [simplify]: Extracting #3: cost 89 inf + 404
3.950 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.954 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.960 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.968 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.977 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.987 * [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.987 * [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.987 * * * * [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.987 * [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.987 * * [simplify]: iters left: 6 (15 enodes)
3.992 * * [simplify]: iters left: 5 (47 enodes)
4.000 * * [simplify]: iters left: 4 (100 enodes)
4.035 * * [simplify]: iters left: 3 (250 enodes)
4.233 * * [simplify]: Extracting #0: cost 1 inf + 0
4.233 * * [simplify]: Extracting #1: cost 7 inf + 0
4.234 * * [simplify]: Extracting #2: cost 38 inf + 0
4.234 * * [simplify]: Extracting #3: cost 89 inf + 404
4.235 * * [simplify]: Extracting #4: cost 105 inf + 13282
4.238 * * [simplify]: Extracting #5: cost 75 inf + 74603
4.244 * * [simplify]: Extracting #6: cost 45 inf + 171652
4.252 * * [simplify]: Extracting #7: cost 3 inf + 235044
4.261 * * [simplify]: Extracting #8: cost 0 inf + 242171
4.270 * [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)))
4.270 * [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))))
4.271 * * * [progress]: adding candidates to table
4.453 * * [progress]: iteration 3 / 4
4.453 * * * [progress]: picking best candidate
4.499 * * * * [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.499 * * * [progress]: localizing error
4.727 * * * [progress]: generating rewritten candidates
4.728 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2)
4.733 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
4.735 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2)
4.735 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
4.738 * * * [progress]: generating series expansions
4.738 * * * * [progress]: [ 1 / 4 ] generating series at (2 2)
4.738 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
4.738 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2)
4.739 * * * * [progress]: [ 4 / 4 ] generating series at (2)
4.739 * * * [progress]: simplifying candidates
4.739 * * * * [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.739 * * * * [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.739 * [simplify]: Simplifying (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2))))
4.739 * * [simplify]: iters left: 4 (9 enodes)
4.741 * * [simplify]: iters left: 3 (24 enodes)
4.752 * * [simplify]: iters left: 2 (53 enodes)
4.763 * * [simplify]: iters left: 1 (140 enodes)
4.868 * * [simplify]: Extracting #0: cost 1 inf + 0
4.868 * * [simplify]: Extracting #1: cost 24 inf + 0
4.868 * * [simplify]: Extracting #2: cost 70 inf + 0
4.868 * * [simplify]: Extracting #3: cost 62 inf + 3454
4.870 * * [simplify]: Extracting #4: cost 19 inf + 33897
4.873 * * [simplify]: Extracting #5: cost 0 inf + 53655
4.875 * [simplify]: Simplified to (+.p16 (*.p16 c a) (real->posit16 0.0))
4.875 * [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.876 * * * * [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.876 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.876 * * [simplify]: iters left: 4 (9 enodes)
4.879 * * [simplify]: iters left: 3 (24 enodes)
4.887 * * [simplify]: iters left: 2 (47 enodes)
4.903 * * [simplify]: iters left: 1 (110 enodes)
4.960 * * [simplify]: Extracting #0: cost 1 inf + 0
4.960 * * [simplify]: Extracting #1: cost 6 inf + 0
4.960 * * [simplify]: Extracting #2: cost 10 inf + 1
4.960 * * [simplify]: Extracting #3: cost 23 inf + 403
4.961 * * [simplify]: Extracting #4: cost 60 inf + 1445
4.962 * * [simplify]: Extracting #5: cost 79 inf + 13843
4.965 * * [simplify]: Extracting #6: cost 73 inf + 57826
4.974 * * [simplify]: Extracting #7: cost 3 inf + 171780
4.986 * * [simplify]: Extracting #8: cost 0 inf + 178629
4.998 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
4.998 * [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.998 * * * * [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.998 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.998 * * [simplify]: iters left: 4 (9 enodes)
5.002 * * [simplify]: iters left: 3 (24 enodes)
5.010 * * [simplify]: iters left: 2 (47 enodes)
5.027 * * [simplify]: iters left: 1 (110 enodes)
5.084 * * [simplify]: Extracting #0: cost 1 inf + 0
5.084 * * [simplify]: Extracting #1: cost 6 inf + 0
5.084 * * [simplify]: Extracting #2: cost 10 inf + 1
5.085 * * [simplify]: Extracting #3: cost 23 inf + 403
5.085 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.086 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.089 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.099 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.111 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.123 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.123 * [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.123 * * * * [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))))))>
5.123 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.124 * * [simplify]: iters left: 4 (9 enodes)
5.127 * * [simplify]: iters left: 3 (24 enodes)
5.135 * * [simplify]: iters left: 2 (47 enodes)
5.152 * * [simplify]: iters left: 1 (110 enodes)
5.207 * * [simplify]: Extracting #0: cost 1 inf + 0
5.207 * * [simplify]: Extracting #1: cost 6 inf + 0
5.207 * * [simplify]: Extracting #2: cost 10 inf + 1
5.208 * * [simplify]: Extracting #3: cost 23 inf + 403
5.208 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.209 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.212 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.224 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.235 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.243 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.243 * [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.243 * * * * [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))))))>
5.244 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.244 * * [simplify]: iters left: 4 (9 enodes)
5.245 * * [simplify]: iters left: 3 (24 enodes)
5.249 * * [simplify]: iters left: 2 (47 enodes)
5.258 * * [simplify]: iters left: 1 (110 enodes)
5.284 * * [simplify]: Extracting #0: cost 1 inf + 0
5.284 * * [simplify]: Extracting #1: cost 6 inf + 0
5.284 * * [simplify]: Extracting #2: cost 10 inf + 1
5.284 * * [simplify]: Extracting #3: cost 23 inf + 403
5.284 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.285 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.286 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.291 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.297 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.304 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.304 * [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.305 * * * [progress]: adding candidates to table
5.397 * * [progress]: iteration 4 / 4
5.397 * * * [progress]: picking best candidate
5.432 * * * * [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.432 * * * [progress]: localizing error
5.759 * * * [progress]: generating rewritten candidates
5.760 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2 2 1)
5.777 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 2)
5.782 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
5.788 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2)
5.789 * * * [progress]: generating series expansions
5.789 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2 2 1)
5.789 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 2)
5.789 * * * * [progress]: [ 3 / 4 ] generating series at (2)
5.789 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2)
5.789 * * * [progress]: simplifying candidates
5.789 * * * * [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.789 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
5.790 * * [simplify]: iters left: 2 (6 enodes)
5.792 * * [simplify]: iters left: 1 (14 enodes)
5.794 * * [simplify]: Extracting #0: cost 1 inf + 0
5.794 * * [simplify]: Extracting #1: cost 3 inf + 0
5.794 * * [simplify]: Extracting #2: cost 6 inf + 0
5.794 * * [simplify]: Extracting #3: cost 2 inf + 325
5.794 * * [simplify]: Extracting #4: cost 0 inf + 1329
5.794 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
5.794 * [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.794 * * * * [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.794 * [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.794 * * [simplify]: iters left: 4 (10 enodes)
5.797 * * [simplify]: iters left: 3 (43 enodes)
5.811 * * [simplify]: iters left: 2 (121 enodes)
5.849 * * [simplify]: iters left: 1 (429 enodes)
6.144 * * [simplify]: Extracting #0: cost 1 inf + 0
6.144 * * [simplify]: Extracting #1: cost 46 inf + 0
6.145 * * [simplify]: Extracting #2: cost 270 inf + 0
6.151 * * [simplify]: Extracting #3: cost 354 inf + 59003
6.165 * * [simplify]: Extracting #4: cost 345 inf + 369227
6.227 * * [simplify]: Extracting #5: cost 22 inf + 1102360
6.300 * * [simplify]: Extracting #6: cost 1 inf + 1150488
6.386 * * [simplify]: Extracting #7: cost 0 inf + 1155051
6.482 * [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.483 * [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.483 * * * * [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.483 * * * * [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.483 * [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.484 * * [simplify]: iters left: 6 (13 enodes)
6.489 * * [simplify]: iters left: 5 (39 enodes)
6.496 * * [simplify]: iters left: 4 (84 enodes)
6.514 * * [simplify]: iters left: 3 (271 enodes)
6.631 * * [simplify]: Extracting #0: cost 1 inf + 0
6.631 * * [simplify]: Extracting #1: cost 6 inf + 0
6.631 * * [simplify]: Extracting #2: cost 10 inf + 1
6.631 * * [simplify]: Extracting #3: cost 66 inf + 403
6.632 * * [simplify]: Extracting #4: cost 230 inf + 1445
6.634 * * [simplify]: Extracting #5: cost 349 inf + 32520
6.642 * * [simplify]: Extracting #6: cost 220 inf + 249925
6.687 * * [simplify]: Extracting #7: cost 28 inf + 656177
6.749 * * [simplify]: Extracting #8: cost 0 inf + 728735
6.789 * * [simplify]: Extracting #9: cost 0 inf + 726535
6.841 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
6.841 * [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)))
6.841 * * * * [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))))))))>
6.841 * * * * [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))))))))>
6.841 * * * * [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))))))))>
6.841 * * * * [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))))))))>
6.841 * * * [progress]: adding candidates to table
7.058 * [progress]: [Phase 3 of 3] Extracting.
7.059 * * [regime]: Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 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 (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))))))))))>)
7.062 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
7.062 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 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 (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))))))))))>)
7.191 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 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 (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))))))))))>)
7.361 * * * * [regimes]: Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 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 (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))))))))))>)
7.552 * * * [regime]: Found split indices: #<option (#s(si 1 116) #s(si 0 256))>
7.553 * [binary-search]: Improving bounds with binary search for b_2 and (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 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 (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))))))))))>)
7.554 * [regimes]: Found splitpoints: (#s(sp 1 b_2 #<cpointer:posit16>) #s(sp 0 b_2 +nan.0)) , with alts (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 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 (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))))))))))>)
7.555 * [simplify]: Simplifying (if (<=.p16 b_2 (real->posit16 -0.091796875)) (/.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))
7.555 * * [simplify]: iters left: 6 (21 enodes)
7.561 * * [simplify]: Extracting #0: cost 1 inf + 0
7.561 * * [simplify]: Extracting #1: cost 4 inf + 0
7.561 * * [simplify]: Extracting #2: cost 10 inf + 0
7.561 * * [simplify]: Extracting #3: cost 12 inf + 2
7.561 * * [simplify]: Extracting #4: cost 13 inf + 84
7.561 * * [simplify]: Extracting #5: cost 15 inf + 152
7.562 * * [simplify]: Extracting #6: cost 11 inf + 716
7.562 * * [simplify]: Extracting #7: cost 6 inf + 3848
7.562 * * [simplify]: Extracting #8: cost 3 inf + 6937
7.563 * * [simplify]: Extracting #9: cost 0 inf + 13357
7.564 * [simplify]: Simplified to (if (<=.p16 b_2 (real->posit16 -0.091796875)) (/.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))
7.564 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
7.620 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
7.622 * * * * [points]: Setting MPFR precision to 64
7.624 * * * * [points]: Setting MPFR precision to 320
7.626 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
7.628 * * * * [points]: Setting MPFR precision to 64
7.631 * * * * [points]: Setting MPFR precision to 320
7.635 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
7.637 * * * * [points]: Setting MPFR precision to 64
7.644 * * * * [points]: Setting MPFR precision to 320
7.652 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
7.653 * * * * [points]: Setting MPFR precision to 64
7.666 * * * * [points]: Setting MPFR precision to 320
7.677 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
7.678 * * * * [points]: Setting MPFR precision to 64
7.693 * * * * [points]: Setting MPFR precision to 320
7.709 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
7.710 * * * * [points]: Setting MPFR precision to 64
7.748 * * * * [points]: Setting MPFR precision to 320
7.808 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
7.810 * * * * [points]: Setting MPFR precision to 64
7.899 * * * * [points]: Setting MPFR precision to 320
8.052 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
8.053 * * * * [points]: Setting MPFR precision to 64
8.273 * * * * [points]: Setting MPFR precision to 320
8.478 * * * * [points]: Computing exacts for 8000 points
8.479 * * * * [points]: Setting MPFR precision to 64
9.854 * * * * [points]: Setting MPFR precision to 320
11.068 * * * * [points]: Filtering points with unrepresentable outputs
11.108 * * * * [points]: Sampled 8000 points with exact outputs
15.656 * [regime-testing]: Baseline error score: 64.0
15.659 * [regime-testing]: Oracle error score: 64.0
15.667 * [regime-testing]: End program error score: 0.4397496702028498