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.123 * * * * [points]: Setting MPFR precision to 64
0.132 * * * * [points]: Setting MPFR precision to 320
0.135 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.137 * * * * [points]: Setting MPFR precision to 64
0.140 * * * * [points]: Setting MPFR precision to 320
0.145 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.147 * * * * [points]: Setting MPFR precision to 64
0.152 * * * * [points]: Setting MPFR precision to 320
0.159 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.160 * * * * [points]: Setting MPFR precision to 64
0.166 * * * * [points]: Setting MPFR precision to 320
0.171 * * * * [points]: Computing exacts for 256 points
0.173 * * * * [points]: Setting MPFR precision to 64
0.196 * * * * [points]: Setting MPFR precision to 320
0.246 * * * * [points]: Filtering points with unrepresentable outputs
0.249 * * * * [points]: Sampled 256 points with exact outputs
0.250 * * * [progress]: [2/2] Setting up program.
0.278 * [progress]: [Phase 2 of 3] Improving.
0.278 * * * * [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.281 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.283 * * [simplify]: iters left: 5 (10 enodes)
0.434 * * [simplify]: iters left: 4 (31 enodes)
0.447 * * [simplify]: iters left: 3 (65 enodes)
0.476 * * [simplify]: iters left: 2 (207 enodes)
0.795 * * [simplify]: Extracting #0: cost 1 inf + 0
0.796 * * [simplify]: Extracting #1: cost 20 inf + 0
0.796 * * [simplify]: Extracting #2: cost 89 inf + 1
0.797 * * [simplify]: Extracting #3: cost 168 inf + 83
0.799 * * [simplify]: Extracting #4: cost 227 inf + 12401
0.806 * * [simplify]: Extracting #5: cost 180 inf + 98398
0.830 * * [simplify]: Extracting #6: cost 61 inf + 349602
0.851 * * [simplify]: Extracting #7: cost 2 inf + 436444
0.869 * * [simplify]: Extracting #8: cost 0 inf + 442330
0.897 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
0.897 * [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.948 * * [progress]: iteration 1 / 4
0.948 * * * [progress]: picking best candidate
0.971 * * * * [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.971 * * * [progress]: localizing error
1.241 * * * [progress]: generating rewritten candidates
1.241 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.245 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1.245 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1.248 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
1.252 * * * [progress]: generating series expansions
1.253 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.253 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1.253 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1.253 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
1.253 * * * [progress]: simplifying candidates
1.253 * * * * [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))>
1.253 * * * * [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))>
1.253 * * * * [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)))))))>
1.254 * [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)))))
1.254 * * [simplify]: iters left: 5 (11 enodes)
1.259 * * [simplify]: iters left: 4 (35 enodes)
1.272 * * [simplify]: iters left: 3 (100 enodes)
1.318 * * [simplify]: iters left: 2 (360 enodes)
1.589 * * [simplify]: Extracting #0: cost 1 inf + 0
1.590 * * [simplify]: Extracting #1: cost 48 inf + 0
1.591 * * [simplify]: Extracting #2: cost 223 inf + 0
1.595 * * [simplify]: Extracting #3: cost 348 inf + 45039
1.617 * * [simplify]: Extracting #4: cost 315 inf + 336131
1.680 * * [simplify]: Extracting #5: cost 84 inf + 852438
1.757 * * [simplify]: Extracting #6: cost 1 inf + 990774
1.814 * * [simplify]: Extracting #7: cost 0 inf + 992777
1.895 * [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.895 * [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.895 * * * * [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.896 * * * * [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.896 * * * * [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.896 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1.896 * * [simplify]: iters left: 5 (10 enodes)
1.900 * * [simplify]: iters left: 4 (31 enodes)
1.912 * * [simplify]: iters left: 3 (65 enodes)
1.939 * * [simplify]: iters left: 2 (207 enodes)
2.054 * * [simplify]: Extracting #0: cost 1 inf + 0
2.054 * * [simplify]: Extracting #1: cost 20 inf + 0
2.054 * * [simplify]: Extracting #2: cost 89 inf + 1
2.054 * * [simplify]: Extracting #3: cost 168 inf + 83
2.055 * * [simplify]: Extracting #4: cost 227 inf + 12401
2.059 * * [simplify]: Extracting #5: cost 180 inf + 98398
2.071 * * [simplify]: Extracting #6: cost 61 inf + 349602
2.109 * * [simplify]: Extracting #7: cost 2 inf + 436444
2.142 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.161 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.161 * [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.161 * * * * [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))>
2.161 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.161 * * [simplify]: iters left: 5 (10 enodes)
2.163 * * [simplify]: iters left: 4 (31 enodes)
2.170 * * [simplify]: iters left: 3 (65 enodes)
2.195 * * [simplify]: iters left: 2 (207 enodes)
2.309 * * [simplify]: Extracting #0: cost 1 inf + 0
2.309 * * [simplify]: Extracting #1: cost 20 inf + 0
2.310 * * [simplify]: Extracting #2: cost 89 inf + 1
2.310 * * [simplify]: Extracting #3: cost 168 inf + 83
2.312 * * [simplify]: Extracting #4: cost 227 inf + 12401
2.319 * * [simplify]: Extracting #5: cost 180 inf + 98398
2.344 * * [simplify]: Extracting #6: cost 61 inf + 349602
2.379 * * [simplify]: Extracting #7: cost 2 inf + 436444
2.412 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.444 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.445 * [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.445 * * * * [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))>
2.445 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.445 * * [simplify]: iters left: 5 (10 enodes)
2.449 * * [simplify]: iters left: 4 (31 enodes)
2.459 * * [simplify]: iters left: 3 (65 enodes)
2.483 * * [simplify]: iters left: 2 (207 enodes)
2.591 * * [simplify]: Extracting #0: cost 1 inf + 0
2.591 * * [simplify]: Extracting #1: cost 20 inf + 0
2.591 * * [simplify]: Extracting #2: cost 89 inf + 1
2.591 * * [simplify]: Extracting #3: cost 168 inf + 83
2.592 * * [simplify]: Extracting #4: cost 227 inf + 12401
2.595 * * [simplify]: Extracting #5: cost 180 inf + 98398
2.607 * * [simplify]: Extracting #6: cost 61 inf + 349602
2.624 * * [simplify]: Extracting #7: cost 2 inf + 436444
2.642 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.659 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.659 * [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.659 * * * * [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.659 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.659 * * [simplify]: iters left: 5 (10 enodes)
2.661 * * [simplify]: iters left: 4 (31 enodes)
2.666 * * [simplify]: iters left: 3 (65 enodes)
2.679 * * [simplify]: iters left: 2 (207 enodes)
2.756 * * [simplify]: Extracting #0: cost 1 inf + 0
2.756 * * [simplify]: Extracting #1: cost 20 inf + 0
2.756 * * [simplify]: Extracting #2: cost 89 inf + 1
2.757 * * [simplify]: Extracting #3: cost 168 inf + 83
2.759 * * [simplify]: Extracting #4: cost 227 inf + 12401
2.765 * * [simplify]: Extracting #5: cost 180 inf + 98398
2.789 * * [simplify]: Extracting #6: cost 61 inf + 349602
2.809 * * [simplify]: Extracting #7: cost 2 inf + 436444
2.827 * * [simplify]: Extracting #8: cost 0 inf + 442330
2.853 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.853 * [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.853 * * * [progress]: adding candidates to table
3.073 * * [progress]: iteration 2 / 4
3.073 * * * [progress]: picking best candidate
3.115 * * * * [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)))))))>
3.115 * * * [progress]: localizing error
3.405 * * * [progress]: generating rewritten candidates
3.405 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
3.413 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
3.416 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2)
3.416 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2 1)
3.419 * * * [progress]: generating series expansions
3.419 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
3.419 * * * * [progress]: [ 2 / 4 ] generating series at (2)
3.419 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2)
3.419 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2 1)
3.419 * * * [progress]: simplifying candidates
3.419 * * * * [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.419 * * * * [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.419 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
3.419 * * [simplify]: iters left: 4 (9 enodes)
3.422 * * [simplify]: iters left: 3 (24 enodes)
3.425 * * [simplify]: iters left: 2 (47 enodes)
3.434 * * [simplify]: iters left: 1 (110 enodes)
3.463 * * [simplify]: Extracting #0: cost 1 inf + 0
3.463 * * [simplify]: Extracting #1: cost 6 inf + 0
3.463 * * [simplify]: Extracting #2: cost 10 inf + 1
3.463 * * [simplify]: Extracting #3: cost 23 inf + 403
3.464 * * [simplify]: Extracting #4: cost 60 inf + 1445
3.465 * * [simplify]: Extracting #5: cost 79 inf + 13843
3.468 * * [simplify]: Extracting #6: cost 73 inf + 57826
3.478 * * [simplify]: Extracting #7: cost 3 inf + 171780
3.489 * * [simplify]: Extracting #8: cost 0 inf + 178629
3.501 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
3.501 * [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.501 * * * * [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.502 * * * * [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.502 * * * * [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.502 * [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.502 * * [simplify]: iters left: 6 (15 enodes)
3.510 * * [simplify]: iters left: 5 (47 enodes)
3.528 * * [simplify]: iters left: 4 (100 enodes)
3.561 * * [simplify]: iters left: 3 (250 enodes)
3.721 * * [simplify]: Extracting #0: cost 1 inf + 0
3.721 * * [simplify]: Extracting #1: cost 7 inf + 0
3.722 * * [simplify]: Extracting #2: cost 38 inf + 0
3.722 * * [simplify]: Extracting #3: cost 89 inf + 404
3.724 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.730 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.743 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.752 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.761 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.770 * [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.770 * [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.770 * * * * [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.770 * [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.770 * * [simplify]: iters left: 6 (15 enodes)
3.773 * * [simplify]: iters left: 5 (47 enodes)
3.784 * * [simplify]: iters left: 4 (100 enodes)
3.807 * * [simplify]: iters left: 3 (250 enodes)
3.946 * * [simplify]: Extracting #0: cost 1 inf + 0
3.946 * * [simplify]: Extracting #1: cost 7 inf + 0
3.946 * * [simplify]: Extracting #2: cost 38 inf + 0
3.946 * * [simplify]: Extracting #3: cost 89 inf + 404
3.947 * * [simplify]: Extracting #4: cost 105 inf + 13282
3.950 * * [simplify]: Extracting #5: cost 75 inf + 74603
3.956 * * [simplify]: Extracting #6: cost 45 inf + 171652
3.964 * * [simplify]: Extracting #7: cost 3 inf + 235044
3.975 * * [simplify]: Extracting #8: cost 0 inf + 242171
3.993 * [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.993 * [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.993 * * * * [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.993 * [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.993 * * [simplify]: iters left: 6 (15 enodes)
4.000 * * [simplify]: iters left: 5 (47 enodes)
4.017 * * [simplify]: iters left: 4 (100 enodes)
4.046 * * [simplify]: iters left: 3 (250 enodes)
4.203 * * [simplify]: Extracting #0: cost 1 inf + 0
4.203 * * [simplify]: Extracting #1: cost 7 inf + 0
4.204 * * [simplify]: Extracting #2: cost 38 inf + 0
4.204 * * [simplify]: Extracting #3: cost 89 inf + 404
4.205 * * [simplify]: Extracting #4: cost 105 inf + 13282
4.208 * * [simplify]: Extracting #5: cost 75 inf + 74603
4.219 * * [simplify]: Extracting #6: cost 45 inf + 171652
4.227 * * [simplify]: Extracting #7: cost 3 inf + 235044
4.237 * * [simplify]: Extracting #8: cost 0 inf + 242171
4.251 * [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.251 * [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.251 * * * * [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)))))))>
4.252 * [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))))))
4.252 * * [simplify]: iters left: 6 (15 enodes)
4.258 * * [simplify]: iters left: 5 (47 enodes)
4.278 * * [simplify]: iters left: 4 (100 enodes)
4.317 * * [simplify]: iters left: 3 (250 enodes)
4.491 * * [simplify]: Extracting #0: cost 1 inf + 0
4.491 * * [simplify]: Extracting #1: cost 7 inf + 0
4.492 * * [simplify]: Extracting #2: cost 38 inf + 0
4.492 * * [simplify]: Extracting #3: cost 89 inf + 404
4.494 * * [simplify]: Extracting #4: cost 105 inf + 13282
4.500 * * [simplify]: Extracting #5: cost 75 inf + 74603
4.512 * * [simplify]: Extracting #6: cost 45 inf + 171652
4.528 * * [simplify]: Extracting #7: cost 3 inf + 235044
4.548 * * [simplify]: Extracting #8: cost 0 inf + 242171
4.566 * [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.566 * [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.566 * * * [progress]: adding candidates to table
4.783 * * [progress]: iteration 3 / 4
4.783 * * * [progress]: picking best candidate
4.834 * * * * [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.834 * * * [progress]: localizing error
5.178 * * * [progress]: generating rewritten candidates
5.178 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2)
5.181 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
5.183 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2)
5.183 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
5.187 * * * [progress]: generating series expansions
5.187 * * * * [progress]: [ 1 / 4 ] generating series at (2 2)
5.187 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
5.187 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2)
5.187 * * * * [progress]: [ 4 / 4 ] generating series at (2)
5.187 * * * [progress]: simplifying candidates
5.187 * * * * [progress]: [ 1 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (neg.p16 b_2))))>
5.187 * * * * [progress]: [ 2 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)))>
5.187 * [simplify]: Simplifying (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2))))
5.187 * * [simplify]: iters left: 4 (9 enodes)
5.189 * * [simplify]: iters left: 3 (24 enodes)
5.194 * * [simplify]: iters left: 2 (53 enodes)
5.205 * * [simplify]: iters left: 1 (140 enodes)
5.273 * * [simplify]: Extracting #0: cost 1 inf + 0
5.273 * * [simplify]: Extracting #1: cost 24 inf + 0
5.273 * * [simplify]: Extracting #2: cost 70 inf + 0
5.274 * * [simplify]: Extracting #3: cost 62 inf + 3454
5.275 * * [simplify]: Extracting #4: cost 19 inf + 33897
5.278 * * [simplify]: Extracting #5: cost 0 inf + 53655
5.282 * [simplify]: Simplified to (+.p16 (*.p16 c a) (real->posit16 0.0))
5.282 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)))
5.282 * * * * [progress]: [ 3 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
5.283 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.283 * * [simplify]: iters left: 4 (9 enodes)
5.285 * * [simplify]: iters left: 3 (24 enodes)
5.289 * * [simplify]: iters left: 2 (47 enodes)
5.297 * * [simplify]: iters left: 1 (110 enodes)
5.340 * * [simplify]: Extracting #0: cost 1 inf + 0
5.340 * * [simplify]: Extracting #1: cost 6 inf + 0
5.340 * * [simplify]: Extracting #2: cost 10 inf + 1
5.340 * * [simplify]: Extracting #3: cost 23 inf + 403
5.340 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.341 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.343 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.348 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.353 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.359 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.359 * [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.359 * * * * [progress]: [ 4 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
5.360 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.360 * * [simplify]: iters left: 4 (9 enodes)
5.361 * * [simplify]: iters left: 3 (24 enodes)
5.365 * * [simplify]: iters left: 2 (47 enodes)
5.374 * * [simplify]: iters left: 1 (110 enodes)
5.401 * * [simplify]: Extracting #0: cost 1 inf + 0
5.401 * * [simplify]: Extracting #1: cost 6 inf + 0
5.401 * * [simplify]: Extracting #2: cost 10 inf + 1
5.401 * * [simplify]: Extracting #3: cost 23 inf + 403
5.401 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.402 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.403 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.408 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.414 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.420 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.420 * [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.420 * * * * [progress]: [ 5 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
5.421 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.421 * * [simplify]: iters left: 4 (9 enodes)
5.422 * * [simplify]: iters left: 3 (24 enodes)
5.427 * * [simplify]: iters left: 2 (47 enodes)
5.435 * * [simplify]: iters left: 1 (110 enodes)
5.464 * * [simplify]: Extracting #0: cost 1 inf + 0
5.464 * * [simplify]: Extracting #1: cost 6 inf + 0
5.464 * * [simplify]: Extracting #2: cost 10 inf + 1
5.465 * * [simplify]: Extracting #3: cost 23 inf + 403
5.465 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.465 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.467 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.472 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.478 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.484 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.484 * [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.484 * * * * [progress]: [ 6 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
5.484 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.484 * * [simplify]: iters left: 4 (9 enodes)
5.486 * * [simplify]: iters left: 3 (24 enodes)
5.490 * * [simplify]: iters left: 2 (47 enodes)
5.498 * * [simplify]: iters left: 1 (110 enodes)
5.527 * * [simplify]: Extracting #0: cost 1 inf + 0
5.527 * * [simplify]: Extracting #1: cost 6 inf + 0
5.527 * * [simplify]: Extracting #2: cost 10 inf + 1
5.527 * * [simplify]: Extracting #3: cost 23 inf + 403
5.527 * * [simplify]: Extracting #4: cost 60 inf + 1445
5.528 * * [simplify]: Extracting #5: cost 79 inf + 13843
5.530 * * [simplify]: Extracting #6: cost 73 inf + 57826
5.535 * * [simplify]: Extracting #7: cost 3 inf + 171780
5.540 * * [simplify]: Extracting #8: cost 0 inf + 178629
5.546 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.546 * [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.546 * * * [progress]: adding candidates to table
5.719 * * [progress]: iteration 4 / 4
5.719 * * * [progress]: picking best candidate
5.752 * * * * [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.752 * * * [progress]: localizing error
6.056 * * * [progress]: generating rewritten candidates
6.056 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2 2 1)
6.064 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 2)
6.066 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
6.069 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2)
6.070 * * * [progress]: generating series expansions
6.070 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2 2 1)
6.070 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 2)
6.070 * * * * [progress]: [ 3 / 4 ] generating series at (2)
6.070 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2)
6.070 * * * [progress]: simplifying candidates
6.070 * * * * [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)))))))))>
6.070 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
6.070 * * [simplify]: iters left: 2 (6 enodes)
6.072 * * [simplify]: iters left: 1 (14 enodes)
6.073 * * [simplify]: Extracting #0: cost 1 inf + 0
6.073 * * [simplify]: Extracting #1: cost 3 inf + 0
6.073 * * [simplify]: Extracting #2: cost 6 inf + 0
6.074 * * [simplify]: Extracting #3: cost 2 inf + 325
6.074 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.074 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
6.074 * [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)))))))))
6.074 * * * * [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))))))))))>
6.074 * [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))))
6.074 * * [simplify]: iters left: 4 (10 enodes)
6.076 * * [simplify]: iters left: 3 (43 enodes)
6.090 * * [simplify]: iters left: 2 (121 enodes)
6.536 * * [simplify]: iters left: 1 (429 enodes)
6.814 * * [simplify]: Extracting #0: cost 1 inf + 0
6.814 * * [simplify]: Extracting #1: cost 46 inf + 0
6.814 * * [simplify]: Extracting #2: cost 270 inf + 0
6.817 * * [simplify]: Extracting #3: cost 354 inf + 59003
6.840 * * [simplify]: Extracting #4: cost 345 inf + 369227
6.900 * * [simplify]: Extracting #5: cost 22 inf + 1102360
6.990 * * [simplify]: Extracting #6: cost 1 inf + 1150488
7.051 * * [simplify]: Extracting #7: cost 0 inf + 1155051
7.127 * [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))))
7.128 * [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))))))))))
7.128 * * * * [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)))))>
7.128 * * * * [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)))))))>
7.128 * [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)))))
7.129 * * [simplify]: iters left: 6 (13 enodes)
7.134 * * [simplify]: iters left: 5 (39 enodes)
7.149 * * [simplify]: iters left: 4 (84 enodes)
7.185 * * [simplify]: iters left: 3 (271 enodes)
7.341 * * [simplify]: Extracting #0: cost 1 inf + 0
7.341 * * [simplify]: Extracting #1: cost 6 inf + 0
7.342 * * [simplify]: Extracting #2: cost 10 inf + 1
7.342 * * [simplify]: Extracting #3: cost 66 inf + 403
7.342 * * [simplify]: Extracting #4: cost 230 inf + 1445
7.344 * * [simplify]: Extracting #5: cost 349 inf + 32520
7.353 * * [simplify]: Extracting #6: cost 220 inf + 249925
7.405 * * [simplify]: Extracting #7: cost 28 inf + 656177
7.456 * * [simplify]: Extracting #8: cost 0 inf + 728735
7.492 * * [simplify]: Extracting #9: cost 0 inf + 726535
7.547 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
7.548 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
7.548 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
7.548 * * * * [progress]: [ 6 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
7.548 * * * * [progress]: [ 7 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
7.548 * * * * [progress]: [ 8 / 8 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))))))>
7.548 * * * [progress]: adding candidates to table
7.795 * [progress]: [Phase 3 of 3] Extracting.
7.796 * * [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 (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 (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 (*.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))))))>)
7.800 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
7.800 * * * * [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 (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 (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 (*.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))))))>)
7.950 * * * * [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 (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 (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 (*.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))))))>)
8.164 * * * * [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 (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 (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 (*.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))))))>)
8.380 * * * [regime]: Found split indices: #<option (#s(si 6 116) #s(si 3 256))>
8.382 * [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 (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 (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 (*.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))))))>)
8.382 * [regimes]: Found splitpoints: (#s(sp 6 b_2 #<cpointer:posit16>) #s(sp 3 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 (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 (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 (*.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))))))>)
8.383 * [simplify]: Simplifying (if (<=.p16 b_2 (real->posit16 -0.091796875)) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))
8.384 * * [simplify]: iters left: 6 (21 enodes)
8.386 * * [simplify]: Extracting #0: cost 1 inf + 0
8.386 * * [simplify]: Extracting #1: cost 4 inf + 0
8.387 * * [simplify]: Extracting #2: cost 10 inf + 0
8.387 * * [simplify]: Extracting #3: cost 12 inf + 2
8.387 * * [simplify]: Extracting #4: cost 13 inf + 84
8.387 * * [simplify]: Extracting #5: cost 15 inf + 152
8.387 * * [simplify]: Extracting #6: cost 11 inf + 716
8.387 * * [simplify]: Extracting #7: cost 6 inf + 3848
8.388 * * [simplify]: Extracting #8: cost 3 inf + 6937
8.388 * * [simplify]: Extracting #9: cost 0 inf + 13357
8.389 * [simplify]: Simplified to (if (<=.p16 b_2 (real->posit16 -0.091796875)) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))
8.389 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
8.452 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
8.454 * * * * [points]: Setting MPFR precision to 64
8.456 * * * * [points]: Setting MPFR precision to 320
8.457 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
8.459 * * * * [points]: Setting MPFR precision to 64
8.462 * * * * [points]: Setting MPFR precision to 320
8.466 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
8.468 * * * * [points]: Setting MPFR precision to 64
8.475 * * * * [points]: Setting MPFR precision to 320
8.482 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
8.484 * * * * [points]: Setting MPFR precision to 64
8.499 * * * * [points]: Setting MPFR precision to 320
8.513 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
8.515 * * * * [points]: Setting MPFR precision to 64
8.546 * * * * [points]: Setting MPFR precision to 320
8.564 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
8.566 * * * * [points]: Setting MPFR precision to 64
8.609 * * * * [points]: Setting MPFR precision to 320
8.661 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
8.663 * * * * [points]: Setting MPFR precision to 64
8.817 * * * * [points]: Setting MPFR precision to 320
8.933 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
8.935 * * * * [points]: Setting MPFR precision to 64
9.156 * * * * [points]: Setting MPFR precision to 320
9.439 * * * * [points]: Computing exacts for 8000 points
9.441 * * * * [points]: Setting MPFR precision to 64
10.348 * * * * [points]: Setting MPFR precision to 320
11.894 * * * * [points]: Filtering points with unrepresentable outputs
11.931 * * * * [points]: Sampled 8000 points with exact outputs
15.546 * [regime-testing]: Baseline error score: 64.0
15.553 * [regime-testing]: Oracle error score: 64.0
15.560 * [regime-testing]: End program error score: 0.4397496702028498