0.003 * [progress]: [Phase 1 of 3] Setting up.
0.005 * * * [progress]: [1/2] Preparing points
0.007 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.010 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.118 * * * * [points]: Setting MPFR precision to 64
0.122 * * * * [points]: Setting MPFR precision to 320
0.124 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.126 * * * * [points]: Setting MPFR precision to 64
0.129 * * * * [points]: Setting MPFR precision to 320
0.132 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.134 * * * * [points]: Setting MPFR precision to 64
0.139 * * * * [points]: Setting MPFR precision to 320
0.144 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.145 * * * * [points]: Setting MPFR precision to 64
0.154 * * * * [points]: Setting MPFR precision to 320
0.162 * * * * [points]: Computing exacts for 256 points
0.164 * * * * [points]: Setting MPFR precision to 64
0.189 * * * * [points]: Setting MPFR precision to 320
0.214 * * * * [points]: Filtering points with unrepresentable outputs
0.216 * * * * [points]: Sampled 256 points with exact outputs
0.216 * * * [progress]: [2/2] Setting up program.
0.233 * [progress]: [Phase 2 of 3] Improving.
0.233 * * * * [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.235 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.236 * * [simplify]: iters left: 5 (10 enodes)
0.244 * * [simplify]: iters left: 4 (31 enodes)
0.254 * * [simplify]: iters left: 3 (65 enodes)
0.275 * * [simplify]: iters left: 2 (207 enodes)
0.422 * * [simplify]: Extracting #0: cost 1 inf + 0
0.422 * * [simplify]: Extracting #1: cost 20 inf + 0
0.423 * * [simplify]: Extracting #2: cost 88 inf + 1
0.424 * * [simplify]: Extracting #3: cost 167 inf + 83
0.426 * * [simplify]: Extracting #4: cost 224 inf + 14445
0.433 * * [simplify]: Extracting #5: cost 183 inf + 98116
0.463 * * [simplify]: Extracting #6: cost 60 inf + 344757
0.479 * * [simplify]: Extracting #7: cost 1 inf + 432442
0.508 * * [simplify]: Extracting #8: cost 0 inf + 435725
0.535 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
0.535 * [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.548 * * [progress]: iteration 1 / 4
0.548 * * * [progress]: picking best candidate
0.557 * * * * [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.557 * * * [progress]: localizing error
0.697 * * * [progress]: generating rewritten candidates
0.697 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.700 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
0.700 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 1)
0.703 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
0.706 * * * [progress]: generating series expansions
0.706 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.707 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
0.707 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 1)
0.707 * * * * [progress]: [ 4 / 4 ] generating series at (2)
0.707 * * * [progress]: simplifying candidates
0.707 * * * * [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.707 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
0.707 * * [simplify]: iters left: 4 (8 enodes)
0.709 * * [simplify]: iters left: 3 (22 enodes)
0.722 * * [simplify]: iters left: 2 (44 enodes)
0.731 * * [simplify]: iters left: 1 (99 enodes)
0.757 * * [simplify]: Extracting #0: cost 1 inf + 0
0.758 * * [simplify]: Extracting #1: cost 2 inf + 0
0.758 * * [simplify]: Extracting #2: cost 3 inf + 0
0.758 * * [simplify]: Extracting #3: cost 17 inf + 0
0.758 * * [simplify]: Extracting #4: cost 57 inf + 0
0.759 * * [simplify]: Extracting #5: cost 89 inf + 1048
0.761 * * [simplify]: Extracting #6: cost 73 inf + 56606
0.771 * * [simplify]: Extracting #7: cost 0 inf + 174728
0.782 * * [simplify]: Extracting #8: cost 0 inf + 172968
0.793 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))
0.793 * [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.793 * * * * [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.793 * [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.794 * * [simplify]: iters left: 5 (11 enodes)
0.798 * * [simplify]: iters left: 4 (35 enodes)
0.811 * * [simplify]: iters left: 3 (100 enodes)
0.851 * * [simplify]: iters left: 2 (359 enodes)
1.048 * * [simplify]: Extracting #0: cost 1 inf + 0
1.048 * * [simplify]: Extracting #1: cost 48 inf + 0
1.049 * * [simplify]: Extracting #2: cost 218 inf + 0
1.051 * * [simplify]: Extracting #3: cost 322 inf + 45040
1.065 * * [simplify]: Extracting #4: cost 299 inf + 342038
1.115 * * [simplify]: Extracting #5: cost 86 inf + 819696
1.180 * * [simplify]: Extracting #6: cost 1 inf + 958399
1.228 * * [simplify]: Extracting #7: cost 0 inf + 960402
1.275 * [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.275 * [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.275 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1.275 * * [simplify]: iters left: 4 (9 enodes)
1.277 * * [simplify]: iters left: 3 (24 enodes)
1.281 * * [simplify]: iters left: 2 (47 enodes)
1.289 * * [simplify]: iters left: 1 (110 enodes)
1.342 * * [simplify]: Extracting #0: cost 1 inf + 0
1.342 * * [simplify]: Extracting #1: cost 6 inf + 0
1.343 * * [simplify]: Extracting #2: cost 10 inf + 1
1.343 * * [simplify]: Extracting #3: cost 23 inf + 403
1.343 * * [simplify]: Extracting #4: cost 60 inf + 1445
1.344 * * [simplify]: Extracting #5: cost 79 inf + 12440
1.347 * * [simplify]: Extracting #6: cost 76 inf + 55663
1.353 * * [simplify]: Extracting #7: cost 8 inf + 160807
1.359 * * [simplify]: Extracting #8: cost 0 inf + 177990
1.364 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1.364 * [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.364 * * * * [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.365 * [simplify]: Simplifying (neg.p16 (*.p16 a c))
1.365 * * [simplify]: iters left: 2 (4 enodes)
1.365 * * [simplify]: iters left: 1 (9 enodes)
1.367 * * [simplify]: Extracting #0: cost 1 inf + 0
1.367 * * [simplify]: Extracting #1: cost 2 inf + 0
1.367 * * [simplify]: Extracting #2: cost 4 inf + 0
1.367 * * [simplify]: Extracting #3: cost 2 inf + 2
1.367 * * [simplify]: Extracting #4: cost 0 inf + 726
1.367 * [simplify]: Simplified to (neg.p16 (*.p16 c a))
1.367 * [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.367 * * * * [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.367 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c)))
1.367 * * [simplify]: iters left: 3 (8 enodes)
1.369 * * [simplify]: iters left: 2 (33 enodes)
1.375 * * [simplify]: iters left: 1 (79 enodes)
1.399 * * [simplify]: Extracting #0: cost 1 inf + 0
1.399 * * [simplify]: Extracting #1: cost 21 inf + 0
1.399 * * [simplify]: Extracting #2: cost 51 inf + 0
1.399 * * [simplify]: Extracting #3: cost 76 inf + 5301
1.401 * * [simplify]: Extracting #4: cost 36 inf + 63309
1.404 * * [simplify]: Extracting #5: cost 2 inf + 115428
1.408 * * [simplify]: Extracting #6: cost 0 inf + 119672
1.412 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
1.412 * [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.412 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
1.412 * * [simplify]: iters left: 2 (6 enodes)
1.413 * * [simplify]: iters left: 1 (14 enodes)
1.415 * * [simplify]: Extracting #0: cost 1 inf + 0
1.415 * * [simplify]: Extracting #1: cost 3 inf + 0
1.415 * * [simplify]: Extracting #2: cost 6 inf + 0
1.415 * * [simplify]: Extracting #3: cost 2 inf + 325
1.415 * * [simplify]: Extracting #4: cost 0 inf + 1329
1.415 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
1.415 * [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.415 * * * * [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.416 * [simplify]: Simplifying (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1.416 * * [simplify]: iters left: 5 (10 enodes)
1.419 * * [simplify]: iters left: 4 (32 enodes)
1.424 * * [simplify]: iters left: 3 (57 enodes)
1.441 * * [simplify]: iters left: 2 (124 enodes)
1.477 * * [simplify]: iters left: 1 (429 enodes)
1.825 * * [simplify]: Extracting #0: cost 1 inf + 0
1.826 * * [simplify]: Extracting #1: cost 10 inf + 0
1.826 * * [simplify]: Extracting #2: cost 34 inf + 1
1.826 * * [simplify]: Extracting #3: cost 92 inf + 2
1.828 * * [simplify]: Extracting #4: cost 331 inf + 404
1.833 * * [simplify]: Extracting #5: cost 487 inf + 33943
1.866 * * [simplify]: Extracting #6: cost 335 inf + 481558
1.939 * * [simplify]: Extracting #7: cost 29 inf + 1060457
2.011 * * [simplify]: Extracting #8: cost 0 inf + 1120774
2.073 * [simplify]: Simplified to (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
2.073 * [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.073 * * * * [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.074 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.074 * * [simplify]: iters left: 5 (10 enodes)
2.078 * * [simplify]: iters left: 4 (31 enodes)
2.090 * * [simplify]: iters left: 3 (65 enodes)
2.110 * * [simplify]: iters left: 2 (207 enodes)
2.190 * * [simplify]: Extracting #0: cost 1 inf + 0
2.190 * * [simplify]: Extracting #1: cost 20 inf + 0
2.190 * * [simplify]: Extracting #2: cost 88 inf + 1
2.191 * * [simplify]: Extracting #3: cost 167 inf + 83
2.193 * * [simplify]: Extracting #4: cost 224 inf + 14445
2.199 * * [simplify]: Extracting #5: cost 183 inf + 98116
2.218 * * [simplify]: Extracting #6: cost 60 inf + 344757
2.234 * * [simplify]: Extracting #7: cost 1 inf + 432442
2.255 * * [simplify]: Extracting #8: cost 0 inf + 435725
2.284 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.285 * [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.285 * * * * [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.285 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.285 * * [simplify]: iters left: 5 (10 enodes)
2.289 * * [simplify]: iters left: 4 (31 enodes)
2.297 * * [simplify]: iters left: 3 (65 enodes)
2.310 * * [simplify]: iters left: 2 (207 enodes)
2.400 * * [simplify]: Extracting #0: cost 1 inf + 0
2.400 * * [simplify]: Extracting #1: cost 20 inf + 0
2.401 * * [simplify]: Extracting #2: cost 88 inf + 1
2.401 * * [simplify]: Extracting #3: cost 167 inf + 83
2.403 * * [simplify]: Extracting #4: cost 224 inf + 14445
2.410 * * [simplify]: Extracting #5: cost 183 inf + 98116
2.432 * * [simplify]: Extracting #6: cost 60 inf + 344757
2.465 * * [simplify]: Extracting #7: cost 1 inf + 432442
2.490 * * [simplify]: Extracting #8: cost 0 inf + 435725
2.507 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.507 * [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.507 * * * * [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.508 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.508 * * [simplify]: iters left: 5 (10 enodes)
2.510 * * [simplify]: iters left: 4 (31 enodes)
2.515 * * [simplify]: iters left: 3 (65 enodes)
2.529 * * [simplify]: iters left: 2 (207 enodes)
2.613 * * [simplify]: Extracting #0: cost 1 inf + 0
2.613 * * [simplify]: Extracting #1: cost 20 inf + 0
2.613 * * [simplify]: Extracting #2: cost 88 inf + 1
2.614 * * [simplify]: Extracting #3: cost 167 inf + 83
2.615 * * [simplify]: Extracting #4: cost 224 inf + 14445
2.618 * * [simplify]: Extracting #5: cost 183 inf + 98116
2.630 * * [simplify]: Extracting #6: cost 60 inf + 344757
2.646 * * [simplify]: Extracting #7: cost 1 inf + 432442
2.675 * * [simplify]: Extracting #8: cost 0 inf + 435725
2.709 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.709 * [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.709 * * * * [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.709 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
2.709 * * [simplify]: iters left: 5 (10 enodes)
2.714 * * [simplify]: iters left: 4 (31 enodes)
2.723 * * [simplify]: iters left: 3 (65 enodes)
2.737 * * [simplify]: iters left: 2 (207 enodes)
2.803 * * [simplify]: Extracting #0: cost 1 inf + 0
2.803 * * [simplify]: Extracting #1: cost 20 inf + 0
2.803 * * [simplify]: Extracting #2: cost 88 inf + 1
2.804 * * [simplify]: Extracting #3: cost 167 inf + 83
2.806 * * [simplify]: Extracting #4: cost 224 inf + 14445
2.810 * * [simplify]: Extracting #5: cost 183 inf + 98116
2.821 * * [simplify]: Extracting #6: cost 60 inf + 344757
2.837 * * [simplify]: Extracting #7: cost 1 inf + 432442
2.854 * * [simplify]: Extracting #8: cost 0 inf + 435725
2.873 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.873 * [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.873 * * * [progress]: adding candidates to table
3.047 * * [progress]: iteration 2 / 4
3.047 * * * [progress]: picking best candidate
3.090 * * * * [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.091 * * * [progress]: localizing error
3.363 * * * [progress]: generating rewritten candidates
3.363 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
3.366 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
3.369 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 2)
3.369 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2 1)
3.372 * * * [progress]: generating series expansions
3.372 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
3.372 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
3.372 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 2)
3.372 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2 1)
3.372 * * * [progress]: simplifying candidates
3.372 * * * * [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.372 * * * * [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.373 * [simplify]: Simplifying (neg.p16 (*.p16 a c))
3.373 * * [simplify]: iters left: 2 (4 enodes)
3.373 * * [simplify]: iters left: 1 (9 enodes)
3.375 * * [simplify]: Extracting #0: cost 1 inf + 0
3.375 * * [simplify]: Extracting #1: cost 2 inf + 0
3.375 * * [simplify]: Extracting #2: cost 4 inf + 0
3.375 * * [simplify]: Extracting #3: cost 2 inf + 2
3.375 * * [simplify]: Extracting #4: cost 0 inf + 726
3.375 * [simplify]: Simplified to (neg.p16 (*.p16 c a))
3.375 * [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.375 * * * * [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.375 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c)))
3.375 * * [simplify]: iters left: 3 (8 enodes)
3.377 * * [simplify]: iters left: 2 (33 enodes)
3.384 * * [simplify]: iters left: 1 (79 enodes)
3.417 * * [simplify]: Extracting #0: cost 1 inf + 0
3.417 * * [simplify]: Extracting #1: cost 21 inf + 0
3.418 * * [simplify]: Extracting #2: cost 51 inf + 0
3.418 * * [simplify]: Extracting #3: cost 76 inf + 5301
3.421 * * [simplify]: Extracting #4: cost 36 inf + 63309
3.432 * * [simplify]: Extracting #5: cost 2 inf + 115428
3.435 * * [simplify]: Extracting #6: cost 0 inf + 119672
3.439 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
3.439 * [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.439 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
3.439 * * [simplify]: iters left: 2 (6 enodes)
3.441 * * [simplify]: iters left: 1 (14 enodes)
3.443 * * [simplify]: Extracting #0: cost 1 inf + 0
3.443 * * [simplify]: Extracting #1: cost 3 inf + 0
3.443 * * [simplify]: Extracting #2: cost 6 inf + 0
3.443 * * [simplify]: Extracting #3: cost 2 inf + 325
3.443 * * [simplify]: Extracting #4: cost 0 inf + 1329
3.443 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
3.443 * [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.443 * * * * [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.443 * [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.443 * * [simplify]: iters left: 6 (15 enodes)
3.447 * * [simplify]: iters left: 5 (40 enodes)
3.456 * * [simplify]: iters left: 4 (102 enodes)
3.496 * * [simplify]: iters left: 3 (250 enodes)
3.623 * * [simplify]: Extracting #0: cost 1 inf + 0
3.623 * * [simplify]: Extracting #1: cost 9 inf + 0
3.624 * * [simplify]: Extracting #2: cost 37 inf + 1
3.624 * * [simplify]: Extracting #3: cost 88 inf + 846
3.626 * * [simplify]: Extracting #4: cost 90 inf + 23777
3.632 * * [simplify]: Extracting #5: cost 79 inf + 69187
3.642 * * [simplify]: Extracting #6: cost 55 inf + 142773
3.657 * * [simplify]: Extracting #7: cost 1 inf + 231486
3.674 * * [simplify]: Extracting #8: cost 0 inf + 234769
3.691 * [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.691 * [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.691 * * * * [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.691 * [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.692 * * [simplify]: iters left: 6 (15 enodes)
3.698 * * [simplify]: iters left: 5 (40 enodes)
3.707 * * [simplify]: iters left: 4 (102 enodes)
3.732 * * [simplify]: iters left: 3 (250 enodes)
3.916 * * [simplify]: Extracting #0: cost 1 inf + 0
3.916 * * [simplify]: Extracting #1: cost 9 inf + 0
3.916 * * [simplify]: Extracting #2: cost 37 inf + 1
3.916 * * [simplify]: Extracting #3: cost 88 inf + 846
3.918 * * [simplify]: Extracting #4: cost 90 inf + 23777
3.924 * * [simplify]: Extracting #5: cost 79 inf + 69187
3.932 * * [simplify]: Extracting #6: cost 55 inf + 142773
3.940 * * [simplify]: Extracting #7: cost 1 inf + 231486
3.948 * * [simplify]: Extracting #8: cost 0 inf + 234769
3.957 * [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.957 * [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.957 * * * * [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))>
3.957 * [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.957 * * [simplify]: iters left: 6 (15 enodes)
3.960 * * [simplify]: iters left: 5 (40 enodes)
3.972 * * [simplify]: iters left: 4 (102 enodes)
4.004 * * [simplify]: iters left: 3 (250 enodes)
4.130 * * [simplify]: Extracting #0: cost 1 inf + 0
4.130 * * [simplify]: Extracting #1: cost 9 inf + 0
4.131 * * [simplify]: Extracting #2: cost 37 inf + 1
4.131 * * [simplify]: Extracting #3: cost 88 inf + 846
4.132 * * [simplify]: Extracting #4: cost 90 inf + 23777
4.136 * * [simplify]: Extracting #5: cost 79 inf + 69187
4.144 * * [simplify]: Extracting #6: cost 55 inf + 142773
4.151 * * [simplify]: Extracting #7: cost 1 inf + 231486
4.160 * * [simplify]: Extracting #8: cost 0 inf + 234769
4.169 * [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.169 * [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.169 * * * * [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.170 * [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.170 * * [simplify]: iters left: 6 (15 enodes)
4.176 * * [simplify]: iters left: 5 (40 enodes)
4.190 * * [simplify]: iters left: 4 (102 enodes)
4.229 * * [simplify]: iters left: 3 (250 enodes)
4.395 * * [simplify]: Extracting #0: cost 1 inf + 0
4.395 * * [simplify]: Extracting #1: cost 9 inf + 0
4.395 * * [simplify]: Extracting #2: cost 37 inf + 1
4.396 * * [simplify]: Extracting #3: cost 88 inf + 846
4.398 * * [simplify]: Extracting #4: cost 90 inf + 23777
4.403 * * [simplify]: Extracting #5: cost 79 inf + 69187
4.417 * * [simplify]: Extracting #6: cost 55 inf + 142773
4.432 * * [simplify]: Extracting #7: cost 1 inf + 231486
4.449 * * [simplify]: Extracting #8: cost 0 inf + 234769
4.466 * [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.466 * [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.467 * * * [progress]: adding candidates to table
4.647 * * [progress]: iteration 3 / 4
4.647 * * * [progress]: picking best candidate
4.710 * * * * [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.710 * * * [progress]: localizing error
4.898 * * * [progress]: generating rewritten candidates
4.898 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
4.900 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
4.903 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 1)
4.904 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 1 1)
4.906 * * * [progress]: generating series expansions
4.906 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
4.907 * * * * [progress]: [ 2 / 4 ] generating series at (2)
4.907 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 1)
4.907 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 1 1)
4.907 * * * [progress]: simplifying candidates
4.907 * * * * [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)))))>
4.907 * [simplify]: Simplifying (neg.p16 b_2)
4.907 * * [simplify]: iters left: 1 (2 enodes)
4.907 * * [simplify]: Extracting #0: cost 1 inf + 0
4.907 * * [simplify]: Extracting #1: cost 2 inf + 0
4.907 * * [simplify]: Extracting #2: cost 1 inf + 1
4.907 * * [simplify]: Extracting #3: cost 0 inf + 82
4.907 * [simplify]: Simplified to (neg.p16 b_2)
4.907 * [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)))))
4.907 * * * * [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)))))>
4.908 * [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))
4.908 * * [simplify]: iters left: 5 (9 enodes)
4.910 * * [simplify]: iters left: 4 (32 enodes)
4.915 * * [simplify]: iters left: 3 (94 enodes)
4.942 * * [simplify]: iters left: 2 (334 enodes)
5.149 * * [simplify]: Extracting #0: cost 1 inf + 0
5.149 * * [simplify]: Extracting #1: cost 45 inf + 0
5.150 * * [simplify]: Extracting #2: cost 220 inf + 0
5.155 * * [simplify]: Extracting #3: cost 326 inf + 50072
5.180 * * [simplify]: Extracting #4: cost 236 inf + 362547
5.238 * * [simplify]: Extracting #5: cost 59 inf + 750749
5.315 * * [simplify]: Extracting #6: cost 1 inf + 849495
5.379 * * [simplify]: Extracting #7: cost 0 inf + 852778
5.418 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
5.419 * [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.419 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.419 * * [simplify]: iters left: 4 (8 enodes)
5.420 * * [simplify]: iters left: 3 (23 enodes)
5.424 * * [simplify]: iters left: 2 (45 enodes)
5.432 * * [simplify]: iters left: 1 (108 enodes)
5.459 * * [simplify]: Extracting #0: cost 1 inf + 0
5.459 * * [simplify]: Extracting #1: cost 3 inf + 0
5.459 * * [simplify]: Extracting #2: cost 3 inf + 1
5.459 * * [simplify]: Extracting #3: cost 17 inf + 1
5.459 * * [simplify]: Extracting #4: cost 55 inf + 322
5.459 * * [simplify]: Extracting #5: cost 78 inf + 10074
5.462 * * [simplify]: Extracting #6: cost 74 inf + 71480
5.467 * * [simplify]: Extracting #7: cost 3 inf + 182984
5.473 * * [simplify]: Extracting #8: cost 0 inf + 190232
5.488 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.488 * [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.488 * * * * [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.489 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) a)
5.489 * * [simplify]: iters left: 3 (7 enodes)
5.492 * * [simplify]: iters left: 2 (14 enodes)
5.497 * * [simplify]: iters left: 1 (23 enodes)
5.505 * * [simplify]: Extracting #0: cost 1 inf + 0
5.505 * * [simplify]: Extracting #1: cost 7 inf + 0
5.505 * * [simplify]: Extracting #2: cost 6 inf + 443
5.505 * * [simplify]: Extracting #3: cost 2 inf + 2412
5.505 * * [simplify]: Extracting #4: cost 0 inf + 1534
5.506 * [simplify]: Simplified to (*.p16 (real->posit16 1.0) c)
5.506 * [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.506 * * * * [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.506 * [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.506 * * [simplify]: iters left: 6 (14 enodes)
5.513 * * [simplify]: iters left: 5 (42 enodes)
5.528 * * [simplify]: iters left: 4 (159 enodes)
5.587 * * [simplify]: Extracting #0: cost 1 inf + 0
5.587 * * [simplify]: Extracting #1: cost 39 inf + 0
5.588 * * [simplify]: Extracting #2: cost 117 inf + 766
5.588 * * [simplify]: Extracting #3: cost 199 inf + 3540
5.589 * * [simplify]: Extracting #4: cost 232 inf + 5390
5.592 * * [simplify]: Extracting #5: cost 157 inf + 82593
5.599 * * [simplify]: Extracting #6: cost 49 inf + 221831
5.612 * * [simplify]: Extracting #7: cost 3 inf + 284472
5.634 * * [simplify]: Extracting #8: cost 0 inf + 291241
5.655 * [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.655 * [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.656 * * * * [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.656 * [simplify]: Simplifying (neg.p16 (*.p16 c a))
5.656 * * [simplify]: iters left: 2 (4 enodes)
5.658 * * [simplify]: iters left: 1 (9 enodes)
5.660 * * [simplify]: Extracting #0: cost 1 inf + 0
5.660 * * [simplify]: Extracting #1: cost 2 inf + 0
5.660 * * [simplify]: Extracting #2: cost 4 inf + 0
5.660 * * [simplify]: Extracting #3: cost 2 inf + 2
5.660 * * [simplify]: Extracting #4: cost 0 inf + 726
5.660 * [simplify]: Simplified to (neg.p16 (*.p16 a c))
5.660 * [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.660 * * * * [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.661 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
5.661 * * [simplify]: iters left: 3 (8 enodes)
5.665 * * [simplify]: iters left: 2 (33 enodes)
5.679 * * [simplify]: iters left: 1 (79 enodes)
5.713 * * [simplify]: Extracting #0: cost 1 inf + 0
5.713 * * [simplify]: Extracting #1: cost 21 inf + 0
5.713 * * [simplify]: Extracting #2: cost 51 inf + 0
5.714 * * [simplify]: Extracting #3: cost 76 inf + 5301
5.717 * * [simplify]: Extracting #4: cost 36 inf + 63309
5.724 * * [simplify]: Extracting #5: cost 2 inf + 115428
5.728 * * [simplify]: Extracting #6: cost 0 inf + 119672
5.732 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
5.732 * [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.733 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
5.733 * * [simplify]: iters left: 2 (6 enodes)
5.734 * * [simplify]: iters left: 1 (14 enodes)
5.736 * * [simplify]: Extracting #0: cost 1 inf + 0
5.736 * * [simplify]: Extracting #1: cost 3 inf + 0
5.736 * * [simplify]: Extracting #2: cost 6 inf + 0
5.736 * * [simplify]: Extracting #3: cost 2 inf + 325
5.736 * * [simplify]: Extracting #4: cost 0 inf + 1329
5.736 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
5.736 * [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.736 * * * * [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.736 * [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.736 * * [simplify]: iters left: 6 (13 enodes)
5.739 * * [simplify]: iters left: 5 (38 enodes)
5.746 * * [simplify]: iters left: 4 (125 enodes)
5.790 * * [simplify]: Extracting #0: cost 1 inf + 0
5.790 * * [simplify]: Extracting #1: cost 32 inf + 0
5.790 * * [simplify]: Extracting #2: cost 72 inf + 1528
5.791 * * [simplify]: Extracting #3: cost 125 inf + 3822
5.792 * * [simplify]: Extracting #4: cost 115 inf + 29783
5.795 * * [simplify]: Extracting #5: cost 48 inf + 113802
5.801 * * [simplify]: Extracting #6: cost 27 inf + 153800
5.808 * * [simplify]: Extracting #7: cost 0 inf + 178777
5.814 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
5.814 * [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))))
5.814 * * * * [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))))>
5.814 * [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.814 * * [simplify]: iters left: 6 (13 enodes)
5.817 * * [simplify]: iters left: 5 (38 enodes)
5.825 * * [simplify]: iters left: 4 (125 enodes)
5.878 * * [simplify]: Extracting #0: cost 1 inf + 0
5.878 * * [simplify]: Extracting #1: cost 32 inf + 0
5.879 * * [simplify]: Extracting #2: cost 72 inf + 1528
5.879 * * [simplify]: Extracting #3: cost 125 inf + 3822
5.882 * * [simplify]: Extracting #4: cost 115 inf + 29783
5.889 * * [simplify]: Extracting #5: cost 48 inf + 113802
5.900 * * [simplify]: Extracting #6: cost 27 inf + 153800
5.914 * * [simplify]: Extracting #7: cost 0 inf + 178777
5.926 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
5.926 * [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))))
5.926 * * * * [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))))>
5.927 * [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.927 * * [simplify]: iters left: 6 (13 enodes)
5.932 * * [simplify]: iters left: 5 (38 enodes)
5.949 * * [simplify]: iters left: 4 (125 enodes)
6.027 * * [simplify]: Extracting #0: cost 1 inf + 0
6.027 * * [simplify]: Extracting #1: cost 32 inf + 0
6.027 * * [simplify]: Extracting #2: cost 72 inf + 1528
6.028 * * [simplify]: Extracting #3: cost 125 inf + 3822
6.029 * * [simplify]: Extracting #4: cost 115 inf + 29783
6.033 * * [simplify]: Extracting #5: cost 48 inf + 113802
6.038 * * [simplify]: Extracting #6: cost 27 inf + 153800
6.044 * * [simplify]: Extracting #7: cost 0 inf + 178777
6.055 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
6.056 * [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.056 * * * * [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.056 * [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.056 * * [simplify]: iters left: 6 (13 enodes)
6.062 * * [simplify]: iters left: 5 (38 enodes)
6.076 * * [simplify]: iters left: 4 (125 enodes)
6.134 * * [simplify]: Extracting #0: cost 1 inf + 0
6.134 * * [simplify]: Extracting #1: cost 32 inf + 0
6.134 * * [simplify]: Extracting #2: cost 72 inf + 1528
6.135 * * [simplify]: Extracting #3: cost 125 inf + 3822
6.136 * * [simplify]: Extracting #4: cost 115 inf + 29783
6.141 * * [simplify]: Extracting #5: cost 48 inf + 113802
6.147 * * [simplify]: Extracting #6: cost 27 inf + 153800
6.153 * * [simplify]: Extracting #7: cost 0 inf + 178777
6.159 * [simplify]: Simplified to (/.p16 (*.p16 a c) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
6.159 * [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.160 * * * [progress]: adding candidates to table
6.400 * * [progress]: iteration 4 / 4
6.400 * * * [progress]: picking best candidate
6.473 * * * * [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.473 * * * [progress]: localizing error
6.621 * * * [progress]: generating rewritten candidates
6.621 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2)
6.623 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2 1)
6.623 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
6.626 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1 1)
6.636 * * * [progress]: generating series expansions
6.636 * * * * [progress]: [ 1 / 4 ] generating series at (2 2)
6.636 * * * * [progress]: [ 2 / 4 ] generating series at (2 2 1)
6.636 * * * * [progress]: [ 3 / 4 ] generating series at (2)
6.637 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1 1)
6.637 * * * [progress]: simplifying candidates
6.637 * * * * [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))))>
6.637 * [simplify]: Simplifying (neg.p16 b_2)
6.637 * * [simplify]: iters left: 1 (2 enodes)
6.637 * * [simplify]: Extracting #0: cost 1 inf + 0
6.637 * * [simplify]: Extracting #1: cost 2 inf + 0
6.637 * * [simplify]: Extracting #2: cost 1 inf + 1
6.637 * * [simplify]: Extracting #3: cost 0 inf + 82
6.637 * [simplify]: Simplified to (neg.p16 b_2)
6.637 * [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))))
6.637 * * * * [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))))>
6.638 * [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))
6.638 * * [simplify]: iters left: 5 (9 enodes)
6.639 * * [simplify]: iters left: 4 (32 enodes)
6.645 * * [simplify]: iters left: 3 (94 enodes)
6.665 * * [simplify]: iters left: 2 (334 enodes)
6.857 * * [simplify]: Extracting #0: cost 1 inf + 0
6.857 * * [simplify]: Extracting #1: cost 45 inf + 0
6.857 * * [simplify]: Extracting #2: cost 220 inf + 0
6.860 * * [simplify]: Extracting #3: cost 326 inf + 50072
6.873 * * [simplify]: Extracting #4: cost 236 inf + 362547
6.911 * * [simplify]: Extracting #5: cost 59 inf + 750749
6.967 * * [simplify]: Extracting #6: cost 1 inf + 849495
7.371 * * [simplify]: Extracting #7: cost 0 inf + 852778
7.409 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
7.409 * [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.409 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.409 * * [simplify]: iters left: 4 (8 enodes)
7.411 * * [simplify]: iters left: 3 (23 enodes)
7.414 * * [simplify]: iters left: 2 (45 enodes)
7.423 * * [simplify]: iters left: 1 (108 enodes)
7.478 * * [simplify]: Extracting #0: cost 1 inf + 0
7.478 * * [simplify]: Extracting #1: cost 3 inf + 0
7.478 * * [simplify]: Extracting #2: cost 3 inf + 1
7.478 * * [simplify]: Extracting #3: cost 17 inf + 1
7.478 * * [simplify]: Extracting #4: cost 55 inf + 322
7.479 * * [simplify]: Extracting #5: cost 78 inf + 10074
7.481 * * [simplify]: Extracting #6: cost 74 inf + 71480
7.486 * * [simplify]: Extracting #7: cost 3 inf + 182984
7.492 * * [simplify]: Extracting #8: cost 0 inf + 190232
7.499 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
7.499 * [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)))))))
7.499 * * * * [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)))>
7.499 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) c)
7.499 * * [simplify]: iters left: 5 (9 enodes)
7.501 * * [simplify]: iters left: 4 (29 enodes)
7.506 * * [simplify]: iters left: 3 (62 enodes)
7.518 * * [simplify]: iters left: 2 (200 enodes)
7.601 * * [simplify]: Extracting #0: cost 1 inf + 0
7.601 * * [simplify]: Extracting #1: cost 20 inf + 0
7.602 * * [simplify]: Extracting #2: cost 94 inf + 1
7.603 * * [simplify]: Extracting #3: cost 162 inf + 1046
7.605 * * [simplify]: Extracting #4: cost 211 inf + 16816
7.612 * * [simplify]: Extracting #5: cost 170 inf + 107511
7.633 * * [simplify]: Extracting #6: cost 69 inf + 300802
7.663 * * [simplify]: Extracting #7: cost 1 inf + 411568
7.698 * * [simplify]: Extracting #8: cost 0 inf + 414291
7.726 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) c)
7.726 * [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)))
7.726 * * * * [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)))>
7.726 * [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)))
7.726 * * [simplify]: iters left: 6 (13 enodes)
7.729 * * [simplify]: iters left: 5 (39 enodes)
7.737 * * [simplify]: iters left: 4 (111 enodes)
7.761 * * [simplify]: iters left: 3 (397 enodes)
7.972 * * [simplify]: Extracting #0: cost 1 inf + 0
7.972 * * [simplify]: Extracting #1: cost 49 inf + 0
7.973 * * [simplify]: Extracting #2: cost 229 inf + 1
7.975 * * [simplify]: Extracting #3: cost 370 inf + 3856
7.986 * * [simplify]: Extracting #4: cost 437 inf + 164665
8.022 * * [simplify]: Extracting #5: cost 164 inf + 726884
8.083 * * [simplify]: Extracting #6: cost 38 inf + 1005389
8.134 * * [simplify]: Extracting #7: cost 1 inf + 1064551
8.184 * * [simplify]: Extracting #8: cost 0 inf + 1067834
8.230 * [simplify]: Simplified to (/.p16 c (-.p16 (real->posit16 0.0) (*.p16 a c)))
8.230 * [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.230 * * * * [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.230 * [simplify]: Simplifying (neg.p16 (*.p16 c a))
8.230 * * [simplify]: iters left: 2 (4 enodes)
8.231 * * [simplify]: iters left: 1 (9 enodes)
8.232 * * [simplify]: Extracting #0: cost 1 inf + 0
8.232 * * [simplify]: Extracting #1: cost 2 inf + 0
8.232 * * [simplify]: Extracting #2: cost 4 inf + 0
8.232 * * [simplify]: Extracting #3: cost 2 inf + 2
8.232 * * [simplify]: Extracting #4: cost 0 inf + 726
8.232 * [simplify]: Simplified to (neg.p16 (*.p16 a c))
8.232 * [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.232 * * * * [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.233 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
8.233 * * [simplify]: iters left: 3 (8 enodes)
8.235 * * [simplify]: iters left: 2 (33 enodes)
8.240 * * [simplify]: iters left: 1 (79 enodes)
8.258 * * [simplify]: Extracting #0: cost 1 inf + 0
8.258 * * [simplify]: Extracting #1: cost 21 inf + 0
8.258 * * [simplify]: Extracting #2: cost 51 inf + 0
8.258 * * [simplify]: Extracting #3: cost 76 inf + 5301
8.260 * * [simplify]: Extracting #4: cost 36 inf + 63309
8.263 * * [simplify]: Extracting #5: cost 2 inf + 115428
8.267 * * [simplify]: Extracting #6: cost 0 inf + 119672
8.272 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
8.272 * [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.273 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
8.273 * * [simplify]: iters left: 2 (6 enodes)
8.275 * * [simplify]: iters left: 1 (14 enodes)
8.279 * * [simplify]: Extracting #0: cost 1 inf + 0
8.279 * * [simplify]: Extracting #1: cost 3 inf + 0
8.279 * * [simplify]: Extracting #2: cost 6 inf + 0
8.279 * * [simplify]: Extracting #3: cost 2 inf + 325
8.279 * * [simplify]: Extracting #4: cost 0 inf + 1329
8.279 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
8.279 * [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.279 * * * * [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.280 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
8.280 * * [simplify]: iters left: 5 (12 enodes)
8.285 * * [simplify]: iters left: 4 (35 enodes)
8.297 * * [simplify]: iters left: 3 (72 enodes)
8.313 * * [simplify]: iters left: 2 (233 enodes)
8.386 * * [simplify]: Extracting #0: cost 1 inf + 0
8.386 * * [simplify]: Extracting #1: cost 33 inf + 0
8.387 * * [simplify]: Extracting #2: cost 124 inf + 1
8.388 * * [simplify]: Extracting #3: cost 177 inf + 647
8.390 * * [simplify]: Extracting #4: cost 237 inf + 8960
8.398 * * [simplify]: Extracting #5: cost 207 inf + 111857
8.423 * * [simplify]: Extracting #6: cost 86 inf + 364602
8.462 * * [simplify]: Extracting #7: cost 3 inf + 484448
8.499 * * [simplify]: Extracting #8: cost 0 inf + 491015
8.533 * [simplify]: Simplified to (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
8.533 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
8.533 * * * * [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)))>
8.533 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
8.534 * * [simplify]: iters left: 5 (12 enodes)
8.536 * * [simplify]: iters left: 4 (35 enodes)
8.542 * * [simplify]: iters left: 3 (72 enodes)
8.556 * * [simplify]: iters left: 2 (233 enodes)
8.625 * * [simplify]: Extracting #0: cost 1 inf + 0
8.625 * * [simplify]: Extracting #1: cost 33 inf + 0
8.626 * * [simplify]: Extracting #2: cost 124 inf + 1
8.626 * * [simplify]: Extracting #3: cost 177 inf + 647
8.627 * * [simplify]: Extracting #4: cost 237 inf + 8960
8.634 * * [simplify]: Extracting #5: cost 207 inf + 111857
8.655 * * [simplify]: Extracting #6: cost 86 inf + 364602
8.689 * * [simplify]: Extracting #7: cost 3 inf + 484448
8.725 * * [simplify]: Extracting #8: cost 0 inf + 491015
8.748 * [simplify]: Simplified to (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
8.748 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)))
8.748 * * * * [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)))>
8.749 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
8.749 * * [simplify]: iters left: 5 (12 enodes)
8.751 * * [simplify]: iters left: 4 (35 enodes)
8.758 * * [simplify]: iters left: 3 (72 enodes)
8.773 * * [simplify]: iters left: 2 (233 enodes)
8.904 * * [simplify]: Extracting #0: cost 1 inf + 0
8.904 * * [simplify]: Extracting #1: cost 33 inf + 0
8.905 * * [simplify]: Extracting #2: cost 124 inf + 1
8.906 * * [simplify]: Extracting #3: cost 177 inf + 647
8.908 * * [simplify]: Extracting #4: cost 237 inf + 8960
8.915 * * [simplify]: Extracting #5: cost 207 inf + 111857
8.940 * * [simplify]: Extracting #6: cost 86 inf + 364602
8.961 * * [simplify]: Extracting #7: cost 3 inf + 484448
8.980 * * [simplify]: Extracting #8: cost 0 inf + 491015
9.005 * [simplify]: Simplified to (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
9.005 * [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.005 * * * * [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.005 * [simplify]: Simplifying (/.p16 (*.p16 (real->posit16 1.0) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
9.005 * * [simplify]: iters left: 5 (12 enodes)
9.011 * * [simplify]: iters left: 4 (35 enodes)
9.022 * * [simplify]: iters left: 3 (72 enodes)
9.050 * * [simplify]: iters left: 2 (233 enodes)
9.160 * * [simplify]: Extracting #0: cost 1 inf + 0
9.160 * * [simplify]: Extracting #1: cost 33 inf + 0
9.161 * * [simplify]: Extracting #2: cost 124 inf + 1
9.161 * * [simplify]: Extracting #3: cost 177 inf + 647
9.162 * * [simplify]: Extracting #4: cost 237 inf + 8960
9.166 * * [simplify]: Extracting #5: cost 207 inf + 111857
9.179 * * [simplify]: Extracting #6: cost 86 inf + 364602
9.196 * * [simplify]: Extracting #7: cost 3 inf + 484448
9.235 * * [simplify]: Extracting #8: cost 0 inf + 491015
9.272 * [simplify]: Simplified to (/.p16 c (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2))
9.272 * [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.272 * * * [progress]: adding candidates to table
9.555 * [progress]: [Phase 3 of 3] Extracting.
9.556 * * [regime]: Finding splitpoints for: (#<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 (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 (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 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 (*.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 (-.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 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<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 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 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
9.562 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
9.562 * * * * [regimes]: Trying to branch on c from (#<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 (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 (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 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 (*.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 (-.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 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<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 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 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
9.815 * * * * [regimes]: Trying to branch on a from (#<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 (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 (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 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 (*.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 (-.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 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<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 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 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
9.972 * * * * [regimes]: Trying to branch on b_2 from (#<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 (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 (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 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 (*.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 (-.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 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<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 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 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
10.219 * * * [regime]: Found split indices: #<option (#s(si 1 114) #s(si 6 256))>
10.221 * [binary-search]: Improving bounds with binary search for b_2 and (#<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 (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 (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 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 (*.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 (-.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 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<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 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 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
10.221 * [regimes]: Found splitpoints: (#s(sp 1 b_2 #<cpointer:posit16>) #s(sp 6 b_2 +nan.0)) , with alts (#<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 (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 (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 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 (*.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 (-.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 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))> #<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 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 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
10.222 * [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.222 * * [simplify]: iters left: 6 (22 enodes)
10.224 * * [simplify]: Extracting #0: cost 1 inf + 0
10.224 * * [simplify]: Extracting #1: cost 4 inf + 0
10.224 * * [simplify]: Extracting #2: cost 10 inf + 0
10.224 * * [simplify]: Extracting #3: cost 14 inf + 2
10.224 * * [simplify]: Extracting #4: cost 11 inf + 87
10.224 * * [simplify]: Extracting #5: cost 12 inf + 155
10.224 * * [simplify]: Extracting #6: cost 11 inf + 798
10.225 * * [simplify]: Extracting #7: cost 8 inf + 2606
10.225 * * [simplify]: Extracting #8: cost 4 inf + 6378
10.225 * * [simplify]: Extracting #9: cost 2 inf + 8504
10.225 * * [simplify]: Extracting #10: cost 1 inf + 10228
10.226 * * [simplify]: Extracting #11: cost 0 inf + 13123
10.226 * [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.226 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
10.261 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
10.263 * * * * [points]: Setting MPFR precision to 64
10.265 * * * * [points]: Setting MPFR precision to 320
10.267 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
10.269 * * * * [points]: Setting MPFR precision to 64
10.273 * * * * [points]: Setting MPFR precision to 320
10.278 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
10.280 * * * * [points]: Setting MPFR precision to 64
10.300 * * * * [points]: Setting MPFR precision to 320
10.308 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
10.310 * * * * [points]: Setting MPFR precision to 64
10.324 * * * * [points]: Setting MPFR precision to 320
10.333 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
10.334 * * * * [points]: Setting MPFR precision to 64
10.350 * * * * [points]: Setting MPFR precision to 320
10.365 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
10.366 * * * * [points]: Setting MPFR precision to 64
10.397 * * * * [points]: Setting MPFR precision to 320
10.454 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
10.492 * * * * [points]: Setting MPFR precision to 64
10.560 * * * * [points]: Setting MPFR precision to 320
10.703 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
10.704 * * * * [points]: Setting MPFR precision to 64
10.896 * * * * [points]: Setting MPFR precision to 320
11.105 * * * * [points]: Computing exacts for 8000 points
11.106 * * * * [points]: Setting MPFR precision to 64
11.929 * * * * [points]: Setting MPFR precision to 320
13.183 * * * * [points]: Filtering points with unrepresentable outputs
13.205 * * * * [points]: Sampled 8000 points with exact outputs
19.441 * [regime-testing]: Baseline error score: 64.0
19.449 * [regime-testing]: Oracle error score: 64.0
19.466 * [regime-testing]: End program error score: 0.4271652250923291