0.004 * [progress]: [Phase 1 of 3] Setting up.
0.005 * * * [progress]: [1/2] Preparing points
0.008 * * * * [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.136 * * * * [points]: Setting MPFR precision to 64
0.141 * * * * [points]: Setting MPFR precision to 320
0.144 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.149 * * * * [points]: Setting MPFR precision to 64
0.152 * * * * [points]: Setting MPFR precision to 320
0.156 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.161 * * * * [points]: Setting MPFR precision to 64
0.168 * * * * [points]: Setting MPFR precision to 320
0.175 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.181 * * * * [points]: Setting MPFR precision to 64
0.194 * * * * [points]: Setting MPFR precision to 320
0.205 * * * * [points]: Computing exacts for 256 points
0.211 * * * * [points]: Setting MPFR precision to 64
0.241 * * * * [points]: Setting MPFR precision to 320
0.273 * * * * [points]: Filtering points with unrepresentable outputs
0.274 * * * * [points]: Sampled 256 points with exact outputs
0.275 * * * [progress]: [2/2] Setting up program.
0.297 * [progress]: [Phase 2 of 3] Improving.
0.329 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
0.331 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
0.333 * * [simplify]: iters left: 6 (16 enodes)
0.349 * * [simplify]: iters left: 5 (45 enodes)
0.366 * * [simplify]: iters left: 4 (91 enodes)
0.406 * * [simplify]: iters left: 3 (310 enodes)
0.779 * * [simplify]: Extracting #0: cost 1 inf + 0
0.779 * * [simplify]: Extracting #1: cost 31 inf + 0
0.781 * * [simplify]: Extracting #2: cost 123 inf + 1
0.782 * * [simplify]: Extracting #3: cost 204 inf + 405
0.784 * * [simplify]: Extracting #4: cost 266 inf + 7226
0.789 * * [simplify]: Extracting #5: cost 283 inf + 80479
0.804 * * [simplify]: Extracting #6: cost 199 inf + 369645
0.838 * * [simplify]: Extracting #7: cost 13 inf + 704259
0.876 * * [simplify]: Extracting #8: cost 0 inf + 731309
0.907 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
0.907 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
0.927 * * [progress]: iteration 1 / 4
0.927 * * * [progress]: picking best candidate
0.945 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
0.945 * * * [progress]: localizing error
1.160 * * * [progress]: generating rewritten candidates
1.160 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.163 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1.163 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1.166 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1 2)
1.171 * * * [progress]: generating series expansions
1.171 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.172 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1.172 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1.172 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1 2)
1.172 * * * [progress]: simplifying candidates
1.172 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
1.172 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1.172 * * [simplify]: iters left: 5 (11 enodes)
1.175 * * [simplify]: iters left: 4 (29 enodes)
1.180 * * [simplify]: iters left: 3 (61 enodes)
1.193 * * [simplify]: iters left: 2 (176 enodes)
1.262 * * [simplify]: Extracting #0: cost 1 inf + 0
1.262 * * [simplify]: Extracting #1: cost 2 inf + 0
1.262 * * [simplify]: Extracting #2: cost 3 inf + 0
1.262 * * [simplify]: Extracting #3: cost 17 inf + 0
1.262 * * [simplify]: Extracting #4: cost 61 inf + 0
1.263 * * [simplify]: Extracting #5: cost 128 inf + 646
1.264 * * [simplify]: Extracting #6: cost 197 inf + 13038
1.267 * * [simplify]: Extracting #7: cost 128 inf + 105782
1.280 * * [simplify]: Extracting #8: cost 11 inf + 322684
1.305 * * [simplify]: Extracting #9: cost 0 inf + 342922
1.325 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
1.325 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))) (*.p16 (real->posit16 2) a)))
1.325 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
1.326 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))
1.326 * * [simplify]: iters left: 6 (14 enodes)
1.332 * * [simplify]: iters left: 5 (42 enodes)
1.348 * * [simplify]: iters left: 4 (117 enodes)
1.398 * * [simplify]: iters left: 3 (426 enodes)
1.736 * * [simplify]: Extracting #0: cost 1 inf + 0
1.736 * * [simplify]: Extracting #1: cost 51 inf + 0
1.736 * * [simplify]: Extracting #2: cost 242 inf + 0
1.738 * * [simplify]: Extracting #3: cost 410 inf + 5216
1.748 * * [simplify]: Extracting #4: cost 403 inf + 280282
1.833 * * [simplify]: Extracting #5: cost 149 inf + 977818
1.923 * * [simplify]: Extracting #6: cost 1 inf + 1265775
2.028 * * [simplify]: Extracting #7: cost 0 inf + 1268699
2.117 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
2.117 * [simplify]: Simplified (2 1 1) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))
2.117 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
2.117 * * [simplify]: iters left: 5 (12 enodes)
2.123 * * [simplify]: iters left: 4 (31 enodes)
2.134 * * [simplify]: iters left: 3 (64 enodes)
2.160 * * [simplify]: iters left: 2 (183 enodes)
2.246 * * [simplify]: Extracting #0: cost 1 inf + 0
2.246 * * [simplify]: Extracting #1: cost 6 inf + 0
2.246 * * [simplify]: Extracting #2: cost 10 inf + 1
2.246 * * [simplify]: Extracting #3: cost 22 inf + 804
2.246 * * [simplify]: Extracting #4: cost 64 inf + 1445
2.247 * * [simplify]: Extracting #5: cost 140 inf + 3371
2.249 * * [simplify]: Extracting #6: cost 220 inf + 13396
2.258 * * [simplify]: Extracting #7: cost 134 inf + 134080
2.283 * * [simplify]: Extracting #8: cost 16 inf + 340223
2.302 * * [simplify]: Extracting #9: cost 0 inf + 376165
2.316 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
2.316 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))
2.316 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
2.316 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
2.317 * * [simplify]: iters left: 6 (15 enodes)
2.320 * * [simplify]: iters left: 5 (41 enodes)
2.335 * * [simplify]: iters left: 4 (85 enodes)
2.362 * * [simplify]: iters left: 3 (287 enodes)
2.958 * * [simplify]: Extracting #0: cost 1 inf + 0
2.958 * * [simplify]: Extracting #1: cost 20 inf + 0
2.958 * * [simplify]: Extracting #2: cost 91 inf + 0
2.959 * * [simplify]: Extracting #3: cost 174 inf + 83
2.961 * * [simplify]: Extracting #4: cost 235 inf + 6260
2.964 * * [simplify]: Extracting #5: cost 262 inf + 53662
2.988 * * [simplify]: Extracting #6: cost 175 inf + 347193
3.037 * * [simplify]: Extracting #7: cost 6 inf + 656891
3.097 * * [simplify]: Extracting #8: cost 0 inf + 669632
3.150 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2))
3.150 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2)) a))
3.150 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
3.151 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))
3.151 * * [simplify]: iters left: 6 (16 enodes)
3.158 * * [simplify]: iters left: 5 (46 enodes)
3.173 * * [simplify]: iters left: 4 (107 enodes)
3.216 * * [simplify]: iters left: 3 (238 enodes)
3.354 * * [simplify]: Extracting #0: cost 1 inf + 0
3.355 * * [simplify]: Extracting #1: cost 26 inf + 0
3.355 * * [simplify]: Extracting #2: cost 38 inf + 1
3.355 * * [simplify]: Extracting #3: cost 39 inf + 85
3.356 * * [simplify]: Extracting #4: cost 49 inf + 2255
3.356 * * [simplify]: Extracting #5: cost 89 inf + 3297
3.358 * * [simplify]: Extracting #6: cost 168 inf + 4900
3.360 * * [simplify]: Extracting #7: cost 235 inf + 13556
3.367 * * [simplify]: Extracting #8: cost 179 inf + 88862
3.388 * * [simplify]: Extracting #9: cost 43 inf + 331719
3.419 * * [simplify]: Extracting #10: cost 2 inf + 398631
3.450 * * [simplify]: Extracting #11: cost 0 inf + 402479
3.483 * [simplify]: Simplified to (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))
3.483 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))))
3.484 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))>
3.484 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
3.484 * * [simplify]: iters left: 2 (4 enodes)
3.486 * * [simplify]: iters left: 1 (8 enodes)
3.489 * * [simplify]: Extracting #0: cost 1 inf + 0
3.489 * * [simplify]: Extracting #1: cost 3 inf + 0
3.489 * * [simplify]: Extracting #2: cost 3 inf + 1
3.489 * * [simplify]: Extracting #3: cost 2 inf + 2
3.489 * * [simplify]: Extracting #4: cost 0 inf + 325
3.489 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
3.489 * [simplify]: Simplified (2 1 2 1 2 1) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c)))) (*.p16 (real->posit16 2) a)))
3.489 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))>
3.489 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
3.490 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
3.490 * * [simplify]: iters left: 6 (16 enodes)
3.497 * * [simplify]: iters left: 5 (45 enodes)
3.513 * * [simplify]: iters left: 4 (91 enodes)
3.550 * * [simplify]: iters left: 3 (310 enodes)
3.765 * * [simplify]: Extracting #0: cost 1 inf + 0
3.765 * * [simplify]: Extracting #1: cost 31 inf + 0
3.766 * * [simplify]: Extracting #2: cost 123 inf + 1
3.767 * * [simplify]: Extracting #3: cost 204 inf + 405
3.769 * * [simplify]: Extracting #4: cost 266 inf + 7226
3.775 * * [simplify]: Extracting #5: cost 283 inf + 80479
3.798 * * [simplify]: Extracting #6: cost 199 inf + 369645
3.826 * * [simplify]: Extracting #7: cost 13 inf + 704259
3.867 * * [simplify]: Extracting #8: cost 0 inf + 731309
3.922 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
3.922 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
3.922 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
3.923 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
3.923 * * [simplify]: iters left: 6 (16 enodes)
3.929 * * [simplify]: iters left: 5 (45 enodes)
3.943 * * [simplify]: iters left: 4 (91 enodes)
3.981 * * [simplify]: iters left: 3 (310 enodes)
4.139 * * [simplify]: Extracting #0: cost 1 inf + 0
4.139 * * [simplify]: Extracting #1: cost 31 inf + 0
4.140 * * [simplify]: Extracting #2: cost 123 inf + 1
4.141 * * [simplify]: Extracting #3: cost 204 inf + 405
4.142 * * [simplify]: Extracting #4: cost 266 inf + 7226
4.148 * * [simplify]: Extracting #5: cost 283 inf + 80479
4.168 * * [simplify]: Extracting #6: cost 199 inf + 369645
4.215 * * [simplify]: Extracting #7: cost 13 inf + 704259
4.275 * * [simplify]: Extracting #8: cost 0 inf + 731309
4.337 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
4.337 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
4.337 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
4.338 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
4.338 * * [simplify]: iters left: 6 (16 enodes)
4.345 * * [simplify]: iters left: 5 (45 enodes)
4.362 * * [simplify]: iters left: 4 (91 enodes)
4.381 * * [simplify]: iters left: 3 (310 enodes)
4.523 * * [simplify]: Extracting #0: cost 1 inf + 0
4.524 * * [simplify]: Extracting #1: cost 31 inf + 0
4.524 * * [simplify]: Extracting #2: cost 123 inf + 1
4.524 * * [simplify]: Extracting #3: cost 204 inf + 405
4.525 * * [simplify]: Extracting #4: cost 266 inf + 7226
4.528 * * [simplify]: Extracting #5: cost 283 inf + 80479
4.548 * * [simplify]: Extracting #6: cost 199 inf + 369645
4.595 * * [simplify]: Extracting #7: cost 13 inf + 704259
4.626 * * [simplify]: Extracting #8: cost 0 inf + 731309
4.670 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
4.670 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
4.670 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
4.670 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
4.670 * * [simplify]: iters left: 6 (16 enodes)
4.674 * * [simplify]: iters left: 5 (45 enodes)
4.682 * * [simplify]: iters left: 4 (91 enodes)
4.702 * * [simplify]: iters left: 3 (310 enodes)
4.837 * * [simplify]: Extracting #0: cost 1 inf + 0
4.837 * * [simplify]: Extracting #1: cost 31 inf + 0
4.837 * * [simplify]: Extracting #2: cost 123 inf + 1
4.838 * * [simplify]: Extracting #3: cost 204 inf + 405
4.839 * * [simplify]: Extracting #4: cost 266 inf + 7226
4.842 * * [simplify]: Extracting #5: cost 283 inf + 80479
4.856 * * [simplify]: Extracting #6: cost 199 inf + 369645
4.887 * * [simplify]: Extracting #7: cost 13 inf + 704259
4.918 * * [simplify]: Extracting #8: cost 0 inf + 731309
4.949 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
4.949 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
4.949 * * * [progress]: adding candidates to table
5.305 * * [progress]: iteration 2 / 4
5.305 * * * [progress]: picking best candidate
5.412 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
5.412 * * * [progress]: localizing error
5.855 * * * [progress]: generating rewritten candidates
5.855 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
5.860 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
5.866 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 2)
5.866 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
5.872 * * * [progress]: generating series expansions
5.873 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
5.873 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
5.873 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 2)
5.873 * * * * [progress]: [ 4 / 4 ] generating series at (2)
5.873 * * * [progress]: simplifying candidates
5.873 * * * * [progress]: [ 1 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (neg.p16 b))) (*.p16 (real->posit16 2) a)))>
5.873 * * * * [progress]: [ 2 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))>
5.873 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2))
5.873 * * [simplify]: iters left: 6 (20 enodes)
5.882 * * [simplify]: iters left: 5 (50 enodes)
5.901 * * [simplify]: iters left: 4 (122 enodes)
5.932 * * [simplify]: iters left: 3 (328 enodes)
6.112 * * [simplify]: Extracting #0: cost 1 inf + 0
6.112 * * [simplify]: Extracting #1: cost 9 inf + 0
6.112 * * [simplify]: Extracting #2: cost 44 inf + 0
6.113 * * [simplify]: Extracting #3: cost 109 inf + 525
6.114 * * [simplify]: Extracting #4: cost 116 inf + 20329
6.116 * * [simplify]: Extracting #5: cost 169 inf + 39293
6.119 * * [simplify]: Extracting #6: cost 223 inf + 75221
6.132 * * [simplify]: Extracting #7: cost 73 inf + 300931
6.150 * * [simplify]: Extracting #8: cost 4 inf + 431926
6.185 * * [simplify]: Extracting #9: cost 0 inf + 439380
6.221 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))
6.221 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))
6.221 * * * * [progress]: [ 3 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
6.222 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))
6.222 * * [simplify]: iters left: 6 (16 enodes)
6.229 * * [simplify]: iters left: 5 (46 enodes)
6.245 * * [simplify]: iters left: 4 (107 enodes)
6.270 * * [simplify]: iters left: 3 (238 enodes)
6.384 * * [simplify]: Extracting #0: cost 1 inf + 0
6.384 * * [simplify]: Extracting #1: cost 26 inf + 0
6.384 * * [simplify]: Extracting #2: cost 38 inf + 1
6.384 * * [simplify]: Extracting #3: cost 39 inf + 85
6.385 * * [simplify]: Extracting #4: cost 49 inf + 2255
6.385 * * [simplify]: Extracting #5: cost 89 inf + 3297
6.386 * * [simplify]: Extracting #6: cost 168 inf + 4900
6.387 * * [simplify]: Extracting #7: cost 235 inf + 13556
6.390 * * [simplify]: Extracting #8: cost 179 inf + 88862
6.400 * * [simplify]: Extracting #9: cost 43 inf + 331719
6.427 * * [simplify]: Extracting #10: cost 2 inf + 398631
6.443 * * [simplify]: Extracting #11: cost 0 inf + 402479
6.465 * [simplify]: Simplified to (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))
6.465 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))))
6.465 * * * * [progress]: [ 4 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
6.465 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a))
6.465 * * [simplify]: iters left: 6 (21 enodes)
6.470 * * [simplify]: iters left: 5 (54 enodes)
6.480 * * [simplify]: iters left: 4 (133 enodes)
6.526 * * [simplify]: iters left: 3 (370 enodes)
6.754 * * [simplify]: Extracting #0: cost 1 inf + 0
6.754 * * [simplify]: Extracting #1: cost 13 inf + 0
6.754 * * [simplify]: Extracting #2: cost 50 inf + 1
6.755 * * [simplify]: Extracting #3: cost 116 inf + 84
6.757 * * [simplify]: Extracting #4: cost 120 inf + 23851
6.762 * * [simplify]: Extracting #5: cost 177 inf + 36966
6.770 * * [simplify]: Extracting #6: cost 214 inf + 84248
6.793 * * [simplify]: Extracting #7: cost 53 inf + 383008
6.811 * * [simplify]: Extracting #8: cost 1 inf + 450242
6.843 * * [simplify]: Extracting #9: cost 0 inf + 446606
6.878 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))
6.878 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))
6.878 * * * * [progress]: [ 5 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
6.878 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a))
6.878 * * [simplify]: iters left: 6 (21 enodes)
6.883 * * [simplify]: iters left: 5 (54 enodes)
6.893 * * [simplify]: iters left: 4 (133 enodes)
6.935 * * [simplify]: iters left: 3 (370 enodes)
7.131 * * [simplify]: Extracting #0: cost 1 inf + 0
7.131 * * [simplify]: Extracting #1: cost 13 inf + 0
7.131 * * [simplify]: Extracting #2: cost 50 inf + 1
7.132 * * [simplify]: Extracting #3: cost 116 inf + 84
7.133 * * [simplify]: Extracting #4: cost 120 inf + 23851
7.135 * * [simplify]: Extracting #5: cost 177 inf + 36966
7.139 * * [simplify]: Extracting #6: cost 214 inf + 84248
7.159 * * [simplify]: Extracting #7: cost 53 inf + 383008
7.199 * * [simplify]: Extracting #8: cost 1 inf + 450242
7.226 * * [simplify]: Extracting #9: cost 0 inf + 446606
7.245 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))
7.245 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))
7.245 * * * * [progress]: [ 6 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
7.245 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a))
7.246 * * [simplify]: iters left: 6 (21 enodes)
7.252 * * [simplify]: iters left: 5 (54 enodes)
7.271 * * [simplify]: iters left: 4 (133 enodes)
7.321 * * [simplify]: iters left: 3 (370 enodes)
7.482 * * [simplify]: Extracting #0: cost 1 inf + 0
7.482 * * [simplify]: Extracting #1: cost 13 inf + 0
7.482 * * [simplify]: Extracting #2: cost 50 inf + 1
7.483 * * [simplify]: Extracting #3: cost 116 inf + 84
7.484 * * [simplify]: Extracting #4: cost 120 inf + 23851
7.486 * * [simplify]: Extracting #5: cost 177 inf + 36966
7.490 * * [simplify]: Extracting #6: cost 214 inf + 84248
7.507 * * [simplify]: Extracting #7: cost 53 inf + 383008
7.526 * * [simplify]: Extracting #8: cost 1 inf + 450242
7.544 * * [simplify]: Extracting #9: cost 0 inf + 446606
7.580 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))
7.580 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))
7.580 * * * * [progress]: [ 7 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
7.581 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a))
7.581 * * [simplify]: iters left: 6 (21 enodes)
7.590 * * [simplify]: iters left: 5 (54 enodes)
7.610 * * [simplify]: iters left: 4 (133 enodes)
7.655 * * [simplify]: iters left: 3 (370 enodes)
7.868 * * [simplify]: Extracting #0: cost 1 inf + 0
7.869 * * [simplify]: Extracting #1: cost 13 inf + 0
7.869 * * [simplify]: Extracting #2: cost 50 inf + 1
7.870 * * [simplify]: Extracting #3: cost 116 inf + 84
7.872 * * [simplify]: Extracting #4: cost 120 inf + 23851
7.880 * * [simplify]: Extracting #5: cost 177 inf + 36966
7.888 * * [simplify]: Extracting #6: cost 214 inf + 84248
7.910 * * [simplify]: Extracting #7: cost 53 inf + 383008
7.928 * * [simplify]: Extracting #8: cost 1 inf + 450242
7.954 * * [simplify]: Extracting #9: cost 0 inf + 446606
7.990 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))
7.990 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))
7.991 * * * [progress]: adding candidates to table
8.332 * * [progress]: iteration 3 / 4
8.333 * * * [progress]: picking best candidate
8.423 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))>
8.423 * * * [progress]: localizing error
8.657 * * * [progress]: generating rewritten candidates
8.657 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2 2)
8.659 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
8.664 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 2 1)
8.664 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2 1 1 2)
8.668 * * * [progress]: generating series expansions
8.668 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2 2)
8.668 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
8.668 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 2 1)
8.668 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2 1 1 2)
8.668 * * * [progress]: simplifying candidates
8.668 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (neg.p16 b)))) a))>
8.668 * [simplify]: Simplifying (neg.p16 b)
8.668 * * [simplify]: iters left: 1 (2 enodes)
8.669 * * [simplify]: Extracting #0: cost 1 inf + 0
8.669 * * [simplify]: Extracting #1: cost 2 inf + 0
8.669 * * [simplify]: Extracting #2: cost 1 inf + 1
8.669 * * [simplify]: Extracting #3: cost 0 inf + 82
8.669 * [simplify]: Simplified to (neg.p16 b)
8.669 * [simplify]: Simplified (2 1 2 2 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (neg.p16 b)))) a))
8.669 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))) a))>
8.669 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b))
8.669 * * [simplify]: iters left: 6 (12 enodes)
8.672 * * [simplify]: iters left: 5 (39 enodes)
8.682 * * [simplify]: iters left: 4 (111 enodes)
8.734 * * [simplify]: iters left: 3 (424 enodes)
9.039 * * [simplify]: Extracting #0: cost 1 inf + 0
9.039 * * [simplify]: Extracting #1: cost 47 inf + 0
9.040 * * [simplify]: Extracting #2: cost 231 inf + 0
9.041 * * [simplify]: Extracting #3: cost 401 inf + 2894
9.048 * * [simplify]: Extracting #4: cost 492 inf + 168349
9.085 * * [simplify]: Extracting #5: cost 182 inf + 869093
9.154 * * [simplify]: Extracting #6: cost 4 inf + 1235379
9.215 * * [simplify]: Extracting #7: cost 0 inf + 1241678
9.328 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 c a) (real->posit16 4)))
9.328 * [simplify]: Simplified (2 1 2 2 1) to (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 c a) (real->posit16 4))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))) a))
9.329 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)
9.329 * * [simplify]: iters left: 5 (11 enodes)
9.334 * * [simplify]: iters left: 4 (30 enodes)
9.345 * * [simplify]: iters left: 3 (62 enodes)
9.370 * * [simplify]: iters left: 2 (176 enodes)
9.469 * * [simplify]: Extracting #0: cost 1 inf + 0
9.469 * * [simplify]: Extracting #1: cost 3 inf + 0
9.469 * * [simplify]: Extracting #2: cost 3 inf + 1
9.469 * * [simplify]: Extracting #3: cost 17 inf + 1
9.469 * * [simplify]: Extracting #4: cost 59 inf + 322
9.470 * * [simplify]: Extracting #5: cost 136 inf + 1287
9.472 * * [simplify]: Extracting #6: cost 205 inf + 12075
9.477 * * [simplify]: Extracting #7: cost 152 inf + 76968
9.486 * * [simplify]: Extracting #8: cost 23 inf + 303821
9.499 * * [simplify]: Extracting #9: cost 0 inf + 355104
9.517 * * [simplify]: Extracting #10: cost 0 inf + 354744
9.540 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))
9.540 * [simplify]: Simplified (2 1 2 2 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))))) a))
9.541 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)) a))>
9.541 * [simplify]: Simplifying (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (real->posit16 2))
9.541 * * [simplify]: iters left: 4 (12 enodes)
9.544 * * [simplify]: iters left: 3 (24 enodes)
9.549 * * [simplify]: iters left: 2 (39 enodes)
9.558 * * [simplify]: iters left: 1 (58 enodes)
9.566 * * [simplify]: Extracting #0: cost 1 inf + 0
9.566 * * [simplify]: Extracting #1: cost 23 inf + 0
9.566 * * [simplify]: Extracting #2: cost 24 inf + 2
9.566 * * [simplify]: Extracting #3: cost 19 inf + 1292
9.566 * * [simplify]: Extracting #4: cost 4 inf + 9488
9.567 * * [simplify]: Extracting #5: cost 0 inf + 12459
9.567 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (real->posit16 2))
9.568 * [simplify]: Simplified (2 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)) a))
9.568 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)) a))>
9.568 * [simplify]: Simplifying (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b))))
9.568 * * [simplify]: iters left: 6 (19 enodes)
9.577 * * [simplify]: iters left: 5 (52 enodes)
9.597 * * [simplify]: iters left: 4 (176 enodes)
9.677 * * [simplify]: Extracting #0: cost 1 inf + 0
9.677 * * [simplify]: Extracting #1: cost 63 inf + 0
9.677 * * [simplify]: Extracting #2: cost 176 inf + 324
9.678 * * [simplify]: Extracting #3: cost 246 inf + 1695
9.681 * * [simplify]: Extracting #4: cost 205 inf + 81804
9.696 * * [simplify]: Extracting #5: cost 71 inf + 335361
9.719 * * [simplify]: Extracting #6: cost 28 inf + 444937
9.743 * * [simplify]: Extracting #7: cost 0 inf + 469248
9.768 * [simplify]: Simplified to (/.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (real->posit16 2)))
9.768 * [simplify]: Simplified (2 1 1) to (λ (a b c) (/.p16 (*.p16 (/.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (real->posit16 2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)) a))
9.768 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))) a))>
9.768 * [simplify]: Simplifying (*.p16 (real->posit16 4) c)
9.768 * * [simplify]: iters left: 2 (4 enodes)
9.769 * * [simplify]: iters left: 1 (8 enodes)
9.771 * * [simplify]: Extracting #0: cost 1 inf + 0
9.771 * * [simplify]: Extracting #1: cost 3 inf + 0
9.771 * * [simplify]: Extracting #2: cost 3 inf + 1
9.771 * * [simplify]: Extracting #3: cost 2 inf + 2
9.771 * * [simplify]: Extracting #4: cost 0 inf + 325
9.771 * [simplify]: Simplified to (*.p16 c (real->posit16 4))
9.771 * [simplify]: Simplified (2 1 2 2 1 1 2 1) to (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c (real->posit16 4)) a))) b))) a))
9.771 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) a))>
9.771 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))>
9.771 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a)
9.771 * * [simplify]: iters left: 6 (19 enodes)
9.776 * * [simplify]: iters left: 5 (51 enodes)
9.786 * * [simplify]: iters left: 4 (168 enodes)
9.893 * * [simplify]: Extracting #0: cost 1 inf + 0
9.893 * * [simplify]: Extracting #1: cost 64 inf + 0
9.894 * * [simplify]: Extracting #2: cost 160 inf + 324
9.895 * * [simplify]: Extracting #3: cost 206 inf + 5787
9.897 * * [simplify]: Extracting #4: cost 188 inf + 49362
9.905 * * [simplify]: Extracting #5: cost 58 inf + 252794
9.920 * * [simplify]: Extracting #6: cost 38 inf + 345962
9.949 * * [simplify]: Extracting #7: cost 28 inf + 383753
9.976 * * [simplify]: Extracting #8: cost 0 inf + 404899
9.992 * * [simplify]: Extracting #9: cost 0 inf + 404579
10.018 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
10.018 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
10.018 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))>
10.018 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a)
10.019 * * [simplify]: iters left: 6 (19 enodes)
10.027 * * [simplify]: iters left: 5 (51 enodes)
10.041 * * [simplify]: iters left: 4 (168 enodes)
10.135 * * [simplify]: Extracting #0: cost 1 inf + 0
10.135 * * [simplify]: Extracting #1: cost 64 inf + 0
10.136 * * [simplify]: Extracting #2: cost 160 inf + 324
10.137 * * [simplify]: Extracting #3: cost 206 inf + 5787
10.139 * * [simplify]: Extracting #4: cost 188 inf + 49362
10.150 * * [simplify]: Extracting #5: cost 58 inf + 252794
10.164 * * [simplify]: Extracting #6: cost 38 inf + 345962
10.180 * * [simplify]: Extracting #7: cost 28 inf + 383753
10.197 * * [simplify]: Extracting #8: cost 0 inf + 404899
10.227 * * [simplify]: Extracting #9: cost 0 inf + 404579
10.261 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
10.261 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
10.261 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))>
10.262 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a)
10.262 * * [simplify]: iters left: 6 (19 enodes)
10.271 * * [simplify]: iters left: 5 (51 enodes)
10.292 * * [simplify]: iters left: 4 (168 enodes)
10.367 * * [simplify]: Extracting #0: cost 1 inf + 0
10.367 * * [simplify]: Extracting #1: cost 64 inf + 0
10.367 * * [simplify]: Extracting #2: cost 160 inf + 324
10.368 * * [simplify]: Extracting #3: cost 206 inf + 5787
10.370 * * [simplify]: Extracting #4: cost 188 inf + 49362
10.379 * * [simplify]: Extracting #5: cost 58 inf + 252794
10.397 * * [simplify]: Extracting #6: cost 38 inf + 345962
10.425 * * [simplify]: Extracting #7: cost 28 inf + 383753
10.442 * * [simplify]: Extracting #8: cost 0 inf + 404899
10.466 * * [simplify]: Extracting #9: cost 0 inf + 404579
10.499 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
10.500 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
10.500 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))>
10.500 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a)
10.500 * * [simplify]: iters left: 6 (19 enodes)
10.511 * * [simplify]: iters left: 5 (51 enodes)
10.532 * * [simplify]: iters left: 4 (168 enodes)
10.614 * * [simplify]: Extracting #0: cost 1 inf + 0
10.614 * * [simplify]: Extracting #1: cost 64 inf + 0
10.615 * * [simplify]: Extracting #2: cost 160 inf + 324
10.616 * * [simplify]: Extracting #3: cost 206 inf + 5787
10.621 * * [simplify]: Extracting #4: cost 188 inf + 49362
10.632 * * [simplify]: Extracting #5: cost 58 inf + 252794
10.645 * * [simplify]: Extracting #6: cost 38 inf + 345962
10.666 * * [simplify]: Extracting #7: cost 28 inf + 383753
10.698 * * [simplify]: Extracting #8: cost 0 inf + 404899
10.731 * * [simplify]: Extracting #9: cost 0 inf + 404579
10.761 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
10.761 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
10.761 * * * [progress]: adding candidates to table
11.195 * * [progress]: iteration 4 / 4
11.195 * * * [progress]: picking best candidate
11.354 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
11.354 * * * [progress]: localizing error
11.658 * * * [progress]: generating rewritten candidates
11.658 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
11.662 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
11.673 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 1)
11.674 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 1 1)
11.682 * * * [progress]: generating series expansions
11.682 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
11.682 * * * * [progress]: [ 2 / 4 ] generating series at (2)
11.682 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 1)
11.682 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 1 1)
11.682 * * * [progress]: simplifying candidates
11.682 * * * * [progress]: [ 1 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)))))>
11.682 * [simplify]: Simplifying (neg.p16 b)
11.683 * * [simplify]: iters left: 1 (2 enodes)
11.683 * * [simplify]: Extracting #0: cost 1 inf + 0
11.683 * * [simplify]: Extracting #1: cost 2 inf + 0
11.683 * * [simplify]: Extracting #2: cost 1 inf + 1
11.683 * * [simplify]: Extracting #3: cost 0 inf + 82
11.683 * [simplify]: Simplified to (neg.p16 b)
11.683 * [simplify]: Simplified (2 2 2 2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)))))
11.683 * * * * [progress]: [ 2 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))))>
11.683 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b))
11.683 * * [simplify]: iters left: 6 (12 enodes)
11.686 * * [simplify]: iters left: 5 (39 enodes)
11.694 * * [simplify]: iters left: 4 (111 enodes)
11.727 * * [simplify]: iters left: 3 (424 enodes)
12.069 * * [simplify]: Extracting #0: cost 1 inf + 0
12.070 * * [simplify]: Extracting #1: cost 47 inf + 0
12.071 * * [simplify]: Extracting #2: cost 231 inf + 0
12.073 * * [simplify]: Extracting #3: cost 401 inf + 2894
12.096 * * [simplify]: Extracting #4: cost 477 inf + 189684
12.167 * * [simplify]: Extracting #5: cost 205 inf + 818645
12.277 * * [simplify]: Extracting #6: cost 11 inf + 1218752
12.397 * * [simplify]: Extracting #7: cost 0 inf + 1243040
12.515 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c))
12.515 * [simplify]: Simplified (2 2 2 1) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))))
12.516 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)
12.516 * * [simplify]: iters left: 6 (11 enodes)
12.521 * * [simplify]: iters left: 5 (30 enodes)
12.531 * * [simplify]: iters left: 4 (62 enodes)
12.554 * * [simplify]: iters left: 3 (175 enodes)
12.654 * * [simplify]: Extracting #0: cost 1 inf + 0
12.654 * * [simplify]: Extracting #1: cost 3 inf + 0
12.654 * * [simplify]: Extracting #2: cost 3 inf + 1
12.655 * * [simplify]: Extracting #3: cost 17 inf + 1
12.655 * * [simplify]: Extracting #4: cost 59 inf + 322
12.656 * * [simplify]: Extracting #5: cost 134 inf + 1287
12.658 * * [simplify]: Extracting #6: cost 200 inf + 13681
12.666 * * [simplify]: Extracting #7: cost 121 inf + 136896
12.689 * * [simplify]: Extracting #8: cost 11 inf + 328936
12.714 * * [simplify]: Extracting #9: cost 1 inf + 344412
12.744 * * [simplify]: Extracting #10: cost 0 inf + 348016
12.773 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
12.773 * [simplify]: Simplified (2 2 2 2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))))))
12.773 * * * * [progress]: [ 3 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))>
12.773 * [simplify]: Simplifying (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a))
12.773 * * [simplify]: iters left: 4 (10 enodes)
12.778 * * [simplify]: iters left: 3 (28 enodes)
12.789 * * [simplify]: iters left: 2 (68 enodes)
12.816 * * [simplify]: iters left: 1 (181 enodes)
12.931 * * [simplify]: Extracting #0: cost 1 inf + 0
12.931 * * [simplify]: Extracting #1: cost 53 inf + 0
12.931 * * [simplify]: Extracting #2: cost 67 inf + 2
12.932 * * [simplify]: Extracting #3: cost 55 inf + 4941
12.935 * * [simplify]: Extracting #4: cost 13 inf + 35459
12.940 * * [simplify]: Extracting #5: cost 0 inf + 45901
12.945 * * [simplify]: Extracting #6: cost 0 inf + 45781
12.950 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 4) (real->posit16 2)) c)
12.950 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (*.p16 (/.p16 (real->posit16 4) (real->posit16 2)) c) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
12.950 * * * * [progress]: [ 4 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 c (/.p16 (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 4)))))>
12.951 * [simplify]: Simplifying (/.p16 (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 4)))
12.951 * * [simplify]: iters left: 6 (16 enodes)
12.959 * * [simplify]: iters left: 5 (52 enodes)
12.981 * * [simplify]: iters left: 4 (151 enodes)
13.053 * * [simplify]: Extracting #0: cost 1 inf + 0
13.053 * * [simplify]: Extracting #1: cost 61 inf + 0
13.054 * * [simplify]: Extracting #2: cost 131 inf + 442
13.055 * * [simplify]: Extracting #3: cost 138 inf + 3384
13.058 * * [simplify]: Extracting #4: cost 144 inf + 17560
13.061 * * [simplify]: Extracting #5: cost 145 inf + 49176
13.078 * * [simplify]: Extracting #6: cost 43 inf + 225184
13.103 * * [simplify]: Extracting #7: cost 1 inf + 288172
13.130 * * [simplify]: Extracting #8: cost 0 inf + 291136
13.154 * [simplify]: Simplified to (/.p16 (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))) (*.p16 a (real->posit16 4)))
13.154 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 c (/.p16 (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))) (*.p16 a (real->posit16 4)))))
13.154 * * * * [progress]: [ 5 / 12 ] simplifiying candidate #<alt (λ (a b c) (*.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))>
13.154 * [simplify]: Simplifying (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b))))
13.155 * * [simplify]: iters left: 6 (17 enodes)
13.163 * * [simplify]: iters left: 5 (56 enodes)
13.186 * * [simplify]: iters left: 4 (223 enodes)
13.319 * * [simplify]: Extracting #0: cost 1 inf + 0
13.320 * * [simplify]: Extracting #1: cost 163 inf + 0
13.322 * * [simplify]: Extracting #2: cost 332 inf + 1086
13.328 * * [simplify]: Extracting #3: cost 295 inf + 82489
13.345 * * [simplify]: Extracting #4: cost 140 inf + 416566
13.386 * * [simplify]: Extracting #5: cost 69 inf + 643113
13.415 * * [simplify]: Extracting #6: cost 27 inf + 729381
13.459 * * [simplify]: Extracting #7: cost 0 inf + 762852
13.521 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))))
13.521 * [simplify]: Simplified (2 1) to (λ (a b c) (*.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
13.522 * * * * [progress]: [ 6 / 12 ] simplifiying candidate #<alt (λ (a b c) (*.p16 (/.p16 c (*.p16 (real->posit16 2) a)) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
13.522 * [simplify]: Simplifying (/.p16 c (*.p16 (real->posit16 2) a))
13.522 * * [simplify]: iters left: 3 (6 enodes)
13.525 * * [simplify]: iters left: 2 (14 enodes)
13.530 * * [simplify]: Extracting #0: cost 1 inf + 0
13.530 * * [simplify]: Extracting #1: cost 5 inf + 0
13.530 * * [simplify]: Extracting #2: cost 4 inf + 2
13.530 * * [simplify]: Extracting #3: cost 5 inf + 2
13.531 * * [simplify]: Extracting #4: cost 0 inf + 1531
13.531 * [simplify]: Simplified to (/.p16 c (*.p16 a (real->posit16 2)))
13.531 * [simplify]: Simplified (2 1) to (λ (a b c) (*.p16 (/.p16 c (*.p16 a (real->posit16 2))) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
13.531 * [simplify]: Simplifying (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))
13.531 * * [simplify]: iters left: 6 (12 enodes)
13.537 * * [simplify]: iters left: 5 (38 enodes)
13.552 * * [simplify]: iters left: 4 (85 enodes)
13.588 * * [simplify]: iters left: 3 (313 enodes)
13.752 * * [simplify]: Extracting #0: cost 1 inf + 0
13.752 * * [simplify]: Extracting #1: cost 43 inf + 0
13.753 * * [simplify]: Extracting #2: cost 167 inf + 1
13.754 * * [simplify]: Extracting #3: cost 219 inf + 1692
13.757 * * [simplify]: Extracting #4: cost 277 inf + 18475
13.768 * * [simplify]: Extracting #5: cost 288 inf + 164609
13.804 * * [simplify]: Extracting #6: cost 183 inf + 485027
13.872 * * [simplify]: Extracting #7: cost 7 inf + 802587
13.941 * * [simplify]: Extracting #8: cost 0 inf + 816574
14.003 * [simplify]: Simplified to (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))
14.003 * [simplify]: Simplified (2 2) to (λ (a b c) (*.p16 (/.p16 c (*.p16 (real->posit16 2) a)) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
14.003 * * * * [progress]: [ 7 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b))))>
14.003 * [simplify]: Simplifying (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
14.003 * * [simplify]: iters left: 4 (7 enodes)
14.005 * * [simplify]: iters left: 3 (16 enodes)
14.008 * * [simplify]: iters left: 2 (22 enodes)
14.013 * * [simplify]: iters left: 1 (23 enodes)
14.016 * * [simplify]: Extracting #0: cost 1 inf + 0
14.016 * * [simplify]: Extracting #1: cost 2 inf + 0
14.016 * * [simplify]: Extracting #2: cost 8 inf + 0
14.016 * * [simplify]: Extracting #3: cost 7 inf + 2
14.016 * * [simplify]: Extracting #4: cost 5 inf + 325
14.016 * * [simplify]: Extracting #5: cost 1 inf + 2014
14.016 * * [simplify]: Extracting #6: cost 0 inf + 2336
14.016 * [simplify]: Simplified to (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
14.016 * [simplify]: Simplified (2 2 2 1 1 2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b))))
14.016 * * * * [progress]: [ 8 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b))))>
14.017 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4)))))
14.017 * * [simplify]: iters left: 5 (11 enodes)
14.019 * * [simplify]: iters left: 4 (40 enodes)
14.029 * * [simplify]: iters left: 3 (105 enodes)
14.082 * * [simplify]: iters left: 2 (407 enodes)
14.545 * * [simplify]: Extracting #0: cost 1 inf + 0
14.546 * * [simplify]: Extracting #1: cost 32 inf + 0
14.546 * * [simplify]: Extracting #2: cost 199 inf + 0
14.547 * * [simplify]: Extracting #3: cost 350 inf + 2571
14.554 * * [simplify]: Extracting #4: cost 491 inf + 119933
14.606 * * [simplify]: Extracting #5: cost 190 inf + 693721
14.695 * * [simplify]: Extracting #6: cost 13 inf + 1107241
14.767 * * [simplify]: Extracting #7: cost 0 inf + 1142772
14.872 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))
14.872 * [simplify]: Simplified (2 2 2 1 1 1) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b))))
14.872 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))
14.872 * * [simplify]: iters left: 4 (9 enodes)
14.876 * * [simplify]: iters left: 3 (21 enodes)
14.883 * * [simplify]: iters left: 2 (27 enodes)
14.891 * * [simplify]: iters left: 1 (28 enodes)
14.899 * * [simplify]: Extracting #0: cost 1 inf + 0
14.899 * * [simplify]: Extracting #1: cost 3 inf + 0
14.899 * * [simplify]: Extracting #2: cost 10 inf + 0
14.899 * * [simplify]: Extracting #3: cost 7 inf + 325
14.899 * * [simplify]: Extracting #4: cost 1 inf + 1935
14.899 * * [simplify]: Extracting #5: cost 0 inf + 2939
14.900 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b))
14.900 * [simplify]: Simplified (2 2 2 1 1 2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b)))) b))))
14.900 * * * * [progress]: [ 9 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
14.900 * [simplify]: Simplifying (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
14.900 * * [simplify]: iters left: 6 (16 enodes)
14.908 * * [simplify]: iters left: 5 (52 enodes)
14.929 * * [simplify]: iters left: 4 (184 enodes)
15.005 * * [simplify]: Extracting #0: cost 1 inf + 0
15.006 * * [simplify]: Extracting #1: cost 111 inf + 0
15.006 * * [simplify]: Extracting #2: cost 228 inf + 885
15.007 * * [simplify]: Extracting #3: cost 205 inf + 26545
15.013 * * [simplify]: Extracting #4: cost 135 inf + 166198
15.030 * * [simplify]: Extracting #5: cost 49 inf + 376248
15.062 * * [simplify]: Extracting #6: cost 17 inf + 448959
15.098 * * [simplify]: Extracting #7: cost 0 inf + 464757
15.133 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
15.133 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
15.134 * * * * [progress]: [ 10 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
15.134 * [simplify]: Simplifying (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
15.134 * * [simplify]: iters left: 6 (16 enodes)
15.141 * * [simplify]: iters left: 5 (52 enodes)
15.164 * * [simplify]: iters left: 4 (184 enodes)
15.272 * * [simplify]: Extracting #0: cost 1 inf + 0
15.272 * * [simplify]: Extracting #1: cost 111 inf + 0
15.273 * * [simplify]: Extracting #2: cost 228 inf + 885
15.276 * * [simplify]: Extracting #3: cost 205 inf + 26545
15.291 * * [simplify]: Extracting #4: cost 135 inf + 166198
15.319 * * [simplify]: Extracting #5: cost 49 inf + 376248
15.354 * * [simplify]: Extracting #6: cost 17 inf + 448959
15.390 * * [simplify]: Extracting #7: cost 0 inf + 464757
15.427 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
15.427 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
15.427 * * * * [progress]: [ 11 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
15.427 * [simplify]: Simplifying (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
15.428 * * [simplify]: iters left: 6 (16 enodes)
15.435 * * [simplify]: iters left: 5 (52 enodes)
15.459 * * [simplify]: iters left: 4 (184 enodes)
15.568 * * [simplify]: Extracting #0: cost 1 inf + 0
15.568 * * [simplify]: Extracting #1: cost 111 inf + 0
15.569 * * [simplify]: Extracting #2: cost 228 inf + 885
15.575 * * [simplify]: Extracting #3: cost 205 inf + 26545
15.586 * * [simplify]: Extracting #4: cost 135 inf + 166198
15.615 * * [simplify]: Extracting #5: cost 49 inf + 376248
15.649 * * [simplify]: Extracting #6: cost 17 inf + 448959
15.686 * * [simplify]: Extracting #7: cost 0 inf + 464757
15.725 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
15.725 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
15.725 * * * * [progress]: [ 12 / 12 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
15.725 * [simplify]: Simplifying (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
15.725 * * [simplify]: iters left: 6 (16 enodes)
15.734 * * [simplify]: iters left: 5 (52 enodes)
15.755 * * [simplify]: iters left: 4 (184 enodes)
15.867 * * [simplify]: Extracting #0: cost 1 inf + 0
15.867 * * [simplify]: Extracting #1: cost 111 inf + 0
15.868 * * [simplify]: Extracting #2: cost 228 inf + 885
15.871 * * [simplify]: Extracting #3: cost 205 inf + 26545
15.882 * * [simplify]: Extracting #4: cost 135 inf + 166198
15.910 * * [simplify]: Extracting #5: cost 49 inf + 376248
15.947 * * [simplify]: Extracting #6: cost 17 inf + 448959
15.984 * * [simplify]: Extracting #7: cost 0 inf + 464757
16.022 * [simplify]: Simplified to (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))
16.022 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
16.023 * * * [progress]: adding candidates to table
16.633 * [progress]: [Phase 3 of 3] Extracting.
16.633 * * [regime]: Finding splitpoints for: (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 c (/.p16 (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 4)))))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))> #<alt (λ (a b c) (*.p16 (/.p16 c (*.p16 (real->posit16 2) a)) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (*.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>)
16.643 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
16.643 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 c (/.p16 (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 4)))))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))> #<alt (λ (a b c) (*.p16 (/.p16 c (*.p16 (real->posit16 2) a)) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (*.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>)
17.019 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 c (/.p16 (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 4)))))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))> #<alt (λ (a b c) (*.p16 (/.p16 c (*.p16 (real->posit16 2) a)) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (*.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>)
17.314 * * * * [regimes]: Trying to branch on b from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 c (/.p16 (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 4)))))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))> #<alt (λ (a b c) (*.p16 (/.p16 c (*.p16 (real->posit16 2) a)) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (*.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>)
17.620 * * * [regime]: Found split indices: #<option (#s(si 9 102) #s(si 0 256))>
17.621 * [binary-search]: Improving bounds with binary search for b and (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 c (/.p16 (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 4)))))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))> #<alt (λ (a b c) (*.p16 (/.p16 c (*.p16 (real->posit16 2) a)) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (*.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>)
17.622 * [regimes]: Found splitpoints: (#s(sp 9 b #<cpointer:posit16>) #s(sp 0 b +nan.0)) , with alts (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 c (/.p16 (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 a (real->posit16 4)))))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))> #<alt (λ (a b c) (*.p16 (/.p16 c (*.p16 (real->posit16 2) a)) (/.p16 (*.p16 a (real->posit16 4)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (*.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (*.p16 b b) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>)
17.623 * [simplify]: Simplifying (if (<=.p16 b (real->posit16 -0.1453857421875)) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))
17.623 * * [simplify]: iters left: 6 (28 enodes)
17.626 * * [simplify]: Extracting #0: cost 1 inf + 0
17.626 * * [simplify]: Extracting #1: cost 4 inf + 0
17.626 * * [simplify]: Extracting #2: cost 10 inf + 0
17.626 * * [simplify]: Extracting #3: cost 14 inf + 2
17.626 * * [simplify]: Extracting #4: cost 19 inf + 3
17.626 * * [simplify]: Extracting #5: cost 16 inf + 155
17.627 * * [simplify]: Extracting #6: cost 16 inf + 798
17.627 * * [simplify]: Extracting #7: cost 12 inf + 3169
17.627 * * [simplify]: Extracting #8: cost 9 inf + 5619
17.627 * * [simplify]: Extracting #9: cost 7 inf + 7426
17.627 * * [simplify]: Extracting #10: cost 5 inf + 10835
17.628 * * [simplify]: Extracting #11: cost 3 inf + 13163
17.628 * * [simplify]: Extracting #12: cost 2 inf + 14848
17.628 * * [simplify]: Extracting #13: cost 1 inf + 16973
17.629 * * [simplify]: Extracting #14: cost 0 inf + 21269
17.629 * [simplify]: Simplified to (if (<=.p16 b (real->posit16 -0.1453857421875)) (/.p16 (/.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))
17.629 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
17.666 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
17.669 * * * * [points]: Setting MPFR precision to 64
17.670 * * * * [points]: Setting MPFR precision to 320
17.671 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
17.674 * * * * [points]: Setting MPFR precision to 64
17.676 * * * * [points]: Setting MPFR precision to 320
17.678 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
17.681 * * * * [points]: Setting MPFR precision to 64
17.686 * * * * [points]: Setting MPFR precision to 320
17.690 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
17.693 * * * * [points]: Setting MPFR precision to 64
17.702 * * * * [points]: Setting MPFR precision to 320
17.711 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
17.728 * * * * [points]: Setting MPFR precision to 64
17.749 * * * * [points]: Setting MPFR precision to 320
17.768 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
17.771 * * * * [points]: Setting MPFR precision to 64
17.810 * * * * [points]: Setting MPFR precision to 320
17.847 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
17.849 * * * * [points]: Setting MPFR precision to 64
17.958 * * * * [points]: Setting MPFR precision to 320
18.068 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
18.072 * * * * [points]: Setting MPFR precision to 64
18.280 * * * * [points]: Setting MPFR precision to 320
18.885 * * * * [points]: Computing exacts for 8000 points
18.891 * * * * [points]: Setting MPFR precision to 64
19.829 * * * * [points]: Setting MPFR precision to 320
20.973 * * * * [points]: Filtering points with unrepresentable outputs
21.034 * * * * [points]: Sampled 8000 points with exact outputs
32.265 * [regime-testing]: Baseline error score: 64.0
32.269 * [regime-testing]: Oracle error score: 64.0
32.276 * [regime-testing]: End program error score: 0.5169347459898948