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.006 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.111 * * * * [points]: Setting MPFR precision to 64
0.116 * * * * [points]: Setting MPFR precision to 320
0.118 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.121 * * * * [points]: Setting MPFR precision to 64
0.125 * * * * [points]: Setting MPFR precision to 320
0.129 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.131 * * * * [points]: Setting MPFR precision to 64
0.137 * * * * [points]: Setting MPFR precision to 320
0.143 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.145 * * * * [points]: Setting MPFR precision to 64
0.193 * * * * [points]: Setting MPFR precision to 320
0.210 * * * * [points]: Computing exacts for 256 points
0.214 * * * * [points]: Setting MPFR precision to 64
0.281 * * * * [points]: Setting MPFR precision to 320
0.311 * * * * [points]: Filtering points with unrepresentable outputs
0.313 * * * * [points]: Sampled 256 points with exact outputs
0.314 * * * [progress]: [2/2] Setting up program.
0.374 * [progress]: [Phase 2 of 3] Improving.
0.375 * * * * [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.377 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.379 * * [simplify]: iters left: 5 (10 enodes)
0.391 * * [simplify]: iters left: 4 (31 enodes)
0.404 * * [simplify]: iters left: 3 (65 enodes)
0.434 * * [simplify]: iters left: 2 (207 enodes)
0.589 * * [simplify]: Extracting #0: cost 1 inf + 0
0.589 * * [simplify]: Extracting #1: cost 20 inf + 0
0.590 * * [simplify]: Extracting #2: cost 88 inf + 1
0.591 * * [simplify]: Extracting #3: cost 167 inf + 83
0.593 * * [simplify]: Extracting #4: cost 224 inf + 14445
0.600 * * [simplify]: Extracting #5: cost 183 inf + 98116
0.631 * * [simplify]: Extracting #6: cost 60 inf + 344757
0.661 * * [simplify]: Extracting #7: cost 1 inf + 432442
0.692 * * [simplify]: Extracting #8: cost 0 inf + 435725
0.723 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
0.724 * [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.744 * * [progress]: iteration 1 / 4
0.744 * * * [progress]: picking best candidate
0.758 * * * * [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.758 * * * [progress]: localizing error
0.905 * * * [progress]: generating rewritten candidates
0.905 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.908 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
0.909 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 1)
0.912 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
0.925 * * * [progress]: generating series expansions
0.925 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.925 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
0.925 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 1)
0.925 * * * * [progress]: [ 4 / 4 ] generating series at (2)
0.926 * * * [progress]: simplifying candidates
0.926 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (neg.p16 b_2) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
0.926 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
0.926 * * [simplify]: iters left: 4 (8 enodes)
0.928 * * [simplify]: iters left: 3 (22 enodes)
0.931 * * [simplify]: iters left: 2 (44 enodes)
0.940 * * [simplify]: iters left: 1 (99 enodes)
0.967 * * [simplify]: Extracting #0: cost 1 inf + 0
0.967 * * [simplify]: Extracting #1: cost 2 inf + 0
0.968 * * [simplify]: Extracting #2: cost 3 inf + 0
0.968 * * [simplify]: Extracting #3: cost 17 inf + 0
0.968 * * [simplify]: Extracting #4: cost 57 inf + 0
0.968 * * [simplify]: Extracting #5: cost 89 inf + 1048
0.970 * * [simplify]: Extracting #6: cost 73 inf + 56606
0.975 * * [simplify]: Extracting #7: cost 0 inf + 174728
0.981 * * [simplify]: Extracting #8: cost 0 inf + 172968
0.987 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))
0.987 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (+.p16 (neg.p16 b_2) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))
0.987 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
0.987 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
0.987 * * [simplify]: iters left: 5 (11 enodes)
0.989 * * [simplify]: iters left: 4 (35 enodes)
0.996 * * [simplify]: iters left: 3 (100 enodes)
1.019 * * [simplify]: iters left: 2 (359 enodes)
1.178 * * [simplify]: Extracting #0: cost 1 inf + 0
1.179 * * [simplify]: Extracting #1: cost 48 inf + 0
1.179 * * [simplify]: Extracting #2: cost 218 inf + 0
1.181 * * [simplify]: Extracting #3: cost 322 inf + 45040
1.194 * * [simplify]: Extracting #4: cost 299 inf + 342038
1.232 * * [simplify]: Extracting #5: cost 86 inf + 819696
1.273 * * [simplify]: Extracting #6: cost 1 inf + 958399
1.316 * * [simplify]: Extracting #7: cost 0 inf + 960402
1.387 * [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.387 * [simplify]: Simplified (2 1 1) 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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
1.387 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1.388 * * [simplify]: iters left: 4 (9 enodes)
1.391 * * [simplify]: iters left: 3 (24 enodes)
1.398 * * [simplify]: iters left: 2 (47 enodes)
1.412 * * [simplify]: iters left: 1 (110 enodes)
1.462 * * [simplify]: Extracting #0: cost 1 inf + 0
1.463 * * [simplify]: Extracting #1: cost 6 inf + 0
1.463 * * [simplify]: Extracting #2: cost 10 inf + 1
1.463 * * [simplify]: Extracting #3: cost 23 inf + 403
1.463 * * [simplify]: Extracting #4: cost 60 inf + 1445
1.464 * * [simplify]: Extracting #5: cost 79 inf + 12440
1.467 * * [simplify]: Extracting #6: cost 76 inf + 55663
1.474 * * [simplify]: Extracting #7: cost 8 inf + 160807
1.484 * * [simplify]: Extracting #8: cost 0 inf + 177990
1.494 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1.494 * [simplify]: Simplified (2 1 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)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1.494 * * * * [progress]: [ 3 / 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.495 * [simplify]: Simplifying (neg.p16 (*.p16 a c))
1.495 * * [simplify]: iters left: 2 (4 enodes)
1.496 * * [simplify]: iters left: 1 (9 enodes)
1.498 * * [simplify]: Extracting #0: cost 1 inf + 0
1.498 * * [simplify]: Extracting #1: cost 2 inf + 0
1.498 * * [simplify]: Extracting #2: cost 4 inf + 0
1.498 * * [simplify]: Extracting #3: cost 2 inf + 2
1.498 * * [simplify]: Extracting #4: cost 0 inf + 726
1.498 * [simplify]: Simplified to (neg.p16 (*.p16 c a))
1.498 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a))))) a))
1.498 * * * * [progress]: [ 4 / 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.499 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c)))
1.499 * * [simplify]: iters left: 3 (8 enodes)
1.502 * * [simplify]: iters left: 2 (33 enodes)
1.513 * * [simplify]: iters left: 1 (79 enodes)
1.545 * * [simplify]: Extracting #0: cost 1 inf + 0
1.545 * * [simplify]: Extracting #1: cost 21 inf + 0
1.546 * * [simplify]: Extracting #2: cost 51 inf + 0
1.546 * * [simplify]: Extracting #3: cost 76 inf + 5301
1.550 * * [simplify]: Extracting #4: cost 36 inf + 63309
1.556 * * [simplify]: Extracting #5: cost 2 inf + 115428
1.563 * * [simplify]: Extracting #6: cost 0 inf + 119672
1.573 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
1.573 * [simplify]: Simplified (2 1 2 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
1.573 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
1.574 * * [simplify]: iters left: 2 (6 enodes)
1.576 * * [simplify]: iters left: 1 (14 enodes)
1.580 * * [simplify]: Extracting #0: cost 1 inf + 0
1.580 * * [simplify]: Extracting #1: cost 3 inf + 0
1.580 * * [simplify]: Extracting #2: cost 6 inf + 0
1.580 * * [simplify]: Extracting #3: cost 2 inf + 325
1.580 * * [simplify]: Extracting #4: cost 0 inf + 1329
1.580 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
1.580 * [simplify]: Simplified (2 1 2 1 2) to (λ (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 c a) (*.p16 b_2 b_2))))) a))
1.581 * * * * [progress]: [ 5 / 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.581 * [simplify]: Simplifying (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1.581 * * [simplify]: iters left: 5 (10 enodes)
1.585 * * [simplify]: iters left: 4 (32 enodes)
1.597 * * [simplify]: iters left: 3 (57 enodes)
1.611 * * [simplify]: iters left: 2 (124 enodes)
1.639 * * [simplify]: iters left: 1 (429 enodes)
1.910 * * [simplify]: Extracting #0: cost 1 inf + 0
1.910 * * [simplify]: Extracting #1: cost 10 inf + 0
1.910 * * [simplify]: Extracting #2: cost 34 inf + 1
1.910 * * [simplify]: Extracting #3: cost 92 inf + 2
1.911 * * [simplify]: Extracting #4: cost 331 inf + 404
1.914 * * [simplify]: Extracting #5: cost 487 inf + 33943
1.946 * * [simplify]: Extracting #6: cost 335 inf + 481558
2.010 * * [simplify]: Extracting #7: cost 29 inf + 1060457
2.074 * * [simplify]: Extracting #8: cost 0 inf + 1120774
2.142 * [simplify]: Simplified to (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
2.142 * [simplify]: Simplified (2 2) to (λ (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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))))
2.143 * * * * [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))>
2.143 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.143 * * [simplify]: iters left: 5 (10 enodes)
2.147 * * [simplify]: iters left: 4 (31 enodes)
2.158 * * [simplify]: iters left: 3 (65 enodes)
2.171 * * [simplify]: iters left: 2 (207 enodes)
2.241 * * [simplify]: Extracting #0: cost 1 inf + 0
2.241 * * [simplify]: Extracting #1: cost 20 inf + 0
2.241 * * [simplify]: Extracting #2: cost 88 inf + 1
2.242 * * [simplify]: Extracting #3: cost 167 inf + 83
2.243 * * [simplify]: Extracting #4: cost 224 inf + 14445
2.248 * * [simplify]: Extracting #5: cost 183 inf + 98116
2.260 * * [simplify]: Extracting #6: cost 60 inf + 344757
2.276 * * [simplify]: Extracting #7: cost 1 inf + 432442
2.304 * * [simplify]: Extracting #8: cost 0 inf + 435725
2.322 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.322 * [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.322 * * * * [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.323 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.323 * * [simplify]: iters left: 5 (10 enodes)
2.325 * * [simplify]: iters left: 4 (31 enodes)
2.331 * * [simplify]: iters left: 3 (65 enodes)
2.356 * * [simplify]: iters left: 2 (207 enodes)
2.439 * * [simplify]: Extracting #0: cost 1 inf + 0
2.439 * * [simplify]: Extracting #1: cost 20 inf + 0
2.439 * * [simplify]: Extracting #2: cost 88 inf + 1
2.440 * * [simplify]: Extracting #3: cost 167 inf + 83
2.441 * * [simplify]: Extracting #4: cost 224 inf + 14445
2.444 * * [simplify]: Extracting #5: cost 183 inf + 98116
2.456 * * [simplify]: Extracting #6: cost 60 inf + 344757
2.476 * * [simplify]: Extracting #7: cost 1 inf + 432442
2.493 * * [simplify]: Extracting #8: cost 0 inf + 435725
2.518 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.518 * [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.518 * * * * [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.521 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.521 * * [simplify]: iters left: 5 (10 enodes)
2.525 * * [simplify]: iters left: 4 (31 enodes)
2.535 * * [simplify]: iters left: 3 (65 enodes)
2.560 * * [simplify]: iters left: 2 (207 enodes)
2.667 * * [simplify]: Extracting #0: cost 1 inf + 0
2.667 * * [simplify]: Extracting #1: cost 20 inf + 0
2.667 * * [simplify]: Extracting #2: cost 88 inf + 1
2.667 * * [simplify]: Extracting #3: cost 167 inf + 83
2.668 * * [simplify]: Extracting #4: cost 224 inf + 14445
2.672 * * [simplify]: Extracting #5: cost 183 inf + 98116
2.683 * * [simplify]: Extracting #6: cost 60 inf + 344757
2.711 * * [simplify]: Extracting #7: cost 1 inf + 432442
2.728 * * [simplify]: Extracting #8: cost 0 inf + 435725
2.753 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.753 * [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.753 * * * * [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.753 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.753 * * [simplify]: iters left: 5 (10 enodes)
2.759 * * [simplify]: iters left: 4 (31 enodes)
2.770 * * [simplify]: iters left: 3 (65 enodes)
2.796 * * [simplify]: iters left: 2 (207 enodes)
2.886 * * [simplify]: Extracting #0: cost 1 inf + 0
2.886 * * [simplify]: Extracting #1: cost 20 inf + 0
2.886 * * [simplify]: Extracting #2: cost 88 inf + 1
2.887 * * [simplify]: Extracting #3: cost 167 inf + 83
2.889 * * [simplify]: Extracting #4: cost 224 inf + 14445
2.895 * * [simplify]: Extracting #5: cost 183 inf + 98116
2.907 * * [simplify]: Extracting #6: cost 60 inf + 344757
2.924 * * [simplify]: Extracting #7: cost 1 inf + 432442
2.948 * * [simplify]: Extracting #8: cost 0 inf + 435725
2.967 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.967 * [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.968 * * * [progress]: adding candidates to table
3.151 * * [progress]: iteration 2 / 4
3.151 * * * [progress]: picking best candidate
3.189 * * * * [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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
3.189 * * * [progress]: localizing error
3.498 * * * [progress]: generating rewritten candidates
3.498 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
3.501 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
3.503 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 2)
3.504 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2 1)
3.507 * * * [progress]: generating series expansions
3.507 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
3.507 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
3.507 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 2)
3.507 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2 1)
3.507 * * * [progress]: simplifying candidates
3.507 * * * * [progress]: [ 1 / 7 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (neg.p16 b_2))) a))>
3.507 * * * * [progress]: [ 2 / 7 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c)))))) a))>
3.507 * [simplify]: Simplifying (neg.p16 (*.p16 a c))
3.507 * * [simplify]: iters left: 2 (4 enodes)
3.508 * * [simplify]: iters left: 1 (9 enodes)
3.509 * * [simplify]: Extracting #0: cost 1 inf + 0
3.509 * * [simplify]: Extracting #1: cost 2 inf + 0
3.509 * * [simplify]: Extracting #2: cost 4 inf + 0
3.509 * * [simplify]: Extracting #3: cost 2 inf + 2
3.509 * * [simplify]: Extracting #4: cost 0 inf + 726
3.509 * [simplify]: Simplified to (neg.p16 (*.p16 c a))
3.509 * [simplify]: Simplified (2 1 2 2 1 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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))))) a))
3.509 * * * * [progress]: [ 3 / 7 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.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))>
3.509 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c)))
3.510 * * [simplify]: iters left: 3 (8 enodes)
3.511 * * [simplify]: iters left: 2 (33 enodes)
3.523 * * [simplify]: iters left: 1 (79 enodes)
3.563 * * [simplify]: Extracting #0: cost 1 inf + 0
3.563 * * [simplify]: Extracting #1: cost 21 inf + 0
3.564 * * [simplify]: Extracting #2: cost 51 inf + 0
3.564 * * [simplify]: Extracting #3: cost 76 inf + 5301
3.567 * * [simplify]: Extracting #4: cost 36 inf + 63309
3.573 * * [simplify]: Extracting #5: cost 2 inf + 115428
3.581 * * [simplify]: Extracting #6: cost 0 inf + 119672
3.588 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
3.588 * [simplify]: Simplified (2 1 2 2 1 1) 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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) a))
3.588 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
3.588 * * [simplify]: iters left: 2 (6 enodes)
3.591 * * [simplify]: iters left: 1 (14 enodes)
3.595 * * [simplify]: Extracting #0: cost 1 inf + 0
3.595 * * [simplify]: Extracting #1: cost 3 inf + 0
3.595 * * [simplify]: Extracting #2: cost 6 inf + 0
3.595 * * [simplify]: Extracting #3: cost 2 inf + 325
3.595 * * [simplify]: Extracting #4: cost 0 inf + 1329
3.595 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
3.595 * [simplify]: Simplified (2 1 2 2 1 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)))) (+.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 c a) (*.p16 b_2 b_2)))))) a))
3.595 * * * * [progress]: [ 4 / 7 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
3.596 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a)
3.596 * * [simplify]: iters left: 6 (15 enodes)
3.602 * * [simplify]: iters left: 5 (40 enodes)
3.617 * * [simplify]: iters left: 4 (102 enodes)
3.657 * * [simplify]: iters left: 3 (250 enodes)
3.801 * * [simplify]: Extracting #0: cost 1 inf + 0
3.802 * * [simplify]: Extracting #1: cost 9 inf + 0
3.802 * * [simplify]: Extracting #2: cost 37 inf + 1
3.802 * * [simplify]: Extracting #3: cost 88 inf + 846
3.803 * * [simplify]: Extracting #4: cost 90 inf + 23777
3.806 * * [simplify]: Extracting #5: cost 79 inf + 69187
3.812 * * [simplify]: Extracting #6: cost 55 inf + 142773
3.820 * * [simplify]: Extracting #7: cost 1 inf + 231486
3.831 * * [simplify]: Extracting #8: cost 0 inf + 234769
3.839 * [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.840 * [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.840 * * * * [progress]: [ 5 / 7 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
3.840 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a)
3.840 * * [simplify]: iters left: 6 (15 enodes)
3.843 * * [simplify]: iters left: 5 (40 enodes)
3.852 * * [simplify]: iters left: 4 (102 enodes)
3.872 * * [simplify]: iters left: 3 (250 enodes)
3.985 * * [simplify]: Extracting #0: cost 1 inf + 0
3.985 * * [simplify]: Extracting #1: cost 9 inf + 0
3.985 * * [simplify]: Extracting #2: cost 37 inf + 1
3.985 * * [simplify]: Extracting #3: cost 88 inf + 846
3.986 * * [simplify]: Extracting #4: cost 90 inf + 23777
3.989 * * [simplify]: Extracting #5: cost 79 inf + 69187
3.995 * * [simplify]: Extracting #6: cost 55 inf + 142773
4.003 * * [simplify]: Extracting #7: cost 1 inf + 231486
4.011 * * [simplify]: Extracting #8: cost 0 inf + 234769
4.020 * [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.020 * [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.020 * * * * [progress]: [ 6 / 7 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
4.020 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a)
4.021 * * [simplify]: iters left: 6 (15 enodes)
4.024 * * [simplify]: iters left: 5 (40 enodes)
4.034 * * [simplify]: iters left: 4 (102 enodes)
4.062 * * [simplify]: iters left: 3 (250 enodes)
4.172 * * [simplify]: Extracting #0: cost 1 inf + 0
4.172 * * [simplify]: Extracting #1: cost 9 inf + 0
4.172 * * [simplify]: Extracting #2: cost 37 inf + 1
4.173 * * [simplify]: Extracting #3: cost 88 inf + 846
4.174 * * [simplify]: Extracting #4: cost 90 inf + 23777
4.176 * * [simplify]: Extracting #5: cost 79 inf + 69187
4.182 * * [simplify]: Extracting #6: cost 55 inf + 142773
4.190 * * [simplify]: Extracting #7: cost 1 inf + 231486
4.198 * * [simplify]: Extracting #8: cost 0 inf + 234769
4.207 * [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.207 * [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.207 * * * * [progress]: [ 7 / 7 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
4.207 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a)
4.207 * * [simplify]: iters left: 6 (15 enodes)
4.213 * * [simplify]: iters left: 5 (40 enodes)
4.227 * * [simplify]: iters left: 4 (102 enodes)
4.269 * * [simplify]: iters left: 3 (250 enodes)
4.418 * * [simplify]: Extracting #0: cost 1 inf + 0
4.419 * * [simplify]: Extracting #1: cost 9 inf + 0
4.419 * * [simplify]: Extracting #2: cost 37 inf + 1
4.419 * * [simplify]: Extracting #3: cost 88 inf + 846
4.420 * * [simplify]: Extracting #4: cost 90 inf + 23777
4.423 * * [simplify]: Extracting #5: cost 79 inf + 69187
4.428 * * [simplify]: Extracting #6: cost 55 inf + 142773
4.436 * * [simplify]: Extracting #7: cost 1 inf + 231486
4.445 * * [simplify]: Extracting #8: cost 0 inf + 234769
4.454 * [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.454 * [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.454 * * * [progress]: adding candidates to table
4.695 * * [progress]: iteration 3 / 4
4.695 * * * [progress]: picking best candidate
4.757 * * * * [pick]: Picked  #<alt (λ (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.757 * * * [progress]: localizing error
4.974 * * * [progress]: generating rewritten candidates
4.974 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
4.978 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
4.985 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 1)
4.985 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 1 1)
5.000 * * * [progress]: generating series expansions
5.000 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
5.001 * * * * [progress]: [ 2 / 4 ] generating series at (2)
5.001 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 1)
5.001 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 1 1)
5.001 * * * [progress]: simplifying candidates
5.001 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (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))) (neg.p16 b_2)))))>
5.001 * [simplify]: Simplifying (neg.p16 b_2)
5.001 * * [simplify]: iters left: 1 (2 enodes)
5.001 * * [simplify]: Extracting #0: cost 1 inf + 0
5.001 * * [simplify]: Extracting #1: cost 2 inf + 0
5.001 * * [simplify]: Extracting #2: cost 1 inf + 1
5.001 * * [simplify]: Extracting #3: cost 0 inf + 82
5.001 * [simplify]: Simplified to (neg.p16 b_2)
5.002 * [simplify]: Simplified (2 2 2 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))) (neg.p16 b_2)))))
5.002 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.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)))))>
5.002 * [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))
5.002 * * [simplify]: iters left: 5 (9 enodes)
5.004 * * [simplify]: iters left: 4 (32 enodes)
5.010 * * [simplify]: iters left: 3 (94 enodes)
5.034 * * [simplify]: iters left: 2 (334 enodes)
5.250 * * [simplify]: Extracting #0: cost 1 inf + 0
5.250 * * [simplify]: Extracting #1: cost 45 inf + 0
5.251 * * [simplify]: Extracting #2: cost 220 inf + 0
5.255 * * [simplify]: Extracting #3: cost 326 inf + 50072
5.268 * * [simplify]: Extracting #4: cost 236 inf + 362547
5.317 * * [simplify]: Extracting #5: cost 59 inf + 750749
5.390 * * [simplify]: Extracting #6: cost 1 inf + 849495
5.449 * * [simplify]: Extracting #7: cost 0 inf + 852778
5.507 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
5.507 * [simplify]: Simplified (2 2 2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))))
5.507 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.507 * * [simplify]: iters left: 4 (8 enodes)
5.509 * * [simplify]: iters left: 3 (23 enodes)
5.512 * * [simplify]: iters left: 2 (45 enodes)
5.520 * * [simplify]: iters left: 1 (108 enodes)
5.565 * * [simplify]: Extracting #0: cost 1 inf + 0
5.565 * * [simplify]: Extracting #1: cost 3 inf + 0
5.565 * * [simplify]: Extracting #2: cost 3 inf + 1
5.566 * * [simplify]: Extracting #3: cost 17 inf + 1
5.566 * * [simplify]: Extracting #4: cost 55 inf + 322
5.567 * * [simplify]: Extracting #5: cost 78 inf + 10074
5.572 * * [simplify]: Extracting #6: cost 74 inf + 71480
5.582 * * [simplify]: Extracting #7: cost 3 inf + 182984
5.591 * * [simplify]: Extracting #8: cost 0 inf + 190232
5.597 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.597 * [simplify]: Simplified (2 2 2 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.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))))))))
5.597 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))>
5.598 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) a)
5.598 * * [simplify]: iters left: 3 (7 enodes)
5.600 * * [simplify]: iters left: 2 (14 enodes)
5.602 * * [simplify]: iters left: 1 (23 enodes)
5.606 * * [simplify]: Extracting #0: cost 1 inf + 0
5.606 * * [simplify]: Extracting #1: cost 7 inf + 0
5.606 * * [simplify]: Extracting #2: cost 6 inf + 443
5.606 * * [simplify]: Extracting #3: cost 2 inf + 2412
5.606 * * [simplify]: Extracting #4: cost 0 inf + 1534
5.606 * [simplify]: Simplified to (*.p16 (real->posit16 1.0) c)
5.606 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
5.606 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.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)))>
5.607 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.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))))
5.607 * * [simplify]: iters left: 6 (14 enodes)
5.610 * * [simplify]: iters left: 5 (42 enodes)
5.622 * * [simplify]: iters left: 4 (159 enodes)
5.717 * * [simplify]: Extracting #0: cost 1 inf + 0
5.717 * * [simplify]: Extracting #1: cost 39 inf + 0
5.718 * * [simplify]: Extracting #2: cost 117 inf + 766
5.719 * * [simplify]: Extracting #3: cost 199 inf + 3540
5.721 * * [simplify]: Extracting #4: cost 232 inf + 5390
5.726 * * [simplify]: Extracting #5: cost 157 inf + 82593
5.735 * * [simplify]: Extracting #6: cost 49 inf + 221831
5.745 * * [simplify]: Extracting #7: cost 3 inf + 284472
5.760 * * [simplify]: Extracting #8: cost 0 inf + 291241
5.781 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
5.781 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (*.p16 (/.p16 (*.p16 a c) (*.p16 a (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
5.782 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))) b_2))))>
5.782 * [simplify]: Simplifying (neg.p16 (*.p16 c a))
5.782 * * [simplify]: iters left: 2 (4 enodes)
5.784 * * [simplify]: iters left: 1 (9 enodes)
5.786 * * [simplify]: Extracting #0: cost 1 inf + 0
5.786 * * [simplify]: Extracting #1: cost 2 inf + 0
5.786 * * [simplify]: Extracting #2: cost 4 inf + 0
5.786 * * [simplify]: Extracting #3: cost 2 inf + 2
5.786 * * [simplify]: Extracting #4: cost 0 inf + 726
5.786 * [simplify]: Simplified to (neg.p16 (*.p16 a c))
5.786 * [simplify]: Simplified (2 2 2 1 1 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) (neg.p16 (*.p16 a c)))) b_2))))
5.786 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.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.787 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
5.787 * * [simplify]: iters left: 3 (8 enodes)
5.790 * * [simplify]: iters left: 2 (33 enodes)
5.802 * * [simplify]: iters left: 1 (79 enodes)
5.837 * * [simplify]: Extracting #0: cost 1 inf + 0
5.837 * * [simplify]: Extracting #1: cost 21 inf + 0
5.838 * * [simplify]: Extracting #2: cost 51 inf + 0
5.838 * * [simplify]: Extracting #3: cost 76 inf + 5301
5.842 * * [simplify]: Extracting #4: cost 36 inf + 63309
5.848 * * [simplify]: Extracting #5: cost 2 inf + 115428
5.856 * * [simplify]: Extracting #6: cost 0 inf + 119672
5.863 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
5.863 * [simplify]: Simplified (2 2 2 1 1 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.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))))
5.863 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
5.863 * * [simplify]: iters left: 2 (6 enodes)
5.866 * * [simplify]: iters left: 1 (14 enodes)
5.869 * * [simplify]: Extracting #0: cost 1 inf + 0
5.869 * * [simplify]: Extracting #1: cost 3 inf + 0
5.870 * * [simplify]: Extracting #2: cost 6 inf + 0
5.870 * * [simplify]: Extracting #3: cost 2 inf + 325
5.870 * * [simplify]: Extracting #4: cost 0 inf + 1329
5.870 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
5.870 * [simplify]: Simplified (2 2 2 1 1 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.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 a c) (*.p16 b_2 b_2)))) b_2))))
5.870 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (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))))>
5.870 * [simplify]: Simplifying (/.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)))
5.870 * * [simplify]: iters left: 6 (13 enodes)
5.876 * * [simplify]: iters left: 5 (38 enodes)
5.891 * * [simplify]: iters left: 4 (125 enodes)
5.979 * * [simplify]: Extracting #0: cost 1 inf + 0
5.979 * * [simplify]: Extracting #1: cost 32 inf + 0
5.980 * * [simplify]: Extracting #2: cost 72 inf + 1528
5.981 * * [simplify]: Extracting #3: cost 125 inf + 3822
5.983 * * [simplify]: Extracting #4: cost 115 inf + 29783
5.990 * * [simplify]: Extracting #5: cost 48 inf + 113802
6.001 * * [simplify]: Extracting #6: cost 27 inf + 153800
6.009 * * [simplify]: Extracting #7: cost 0 inf + 178777
6.018 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
6.018 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))))
6.018 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (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))))>
6.018 * [simplify]: Simplifying (/.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)))
6.018 * * [simplify]: iters left: 6 (13 enodes)
6.022 * * [simplify]: iters left: 5 (38 enodes)
6.031 * * [simplify]: iters left: 4 (125 enodes)
6.118 * * [simplify]: Extracting #0: cost 1 inf + 0
6.118 * * [simplify]: Extracting #1: cost 32 inf + 0
6.118 * * [simplify]: Extracting #2: cost 72 inf + 1528
6.119 * * [simplify]: Extracting #3: cost 125 inf + 3822
6.121 * * [simplify]: Extracting #4: cost 115 inf + 29783
6.128 * * [simplify]: Extracting #5: cost 48 inf + 113802
6.143 * * [simplify]: Extracting #6: cost 27 inf + 153800
6.155 * * [simplify]: Extracting #7: cost 0 inf + 178777
6.168 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
6.168 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))))
6.168 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (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))))>
6.169 * [simplify]: Simplifying (/.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)))
6.169 * * [simplify]: iters left: 6 (13 enodes)
6.175 * * [simplify]: iters left: 5 (38 enodes)
6.190 * * [simplify]: iters left: 4 (125 enodes)
6.269 * * [simplify]: Extracting #0: cost 1 inf + 0
6.269 * * [simplify]: Extracting #1: cost 32 inf + 0
6.270 * * [simplify]: Extracting #2: cost 72 inf + 1528
6.270 * * [simplify]: Extracting #3: cost 125 inf + 3822
6.271 * * [simplify]: Extracting #4: cost 115 inf + 29783
6.275 * * [simplify]: Extracting #5: cost 48 inf + 113802
6.281 * * [simplify]: Extracting #6: cost 27 inf + 153800
6.287 * * [simplify]: Extracting #7: cost 0 inf + 178777
6.299 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
6.299 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))))
6.299 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (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))))>
6.299 * [simplify]: Simplifying (/.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)))
6.300 * * [simplify]: iters left: 6 (13 enodes)
6.305 * * [simplify]: iters left: 5 (38 enodes)
6.321 * * [simplify]: iters left: 4 (125 enodes)
6.411 * * [simplify]: Extracting #0: cost 1 inf + 0
6.412 * * [simplify]: Extracting #1: cost 32 inf + 0
6.412 * * [simplify]: Extracting #2: cost 72 inf + 1528
6.413 * * [simplify]: Extracting #3: cost 125 inf + 3822
6.415 * * [simplify]: Extracting #4: cost 115 inf + 29783
6.422 * * [simplify]: Extracting #5: cost 48 inf + 113802
6.434 * * [simplify]: Extracting #6: cost 27 inf + 153800
6.446 * * [simplify]: Extracting #7: cost 0 inf + 178777
6.459 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
6.459 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))))
6.459 * * * [progress]: adding candidates to table
6.783 * * [progress]: iteration 4 / 4
6.783 * * * [progress]: picking best candidate
6.863 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))>
6.863 * * * [progress]: localizing error
7.044 * * * [progress]: generating rewritten candidates
7.044 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2)
7.045 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 1)
7.046 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
7.049 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1 1)
7.052 * * * [progress]: generating series expansions
7.052 * * * * [progress]: [ 1 / 4 ] generating series at (2 2)
7.052 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 1)
7.052 * * * * [progress]: [ 3 / 4 ] generating series at (2)
7.052 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1 1)
7.052 * * * [progress]: simplifying candidates
7.052 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))))>
7.052 * [simplify]: Simplifying (neg.p16 b_2)
7.052 * * [simplify]: iters left: 1 (2 enodes)
7.053 * * [simplify]: Extracting #0: cost 1 inf + 0
7.053 * * [simplify]: Extracting #1: cost 2 inf + 0
7.053 * * [simplify]: Extracting #2: cost 1 inf + 1
7.053 * * [simplify]: Extracting #3: cost 0 inf + 82
7.053 * [simplify]: Simplified to (neg.p16 b_2)
7.053 * [simplify]: Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))))
7.053 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) 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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
7.053 * [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.053 * * [simplify]: iters left: 5 (9 enodes)
7.055 * * [simplify]: iters left: 4 (32 enodes)
7.060 * * [simplify]: iters left: 3 (94 enodes)
7.092 * * [simplify]: iters left: 2 (334 enodes)
7.312 * * [simplify]: Extracting #0: cost 1 inf + 0
7.312 * * [simplify]: Extracting #1: cost 45 inf + 0
7.312 * * [simplify]: Extracting #2: cost 220 inf + 0
7.315 * * [simplify]: Extracting #3: cost 326 inf + 50072
7.327 * * [simplify]: Extracting #4: cost 236 inf + 362547
7.356 * * [simplify]: Extracting #5: cost 59 inf + 750749
7.809 * * [simplify]: Extracting #6: cost 1 inf + 849495
7.860 * * [simplify]: Extracting #7: cost 0 inf + 852778
7.906 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
7.906 * [simplify]: Simplified (2 2 1) to (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
7.906 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.906 * * [simplify]: iters left: 4 (8 enodes)
7.908 * * [simplify]: iters left: 3 (23 enodes)
7.911 * * [simplify]: iters left: 2 (45 enodes)
7.935 * * [simplify]: iters left: 1 (108 enodes)
7.990 * * [simplify]: Extracting #0: cost 1 inf + 0
7.990 * * [simplify]: Extracting #1: cost 3 inf + 0
7.991 * * [simplify]: Extracting #2: cost 3 inf + 1
7.991 * * [simplify]: Extracting #3: cost 17 inf + 1
7.991 * * [simplify]: Extracting #4: cost 55 inf + 322
7.992 * * [simplify]: Extracting #5: cost 78 inf + 10074
7.996 * * [simplify]: Extracting #6: cost 74 inf + 71480
8.007 * * [simplify]: Extracting #7: cost 3 inf + 182984
8.019 * * [simplify]: Extracting #8: cost 0 inf + 190232
8.031 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.031 * [simplify]: Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) 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 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))
8.031 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)))>
8.032 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)
8.032 * * [simplify]: iters left: 5 (9 enodes)
8.035 * * [simplify]: iters left: 4 (29 enodes)
8.043 * * [simplify]: iters left: 3 (62 enodes)
8.056 * * [simplify]: iters left: 2 (200 enodes)
8.138 * * [simplify]: Extracting #0: cost 1 inf + 0
8.138 * * [simplify]: Extracting #1: cost 20 inf + 0
8.139 * * [simplify]: Extracting #2: cost 94 inf + 1
8.140 * * [simplify]: Extracting #3: cost 162 inf + 1046
8.142 * * [simplify]: Extracting #4: cost 211 inf + 16816
8.148 * * [simplify]: Extracting #5: cost 170 inf + 107511
8.162 * * [simplify]: Extracting #6: cost 69 inf + 300802
8.179 * * [simplify]: Extracting #7: cost 1 inf + 411568
8.201 * * [simplify]: Extracting #8: cost 0 inf + 414291
8.217 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) c)
8.217 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) c)))
8.217 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (*.p16 (/.p16 (*.p16 (real->posit16 1.0) c) (-.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)))>
8.217 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.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.218 * * [simplify]: iters left: 6 (13 enodes)
8.221 * * [simplify]: iters left: 5 (39 enodes)
8.229 * * [simplify]: iters left: 4 (111 enodes)
8.282 * * [simplify]: iters left: 3 (397 enodes)
8.535 * * [simplify]: Extracting #0: cost 1 inf + 0
8.536 * * [simplify]: Extracting #1: cost 49 inf + 0
8.537 * * [simplify]: Extracting #2: cost 229 inf + 1
8.539 * * [simplify]: Extracting #3: cost 370 inf + 3856
8.551 * * [simplify]: Extracting #4: cost 437 inf + 164665
8.610 * * [simplify]: Extracting #5: cost 164 inf + 726884
8.692 * * [simplify]: Extracting #6: cost 38 inf + 1005389
8.787 * * [simplify]: Extracting #7: cost 1 inf + 1064551
8.847 * * [simplify]: Extracting #8: cost 0 inf + 1067834
8.919 * [simplify]: Simplified to (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c)))
8.919 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (*.p16 (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
8.920 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))) b_2)))>
8.920 * [simplify]: Simplifying (neg.p16 (*.p16 c a))
8.920 * * [simplify]: iters left: 2 (4 enodes)
8.922 * * [simplify]: iters left: 1 (9 enodes)
8.925 * * [simplify]: Extracting #0: cost 1 inf + 0
8.925 * * [simplify]: Extracting #1: cost 2 inf + 0
8.925 * * [simplify]: Extracting #2: cost 4 inf + 0
8.925 * * [simplify]: Extracting #3: cost 2 inf + 2
8.925 * * [simplify]: Extracting #4: cost 0 inf + 726
8.925 * [simplify]: Simplified to (neg.p16 (*.p16 a c))
8.925 * [simplify]: Simplified (2 2 1 1 2) to (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c)))) b_2)))
8.925 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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)))>
8.926 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
8.926 * * [simplify]: iters left: 3 (8 enodes)
8.930 * * [simplify]: iters left: 2 (33 enodes)
8.941 * * [simplify]: iters left: 1 (79 enodes)
8.958 * * [simplify]: Extracting #0: cost 1 inf + 0
8.958 * * [simplify]: Extracting #1: cost 21 inf + 0
8.958 * * [simplify]: Extracting #2: cost 51 inf + 0
8.958 * * [simplify]: Extracting #3: cost 76 inf + 5301
8.960 * * [simplify]: Extracting #4: cost 36 inf + 63309
8.963 * * [simplify]: Extracting #5: cost 2 inf + 115428
8.967 * * [simplify]: Extracting #6: cost 0 inf + 119672
8.971 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
8.971 * [simplify]: Simplified (2 2 1 1 1) to (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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)))
8.971 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
8.971 * * [simplify]: iters left: 2 (6 enodes)
8.973 * * [simplify]: iters left: 1 (14 enodes)
8.977 * * [simplify]: Extracting #0: cost 1 inf + 0
8.977 * * [simplify]: Extracting #1: cost 3 inf + 0
8.977 * * [simplify]: Extracting #2: cost 6 inf + 0
8.977 * * [simplify]: Extracting #3: cost 2 inf + 325
8.977 * * [simplify]: Extracting #4: cost 0 inf + 1329
8.977 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
8.977 * [simplify]: Simplified (2 2 1 1 2) to (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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)))
8.977 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))>
8.978 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
8.978 * * [simplify]: iters left: 5 (12 enodes)
8.984 * * [simplify]: iters left: 4 (35 enodes)
8.996 * * [simplify]: iters left: 3 (72 enodes)
9.024 * * [simplify]: iters left: 2 (233 enodes)
9.133 * * [simplify]: Extracting #0: cost 1 inf + 0
9.133 * * [simplify]: Extracting #1: cost 33 inf + 0
9.134 * * [simplify]: Extracting #2: cost 124 inf + 1
9.134 * * [simplify]: Extracting #3: cost 177 inf + 647
9.135 * * [simplify]: Extracting #4: cost 237 inf + 8960
9.139 * * [simplify]: Extracting #5: cost 207 inf + 111857
9.152 * * [simplify]: Extracting #6: cost 86 inf + 364602
9.173 * * [simplify]: Extracting #7: cost 3 inf + 484448
9.193 * * [simplify]: Extracting #8: cost 0 inf + 491015
9.227 * [simplify]: Simplified to (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
9.227 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
9.227 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))>
9.227 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
9.227 * * [simplify]: iters left: 5 (12 enodes)
9.232 * * [simplify]: iters left: 4 (35 enodes)
9.243 * * [simplify]: iters left: 3 (72 enodes)
9.266 * * [simplify]: iters left: 2 (233 enodes)
9.374 * * [simplify]: Extracting #0: cost 1 inf + 0
9.374 * * [simplify]: Extracting #1: cost 33 inf + 0
9.375 * * [simplify]: Extracting #2: cost 124 inf + 1
9.376 * * [simplify]: Extracting #3: cost 177 inf + 647
9.378 * * [simplify]: Extracting #4: cost 237 inf + 8960
9.385 * * [simplify]: Extracting #5: cost 207 inf + 111857
9.411 * * [simplify]: Extracting #6: cost 86 inf + 364602
9.446 * * [simplify]: Extracting #7: cost 3 inf + 484448
9.486 * * [simplify]: Extracting #8: cost 0 inf + 491015
9.522 * [simplify]: Simplified to (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
9.523 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
9.523 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))>
9.523 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
9.523 * * [simplify]: iters left: 5 (12 enodes)
9.526 * * [simplify]: iters left: 4 (35 enodes)
9.532 * * [simplify]: iters left: 3 (72 enodes)
9.546 * * [simplify]: iters left: 2 (233 enodes)
9.615 * * [simplify]: Extracting #0: cost 1 inf + 0
9.615 * * [simplify]: Extracting #1: cost 33 inf + 0
9.616 * * [simplify]: Extracting #2: cost 124 inf + 1
9.616 * * [simplify]: Extracting #3: cost 177 inf + 647
9.617 * * [simplify]: Extracting #4: cost 237 inf + 8960
9.621 * * [simplify]: Extracting #5: cost 207 inf + 111857
9.643 * * [simplify]: Extracting #6: cost 86 inf + 364602
9.674 * * [simplify]: Extracting #7: cost 3 inf + 484448
9.693 * * [simplify]: Extracting #8: cost 0 inf + 491015
9.716 * [simplify]: Simplified to (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
9.716 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
9.716 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))>
9.717 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
9.717 * * [simplify]: iters left: 5 (12 enodes)
9.724 * * [simplify]: iters left: 4 (35 enodes)
9.737 * * [simplify]: iters left: 3 (72 enodes)
9.765 * * [simplify]: iters left: 2 (233 enodes)
9.868 * * [simplify]: Extracting #0: cost 1 inf + 0
9.868 * * [simplify]: Extracting #1: cost 33 inf + 0
9.869 * * [simplify]: Extracting #2: cost 124 inf + 1
9.869 * * [simplify]: Extracting #3: cost 177 inf + 647
9.870 * * [simplify]: Extracting #4: cost 237 inf + 8960
9.880 * * [simplify]: Extracting #5: cost 207 inf + 111857
9.905 * * [simplify]: Extracting #6: cost 86 inf + 364602
9.940 * * [simplify]: Extracting #7: cost 3 inf + 484448
9.974 * * [simplify]: Extracting #8: cost 0 inf + 491015
10.008 * [simplify]: Simplified to (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
10.008 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
10.008 * * * [progress]: adding candidates to table
10.288 * [progress]: [Phase 3 of 3] Extracting.
10.288 * * [regime]: Finding splitpoints for: (#<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)))) (+.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 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)))> #<alt (λ (a b_2 c) (*.p16 (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.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)))))> #<alt (λ (a b_2 c) (*.p16 (/.p16 (*.p16 a c) (*.p16 a (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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 (real->posit16 1.0) 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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (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))))> #<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 (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)))))))> #<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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
10.292 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
10.292 * * * * [regimes]: Trying to branch on c from (#<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)))) (+.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 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)))> #<alt (λ (a b_2 c) (*.p16 (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.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)))))> #<alt (λ (a b_2 c) (*.p16 (/.p16 (*.p16 a c) (*.p16 a (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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 (real->posit16 1.0) 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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (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))))> #<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 (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)))))))> #<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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
10.539 * * * * [regimes]: Trying to branch on a from (#<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)))) (+.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 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)))> #<alt (λ (a b_2 c) (*.p16 (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.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)))))> #<alt (λ (a b_2 c) (*.p16 (/.p16 (*.p16 a c) (*.p16 a (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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 (real->posit16 1.0) 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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (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))))> #<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 (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)))))))> #<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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
10.710 * * * * [regimes]: Trying to branch on b_2 from (#<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)))) (+.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 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)))> #<alt (λ (a b_2 c) (*.p16 (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.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)))))> #<alt (λ (a b_2 c) (*.p16 (/.p16 (*.p16 a c) (*.p16 a (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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 (real->posit16 1.0) 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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (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))))> #<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 (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)))))))> #<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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
10.940 * * * [regime]: Found split indices: #<option (#s(si 1 114) #s(si 8 256))>
10.942 * [binary-search]: Improving bounds with binary search for b_2 and (#<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)))) (+.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 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)))> #<alt (λ (a b_2 c) (*.p16 (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.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)))))> #<alt (λ (a b_2 c) (*.p16 (/.p16 (*.p16 a c) (*.p16 a (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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 (real->posit16 1.0) 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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (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))))> #<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 (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)))))))> #<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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
10.942 * [regimes]: Found splitpoints: (#s(sp 1 b_2 #<cpointer:posit16>) #s(sp 8 b_2 +nan.0)) , with alts (#<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)))) (+.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 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)))> #<alt (λ (a b_2 c) (*.p16 (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (/.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)))))> #<alt (λ (a b_2 c) (*.p16 (/.p16 (*.p16 a c) (*.p16 a (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))> #<alt (λ (a b_2 c) (/.p16 (*.p16 (real->posit16 1.0) c) (-.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 (real->posit16 1.0) 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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (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))))> #<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 (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)))))))> #<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)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
10.943 * [simplify]: Simplifying (if (<=.p16 b_2 (real->posit16 -0.07232666015625)) (/.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))
10.943 * * [simplify]: iters left: 6 (22 enodes)
10.945 * * [simplify]: Extracting #0: cost 1 inf + 0
10.945 * * [simplify]: Extracting #1: cost 4 inf + 0
10.945 * * [simplify]: Extracting #2: cost 10 inf + 0
10.945 * * [simplify]: Extracting #3: cost 14 inf + 2
10.945 * * [simplify]: Extracting #4: cost 11 inf + 87
10.945 * * [simplify]: Extracting #5: cost 12 inf + 155
10.945 * * [simplify]: Extracting #6: cost 11 inf + 798
10.945 * * [simplify]: Extracting #7: cost 8 inf + 2606
10.945 * * [simplify]: Extracting #8: cost 4 inf + 6378
10.945 * * [simplify]: Extracting #9: cost 2 inf + 8504
10.946 * * [simplify]: Extracting #10: cost 1 inf + 10228
10.946 * * [simplify]: Extracting #11: cost 0 inf + 13123
10.946 * [simplify]: Simplified to (if (<=.p16 b_2 (real->posit16 -0.07232666015625)) (/.p16 (real->posit16 1.0) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))
10.946 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
10.985 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
10.986 * * * * [points]: Setting MPFR precision to 64
10.988 * * * * [points]: Setting MPFR precision to 320
10.989 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
10.990 * * * * [points]: Setting MPFR precision to 64
10.992 * * * * [points]: Setting MPFR precision to 320
10.994 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
10.996 * * * * [points]: Setting MPFR precision to 64
11.000 * * * * [points]: Setting MPFR precision to 320
11.008 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
11.010 * * * * [points]: Setting MPFR precision to 64
11.020 * * * * [points]: Setting MPFR precision to 320
11.029 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
11.030 * * * * [points]: Setting MPFR precision to 64
11.046 * * * * [points]: Setting MPFR precision to 320
11.068 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
11.070 * * * * [points]: Setting MPFR precision to 64
11.162 * * * * [points]: Setting MPFR precision to 320
11.219 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
11.221 * * * * [points]: Setting MPFR precision to 64
11.338 * * * * [points]: Setting MPFR precision to 320
11.423 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
11.424 * * * * [points]: Setting MPFR precision to 64
11.605 * * * * [points]: Setting MPFR precision to 320
11.804 * * * * [points]: Computing exacts for 8000 points
11.805 * * * * [points]: Setting MPFR precision to 64
12.809 * * * * [points]: Setting MPFR precision to 320
14.226 * * * * [points]: Filtering points with unrepresentable outputs
14.269 * * * * [points]: Sampled 8000 points with exact outputs
20.218 * [regime-testing]: Baseline error score: 64.0
20.222 * [regime-testing]: Oracle error score: 64.0
20.229 * [regime-testing]: End program error score: 0.4271652250923291