0.002 * [progress]: [Phase 1 of 3] Setting up.
0.003 * * * [progress]: [1/2] Preparing points
0.005 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.007 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.210 * * * * [points]: Setting MPFR precision to 64
0.216 * * * * [points]: Setting MPFR precision to 320
0.218 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.221 * * * * [points]: Setting MPFR precision to 64
0.224 * * * * [points]: Setting MPFR precision to 320
0.228 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.230 * * * * [points]: Setting MPFR precision to 64
0.238 * * * * [points]: Setting MPFR precision to 320
0.245 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.247 * * * * [points]: Setting MPFR precision to 64
0.258 * * * * [points]: Setting MPFR precision to 320
0.269 * * * * [points]: Computing exacts for 256 points
0.271 * * * * [points]: Setting MPFR precision to 64
0.290 * * * * [points]: Setting MPFR precision to 320
0.307 * * * * [points]: Filtering points with unrepresentable outputs
0.308 * * * * [points]: Sampled 256 points with exact outputs
0.309 * * * [progress]: [2/2] Setting up program.
0.321 * [progress]: [Phase 2 of 3] Improving.
0.322 * * * * [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.323 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.325 * * [simplify]: iters left: 5 (10 enodes)
0.334 * * [simplify]: iters left: 4 (25 enodes)
0.343 * * [simplify]: iters left: 3 (48 enodes)
0.361 * * [simplify]: iters left: 2 (111 enodes)
0.452 * * [simplify]: iters left: 1 (394 enodes)
0.761 * * [simplify]: Extracting #0: cost 1 inf + 0
0.762 * * [simplify]: Extracting #1: cost 10 inf + 0
0.762 * * [simplify]: Extracting #2: cost 35 inf + 1
0.762 * * [simplify]: Extracting #3: cost 92 inf + 83
0.763 * * [simplify]: Extracting #4: cost 333 inf + 1810
0.765 * * [simplify]: Extracting #5: cost 518 inf + 5618
0.773 * * [simplify]: Extracting #6: cost 470 inf + 184191
0.829 * * [simplify]: Extracting #7: cost 61 inf + 918877
0.896 * * [simplify]: Extracting #8: cost 0 inf + 1055660
0.978 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
0.978 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
0.992 * * [progress]: iteration 1 / 4
0.992 * * * [progress]: picking best candidate
0.996 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
0.997 * * * [progress]: localizing error
1.124 * * * [progress]: generating rewritten candidates
1.125 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.129 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
1.131 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
1.132 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1.139 * * * [progress]: generating series expansions
1.139 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.139 * * * * [progress]: [ 2 / 4 ] generating series at (2)
1.139 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
1.140 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1.140 * * * [progress]: simplifying candidates
1.140 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2)) a))>
1.140 * [simplify]: Simplifying (neg.p16 b_2)
1.140 * * [simplify]: iters left: 1 (2 enodes)
1.141 * * [simplify]: Extracting #0: cost 1 inf + 0
1.141 * * [simplify]: Extracting #1: cost 2 inf + 0
1.141 * * [simplify]: Extracting #2: cost 1 inf + 1
1.141 * * [simplify]: Extracting #3: cost 0 inf + 82
1.141 * [simplify]: Simplified to (neg.p16 b_2)
1.141 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2)) a))
1.141 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1.141 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
1.142 * * [simplify]: iters left: 5 (9 enodes)
1.145 * * [simplify]: iters left: 4 (32 enodes)
1.157 * * [simplify]: iters left: 3 (94 enodes)
1.199 * * [simplify]: iters left: 2 (340 enodes)
1.442 * * [simplify]: Extracting #0: cost 1 inf + 0
1.442 * * [simplify]: Extracting #1: cost 50 inf + 0
1.442 * * [simplify]: Extracting #2: cost 240 inf + 0
1.445 * * [simplify]: Extracting #3: cost 363 inf + 51025
1.466 * * [simplify]: Extracting #4: cost 279 inf + 363866
1.527 * * [simplify]: Extracting #5: cost 63 inf + 808744
1.597 * * [simplify]: Extracting #6: cost 1 inf + 916546
1.654 * * [simplify]: Extracting #7: cost 0 inf + 919829
1.710 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1.710 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1.710 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1.710 * * [simplify]: iters left: 4 (8 enodes)
1.712 * * [simplify]: iters left: 3 (23 enodes)
1.716 * * [simplify]: iters left: 2 (45 enodes)
1.725 * * [simplify]: iters left: 1 (108 enodes)
1.764 * * [simplify]: Extracting #0: cost 1 inf + 0
1.764 * * [simplify]: Extracting #1: cost 3 inf + 0
1.764 * * [simplify]: Extracting #2: cost 3 inf + 1
1.764 * * [simplify]: Extracting #3: cost 17 inf + 1
1.764 * * [simplify]: Extracting #4: cost 55 inf + 322
1.766 * * [simplify]: Extracting #5: cost 80 inf + 11197
1.769 * * [simplify]: Extracting #6: cost 84 inf + 56173
1.779 * * [simplify]: Extracting #7: cost 7 inf + 177856
1.793 * * [simplify]: Extracting #8: cost 0 inf + 193436
1.806 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1.806 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
1.807 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
1.807 * [simplify]: Simplifying (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
1.807 * * [simplify]: iters left: 5 (9 enodes)
1.811 * * [simplify]: iters left: 4 (31 enodes)
1.822 * * [simplify]: iters left: 3 (55 enodes)
1.839 * * [simplify]: iters left: 2 (114 enodes)
1.866 * * [simplify]: iters left: 1 (406 enodes)
2.198 * * [simplify]: Extracting #0: cost 1 inf + 0
2.198 * * [simplify]: Extracting #1: cost 5 inf + 0
2.198 * * [simplify]: Extracting #2: cost 6 inf + 1
2.198 * * [simplify]: Extracting #3: cost 5 inf + 324
2.199 * * [simplify]: Extracting #4: cost 51 inf + 324
2.199 * * [simplify]: Extracting #5: cost 257 inf + 645
2.201 * * [simplify]: Extracting #6: cost 464 inf + 11760
2.219 * * [simplify]: Extracting #7: cost 370 inf + 309548
2.292 * * [simplify]: Extracting #8: cost 43 inf + 972742
2.337 * * [simplify]: Extracting #9: cost 0 inf + 1034433
2.406 * * [simplify]: Extracting #10: cost 0 inf + 1033793
2.489 * [simplify]: Simplified to (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.489 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)))
2.489 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))) b_2) a))>
2.490 * [simplify]: Simplifying (neg.p16 (*.p16 c a))
2.490 * * [simplify]: iters left: 2 (4 enodes)
2.491 * * [simplify]: iters left: 1 (9 enodes)
2.494 * * [simplify]: Extracting #0: cost 1 inf + 0
2.494 * * [simplify]: Extracting #1: cost 2 inf + 0
2.494 * * [simplify]: Extracting #2: cost 4 inf + 0
2.494 * * [simplify]: Extracting #3: cost 2 inf + 2
2.494 * * [simplify]: Extracting #4: cost 0 inf + 726
2.494 * [simplify]: Simplified to (neg.p16 (*.p16 a c))
2.494 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c)))) b_2) a))
2.494 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
2.494 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
2.494 * * [simplify]: iters left: 3 (8 enodes)
2.498 * * [simplify]: iters left: 2 (33 enodes)
2.509 * * [simplify]: iters left: 1 (79 enodes)
2.525 * * [simplify]: Extracting #0: cost 1 inf + 0
2.525 * * [simplify]: Extracting #1: cost 21 inf + 0
2.526 * * [simplify]: Extracting #2: cost 51 inf + 0
2.526 * * [simplify]: Extracting #3: cost 77 inf + 5301
2.528 * * [simplify]: Extracting #4: cost 37 inf + 63309
2.531 * * [simplify]: Extracting #5: cost 2 inf + 116709
2.535 * * [simplify]: Extracting #6: cost 0 inf + 120953
2.539 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
2.539 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
2.539 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
2.539 * * [simplify]: iters left: 2 (6 enodes)
2.541 * * [simplify]: iters left: 1 (14 enodes)
2.543 * * [simplify]: Extracting #0: cost 1 inf + 0
2.543 * * [simplify]: Extracting #1: cost 3 inf + 0
2.543 * * [simplify]: Extracting #2: cost 6 inf + 0
2.543 * * [simplify]: Extracting #3: cost 2 inf + 325
2.543 * * [simplify]: Extracting #4: cost 0 inf + 1329
2.543 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
2.543 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))) b_2) a))
2.543 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
2.544 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.544 * * [simplify]: iters left: 5 (9 enodes)
2.547 * * [simplify]: iters left: 4 (29 enodes)
2.557 * * [simplify]: iters left: 3 (62 enodes)
2.569 * * [simplify]: iters left: 2 (199 enodes)
2.631 * * [simplify]: Extracting #0: cost 1 inf + 0
2.631 * * [simplify]: Extracting #1: cost 20 inf + 0
2.631 * * [simplify]: Extracting #2: cost 94 inf + 1
2.632 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.633 * * [simplify]: Extracting #4: cost 205 inf + 21625
2.636 * * [simplify]: Extracting #5: cost 170 inf + 98466
2.648 * * [simplify]: Extracting #6: cost 65 inf + 303687
2.664 * * [simplify]: Extracting #7: cost 1 inf + 408042
2.692 * * [simplify]: Extracting #8: cost 0 inf + 411325
2.723 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.723 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
2.724 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
2.724 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.724 * * [simplify]: iters left: 5 (9 enodes)
3.018 * * [simplify]: iters left: 4 (29 enodes)
3.029 * * [simplify]: iters left: 3 (62 enodes)
3.052 * * [simplify]: iters left: 2 (199 enodes)
3.172 * * [simplify]: Extracting #0: cost 1 inf + 0
3.172 * * [simplify]: Extracting #1: cost 20 inf + 0
3.173 * * [simplify]: Extracting #2: cost 94 inf + 1
3.173 * * [simplify]: Extracting #3: cost 162 inf + 1046
3.176 * * [simplify]: Extracting #4: cost 205 inf + 21625
3.182 * * [simplify]: Extracting #5: cost 170 inf + 98466
3.203 * * [simplify]: Extracting #6: cost 65 inf + 303687
3.233 * * [simplify]: Extracting #7: cost 1 inf + 408042
3.258 * * [simplify]: Extracting #8: cost 0 inf + 411325
3.274 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
3.274 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
3.274 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
3.275 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
3.275 * * [simplify]: iters left: 5 (9 enodes)
3.277 * * [simplify]: iters left: 4 (29 enodes)
3.283 * * [simplify]: iters left: 3 (62 enodes)
3.295 * * [simplify]: iters left: 2 (199 enodes)
3.365 * * [simplify]: Extracting #0: cost 1 inf + 0
3.365 * * [simplify]: Extracting #1: cost 20 inf + 0
3.366 * * [simplify]: Extracting #2: cost 94 inf + 1
3.367 * * [simplify]: Extracting #3: cost 162 inf + 1046
3.369 * * [simplify]: Extracting #4: cost 205 inf + 21625
3.376 * * [simplify]: Extracting #5: cost 170 inf + 98466
3.396 * * [simplify]: Extracting #6: cost 65 inf + 303687
3.426 * * [simplify]: Extracting #7: cost 1 inf + 408042
3.454 * * [simplify]: Extracting #8: cost 0 inf + 411325
3.482 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
3.482 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
3.482 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
3.482 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
3.482 * * [simplify]: iters left: 5 (9 enodes)
3.485 * * [simplify]: iters left: 4 (29 enodes)
3.494 * * [simplify]: iters left: 3 (62 enodes)
3.517 * * [simplify]: iters left: 2 (199 enodes)
3.593 * * [simplify]: Extracting #0: cost 1 inf + 0
3.593 * * [simplify]: Extracting #1: cost 20 inf + 0
3.593 * * [simplify]: Extracting #2: cost 94 inf + 1
3.593 * * [simplify]: Extracting #3: cost 162 inf + 1046
3.595 * * [simplify]: Extracting #4: cost 205 inf + 21625
3.598 * * [simplify]: Extracting #5: cost 170 inf + 98466
3.612 * * [simplify]: Extracting #6: cost 65 inf + 303687
3.633 * * [simplify]: Extracting #7: cost 1 inf + 408042
3.649 * * [simplify]: Extracting #8: cost 0 inf + 411325
3.666 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
3.666 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
3.666 * * * [progress]: adding candidates to table
3.764 * * [progress]: iteration 2 / 4
3.765 * * * [progress]: picking best candidate
3.800 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
3.800 * * * [progress]: localizing error
4.054 * * * [progress]: generating rewritten candidates
4.054 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
4.066 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
4.068 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
4.070 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
4.071 * * * [progress]: generating series expansions
4.071 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
4.071 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
4.071 * * * * [progress]: [ 3 / 4 ] generating series at (2)
4.071 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
4.071 * * * [progress]: simplifying candidates
4.071 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
4.071 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
4.071 * * [simplify]: iters left: 3 (8 enodes)
4.073 * * [simplify]: iters left: 2 (22 enodes)
4.077 * * [simplify]: iters left: 1 (45 enodes)
4.085 * * [simplify]: Extracting #0: cost 1 inf + 0
4.085 * * [simplify]: Extracting #1: cost 10 inf + 0
4.085 * * [simplify]: Extracting #2: cost 26 inf + 0
4.085 * * [simplify]: Extracting #3: cost 37 inf + 0
4.085 * * [simplify]: Extracting #4: cost 47 inf + 2734
4.086 * * [simplify]: Extracting #5: cost 18 inf + 30834
4.094 * * [simplify]: Extracting #6: cost 0 inf + 59476
4.097 * * [simplify]: Extracting #7: cost 0 inf + 58996
4.100 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
4.100 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (/.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) b_2) a))
4.101 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (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 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>
4.101 * [simplify]: Simplifying (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))))
4.101 * * [simplify]: iters left: 4 (10 enodes)
4.104 * * [simplify]: iters left: 3 (34 enodes)
4.111 * * [simplify]: iters left: 2 (91 enodes)
4.132 * * [simplify]: iters left: 1 (280 enodes)
4.315 * * [simplify]: Extracting #0: cost 1 inf + 0
4.315 * * [simplify]: Extracting #1: cost 20 inf + 0
4.315 * * [simplify]: Extracting #2: cost 96 inf + 0
4.316 * * [simplify]: Extracting #3: cost 106 inf + 12956
4.321 * * [simplify]: Extracting #4: cost 19 inf + 129586
4.328 * * [simplify]: Extracting #5: cost 0 inf + 160920
4.338 * * [simplify]: Extracting #6: cost 0 inf + 159960
4.352 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))
4.352 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (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 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c)))))) b_2) a))
4.353 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 b_2)) a))>
4.353 * [simplify]: Simplifying (neg.p16 b_2)
4.353 * * [simplify]: iters left: 1 (2 enodes)
4.354 * * [simplify]: Extracting #0: cost 1 inf + 0
4.354 * * [simplify]: Extracting #1: cost 2 inf + 0
4.354 * * [simplify]: Extracting #2: cost 1 inf + 1
4.354 * * [simplify]: Extracting #3: cost 0 inf + 82
4.354 * [simplify]: Simplified to (neg.p16 b_2)
4.354 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 b_2)) a))
4.354 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
4.355 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2))
4.355 * * [simplify]: iters left: 6 (13 enodes)
4.361 * * [simplify]: iters left: 5 (47 enodes)
4.380 * * [simplify]: iters left: 4 (118 enodes)
4.439 * * [simplify]: iters left: 3 (482 enodes)
4.922 * * [simplify]: Extracting #0: cost 1 inf + 0
4.922 * * [simplify]: Extracting #1: cost 47 inf + 0
4.923 * * [simplify]: Extracting #2: cost 266 inf + 0
4.925 * * [simplify]: Extracting #3: cost 536 inf + 28392
4.946 * * [simplify]: Extracting #4: cost 646 inf + 405570
5.009 * * [simplify]: Extracting #5: cost 179 inf + 1412113
5.140 * * [simplify]: Extracting #6: cost 2 inf + 1774901
5.251 * * [simplify]: Extracting #7: cost 0 inf + 1777784
5.342 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
5.342 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))
5.343 * [simplify]: Simplifying (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)
5.343 * * [simplify]: iters left: 6 (12 enodes)
5.346 * * [simplify]: iters left: 5 (38 enodes)
5.353 * * [simplify]: iters left: 4 (86 enodes)
5.373 * * [simplify]: iters left: 3 (285 enodes)
5.539 * * [simplify]: Extracting #0: cost 1 inf + 0
5.539 * * [simplify]: Extracting #1: cost 3 inf + 0
5.539 * * [simplify]: Extracting #2: cost 3 inf + 1
5.539 * * [simplify]: Extracting #3: cost 60 inf + 1
5.540 * * [simplify]: Extracting #4: cost 225 inf + 322
5.543 * * [simplify]: Extracting #5: cost 353 inf + 24300
5.554 * * [simplify]: Extracting #6: cost 198 inf + 338281
5.584 * * [simplify]: Extracting #7: cost 14 inf + 719955
5.653 * * [simplify]: Extracting #8: cost 0 inf + 754556
5.709 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.709 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
5.709 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
5.710 * [simplify]: Simplifying (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))
5.710 * * [simplify]: iters left: 6 (13 enodes)
5.713 * * [simplify]: iters left: 5 (46 enodes)
5.721 * * [simplify]: iters left: 4 (94 enodes)
5.741 * * [simplify]: iters left: 3 (279 enodes)
5.907 * * [simplify]: Extracting #0: cost 1 inf + 0
5.907 * * [simplify]: Extracting #1: cost 5 inf + 0
5.907 * * [simplify]: Extracting #2: cost 6 inf + 1
5.908 * * [simplify]: Extracting #3: cost 5 inf + 324
5.908 * * [simplify]: Extracting #4: cost 62 inf + 324
5.908 * * [simplify]: Extracting #5: cost 227 inf + 645
5.910 * * [simplify]: Extracting #6: cost 373 inf + 17528
5.921 * * [simplify]: Extracting #7: cost 255 inf + 233381
5.947 * * [simplify]: Extracting #8: cost 42 inf + 659523
5.991 * * [simplify]: Extracting #9: cost 1 inf + 762007
6.058 * * [simplify]: Extracting #10: cost 0 inf + 765050
6.125 * [simplify]: Simplified to (*.p16 a (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
6.125 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))
6.125 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
6.125 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
6.126 * * [simplify]: iters left: 3 (8 enodes)
6.129 * * [simplify]: iters left: 2 (33 enodes)
6.140 * * [simplify]: iters left: 1 (79 enodes)
6.158 * * [simplify]: Extracting #0: cost 1 inf + 0
6.158 * * [simplify]: Extracting #1: cost 21 inf + 0
6.159 * * [simplify]: Extracting #2: cost 51 inf + 0
6.159 * * [simplify]: Extracting #3: cost 77 inf + 5301
6.163 * * [simplify]: Extracting #4: cost 37 inf + 63309
6.170 * * [simplify]: Extracting #5: cost 2 inf + 116709
6.177 * * [simplify]: Extracting #6: cost 0 inf + 120953
6.185 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
6.185 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
6.185 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
6.185 * * [simplify]: iters left: 2 (6 enodes)
6.187 * * [simplify]: iters left: 1 (14 enodes)
6.192 * * [simplify]: Extracting #0: cost 1 inf + 0
6.192 * * [simplify]: Extracting #1: cost 3 inf + 0
6.192 * * [simplify]: Extracting #2: cost 6 inf + 0
6.193 * * [simplify]: Extracting #3: cost 2 inf + 325
6.193 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.193 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
6.193 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))) b_2) a))
6.193 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
6.193 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
6.193 * * [simplify]: iters left: 3 (8 enodes)
6.197 * * [simplify]: iters left: 2 (33 enodes)
6.209 * * [simplify]: iters left: 1 (79 enodes)
6.229 * * [simplify]: Extracting #0: cost 1 inf + 0
6.230 * * [simplify]: Extracting #1: cost 21 inf + 0
6.230 * * [simplify]: Extracting #2: cost 51 inf + 0
6.230 * * [simplify]: Extracting #3: cost 77 inf + 5301
6.232 * * [simplify]: Extracting #4: cost 37 inf + 63309
6.235 * * [simplify]: Extracting #5: cost 2 inf + 116709
6.239 * * [simplify]: Extracting #6: cost 0 inf + 120953
6.243 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
6.243 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
6.243 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
6.243 * * [simplify]: iters left: 2 (6 enodes)
6.246 * * [simplify]: iters left: 1 (14 enodes)
6.249 * * [simplify]: Extracting #0: cost 1 inf + 0
6.250 * * [simplify]: Extracting #1: cost 3 inf + 0
6.250 * * [simplify]: Extracting #2: cost 6 inf + 0
6.250 * * [simplify]: Extracting #3: cost 2 inf + 325
6.250 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.250 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
6.250 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))) b_2) a))
6.250 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
6.250 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
6.251 * * [simplify]: iters left: 3 (8 enodes)
6.254 * * [simplify]: iters left: 2 (33 enodes)
6.266 * * [simplify]: iters left: 1 (79 enodes)
6.300 * * [simplify]: Extracting #0: cost 1 inf + 0
6.300 * * [simplify]: Extracting #1: cost 21 inf + 0
6.300 * * [simplify]: Extracting #2: cost 51 inf + 0
6.301 * * [simplify]: Extracting #3: cost 77 inf + 5301
6.302 * * [simplify]: Extracting #4: cost 37 inf + 63309
6.307 * * [simplify]: Extracting #5: cost 2 inf + 116709
6.311 * * [simplify]: Extracting #6: cost 0 inf + 120953
6.315 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
6.315 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
6.315 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
6.315 * * [simplify]: iters left: 2 (6 enodes)
6.316 * * [simplify]: iters left: 1 (14 enodes)
6.319 * * [simplify]: Extracting #0: cost 1 inf + 0
6.319 * * [simplify]: Extracting #1: cost 3 inf + 0
6.319 * * [simplify]: Extracting #2: cost 6 inf + 0
6.319 * * [simplify]: Extracting #3: cost 2 inf + 325
6.319 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.319 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
6.319 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))) b_2) a))
6.319 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
6.319 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
6.319 * * [simplify]: iters left: 3 (8 enodes)
6.321 * * [simplify]: iters left: 2 (33 enodes)
6.327 * * [simplify]: iters left: 1 (79 enodes)
6.348 * * [simplify]: Extracting #0: cost 1 inf + 0
6.348 * * [simplify]: Extracting #1: cost 21 inf + 0
6.348 * * [simplify]: Extracting #2: cost 51 inf + 0
6.349 * * [simplify]: Extracting #3: cost 77 inf + 5301
6.352 * * [simplify]: Extracting #4: cost 37 inf + 63309
6.359 * * [simplify]: Extracting #5: cost 2 inf + 116709
6.367 * * [simplify]: Extracting #6: cost 0 inf + 120953
6.371 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
6.371 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
6.371 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
6.371 * * [simplify]: iters left: 2 (6 enodes)
6.373 * * [simplify]: iters left: 1 (14 enodes)
6.375 * * [simplify]: Extracting #0: cost 1 inf + 0
6.375 * * [simplify]: Extracting #1: cost 3 inf + 0
6.375 * * [simplify]: Extracting #2: cost 6 inf + 0
6.375 * * [simplify]: Extracting #3: cost 2 inf + 325
6.375 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.375 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
6.375 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))) b_2) a))
6.375 * * * [progress]: adding candidates to table
6.533 * * [progress]: iteration 3 / 4
6.533 * * * [progress]: picking best candidate
6.556 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.556 * * * [progress]: localizing error
6.756 * * * [progress]: generating rewritten candidates
6.756 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
6.759 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
6.762 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
6.767 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
6.773 * * * [progress]: generating series expansions
6.773 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
6.773 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
6.773 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
6.773 * * * * [progress]: [ 4 / 4 ] generating series at (2)
6.773 * * * [progress]: simplifying candidates
6.773 * * * * [progress]: [ 1 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.774 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.774 * * [simplify]: iters left: 4 (8 enodes)
6.775 * * [simplify]: iters left: 3 (23 enodes)
6.780 * * [simplify]: iters left: 2 (45 enodes)
6.788 * * [simplify]: iters left: 1 (108 enodes)
6.825 * * [simplify]: Extracting #0: cost 1 inf + 0
6.826 * * [simplify]: Extracting #1: cost 3 inf + 0
6.826 * * [simplify]: Extracting #2: cost 3 inf + 1
6.826 * * [simplify]: Extracting #3: cost 17 inf + 1
6.826 * * [simplify]: Extracting #4: cost 55 inf + 322
6.827 * * [simplify]: Extracting #5: cost 80 inf + 11197
6.831 * * [simplify]: Extracting #6: cost 84 inf + 56173
6.841 * * [simplify]: Extracting #7: cost 7 inf + 177856
6.854 * * [simplify]: Extracting #8: cost 0 inf + 193436
6.861 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
6.862 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
6.862 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.862 * * [simplify]: iters left: 4 (8 enodes)
6.864 * * [simplify]: iters left: 3 (28 enodes)
6.869 * * [simplify]: iters left: 2 (59 enodes)
6.880 * * [simplify]: iters left: 1 (178 enodes)
6.948 * * [simplify]: Extracting #0: cost 1 inf + 0
6.948 * * [simplify]: Extracting #1: cost 12 inf + 0
6.948 * * [simplify]: Extracting #2: cost 64 inf + 1
6.949 * * [simplify]: Extracting #3: cost 140 inf + 403
6.950 * * [simplify]: Extracting #4: cost 187 inf + 15607
6.954 * * [simplify]: Extracting #5: cost 136 inf + 133387
6.966 * * [simplify]: Extracting #6: cost 33 inf + 315910
6.982 * * [simplify]: Extracting #7: cost 1 inf + 363183
7.010 * * [simplify]: Extracting #8: cost 0 inf + 364746
7.027 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
7.027 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
7.028 * * * * [progress]: [ 2 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
7.028 * [simplify]: Simplifying (neg.p16 (*.p16 b_2 b_2))
7.028 * * [simplify]: iters left: 2 (3 enodes)
7.028 * * [simplify]: iters left: 1 (5 enodes)
7.029 * * [simplify]: Extracting #0: cost 1 inf + 0
7.029 * * [simplify]: Extracting #1: cost 2 inf + 0
7.029 * * [simplify]: Extracting #2: cost 3 inf + 0
7.029 * * [simplify]: Extracting #3: cost 2 inf + 1
7.029 * * [simplify]: Extracting #4: cost 0 inf + 723
7.029 * [simplify]: Simplified to (neg.p16 (*.p16 b_2 b_2))
7.029 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
7.029 * * * * [progress]: [ 3 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
7.030 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))
7.030 * * [simplify]: iters left: 6 (11 enodes)
7.032 * * [simplify]: iters left: 5 (43 enodes)
7.041 * * [simplify]: iters left: 4 (139 enodes)
7.117 * * [simplify]: Extracting #0: cost 1 inf + 0
7.117 * * [simplify]: Extracting #1: cost 32 inf + 0
7.117 * * [simplify]: Extracting #2: cost 85 inf + 0
7.118 * * [simplify]: Extracting #3: cost 152 inf + 1364
7.120 * * [simplify]: Extracting #4: cost 166 inf + 20000
7.129 * * [simplify]: Extracting #5: cost 75 inf + 165167
7.148 * * [simplify]: Extracting #6: cost 1 inf + 282810
7.166 * * [simplify]: Extracting #7: cost 0 inf + 285213
7.178 * [simplify]: Simplified to (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2))))
7.178 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
7.178 * [simplify]: Simplifying (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
7.178 * * [simplify]: iters left: 5 (9 enodes)
7.180 * * [simplify]: iters left: 4 (24 enodes)
7.184 * * [simplify]: iters left: 3 (52 enodes)
7.196 * * [simplify]: iters left: 2 (126 enodes)
7.253 * * [simplify]: iters left: 1 (448 enodes)
7.519 * * [simplify]: Extracting #0: cost 1 inf + 0
7.520 * * [simplify]: Extracting #1: cost 21 inf + 0
7.523 * * [simplify]: Extracting #2: cost 138 inf + 0
7.525 * * [simplify]: Extracting #3: cost 398 inf + 4059
7.529 * * [simplify]: Extracting #4: cost 479 inf + 121592
7.567 * * [simplify]: Extracting #5: cost 171 inf + 722802
7.659 * * [simplify]: Extracting #6: cost 1 inf + 1087820
7.755 * * [simplify]: Extracting #7: cost 0 inf + 1091423
7.852 * [simplify]: Simplified to (+.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (*.p16 b_2 b_2))
7.852 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
7.853 * * * * [progress]: [ 4 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
7.853 * * * * [progress]: [ 5 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
7.853 * [simplify]: Simplifying (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
7.853 * * [simplify]: iters left: 5 (10 enodes)
7.857 * * [simplify]: iters left: 4 (30 enodes)
7.867 * * [simplify]: iters left: 3 (62 enodes)
7.893 * * [simplify]: iters left: 2 (195 enodes)
8.000 * * [simplify]: Extracting #0: cost 1 inf + 0
8.001 * * [simplify]: Extracting #1: cost 19 inf + 0
8.001 * * [simplify]: Extracting #2: cost 92 inf + 0
8.002 * * [simplify]: Extracting #3: cost 147 inf + 685
8.004 * * [simplify]: Extracting #4: cost 197 inf + 18145
8.015 * * [simplify]: Extracting #5: cost 136 inf + 180081
8.039 * * [simplify]: Extracting #6: cost 44 inf + 357497
8.068 * * [simplify]: Extracting #7: cost 1 inf + 421516
8.097 * * [simplify]: Extracting #8: cost 0 inf + 424799
8.126 * [simplify]: Simplified to (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
8.126 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))) a))
8.126 * * * * [progress]: [ 6 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))>
8.126 * [simplify]: Simplifying (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))
8.126 * * [simplify]: iters left: 6 (11 enodes)
8.130 * * [simplify]: iters left: 5 (34 enodes)
8.146 * * [simplify]: iters left: 4 (120 enodes)
8.201 * * [simplify]: iters left: 3 (324 enodes)
8.358 * * [simplify]: Extracting #0: cost 1 inf + 0
8.358 * * [simplify]: Extracting #1: cost 56 inf + 0
8.359 * * [simplify]: Extracting #2: cost 156 inf + 0
8.361 * * [simplify]: Extracting #3: cost 277 inf + 3087
8.365 * * [simplify]: Extracting #4: cost 283 inf + 34132
8.388 * * [simplify]: Extracting #5: cost 117 inf + 305537
8.433 * * [simplify]: Extracting #6: cost 0 inf + 511038
8.481 * * [simplify]: Extracting #7: cost 0 inf + 508518
8.526 * [simplify]: Simplified to (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
8.526 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) a))
8.526 * * * * [progress]: [ 7 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
8.527 * [simplify]: Simplifying (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
8.527 * * [simplify]: iters left: 5 (9 enodes)
8.530 * * [simplify]: iters left: 4 (31 enodes)
8.540 * * [simplify]: iters left: 3 (55 enodes)
8.558 * * [simplify]: iters left: 2 (114 enodes)
8.587 * * [simplify]: iters left: 1 (406 enodes)
8.935 * * [simplify]: Extracting #0: cost 1 inf + 0
8.935 * * [simplify]: Extracting #1: cost 5 inf + 0
8.935 * * [simplify]: Extracting #2: cost 6 inf + 1
8.935 * * [simplify]: Extracting #3: cost 5 inf + 324
8.936 * * [simplify]: Extracting #4: cost 51 inf + 324
8.937 * * [simplify]: Extracting #5: cost 257 inf + 645
8.941 * * [simplify]: Extracting #6: cost 464 inf + 11760
8.966 * * [simplify]: Extracting #7: cost 370 inf + 309548
9.034 * * [simplify]: Extracting #8: cost 43 inf + 972742
9.117 * * [simplify]: Extracting #9: cost 0 inf + 1034433
9.179 * * [simplify]: Extracting #10: cost 0 inf + 1033793
9.223 * [simplify]: Simplified to (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
9.223 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)))
9.224 * * * * [progress]: [ 8 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
9.224 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
9.224 * * [simplify]: iters left: 5 (9 enodes)
9.226 * * [simplify]: iters left: 4 (32 enodes)
9.232 * * [simplify]: iters left: 3 (94 enodes)
9.255 * * [simplify]: iters left: 2 (340 enodes)
9.534 * * [simplify]: Extracting #0: cost 1 inf + 0
9.534 * * [simplify]: Extracting #1: cost 50 inf + 0
9.535 * * [simplify]: Extracting #2: cost 240 inf + 0
9.540 * * [simplify]: Extracting #3: cost 363 inf + 51025
9.567 * * [simplify]: Extracting #4: cost 279 inf + 363866
9.620 * * [simplify]: Extracting #5: cost 63 inf + 808744
9.696 * * [simplify]: Extracting #6: cost 1 inf + 916546
9.757 * * [simplify]: Extracting #7: cost 0 inf + 919829
9.836 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
9.836 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
9.836 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
9.836 * * [simplify]: iters left: 4 (8 enodes)
9.839 * * [simplify]: iters left: 3 (23 enodes)
9.847 * * [simplify]: iters left: 2 (45 enodes)
9.863 * * [simplify]: iters left: 1 (108 enodes)
9.902 * * [simplify]: Extracting #0: cost 1 inf + 0
9.903 * * [simplify]: Extracting #1: cost 3 inf + 0
9.903 * * [simplify]: Extracting #2: cost 3 inf + 1
9.903 * * [simplify]: Extracting #3: cost 17 inf + 1
9.903 * * [simplify]: Extracting #4: cost 55 inf + 322
9.903 * * [simplify]: Extracting #5: cost 80 inf + 11197
9.906 * * [simplify]: Extracting #6: cost 84 inf + 56173
9.911 * * [simplify]: Extracting #7: cost 7 inf + 177856
9.918 * * [simplify]: Extracting #8: cost 0 inf + 193436
9.929 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
9.929 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
9.929 * * * * [progress]: [ 9 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
9.930 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
9.930 * * [simplify]: iters left: 5 (9 enodes)
9.934 * * [simplify]: iters left: 4 (32 enodes)
9.945 * * [simplify]: iters left: 3 (94 enodes)
9.968 * * [simplify]: iters left: 2 (340 enodes)
10.210 * * [simplify]: Extracting #0: cost 1 inf + 0
10.210 * * [simplify]: Extracting #1: cost 50 inf + 0
10.211 * * [simplify]: Extracting #2: cost 240 inf + 0
10.217 * * [simplify]: Extracting #3: cost 363 inf + 51025
10.244 * * [simplify]: Extracting #4: cost 279 inf + 363866
10.301 * * [simplify]: Extracting #5: cost 63 inf + 808744
10.351 * * [simplify]: Extracting #6: cost 1 inf + 916546
10.430 * * [simplify]: Extracting #7: cost 0 inf + 919829
10.487 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
10.487 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
10.487 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
10.488 * * [simplify]: iters left: 4 (8 enodes)
10.489 * * [simplify]: iters left: 3 (23 enodes)
10.493 * * [simplify]: iters left: 2 (45 enodes)
10.502 * * [simplify]: iters left: 1 (108 enodes)
10.559 * * [simplify]: Extracting #0: cost 1 inf + 0
10.559 * * [simplify]: Extracting #1: cost 3 inf + 0
10.559 * * [simplify]: Extracting #2: cost 3 inf + 1
10.559 * * [simplify]: Extracting #3: cost 17 inf + 1
10.559 * * [simplify]: Extracting #4: cost 55 inf + 322
10.560 * * [simplify]: Extracting #5: cost 80 inf + 11197
10.564 * * [simplify]: Extracting #6: cost 84 inf + 56173
10.574 * * [simplify]: Extracting #7: cost 7 inf + 177856
10.583 * * [simplify]: Extracting #8: cost 0 inf + 193436
10.590 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
10.590 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
10.590 * * * * [progress]: [ 10 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
10.590 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
10.590 * * [simplify]: iters left: 5 (9 enodes)
10.592 * * [simplify]: iters left: 4 (32 enodes)
10.598 * * [simplify]: iters left: 3 (94 enodes)
10.619 * * [simplify]: iters left: 2 (340 enodes)
10.850 * * [simplify]: Extracting #0: cost 1 inf + 0
10.850 * * [simplify]: Extracting #1: cost 50 inf + 0
10.850 * * [simplify]: Extracting #2: cost 240 inf + 0
10.853 * * [simplify]: Extracting #3: cost 363 inf + 51025
10.866 * * [simplify]: Extracting #4: cost 279 inf + 363866
10.904 * * [simplify]: Extracting #5: cost 63 inf + 808744
10.961 * * [simplify]: Extracting #6: cost 1 inf + 916546
11.042 * * [simplify]: Extracting #7: cost 0 inf + 919829
11.124 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
11.125 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
11.125 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
11.125 * * [simplify]: iters left: 4 (8 enodes)
11.128 * * [simplify]: iters left: 3 (23 enodes)
11.136 * * [simplify]: iters left: 2 (45 enodes)
11.152 * * [simplify]: iters left: 1 (108 enodes)
11.209 * * [simplify]: Extracting #0: cost 1 inf + 0
11.209 * * [simplify]: Extracting #1: cost 3 inf + 0
11.209 * * [simplify]: Extracting #2: cost 3 inf + 1
11.209 * * [simplify]: Extracting #3: cost 17 inf + 1
11.209 * * [simplify]: Extracting #4: cost 55 inf + 322
11.210 * * [simplify]: Extracting #5: cost 80 inf + 11197
11.214 * * [simplify]: Extracting #6: cost 84 inf + 56173
11.225 * * [simplify]: Extracting #7: cost 7 inf + 177856
11.239 * * [simplify]: Extracting #8: cost 0 inf + 193436
11.252 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
11.252 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
11.252 * * * * [progress]: [ 11 / 11 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
11.253 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
11.253 * * [simplify]: iters left: 5 (9 enodes)
11.257 * * [simplify]: iters left: 4 (32 enodes)
11.270 * * [simplify]: iters left: 3 (94 enodes)
11.313 * * [simplify]: iters left: 2 (340 enodes)
11.570 * * [simplify]: Extracting #0: cost 1 inf + 0
11.571 * * [simplify]: Extracting #1: cost 50 inf + 0
11.571 * * [simplify]: Extracting #2: cost 240 inf + 0
11.574 * * [simplify]: Extracting #3: cost 363 inf + 51025
11.587 * * [simplify]: Extracting #4: cost 279 inf + 363866
11.620 * * [simplify]: Extracting #5: cost 63 inf + 808744
11.703 * * [simplify]: Extracting #6: cost 1 inf + 916546
11.781 * * [simplify]: Extracting #7: cost 0 inf + 919829
11.861 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
11.862 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
11.862 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
11.862 * * [simplify]: iters left: 4 (8 enodes)
11.866 * * [simplify]: iters left: 3 (23 enodes)
11.873 * * [simplify]: iters left: 2 (45 enodes)
11.889 * * [simplify]: iters left: 1 (108 enodes)
11.945 * * [simplify]: Extracting #0: cost 1 inf + 0
11.945 * * [simplify]: Extracting #1: cost 3 inf + 0
11.945 * * [simplify]: Extracting #2: cost 3 inf + 1
11.945 * * [simplify]: Extracting #3: cost 17 inf + 1
11.945 * * [simplify]: Extracting #4: cost 55 inf + 322
11.946 * * [simplify]: Extracting #5: cost 80 inf + 11197
11.950 * * [simplify]: Extracting #6: cost 84 inf + 56173
11.962 * * [simplify]: Extracting #7: cost 7 inf + 177856
11.976 * * [simplify]: Extracting #8: cost 0 inf + 193436
11.989 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
11.989 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
11.990 * * * [progress]: adding candidates to table
12.106 * * [progress]: iteration 4 / 4
12.106 * * * [progress]: picking best candidate
12.141 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
12.141 * * * [progress]: localizing error
12.365 * * * [progress]: generating rewritten candidates
12.365 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
12.370 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
12.376 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
12.379 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
12.389 * * * [progress]: generating series expansions
12.389 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
12.389 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
12.389 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
12.389 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
12.389 * * * [progress]: simplifying candidates
12.389 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
12.389 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
12.389 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
12.390 * [simplify]: Simplifying (neg.p16 b_2)
12.390 * * [simplify]: iters left: 1 (2 enodes)
12.391 * * [simplify]: Extracting #0: cost 1 inf + 0
12.391 * * [simplify]: Extracting #1: cost 2 inf + 0
12.391 * * [simplify]: Extracting #2: cost 1 inf + 1
12.391 * * [simplify]: Extracting #3: cost 0 inf + 82
12.391 * [simplify]: Simplified to (neg.p16 b_2)
12.391 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
12.391 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
12.391 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
12.391 * * [simplify]: iters left: 5 (9 enodes)
12.395 * * [simplify]: iters left: 4 (32 enodes)
12.407 * * [simplify]: iters left: 3 (94 enodes)
12.444 * * [simplify]: iters left: 2 (340 enodes)
12.620 * * [simplify]: Extracting #0: cost 1 inf + 0
12.620 * * [simplify]: Extracting #1: cost 50 inf + 0
12.621 * * [simplify]: Extracting #2: cost 240 inf + 0
12.626 * * [simplify]: Extracting #3: cost 363 inf + 51025
12.651 * * [simplify]: Extracting #4: cost 279 inf + 363866
12.707 * * [simplify]: Extracting #5: cost 63 inf + 808744
12.752 * * [simplify]: Extracting #6: cost 1 inf + 916546
12.811 * * [simplify]: Extracting #7: cost 0 inf + 919829
12.861 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
12.861 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
12.861 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
12.862 * * [simplify]: iters left: 4 (8 enodes)
12.863 * * [simplify]: iters left: 3 (23 enodes)
12.867 * * [simplify]: iters left: 2 (45 enodes)
12.874 * * [simplify]: iters left: 1 (108 enodes)
12.902 * * [simplify]: Extracting #0: cost 1 inf + 0
12.902 * * [simplify]: Extracting #1: cost 3 inf + 0
12.902 * * [simplify]: Extracting #2: cost 3 inf + 1
12.902 * * [simplify]: Extracting #3: cost 17 inf + 1
12.902 * * [simplify]: Extracting #4: cost 55 inf + 322
12.902 * * [simplify]: Extracting #5: cost 80 inf + 11197
12.904 * * [simplify]: Extracting #6: cost 84 inf + 56173
12.912 * * [simplify]: Extracting #7: cost 7 inf + 177856
12.927 * * [simplify]: Extracting #8: cost 0 inf + 193436
12.937 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
12.937 * [simplify]: Simplified (2 1 1 2 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
12.938 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
12.938 * [simplify]: Simplifying (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
12.938 * * [simplify]: iters left: 5 (10 enodes)
12.940 * * [simplify]: iters left: 4 (30 enodes)
12.945 * * [simplify]: iters left: 3 (62 enodes)
12.957 * * [simplify]: iters left: 2 (195 enodes)
13.017 * * [simplify]: Extracting #0: cost 1 inf + 0
13.017 * * [simplify]: Extracting #1: cost 19 inf + 0
13.017 * * [simplify]: Extracting #2: cost 92 inf + 0
13.018 * * [simplify]: Extracting #3: cost 147 inf + 685
13.019 * * [simplify]: Extracting #4: cost 197 inf + 18145
13.025 * * [simplify]: Extracting #5: cost 136 inf + 180081
13.040 * * [simplify]: Extracting #6: cost 44 inf + 357497
13.073 * * [simplify]: Extracting #7: cost 1 inf + 421516
13.097 * * [simplify]: Extracting #8: cost 0 inf + 424799
13.123 * [simplify]: Simplified to (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
13.123 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))) a))
13.123 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
13.124 * [simplify]: Simplifying (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
13.124 * * [simplify]: iters left: 5 (9 enodes)
13.128 * * [simplify]: iters left: 4 (30 enodes)
13.138 * * [simplify]: iters left: 3 (65 enodes)
13.164 * * [simplify]: iters left: 2 (154 enodes)
13.233 * * [simplify]: iters left: 1 (482 enodes)
13.580 * * [simplify]: Extracting #0: cost 1 inf + 0
13.580 * * [simplify]: Extracting #1: cost 24 inf + 0
13.581 * * [simplify]: Extracting #2: cost 122 inf + 0
13.584 * * [simplify]: Extracting #3: cost 346 inf + 19576
13.593 * * [simplify]: Extracting #4: cost 490 inf + 110433
13.617 * * [simplify]: Extracting #5: cost 235 inf + 604158
13.692 * * [simplify]: Extracting #6: cost 13 inf + 1060306
13.776 * * [simplify]: Extracting #7: cost 0 inf + 1079456
13.853 * [simplify]: Simplified to (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
13.853 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) a))
13.854 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
13.854 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
13.854 * * [simplify]: iters left: 4 (8 enodes)
13.857 * * [simplify]: iters left: 3 (23 enodes)
13.865 * * [simplify]: iters left: 2 (45 enodes)
13.883 * * [simplify]: iters left: 1 (108 enodes)
13.921 * * [simplify]: Extracting #0: cost 1 inf + 0
13.922 * * [simplify]: Extracting #1: cost 3 inf + 0
13.922 * * [simplify]: Extracting #2: cost 3 inf + 1
13.922 * * [simplify]: Extracting #3: cost 17 inf + 1
13.922 * * [simplify]: Extracting #4: cost 55 inf + 322
13.922 * * [simplify]: Extracting #5: cost 80 inf + 11197
13.924 * * [simplify]: Extracting #6: cost 84 inf + 56173
13.929 * * [simplify]: Extracting #7: cost 7 inf + 177856
13.937 * * [simplify]: Extracting #8: cost 0 inf + 193436
13.948 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
13.948 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
13.949 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
13.949 * * [simplify]: iters left: 4 (8 enodes)
13.952 * * [simplify]: iters left: 3 (28 enodes)
13.960 * * [simplify]: iters left: 2 (59 enodes)
13.982 * * [simplify]: iters left: 1 (178 enodes)
14.091 * * [simplify]: Extracting #0: cost 1 inf + 0
14.091 * * [simplify]: Extracting #1: cost 12 inf + 0
14.091 * * [simplify]: Extracting #2: cost 64 inf + 1
14.092 * * [simplify]: Extracting #3: cost 140 inf + 403
14.094 * * [simplify]: Extracting #4: cost 187 inf + 15607
14.102 * * [simplify]: Extracting #5: cost 136 inf + 133387
14.128 * * [simplify]: Extracting #6: cost 33 inf + 315910
14.155 * * [simplify]: Extracting #7: cost 1 inf + 363183
14.183 * * [simplify]: Extracting #8: cost 0 inf + 364746
14.198 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
14.198 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
14.198 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
14.198 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.198 * * [simplify]: iters left: 4 (8 enodes)
14.200 * * [simplify]: iters left: 3 (23 enodes)
14.204 * * [simplify]: iters left: 2 (45 enodes)
14.212 * * [simplify]: iters left: 1 (108 enodes)
14.249 * * [simplify]: Extracting #0: cost 1 inf + 0
14.249 * * [simplify]: Extracting #1: cost 3 inf + 0
14.249 * * [simplify]: Extracting #2: cost 3 inf + 1
14.249 * * [simplify]: Extracting #3: cost 17 inf + 1
14.249 * * [simplify]: Extracting #4: cost 55 inf + 322
14.250 * * [simplify]: Extracting #5: cost 80 inf + 11197
14.254 * * [simplify]: Extracting #6: cost 84 inf + 56173
14.265 * * [simplify]: Extracting #7: cost 7 inf + 177856
14.279 * * [simplify]: Extracting #8: cost 0 inf + 193436
14.292 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
14.292 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
14.292 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.292 * * [simplify]: iters left: 4 (8 enodes)
14.296 * * [simplify]: iters left: 3 (28 enodes)
14.306 * * [simplify]: iters left: 2 (59 enodes)
14.328 * * [simplify]: iters left: 1 (178 enodes)
14.406 * * [simplify]: Extracting #0: cost 1 inf + 0
14.406 * * [simplify]: Extracting #1: cost 12 inf + 0
14.407 * * [simplify]: Extracting #2: cost 64 inf + 1
14.407 * * [simplify]: Extracting #3: cost 140 inf + 403
14.409 * * [simplify]: Extracting #4: cost 187 inf + 15607
14.419 * * [simplify]: Extracting #5: cost 136 inf + 133387
14.430 * * [simplify]: Extracting #6: cost 33 inf + 315910
14.445 * * [simplify]: Extracting #7: cost 1 inf + 363183
14.463 * * [simplify]: Extracting #8: cost 0 inf + 364746
14.479 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
14.479 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
14.479 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
14.480 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.480 * * [simplify]: iters left: 4 (8 enodes)
14.481 * * [simplify]: iters left: 3 (23 enodes)
14.485 * * [simplify]: iters left: 2 (45 enodes)
14.493 * * [simplify]: iters left: 1 (108 enodes)
14.520 * * [simplify]: Extracting #0: cost 1 inf + 0
14.520 * * [simplify]: Extracting #1: cost 3 inf + 0
14.520 * * [simplify]: Extracting #2: cost 3 inf + 1
14.520 * * [simplify]: Extracting #3: cost 17 inf + 1
14.520 * * [simplify]: Extracting #4: cost 55 inf + 322
14.520 * * [simplify]: Extracting #5: cost 80 inf + 11197
14.522 * * [simplify]: Extracting #6: cost 84 inf + 56173
14.527 * * [simplify]: Extracting #7: cost 7 inf + 177856
14.538 * * [simplify]: Extracting #8: cost 0 inf + 193436
14.551 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
14.551 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
14.552 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.552 * * [simplify]: iters left: 4 (8 enodes)
14.555 * * [simplify]: iters left: 3 (28 enodes)
14.565 * * [simplify]: iters left: 2 (59 enodes)
14.587 * * [simplify]: iters left: 1 (178 enodes)
14.696 * * [simplify]: Extracting #0: cost 1 inf + 0
14.696 * * [simplify]: Extracting #1: cost 12 inf + 0
14.696 * * [simplify]: Extracting #2: cost 64 inf + 1
14.697 * * [simplify]: Extracting #3: cost 140 inf + 403
14.699 * * [simplify]: Extracting #4: cost 187 inf + 15607
14.707 * * [simplify]: Extracting #5: cost 136 inf + 133387
14.725 * * [simplify]: Extracting #6: cost 33 inf + 315910
14.739 * * [simplify]: Extracting #7: cost 1 inf + 363183
14.754 * * [simplify]: Extracting #8: cost 0 inf + 364746
14.768 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
14.768 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
14.768 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
14.768 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.768 * * [simplify]: iters left: 4 (8 enodes)
14.770 * * [simplify]: iters left: 3 (23 enodes)
14.774 * * [simplify]: iters left: 2 (45 enodes)
14.783 * * [simplify]: iters left: 1 (108 enodes)
14.810 * * [simplify]: Extracting #0: cost 1 inf + 0
14.810 * * [simplify]: Extracting #1: cost 3 inf + 0
14.810 * * [simplify]: Extracting #2: cost 3 inf + 1
14.810 * * [simplify]: Extracting #3: cost 17 inf + 1
14.810 * * [simplify]: Extracting #4: cost 55 inf + 322
14.811 * * [simplify]: Extracting #5: cost 80 inf + 11197
14.813 * * [simplify]: Extracting #6: cost 84 inf + 56173
14.818 * * [simplify]: Extracting #7: cost 7 inf + 177856
14.825 * * [simplify]: Extracting #8: cost 0 inf + 193436
14.831 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
14.831 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
14.832 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.832 * * [simplify]: iters left: 4 (8 enodes)
14.833 * * [simplify]: iters left: 3 (28 enodes)
14.838 * * [simplify]: iters left: 2 (59 enodes)
14.851 * * [simplify]: iters left: 1 (178 enodes)
14.903 * * [simplify]: Extracting #0: cost 1 inf + 0
14.903 * * [simplify]: Extracting #1: cost 12 inf + 0
14.903 * * [simplify]: Extracting #2: cost 64 inf + 1
14.904 * * [simplify]: Extracting #3: cost 140 inf + 403
14.905 * * [simplify]: Extracting #4: cost 187 inf + 15607
14.909 * * [simplify]: Extracting #5: cost 136 inf + 133387
14.923 * * [simplify]: Extracting #6: cost 33 inf + 315910
14.937 * * [simplify]: Extracting #7: cost 1 inf + 363183
14.952 * * [simplify]: Extracting #8: cost 0 inf + 364746
14.967 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
14.967 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
14.967 * * * [progress]: adding candidates to table
15.066 * [progress]: [Phase 3 of 3] Extracting.
15.066 * * [regime]: Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>)
15.070 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
15.070 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>)
15.177 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>)
15.279 * * * * [regimes]: Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>)
15.381 * * * [regime]: Found split indices: #<option (#s(si 2 256))>
15.381 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
15.381 * * [simplify]: iters left: 5 (9 enodes)
15.382 * * [simplify]: Extracting #0: cost 1 inf + 0
15.382 * * [simplify]: Extracting #1: cost 3 inf + 0
15.382 * * [simplify]: Extracting #2: cost 4 inf + 1
15.382 * * [simplify]: Extracting #3: cost 4 inf + 2
15.382 * * [simplify]: Extracting #4: cost 6 inf + 2
15.382 * * [simplify]: Extracting #5: cost 6 inf + 323
15.382 * * [simplify]: Extracting #6: cost 0 inf + 4258
15.382 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
15.382 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
15.417 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
15.419 * * * * [points]: Setting MPFR precision to 64
15.420 * * * * [points]: Setting MPFR precision to 320
15.421 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
15.422 * * * * [points]: Setting MPFR precision to 64
15.424 * * * * [points]: Setting MPFR precision to 320
15.426 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
15.427 * * * * [points]: Setting MPFR precision to 64
15.432 * * * * [points]: Setting MPFR precision to 320
15.436 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
15.437 * * * * [points]: Setting MPFR precision to 64
15.456 * * * * [points]: Setting MPFR precision to 320
15.464 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
15.466 * * * * [points]: Setting MPFR precision to 64
15.483 * * * * [points]: Setting MPFR precision to 320
15.501 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
15.502 * * * * [points]: Setting MPFR precision to 64
15.535 * * * * [points]: Setting MPFR precision to 320
15.570 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
15.571 * * * * [points]: Setting MPFR precision to 64
15.668 * * * * [points]: Setting MPFR precision to 320
15.770 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
15.771 * * * * [points]: Setting MPFR precision to 64
15.944 * * * * [points]: Setting MPFR precision to 320
16.215 * * * * [points]: Computing exacts for 8000 points
16.217 * * * * [points]: Setting MPFR precision to 64
17.626 * * * * [points]: Setting MPFR precision to 320
18.555 * * * * [points]: Filtering points with unrepresentable outputs
18.602 * * * * [points]: Sampled 8000 points with exact outputs
21.039 * [regime-testing]: Baseline error score: 64.0
21.046 * [regime-testing]: Oracle error score: 64.0
21.060 * [regime-testing]: End program error score: 1.6949216928040012