0.004 * [progress]: [Phase 1 of 3] Setting up.
0.005 * * * [progress]: [1/2] Preparing points
0.007 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.010 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.115 * * * * [points]: Setting MPFR precision to 64
0.119 * * * * [points]: Setting MPFR precision to 320
0.122 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.124 * * * * [points]: Setting MPFR precision to 64
0.127 * * * * [points]: Setting MPFR precision to 320
0.130 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.132 * * * * [points]: Setting MPFR precision to 64
0.138 * * * * [points]: Setting MPFR precision to 320
0.144 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.146 * * * * [points]: Setting MPFR precision to 64
0.156 * * * * [points]: Setting MPFR precision to 320
0.166 * * * * [points]: Computing exacts for 256 points
0.168 * * * * [points]: Setting MPFR precision to 64
0.196 * * * * [points]: Setting MPFR precision to 320
0.218 * * * * [points]: Filtering points with unrepresentable outputs
0.219 * * * * [points]: Sampled 256 points with exact outputs
0.220 * * * [progress]: [2/2] Setting up program.
0.231 * [progress]: [Phase 2 of 3] Improving.
0.231 * * * * [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.232 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.233 * * [simplify]: iters left: 5 (10 enodes)
0.238 * * [simplify]: iters left: 4 (31 enodes)
0.246 * * [simplify]: iters left: 3 (65 enodes)
0.272 * * [simplify]: iters left: 2 (207 enodes)
0.403 * * [simplify]: Extracting #0: cost 1 inf + 0
0.404 * * [simplify]: Extracting #1: cost 20 inf + 0
0.404 * * [simplify]: Extracting #2: cost 89 inf + 1
0.405 * * [simplify]: Extracting #3: cost 168 inf + 83
0.406 * * [simplify]: Extracting #4: cost 227 inf + 12401
0.409 * * [simplify]: Extracting #5: cost 180 inf + 98398
0.432 * * [simplify]: Extracting #6: cost 61 inf + 349602
0.465 * * [simplify]: Extracting #7: cost 2 inf + 436444
0.482 * * [simplify]: Extracting #8: cost 0 inf + 442330
0.500 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
0.500 * [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.512 * * [progress]: iteration 1 / 4
0.512 * * * [progress]: picking best candidate
0.528 * * * * [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.528 * * * [progress]: localizing error
0.674 * * * [progress]: generating rewritten candidates
0.674 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.678 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
0.679 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
0.682 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
0.686 * * * [progress]: generating series expansions
0.687 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.687 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
0.687 * * * * [progress]: [ 3 / 4 ] generating series at (2)
0.687 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
0.687 * * * [progress]: simplifying candidates
0.687 * * * * [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.687 * * * * [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.687 * * * * [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.687 * [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.687 * * [simplify]: iters left: 5 (11 enodes)
0.690 * * [simplify]: iters left: 4 (35 enodes)
0.712 * * [simplify]: iters left: 3 (100 enodes)
0.759 * * [simplify]: iters left: 2 (360 enodes)
1.076 * * [simplify]: Extracting #0: cost 1 inf + 0
1.076 * * [simplify]: Extracting #1: cost 48 inf + 0
1.077 * * [simplify]: Extracting #2: cost 223 inf + 0
1.079 * * [simplify]: Extracting #3: cost 348 inf + 45039
1.100 * * [simplify]: Extracting #4: cost 315 inf + 336131
1.140 * * [simplify]: Extracting #5: cost 84 inf + 852438
1.195 * * [simplify]: Extracting #6: cost 1 inf + 990774
1.276 * * [simplify]: Extracting #7: cost 0 inf + 992777
1.331 * [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.331 * [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.331 * * * * [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.331 * * * * [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.331 * * * * [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.332 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.332 * * [simplify]: iters left: 5 (10 enodes)
1.336 * * [simplify]: iters left: 4 (31 enodes)
1.346 * * [simplify]: iters left: 3 (65 enodes)
1.371 * * [simplify]: iters left: 2 (207 enodes)
1.460 * * [simplify]: Extracting #0: cost 1 inf + 0
1.460 * * [simplify]: Extracting #1: cost 20 inf + 0
1.461 * * [simplify]: Extracting #2: cost 89 inf + 1
1.461 * * [simplify]: Extracting #3: cost 168 inf + 83
1.463 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.470 * * [simplify]: Extracting #5: cost 180 inf + 98398
1.493 * * [simplify]: Extracting #6: cost 61 inf + 349602
1.527 * * [simplify]: Extracting #7: cost 2 inf + 436444
1.559 * * [simplify]: Extracting #8: cost 0 inf + 442330
1.594 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.594 * [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.594 * * * * [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.594 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.594 * * [simplify]: iters left: 5 (10 enodes)
1.598 * * [simplify]: iters left: 4 (31 enodes)
1.609 * * [simplify]: iters left: 3 (65 enodes)
1.634 * * [simplify]: iters left: 2 (207 enodes)
1.749 * * [simplify]: Extracting #0: cost 1 inf + 0
1.749 * * [simplify]: Extracting #1: cost 20 inf + 0
1.749 * * [simplify]: Extracting #2: cost 89 inf + 1
1.750 * * [simplify]: Extracting #3: cost 168 inf + 83
1.751 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.754 * * [simplify]: Extracting #5: cost 180 inf + 98398
1.766 * * [simplify]: Extracting #6: cost 61 inf + 349602
1.783 * * [simplify]: Extracting #7: cost 2 inf + 436444
1.816 * * [simplify]: Extracting #8: cost 0 inf + 442330
1.849 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.849 * [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.849 * * * * [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.849 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.849 * * [simplify]: iters left: 5 (10 enodes)
1.855 * * [simplify]: iters left: 4 (31 enodes)
1.866 * * [simplify]: iters left: 3 (65 enodes)
1.892 * * [simplify]: iters left: 2 (207 enodes)
1.983 * * [simplify]: Extracting #0: cost 1 inf + 0
1.983 * * [simplify]: Extracting #1: cost 20 inf + 0
1.984 * * [simplify]: Extracting #2: cost 89 inf + 1
1.984 * * [simplify]: Extracting #3: cost 168 inf + 83
1.986 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.993 * * [simplify]: Extracting #5: cost 180 inf + 98398
2.007 * * [simplify]: Extracting #6: cost 61 inf + 349602
2.023 * * [simplify]: Extracting #7: cost 2 inf + 436444
2.040 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.057 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.057 * [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.057 * * * * [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.057 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.057 * * [simplify]: iters left: 5 (10 enodes)
2.059 * * [simplify]: iters left: 4 (31 enodes)
2.066 * * [simplify]: iters left: 3 (65 enodes)
2.079 * * [simplify]: iters left: 2 (207 enodes)
2.192 * * [simplify]: Extracting #0: cost 1 inf + 0
2.192 * * [simplify]: Extracting #1: cost 20 inf + 0
2.193 * * [simplify]: Extracting #2: cost 89 inf + 1
2.193 * * [simplify]: Extracting #3: cost 168 inf + 83
2.194 * * [simplify]: Extracting #4: cost 227 inf + 12401
2.197 * * [simplify]: Extracting #5: cost 180 inf + 98398
2.209 * * [simplify]: Extracting #6: cost 61 inf + 349602
2.225 * * [simplify]: Extracting #7: cost 2 inf + 436444
2.257 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.289 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.290 * [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.290 * * * [progress]: adding candidates to table
2.583 * * [progress]: iteration 2 / 4
2.583 * * * [progress]: picking best candidate
2.620 * * * * [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.620 * * * [progress]: localizing error
2.994 * * * [progress]: generating rewritten candidates
2.994 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
3.000 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
3.005 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2)
3.006 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2 1)
3.011 * * * [progress]: generating series expansions
3.011 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
3.012 * * * * [progress]: [ 2 / 4 ] generating series at (2)
3.012 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2)
3.012 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2 1)
3.012 * * * [progress]: simplifying candidates
3.012 * * * * [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)))))>
3.012 * * * * [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))))))>
3.012 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
3.012 * * [simplify]: iters left: 4 (9 enodes)
3.016 * * [simplify]: iters left: 3 (24 enodes)
3.020 * * [simplify]: iters left: 2 (47 enodes)
3.029 * * [simplify]: iters left: 1 (110 enodes)
3.078 * * [simplify]: Extracting #0: cost 1 inf + 0
3.078 * * [simplify]: Extracting #1: cost 6 inf + 0
3.078 * * [simplify]: Extracting #2: cost 10 inf + 1
3.078 * * [simplify]: Extracting #3: cost 23 inf + 403
3.078 * * [simplify]: Extracting #4: cost 60 inf + 1445
3.079 * * [simplify]: Extracting #5: cost 79 inf + 13843
3.082 * * [simplify]: Extracting #6: cost 73 inf + 57826
3.092 * * [simplify]: Extracting #7: cost 3 inf + 171780
3.104 * * [simplify]: Extracting #8: cost 0 inf + 178629
3.116 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
3.117 * [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.117 * * * * [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.117 * * * * [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.117 * * * * [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.117 * [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.118 * * [simplify]: iters left: 6 (15 enodes)
3.124 * * [simplify]: iters left: 5 (47 enodes)
3.142 * * [simplify]: iters left: 4 (100 enodes)
3.182 * * [simplify]: iters left: 3 (250 enodes)
3.369 * * [simplify]: Extracting #0: cost 1 inf + 0
3.369 * * [simplify]: Extracting #1: cost 7 inf + 0
3.369 * * [simplify]: Extracting #2: cost 38 inf + 0
3.370 * * [simplify]: Extracting #3: cost 89 inf + 404
3.370 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.373 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.379 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.390 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.405 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.418 * [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.418 * [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.418 * * * * [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.418 * [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.419 * * [simplify]: iters left: 6 (15 enodes)
3.422 * * [simplify]: iters left: 5 (47 enodes)
3.431 * * [simplify]: iters left: 4 (100 enodes)
3.458 * * [simplify]: iters left: 3 (250 enodes)
3.614 * * [simplify]: Extracting #0: cost 1 inf + 0
3.614 * * [simplify]: Extracting #1: cost 7 inf + 0
3.614 * * [simplify]: Extracting #2: cost 38 inf + 0
3.614 * * [simplify]: Extracting #3: cost 89 inf + 404
3.616 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.621 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.628 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.637 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.646 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.664 * [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.664 * [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.664 * * * * [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.665 * [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.665 * * [simplify]: iters left: 6 (15 enodes)
3.672 * * [simplify]: iters left: 5 (47 enodes)
3.689 * * [simplify]: iters left: 4 (100 enodes)
3.717 * * [simplify]: iters left: 3 (250 enodes)
3.857 * * [simplify]: Extracting #0: cost 1 inf + 0
3.857 * * [simplify]: Extracting #1: cost 7 inf + 0
3.857 * * [simplify]: Extracting #2: cost 38 inf + 0
3.858 * * [simplify]: Extracting #3: cost 89 inf + 404
3.859 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.865 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.878 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.895 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.913 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.931 * [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.931 * [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.931 * * * * [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.931 * [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.931 * * [simplify]: iters left: 6 (15 enodes)
3.938 * * [simplify]: iters left: 5 (47 enodes)
3.958 * * [simplify]: iters left: 4 (100 enodes)
3.995 * * [simplify]: iters left: 3 (250 enodes)
4.177 * * [simplify]: Extracting #0: cost 1 inf + 0
4.177 * * [simplify]: Extracting #1: cost 7 inf + 0
4.177 * * [simplify]: Extracting #2: cost 38 inf + 0
4.178 * * [simplify]: Extracting #3: cost 89 inf + 404
4.179 * * [simplify]: Extracting #4: cost 105 inf + 13282
4.186 * * [simplify]: Extracting #5: cost 75 inf + 74603
4.198 * * [simplify]: Extracting #6: cost 45 inf + 171652
4.215 * * [simplify]: Extracting #7: cost 3 inf + 235044
4.234 * * [simplify]: Extracting #8: cost 0 inf + 242171
4.247 * [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.247 * [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.247 * * * [progress]: adding candidates to table
4.532 * * [progress]: iteration 3 / 4
4.532 * * * [progress]: picking best candidate
4.600 * * * * [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.600 * * * [progress]: localizing error
4.943 * * * [progress]: generating rewritten candidates
4.943 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2)
4.946 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
4.948 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2)
4.948 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 1)
4.951 * * * [progress]: generating series expansions
4.951 * * * * [progress]: [ 1 / 4 ] generating series at (2 2)
4.951 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
4.951 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2)
4.952 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 1)
4.952 * * * [progress]: simplifying candidates
4.952 * * * * [progress]: [ 1 / 7 ] 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.952 * * * * [progress]: [ 2 / 7 ] 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) (neg.p16 (*.p16 a c)))))))>
4.952 * * * * [progress]: [ 3 / 7 ] 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)))))))>
4.952 * * * * [progress]: [ 4 / 7 ] 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.952 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.952 * * [simplify]: iters left: 4 (9 enodes)
4.954 * * [simplify]: iters left: 3 (24 enodes)
4.957 * * [simplify]: iters left: 2 (47 enodes)
4.971 * * [simplify]: iters left: 1 (110 enodes)
5.002 * * [simplify]: Extracting #0: cost 1 inf + 0
5.002 * * [simplify]: Extracting #1: cost 6 inf + 0
5.002 * * [simplify]: Extracting #2: cost 10 inf + 1
5.002 * * [simplify]: Extracting #3: cost 23 inf + 403
5.002 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.003 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.004 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.009 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.015 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.021 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.021 * [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.021 * * * * [progress]: [ 5 / 7 ] 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.021 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.021 * * [simplify]: iters left: 4 (9 enodes)
5.023 * * [simplify]: iters left: 3 (24 enodes)
5.027 * * [simplify]: iters left: 2 (47 enodes)
5.035 * * [simplify]: iters left: 1 (110 enodes)
5.069 * * [simplify]: Extracting #0: cost 1 inf + 0
5.069 * * [simplify]: Extracting #1: cost 6 inf + 0
5.069 * * [simplify]: Extracting #2: cost 10 inf + 1
5.070 * * [simplify]: Extracting #3: cost 23 inf + 403
5.070 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.071 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.074 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.084 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.095 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.107 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.107 * [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.108 * * * * [progress]: [ 6 / 7 ] 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.108 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.108 * * [simplify]: iters left: 4 (9 enodes)
5.112 * * [simplify]: iters left: 3 (24 enodes)
5.120 * * [simplify]: iters left: 2 (47 enodes)
5.137 * * [simplify]: iters left: 1 (110 enodes)
5.193 * * [simplify]: Extracting #0: cost 1 inf + 0
5.193 * * [simplify]: Extracting #1: cost 6 inf + 0
5.193 * * [simplify]: Extracting #2: cost 10 inf + 1
5.193 * * [simplify]: Extracting #3: cost 23 inf + 403
5.193 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.194 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.197 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.202 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.208 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.214 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.214 * [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.215 * * * * [progress]: [ 7 / 7 ] 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.215 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.215 * * [simplify]: iters left: 4 (9 enodes)
5.217 * * [simplify]: iters left: 3 (24 enodes)
5.221 * * [simplify]: iters left: 2 (47 enodes)
5.229 * * [simplify]: iters left: 1 (110 enodes)
5.256 * * [simplify]: Extracting #0: cost 1 inf + 0
5.256 * * [simplify]: Extracting #1: cost 6 inf + 0
5.256 * * [simplify]: Extracting #2: cost 10 inf + 1
5.258 * * [simplify]: Extracting #3: cost 23 inf + 403
5.258 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.259 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.260 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.265 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.272 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.277 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.278 * [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.278 * * * [progress]: adding candidates to table
5.395 * * [progress]: iteration 4 / 4
5.395 * * * [progress]: picking best candidate
5.426 * * * * [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.426 * * * [progress]: localizing error
5.741 * * * [progress]: generating rewritten candidates
5.742 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2 2 1)
5.750 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 2)
5.753 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
5.755 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2)
5.756 * * * [progress]: generating series expansions
5.756 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2 2 1)
5.756 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 2)
5.756 * * * * [progress]: [ 3 / 4 ] generating series at (2)
5.756 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2)
5.756 * * * [progress]: simplifying candidates
5.756 * * * * [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.756 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
5.757 * * [simplify]: iters left: 2 (6 enodes)
5.758 * * [simplify]: iters left: 1 (14 enodes)
5.760 * * [simplify]: Extracting #0: cost 1 inf + 0
5.760 * * [simplify]: Extracting #1: cost 3 inf + 0
5.760 * * [simplify]: Extracting #2: cost 6 inf + 0
5.760 * * [simplify]: Extracting #3: cost 2 inf + 325
5.760 * * [simplify]: Extracting #4: cost 0 inf + 1329
5.760 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
5.760 * [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.760 * * * * [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.760 * [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.760 * * [simplify]: iters left: 4 (10 enodes)
5.763 * * [simplify]: iters left: 3 (43 enodes)
5.773 * * [simplify]: iters left: 2 (121 enodes)
5.817 * * [simplify]: iters left: 1 (429 enodes)
6.130 * * [simplify]: Extracting #0: cost 1 inf + 0
6.131 * * [simplify]: Extracting #1: cost 46 inf + 0
6.132 * * [simplify]: Extracting #2: cost 270 inf + 0
6.137 * * [simplify]: Extracting #3: cost 354 inf + 59003
6.161 * * [simplify]: Extracting #4: cost 345 inf + 369227
6.217 * * [simplify]: Extracting #5: cost 22 inf + 1102360
6.326 * * [simplify]: Extracting #6: cost 1 inf + 1150488
6.434 * * [simplify]: Extracting #7: cost 0 inf + 1155051
6.515 * [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.515 * [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.515 * * * * [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.515 * * * * [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.515 * [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.516 * * [simplify]: iters left: 6 (13 enodes)
6.521 * * [simplify]: iters left: 5 (39 enodes)
6.535 * * [simplify]: iters left: 4 (84 enodes)
6.571 * * [simplify]: iters left: 3 (271 enodes)
6.723 * * [simplify]: Extracting #0: cost 1 inf + 0
6.723 * * [simplify]: Extracting #1: cost 6 inf + 0
6.723 * * [simplify]: Extracting #2: cost 10 inf + 1
6.723 * * [simplify]: Extracting #3: cost 66 inf + 403
6.724 * * [simplify]: Extracting #4: cost 230 inf + 1445
6.728 * * [simplify]: Extracting #5: cost 349 inf + 32520
6.739 * * [simplify]: Extracting #6: cost 220 inf + 249925
6.765 * * [simplify]: Extracting #7: cost 28 inf + 656177
6.827 * * [simplify]: Extracting #8: cost 0 inf + 728735
6.878 * * [simplify]: Extracting #9: cost 0 inf + 726535
6.911 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
6.911 * [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.911 * * * * [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.911 * * * * [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.911 * * * * [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.911 * * * * [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.911 * * * [progress]: adding candidates to table
7.098 * [progress]: [Phase 3 of 3] Extracting.
7.098 * * [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 (-.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 (+.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 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 b_2 b_2) (*.p16 a c)))))))> #<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))>)
7.102 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
7.102 * * * * [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 (-.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 (+.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 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 b_2 b_2) (*.p16 a c)))))))> #<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))>)
7.267 * * * * [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 (-.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 (+.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 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 b_2 b_2) (*.p16 a c)))))))> #<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))>)
7.496 * * * * [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 (-.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 (+.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 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 b_2 b_2) (*.p16 a c)))))))> #<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))>)
7.626 * * * [regime]: Found split indices: #<option (#s(si 2 132) #s(si 4 256))>
7.627 * [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 (-.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 (+.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 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 b_2 b_2) (*.p16 a c)))))))> #<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))>)
7.628 * [regimes]: Found splitpoints: (#s(sp 2 b_2 #<cpointer:posit16>) #s(sp 4 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 (-.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 (+.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 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 b_2 b_2) (*.p16 a c)))))))> #<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))>)
7.628 * [simplify]: Simplifying (if (<=.p16 b_2 (real->posit16 0.0292205810546875)) (/.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.628 * * [simplify]: iters left: 6 (21 enodes)
7.630 * * [simplify]: Extracting #0: cost 1 inf + 0
7.630 * * [simplify]: Extracting #1: cost 4 inf + 0
7.630 * * [simplify]: Extracting #2: cost 10 inf + 0
7.630 * * [simplify]: Extracting #3: cost 12 inf + 2
7.630 * * [simplify]: Extracting #4: cost 13 inf + 84
7.630 * * [simplify]: Extracting #5: cost 15 inf + 152
7.630 * * [simplify]: Extracting #6: cost 11 inf + 716
7.630 * * [simplify]: Extracting #7: cost 6 inf + 3848
7.630 * * [simplify]: Extracting #8: cost 3 inf + 6937
7.631 * * [simplify]: Extracting #9: cost 0 inf + 13357
7.631 * [simplify]: Simplified to (if (<=.p16 b_2 (real->posit16 0.0292205810546875)) (/.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.631 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
7.669 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
7.671 * * * * [points]: Setting MPFR precision to 64
7.673 * * * * [points]: Setting MPFR precision to 320
7.674 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
7.676 * * * * [points]: Setting MPFR precision to 64
7.680 * * * * [points]: Setting MPFR precision to 320
7.683 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
7.685 * * * * [points]: Setting MPFR precision to 64
7.691 * * * * [points]: Setting MPFR precision to 320
7.698 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
7.700 * * * * [points]: Setting MPFR precision to 64
7.713 * * * * [points]: Setting MPFR precision to 320
7.726 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
7.728 * * * * [points]: Setting MPFR precision to 64
7.781 * * * * [points]: Setting MPFR precision to 320
7.812 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
7.815 * * * * [points]: Setting MPFR precision to 64
7.874 * * * * [points]: Setting MPFR precision to 320
7.934 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
7.936 * * * * [points]: Setting MPFR precision to 64
8.109 * * * * [points]: Setting MPFR precision to 320
8.232 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
8.235 * * * * [points]: Setting MPFR precision to 64
8.525 * * * * [points]: Setting MPFR precision to 320
8.866 * * * * [points]: Computing exacts for 8000 points
8.868 * * * * [points]: Setting MPFR precision to 64
10.300 * * * * [points]: Setting MPFR precision to 320
11.291 * * * * [points]: Filtering points with unrepresentable outputs
11.310 * * * * [points]: Sampled 8000 points with exact outputs
14.913 * [regime-testing]: Baseline error score: 64.0
14.917 * [regime-testing]: Oracle error score: 64.0
14.924 * [regime-testing]: End program error score: 0.44923254724481226