0.003 * [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.071 * * * * [points]: Setting MPFR precision to 64
0.075 * * * * [points]: Setting MPFR precision to 320
0.077 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.079 * * * * [points]: Setting MPFR precision to 64
0.082 * * * * [points]: Setting MPFR precision to 320
0.084 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.085 * * * * [points]: Setting MPFR precision to 64
0.088 * * * * [points]: Setting MPFR precision to 320
0.092 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.093 * * * * [points]: Setting MPFR precision to 64
0.099 * * * * [points]: Setting MPFR precision to 320
0.105 * * * * [points]: Computing exacts for 256 points
0.106 * * * * [points]: Setting MPFR precision to 64
0.123 * * * * [points]: Setting MPFR precision to 320
0.144 * * * * [points]: Filtering points with unrepresentable outputs
0.146 * * * * [points]: Sampled 256 points with exact outputs
0.147 * * * [progress]: [2/2] Setting up program.
0.206 * [progress]: [Phase 2 of 3] Improving.
0.206 * * * * [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.208 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.209 * * [simplify]: iters left: 5 (10 enodes)
0.214 * * [simplify]: iters left: 4 (31 enodes)
0.221 * * [simplify]: iters left: 3 (65 enodes)
0.233 * * [simplify]: iters left: 2 (207 enodes)
0.347 * * [simplify]: Extracting #0: cost 1 inf + 0
0.348 * * [simplify]: Extracting #1: cost 20 inf + 0
0.348 * * [simplify]: Extracting #2: cost 89 inf + 1
0.348 * * [simplify]: Extracting #3: cost 168 inf + 83
0.349 * * [simplify]: Extracting #4: cost 227 inf + 12401
0.353 * * [simplify]: Extracting #5: cost 180 inf + 98398
0.364 * * [simplify]: Extracting #6: cost 61 inf + 349602
0.381 * * [simplify]: Extracting #7: cost 2 inf + 436444
0.411 * * [simplify]: Extracting #8: cost 0 inf + 442330
0.431 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
0.432 * [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.443 * * [progress]: iteration 1 / 4
0.443 * * * [progress]: picking best candidate
0.458 * * * * [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.458 * * * [progress]: localizing error
0.647 * * * [progress]: generating rewritten candidates
0.647 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.650 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
0.651 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
0.653 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
0.657 * * * [progress]: generating series expansions
0.658 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.658 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
0.658 * * * * [progress]: [ 3 / 4 ] generating series at (2)
0.658 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
0.658 * * * [progress]: simplifying candidates
0.658 * * * * [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.658 * * * * [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.658 * * * * [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.658 * [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.658 * * [simplify]: iters left: 5 (11 enodes)
0.661 * * [simplify]: iters left: 4 (35 enodes)
0.667 * * [simplify]: iters left: 3 (100 enodes)
0.706 * * [simplify]: iters left: 2 (360 enodes)
0.965 * * [simplify]: Extracting #0: cost 1 inf + 0
0.965 * * [simplify]: Extracting #1: cost 48 inf + 0
0.966 * * [simplify]: Extracting #2: cost 223 inf + 0
0.970 * * [simplify]: Extracting #3: cost 348 inf + 45039
0.995 * * [simplify]: Extracting #4: cost 315 inf + 336131
1.066 * * [simplify]: Extracting #5: cost 84 inf + 852438
1.147 * * [simplify]: Extracting #6: cost 1 inf + 990774
1.204 * * [simplify]: Extracting #7: cost 0 inf + 992777
1.261 * [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.261 * [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.261 * * * * [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.261 * * * * [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.261 * * * * [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.261 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.261 * * [simplify]: iters left: 5 (10 enodes)
1.265 * * [simplify]: iters left: 4 (31 enodes)
1.276 * * [simplify]: iters left: 3 (65 enodes)
1.295 * * [simplify]: iters left: 2 (207 enodes)
1.370 * * [simplify]: Extracting #0: cost 1 inf + 0
1.370 * * [simplify]: Extracting #1: cost 20 inf + 0
1.371 * * [simplify]: Extracting #2: cost 89 inf + 1
1.371 * * [simplify]: Extracting #3: cost 168 inf + 83
1.373 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.380 * * [simplify]: Extracting #5: cost 180 inf + 98398
1.403 * * [simplify]: Extracting #6: cost 61 inf + 349602
1.422 * * [simplify]: Extracting #7: cost 2 inf + 436444
1.442 * * [simplify]: Extracting #8: cost 0 inf + 442330
1.474 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.474 * [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.474 * * * * [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.475 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.475 * * [simplify]: iters left: 5 (10 enodes)
1.479 * * [simplify]: iters left: 4 (31 enodes)
1.490 * * [simplify]: iters left: 3 (65 enodes)
1.515 * * [simplify]: iters left: 2 (207 enodes)
1.589 * * [simplify]: Extracting #0: cost 1 inf + 0
1.589 * * [simplify]: Extracting #1: cost 20 inf + 0
1.589 * * [simplify]: Extracting #2: cost 89 inf + 1
1.589 * * [simplify]: Extracting #3: cost 168 inf + 83
1.590 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.593 * * [simplify]: Extracting #5: cost 180 inf + 98398
1.605 * * [simplify]: Extracting #6: cost 61 inf + 349602
1.637 * * [simplify]: Extracting #7: cost 2 inf + 436444
1.669 * * [simplify]: Extracting #8: cost 0 inf + 442330
1.688 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.688 * [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.688 * * * * [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.688 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.689 * * [simplify]: iters left: 5 (10 enodes)
1.690 * * [simplify]: iters left: 4 (31 enodes)
1.696 * * [simplify]: iters left: 3 (65 enodes)
1.714 * * [simplify]: iters left: 2 (207 enodes)
1.823 * * [simplify]: Extracting #0: cost 1 inf + 0
1.823 * * [simplify]: Extracting #1: cost 20 inf + 0
1.824 * * [simplify]: Extracting #2: cost 89 inf + 1
1.824 * * [simplify]: Extracting #3: cost 168 inf + 83
1.826 * * [simplify]: Extracting #4: cost 227 inf + 12401
1.833 * * [simplify]: Extracting #5: cost 180 inf + 98398
1.856 * * [simplify]: Extracting #6: cost 61 inf + 349602
1.891 * * [simplify]: Extracting #7: cost 2 inf + 436444
1.923 * * [simplify]: Extracting #8: cost 0 inf + 442330
1.945 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1.945 * [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.945 * * * * [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))>
1.945 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.945 * * [simplify]: iters left: 5 (10 enodes)
1.947 * * [simplify]: iters left: 4 (31 enodes)
1.952 * * [simplify]: iters left: 3 (65 enodes)
1.965 * * [simplify]: iters left: 2 (207 enodes)
2.060 * * [simplify]: Extracting #0: cost 1 inf + 0
2.060 * * [simplify]: Extracting #1: cost 20 inf + 0
2.061 * * [simplify]: Extracting #2: cost 89 inf + 1
2.062 * * [simplify]: Extracting #3: cost 168 inf + 83
2.063 * * [simplify]: Extracting #4: cost 227 inf + 12401
2.070 * * [simplify]: Extracting #5: cost 180 inf + 98398
2.093 * * [simplify]: Extracting #6: cost 61 inf + 349602
2.127 * * [simplify]: Extracting #7: cost 2 inf + 436444
2.160 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.183 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.183 * [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.183 * * * [progress]: adding candidates to table
2.449 * * [progress]: iteration 2 / 4
2.449 * * * [progress]: picking best candidate
2.510 * * * * [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.510 * * * [progress]: localizing error
2.777 * * * [progress]: generating rewritten candidates
2.777 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
2.779 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
2.782 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2)
2.782 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2 1)
2.786 * * * [progress]: generating series expansions
2.786 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
2.786 * * * * [progress]: [ 2 / 4 ] generating series at (2)
2.786 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2)
2.786 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2 1)
2.786 * * * [progress]: simplifying candidates
2.786 * * * * [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.786 * * * * [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.786 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
2.786 * * [simplify]: iters left: 4 (9 enodes)
2.788 * * [simplify]: iters left: 3 (24 enodes)
2.792 * * [simplify]: iters left: 2 (47 enodes)
2.800 * * [simplify]: iters left: 1 (110 enodes)
2.831 * * [simplify]: Extracting #0: cost 1 inf + 0
2.832 * * [simplify]: Extracting #1: cost 6 inf + 0
2.832 * * [simplify]: Extracting #2: cost 10 inf + 1
2.832 * * [simplify]: Extracting #3: cost 23 inf + 403
2.832 * * [simplify]: Extracting #4: cost 60 inf + 1445
2.832 * * [simplify]: Extracting #5: cost 79 inf + 13843
2.834 * * [simplify]: Extracting #6: cost 73 inf + 57826
2.839 * * [simplify]: Extracting #7: cost 3 inf + 171780
2.845 * * [simplify]: Extracting #8: cost 0 inf + 178629
2.853 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
2.853 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
2.853 * * * * [progress]: [ 3 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c))))))))>
2.853 * * * * [progress]: [ 4 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
2.853 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
2.853 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
2.854 * * [simplify]: iters left: 6 (15 enodes)
2.857 * * [simplify]: iters left: 5 (47 enodes)
2.873 * * [simplify]: iters left: 4 (100 enodes)
2.910 * * [simplify]: iters left: 3 (250 enodes)
3.078 * * [simplify]: Extracting #0: cost 1 inf + 0
3.078 * * [simplify]: Extracting #1: cost 7 inf + 0
3.078 * * [simplify]: Extracting #2: cost 38 inf + 0
3.078 * * [simplify]: Extracting #3: cost 89 inf + 404
3.080 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.086 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.098 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.115 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.133 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.144 * [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.144 * [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.145 * * * * [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.145 * [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.145 * * [simplify]: iters left: 6 (15 enodes)
3.148 * * [simplify]: iters left: 5 (47 enodes)
3.156 * * [simplify]: iters left: 4 (100 enodes)
3.186 * * [simplify]: iters left: 3 (250 enodes)
3.331 * * [simplify]: Extracting #0: cost 1 inf + 0
3.331 * * [simplify]: Extracting #1: cost 7 inf + 0
3.331 * * [simplify]: Extracting #2: cost 38 inf + 0
3.332 * * [simplify]: Extracting #3: cost 89 inf + 404
3.334 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.340 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.352 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.370 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.388 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.406 * [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.406 * [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.406 * * * * [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.406 * [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.407 * * [simplify]: iters left: 6 (15 enodes)
3.413 * * [simplify]: iters left: 5 (47 enodes)
3.432 * * [simplify]: iters left: 4 (100 enodes)
3.473 * * [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.615 * * [simplify]: Extracting #2: cost 38 inf + 0
3.615 * * [simplify]: Extracting #3: cost 89 inf + 404
3.616 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.623 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.637 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.654 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.667 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.676 * [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.676 * [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]: [ 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.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.677 * * [simplify]: iters left: 6 (15 enodes)
3.680 * * [simplify]: iters left: 5 (47 enodes)
3.689 * * [simplify]: iters left: 4 (100 enodes)
3.709 * * [simplify]: iters left: 3 (250 enodes)
3.837 * * [simplify]: Extracting #0: cost 1 inf + 0
3.837 * * [simplify]: Extracting #1: cost 7 inf + 0
3.837 * * [simplify]: Extracting #2: cost 38 inf + 0
3.837 * * [simplify]: Extracting #3: cost 89 inf + 404
3.839 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.845 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.858 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.874 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.883 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.892 * [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.892 * [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.892 * * * [progress]: adding candidates to table
4.116 * * [progress]: iteration 3 / 4
4.117 * * * [progress]: picking best candidate
4.197 * * * * [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.197 * * * [progress]: localizing error
4.595 * * * [progress]: generating rewritten candidates
4.595 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2)
4.598 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
4.600 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2)
4.600 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 1)
4.603 * * * [progress]: generating series expansions
4.603 * * * * [progress]: [ 1 / 4 ] generating series at (2 2)
4.603 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
4.603 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2)
4.603 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 1)
4.603 * * * [progress]: simplifying candidates
4.603 * * * * [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.603 * * * * [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.603 * * * * [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.603 * * * * [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.604 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.604 * * [simplify]: iters left: 4 (9 enodes)
4.605 * * [simplify]: iters left: 3 (24 enodes)
4.609 * * [simplify]: iters left: 2 (47 enodes)
4.618 * * [simplify]: iters left: 1 (110 enodes)
4.667 * * [simplify]: Extracting #0: cost 1 inf + 0
4.667 * * [simplify]: Extracting #1: cost 6 inf + 0
4.667 * * [simplify]: Extracting #2: cost 10 inf + 1
4.667 * * [simplify]: Extracting #3: cost 23 inf + 403
4.668 * * [simplify]: Extracting #4: cost 60 inf + 1445
4.669 * * [simplify]: Extracting #5: cost 79 inf + 13843
4.672 * * [simplify]: Extracting #6: cost 73 inf + 57826
4.682 * * [simplify]: Extracting #7: cost 3 inf + 171780
4.693 * * [simplify]: Extracting #8: cost 0 inf + 178629
4.705 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
4.705 * [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.706 * * * * [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))))))>
4.706 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.706 * * [simplify]: iters left: 4 (9 enodes)
4.710 * * [simplify]: iters left: 3 (24 enodes)
4.718 * * [simplify]: iters left: 2 (47 enodes)
4.735 * * [simplify]: iters left: 1 (110 enodes)
4.777 * * [simplify]: Extracting #0: cost 1 inf + 0
4.777 * * [simplify]: Extracting #1: cost 6 inf + 0
4.777 * * [simplify]: Extracting #2: cost 10 inf + 1
4.777 * * [simplify]: Extracting #3: cost 23 inf + 403
4.777 * * [simplify]: Extracting #4: cost 60 inf + 1445
4.778 * * [simplify]: Extracting #5: cost 79 inf + 13843
4.779 * * [simplify]: Extracting #6: cost 73 inf + 57826
4.784 * * [simplify]: Extracting #7: cost 3 inf + 171780
4.791 * * [simplify]: Extracting #8: cost 0 inf + 178629
4.797 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
4.797 * [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.798 * * * * [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))))))>
4.798 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.798 * * [simplify]: iters left: 4 (9 enodes)
4.800 * * [simplify]: iters left: 3 (24 enodes)
4.804 * * [simplify]: iters left: 2 (47 enodes)
4.812 * * [simplify]: iters left: 1 (110 enodes)
4.857 * * [simplify]: Extracting #0: cost 1 inf + 0
4.857 * * [simplify]: Extracting #1: cost 6 inf + 0
4.857 * * [simplify]: Extracting #2: cost 10 inf + 1
4.857 * * [simplify]: Extracting #3: cost 23 inf + 403
4.857 * * [simplify]: Extracting #4: cost 60 inf + 1445
4.859 * * [simplify]: Extracting #5: cost 79 inf + 13843
4.862 * * [simplify]: Extracting #6: cost 73 inf + 57826
4.872 * * [simplify]: Extracting #7: cost 3 inf + 171780
4.883 * * [simplify]: Extracting #8: cost 0 inf + 178629
4.895 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
4.895 * [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.896 * * * * [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))))))>
4.896 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
4.896 * * [simplify]: iters left: 4 (9 enodes)
4.901 * * [simplify]: iters left: 3 (24 enodes)
4.909 * * [simplify]: iters left: 2 (47 enodes)
4.927 * * [simplify]: iters left: 1 (110 enodes)
4.979 * * [simplify]: Extracting #0: cost 1 inf + 0
4.979 * * [simplify]: Extracting #1: cost 6 inf + 0
4.979 * * [simplify]: Extracting #2: cost 10 inf + 1
4.979 * * [simplify]: Extracting #3: cost 23 inf + 403
4.980 * * [simplify]: Extracting #4: cost 60 inf + 1445
4.980 * * [simplify]: Extracting #5: cost 79 inf + 13843
4.982 * * [simplify]: Extracting #6: cost 73 inf + 57826
4.987 * * [simplify]: Extracting #7: cost 3 inf + 171780
4.992 * * [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]: adding candidates to table
5.162 * * [progress]: iteration 4 / 4
5.162 * * * [progress]: picking best candidate
5.207 * * * * [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.207 * * * [progress]: localizing error
5.659 * * * [progress]: generating rewritten candidates
5.659 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2 2 1)
5.675 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 2)
5.681 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
5.684 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2)
5.685 * * * [progress]: generating series expansions
5.685 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2 2 1)
5.685 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 2)
5.685 * * * * [progress]: [ 3 / 4 ] generating series at (2)
5.685 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2)
5.685 * * * [progress]: simplifying candidates
5.685 * * * * [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.685 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
5.685 * * [simplify]: iters left: 2 (6 enodes)
5.686 * * [simplify]: iters left: 1 (14 enodes)
5.695 * * [simplify]: Extracting #0: cost 1 inf + 0
5.695 * * [simplify]: Extracting #1: cost 3 inf + 0
5.695 * * [simplify]: Extracting #2: cost 6 inf + 0
5.695 * * [simplify]: Extracting #3: cost 2 inf + 325
5.695 * * [simplify]: Extracting #4: cost 0 inf + 1329
5.695 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
5.695 * [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.695 * * * * [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.696 * [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.696 * * [simplify]: iters left: 4 (10 enodes)
5.698 * * [simplify]: iters left: 3 (43 enodes)
5.707 * * [simplify]: iters left: 2 (121 enodes)
5.737 * * [simplify]: iters left: 1 (429 enodes)
5.987 * * [simplify]: Extracting #0: cost 1 inf + 0
5.987 * * [simplify]: Extracting #1: cost 46 inf + 0
5.988 * * [simplify]: Extracting #2: cost 270 inf + 0
5.993 * * [simplify]: Extracting #3: cost 354 inf + 59003
6.021 * * [simplify]: Extracting #4: cost 345 inf + 369227
6.109 * * [simplify]: Extracting #5: cost 22 inf + 1102360
6.219 * * [simplify]: Extracting #6: cost 1 inf + 1150488
6.321 * * [simplify]: Extracting #7: cost 0 inf + 1155051
6.378 * [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.378 * [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.378 * * * * [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.378 * * * * [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.378 * [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.378 * * [simplify]: iters left: 6 (13 enodes)
6.382 * * [simplify]: iters left: 5 (39 enodes)
6.389 * * [simplify]: iters left: 4 (84 enodes)
6.415 * * [simplify]: iters left: 3 (271 enodes)
6.562 * * [simplify]: Extracting #0: cost 1 inf + 0
6.562 * * [simplify]: Extracting #1: cost 6 inf + 0
6.562 * * [simplify]: Extracting #2: cost 10 inf + 1
6.563 * * [simplify]: Extracting #3: cost 66 inf + 403
6.564 * * [simplify]: Extracting #4: cost 230 inf + 1445
6.568 * * [simplify]: Extracting #5: cost 349 inf + 32520
6.584 * * [simplify]: Extracting #6: cost 220 inf + 249925
6.635 * * [simplify]: Extracting #7: cost 28 inf + 656177
6.699 * * [simplify]: Extracting #8: cost 0 inf + 728735
6.764 * * [simplify]: Extracting #9: cost 0 inf + 726535
6.827 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
6.828 * [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.828 * * * * [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.828 * * * * [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.828 * * * * [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.828 * * * * [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.828 * * * [progress]: adding candidates to table
6.999 * [progress]: [Phase 3 of 3] Extracting.
7.000 * * [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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 (*.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 (*.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 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>)
7.003 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
7.004 * * * * [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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 (*.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 (*.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 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>)
7.130 * * * * [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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 (*.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 (*.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 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>)
7.297 * * * * [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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 (*.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 (*.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 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>)
7.427 * * * [regime]: Found split indices: #<option (#s(si 3 132) #s(si 1 256))>
7.428 * [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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 (*.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 (*.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 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>)
7.429 * [regimes]: Found splitpoints: (#s(sp 3 b_2 #<cpointer:posit16>) #s(sp 1 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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<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 (*.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 (*.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 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>)
7.429 * [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.430 * * [simplify]: iters left: 6 (21 enodes)
7.431 * * [simplify]: Extracting #0: cost 1 inf + 0
7.431 * * [simplify]: Extracting #1: cost 4 inf + 0
7.431 * * [simplify]: Extracting #2: cost 10 inf + 0
7.431 * * [simplify]: Extracting #3: cost 12 inf + 2
7.431 * * [simplify]: Extracting #4: cost 13 inf + 84
7.431 * * [simplify]: Extracting #5: cost 15 inf + 152
7.431 * * [simplify]: Extracting #6: cost 11 inf + 716
7.431 * * [simplify]: Extracting #7: cost 6 inf + 3848
7.432 * * [simplify]: Extracting #8: cost 3 inf + 6937
7.432 * * [simplify]: Extracting #9: cost 0 inf + 13357
7.432 * [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.432 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
7.467 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
7.469 * * * * [points]: Setting MPFR precision to 64
7.470 * * * * [points]: Setting MPFR precision to 320
7.471 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
7.472 * * * * [points]: Setting MPFR precision to 64
7.474 * * * * [points]: Setting MPFR precision to 320
7.476 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
7.478 * * * * [points]: Setting MPFR precision to 64
7.481 * * * * [points]: Setting MPFR precision to 320
7.485 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
7.487 * * * * [points]: Setting MPFR precision to 64
7.495 * * * * [points]: Setting MPFR precision to 320
7.503 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
7.504 * * * * [points]: Setting MPFR precision to 64
7.520 * * * * [points]: Setting MPFR precision to 320
7.537 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
7.538 * * * * [points]: Setting MPFR precision to 64
7.596 * * * * [points]: Setting MPFR precision to 320
7.630 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
7.631 * * * * [points]: Setting MPFR precision to 64
7.724 * * * * [points]: Setting MPFR precision to 320
7.867 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
7.869 * * * * [points]: Setting MPFR precision to 64
8.024 * * * * [points]: Setting MPFR precision to 320
8.192 * * * * [points]: Computing exacts for 8000 points
8.194 * * * * [points]: Setting MPFR precision to 64
9.156 * * * * [points]: Setting MPFR precision to 320
9.891 * * * * [points]: Filtering points with unrepresentable outputs
9.913 * * * * [points]: Sampled 8000 points with exact outputs
13.610 * [regime-testing]: Baseline error score: 64.0
13.614 * [regime-testing]: Oracle error score: 64.0
13.620 * [regime-testing]: End program error score: 0.44923254724481226