0.004 * [progress]: [Phase 1 of 3] Setting up.
0.007 * * * [progress]: [1/2] Preparing points
0.009 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.013 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.135 * * * * [points]: Setting MPFR precision to 64
0.140 * * * * [points]: Setting MPFR precision to 320
0.143 * * * * [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.160 * * * * [points]: Setting MPFR precision to 64
0.166 * * * * [points]: Setting MPFR precision to 320
0.173 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.178 * * * * [points]: Setting MPFR precision to 64
0.190 * * * * [points]: Setting MPFR precision to 320
0.201 * * * * [points]: Computing exacts for 256 points
0.206 * * * * [points]: Setting MPFR precision to 64
0.239 * * * * [points]: Setting MPFR precision to 320
0.272 * * * * [points]: Filtering points with unrepresentable outputs
0.274 * * * * [points]: Sampled 256 points with exact outputs
0.275 * * * [progress]: [2/2] Setting up program.
0.347 * [progress]: [Phase 2 of 3] Improving.
0.347 * * * * [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.349 * [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.350 * * [simplify]: iters left: 6 (16 enodes)
0.364 * * [simplify]: iters left: 5 (39 enodes)
0.379 * * [simplify]: iters left: 4 (72 enodes)
0.409 * * [simplify]: iters left: 3 (196 enodes)
0.510 * * [simplify]: Extracting #0: cost 1 inf + 0
0.510 * * [simplify]: Extracting #1: cost 5 inf + 0
0.511 * * [simplify]: Extracting #2: cost 11 inf + 1
0.511 * * [simplify]: Extracting #3: cost 16 inf + 2
0.511 * * [simplify]: Extracting #4: cost 26 inf + 807
0.512 * * [simplify]: Extracting #5: cost 66 inf + 1770
0.513 * * [simplify]: Extracting #6: cost 134 inf + 3695
0.515 * * [simplify]: Extracting #7: cost 206 inf + 14082
0.522 * * [simplify]: Extracting #8: cost 137 inf + 107885
0.542 * * [simplify]: Extracting #9: cost 38 inf + 285888
0.569 * * [simplify]: Extracting #10: cost 3 inf + 348921
0.593 * * [simplify]: Extracting #11: cost 0 inf + 357092
0.626 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
0.627 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))
0.670 * * [progress]: iteration 1 / 4
0.670 * * * [progress]: picking best candidate
0.684 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
0.684 * * * [progress]: localizing error
0.862 * * * [progress]: generating rewritten candidates
0.862 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.865 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
0.877 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
0.882 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
0.884 * * * [progress]: generating series expansions
0.884 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.884 * * * * [progress]: [ 2 / 4 ] generating series at (2)
0.884 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
0.884 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
0.884 * * * [progress]: simplifying candidates
0.884 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))>
0.884 * [simplify]: Simplifying (neg.p16 b)
0.884 * * [simplify]: iters left: 1 (2 enodes)
0.885 * * [simplify]: Extracting #0: cost 1 inf + 0
0.885 * * [simplify]: Extracting #1: cost 2 inf + 0
0.885 * * [simplify]: Extracting #2: cost 1 inf + 1
0.885 * * [simplify]: Extracting #3: cost 0 inf + 82
0.885 * [simplify]: Simplified to (neg.p16 b)
0.885 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))
0.885 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))>
0.885 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))
0.885 * * [simplify]: iters left: 6 (12 enodes)
0.888 * * [simplify]: iters left: 5 (39 enodes)
0.896 * * [simplify]: iters left: 4 (111 enodes)
0.941 * * [simplify]: iters left: 3 (422 enodes)
1.219 * * [simplify]: Extracting #0: cost 1 inf + 0
1.219 * * [simplify]: Extracting #1: cost 45 inf + 0
1.220 * * [simplify]: Extracting #2: cost 218 inf + 0
1.221 * * [simplify]: Extracting #3: cost 370 inf + 2894
1.234 * * [simplify]: Extracting #4: cost 452 inf + 174728
1.275 * * [simplify]: Extracting #5: cost 194 inf + 773405
1.326 * * [simplify]: Extracting #6: cost 9 inf + 1160355
1.400 * * [simplify]: Extracting #7: cost 0 inf + 1181311
1.499 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4)))
1.499 * [simplify]: Simplified (2 1 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))
1.499 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1.499 * * [simplify]: iters left: 5 (11 enodes)
1.503 * * [simplify]: iters left: 4 (30 enodes)
1.508 * * [simplify]: iters left: 3 (62 enodes)
1.522 * * [simplify]: iters left: 2 (181 enodes)
1.619 * * [simplify]: Extracting #0: cost 1 inf + 0
1.619 * * [simplify]: Extracting #1: cost 3 inf + 0
1.619 * * [simplify]: Extracting #2: cost 3 inf + 1
1.619 * * [simplify]: Extracting #3: cost 17 inf + 1
1.619 * * [simplify]: Extracting #4: cost 59 inf + 322
1.620 * * [simplify]: Extracting #5: cost 140 inf + 1287
1.622 * * [simplify]: Extracting #6: cost 197 inf + 13674
1.628 * * [simplify]: Extracting #7: cost 148 inf + 70160
1.645 * * [simplify]: Extracting #8: cost 22 inf + 301653
1.670 * * [simplify]: Extracting #9: cost 0 inf + 348970
1.696 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
1.696 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))) (*.p16 (real->posit16 2) a)))
1.696 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
1.697 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
1.697 * * [simplify]: iters left: 6 (14 enodes)
1.702 * * [simplify]: iters left: 5 (39 enodes)
1.712 * * [simplify]: iters left: 4 (82 enodes)
1.730 * * [simplify]: iters left: 3 (290 enodes)
1.913 * * [simplify]: Extracting #0: cost 1 inf + 0
1.913 * * [simplify]: Extracting #1: cost 20 inf + 0
1.913 * * [simplify]: Extracting #2: cost 96 inf + 0
1.914 * * [simplify]: Extracting #3: cost 169 inf + 1046
1.916 * * [simplify]: Extracting #4: cost 227 inf + 7305
1.920 * * [simplify]: Extracting #5: cost 249 inf + 62943
1.949 * * [simplify]: Extracting #6: cost 153 inf + 344310
1.980 * * [simplify]: Extracting #7: cost 8 inf + 619712
2.016 * * [simplify]: Extracting #8: cost 0 inf + 637660
2.042 * * [simplify]: Extracting #9: cost 0 inf + 637340
2.070 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
2.070 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2)) a))
2.070 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))>
2.070 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))
2.070 * * [simplify]: iters left: 6 (15 enodes)
2.076 * * [simplify]: iters left: 5 (45 enodes)
2.086 * * [simplify]: iters left: 4 (105 enodes)
2.107 * * [simplify]: iters left: 3 (240 enodes)
2.221 * * [simplify]: Extracting #0: cost 1 inf + 0
2.222 * * [simplify]: Extracting #1: cost 21 inf + 0
2.222 * * [simplify]: Extracting #2: cost 27 inf + 1
2.222 * * [simplify]: Extracting #3: cost 24 inf + 326
2.222 * * [simplify]: Extracting #4: cost 35 inf + 1613
2.222 * * [simplify]: Extracting #5: cost 76 inf + 1934
2.223 * * [simplify]: Extracting #6: cost 154 inf + 3859
2.224 * * [simplify]: Extracting #7: cost 223 inf + 10912
2.227 * * [simplify]: Extracting #8: cost 165 inf + 84380
2.237 * * [simplify]: Extracting #9: cost 51 inf + 283434
2.261 * * [simplify]: Extracting #10: cost 3 inf + 373922
2.280 * * [simplify]: Extracting #11: cost 0 inf + 380294
2.299 * [simplify]: Simplified to (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 a (real->posit16 2)))
2.299 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 a (real->posit16 2)))))
2.299 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
2.299 * [simplify]: Simplifying (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
2.300 * * [simplify]: iters left: 3 (7 enodes)
2.303 * * [simplify]: iters left: 2 (16 enodes)
2.308 * * [simplify]: iters left: 1 (22 enodes)
2.315 * * [simplify]: Extracting #0: cost 1 inf + 0
2.315 * * [simplify]: Extracting #1: cost 2 inf + 0
2.315 * * [simplify]: Extracting #2: cost 8 inf + 0
2.315 * * [simplify]: Extracting #3: cost 7 inf + 2
2.315 * * [simplify]: Extracting #4: cost 0 inf + 2336
2.315 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 a c) (real->posit16 4)))
2.315 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 a c) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))
2.315 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
2.316 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4))))
2.316 * * [simplify]: iters left: 4 (11 enodes)
2.319 * * [simplify]: iters left: 3 (40 enodes)
2.329 * * [simplify]: iters left: 2 (100 enodes)
2.354 * * [simplify]: iters left: 1 (362 enodes)
2.617 * * [simplify]: Extracting #0: cost 1 inf + 0
2.617 * * [simplify]: Extracting #1: cost 32 inf + 0
2.618 * * [simplify]: Extracting #2: cost 201 inf + 0
2.621 * * [simplify]: Extracting #3: cost 322 inf + 3534
2.630 * * [simplify]: Extracting #4: cost 446 inf + 85826
2.684 * * [simplify]: Extracting #5: cost 150 inf + 651907
2.741 * * [simplify]: Extracting #6: cost 18 inf + 952407
2.825 * * [simplify]: Extracting #7: cost 0 inf + 997559
2.879 * * [simplify]: Extracting #8: cost 0 inf + 994839
2.943 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))
2.943 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))
2.944 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))
2.944 * * [simplify]: iters left: 3 (9 enodes)
2.949 * * [simplify]: iters left: 2 (21 enodes)
2.955 * * [simplify]: iters left: 1 (27 enodes)
2.966 * * [simplify]: Extracting #0: cost 1 inf + 0
2.966 * * [simplify]: Extracting #1: cost 3 inf + 0
2.966 * * [simplify]: Extracting #2: cost 10 inf + 0
2.966 * * [simplify]: Extracting #3: cost 7 inf + 325
2.966 * * [simplify]: Extracting #4: cost 5 inf + 647
2.966 * * [simplify]: Extracting #5: cost 1 inf + 2617
2.966 * * [simplify]: Extracting #6: cost 0 inf + 2939
2.967 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
2.967 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)))) b) (*.p16 (real->posit16 2) a)))
2.967 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
2.967 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
2.968 * * [simplify]: iters left: 6 (15 enodes)
2.975 * * [simplify]: iters left: 5 (43 enodes)
2.991 * * [simplify]: iters left: 4 (88 enodes)
3.027 * * [simplify]: iters left: 3 (308 enodes)
3.169 * * [simplify]: Extracting #0: cost 1 inf + 0
3.169 * * [simplify]: Extracting #1: cost 31 inf + 0
3.170 * * [simplify]: Extracting #2: cost 125 inf + 1
3.170 * * [simplify]: Extracting #3: cost 192 inf + 3056
3.171 * * [simplify]: Extracting #4: cost 252 inf + 8914
3.174 * * [simplify]: Extracting #5: cost 288 inf + 55001
3.190 * * [simplify]: Extracting #6: cost 174 inf + 365952
3.230 * * [simplify]: Extracting #7: cost 7 inf + 676616
3.682 * * [simplify]: Extracting #8: cost 0 inf + 688601
3.713 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
3.713 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
3.713 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
3.714 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
3.714 * * [simplify]: iters left: 6 (15 enodes)
3.722 * * [simplify]: iters left: 5 (43 enodes)
3.737 * * [simplify]: iters left: 4 (88 enodes)
3.772 * * [simplify]: iters left: 3 (308 enodes)
3.923 * * [simplify]: Extracting #0: cost 1 inf + 0
3.923 * * [simplify]: Extracting #1: cost 31 inf + 0
3.923 * * [simplify]: Extracting #2: cost 125 inf + 1
3.924 * * [simplify]: Extracting #3: cost 192 inf + 3056
3.925 * * [simplify]: Extracting #4: cost 252 inf + 8914
3.927 * * [simplify]: Extracting #5: cost 288 inf + 55001
3.953 * * [simplify]: Extracting #6: cost 174 inf + 365952
4.009 * * [simplify]: Extracting #7: cost 7 inf + 676616
4.066 * * [simplify]: Extracting #8: cost 0 inf + 688601
4.114 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
4.114 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
4.114 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
4.114 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
4.115 * * [simplify]: iters left: 6 (15 enodes)
4.119 * * [simplify]: iters left: 5 (43 enodes)
4.127 * * [simplify]: iters left: 4 (88 enodes)
4.147 * * [simplify]: iters left: 3 (308 enodes)
4.306 * * [simplify]: Extracting #0: cost 1 inf + 0
4.306 * * [simplify]: Extracting #1: cost 31 inf + 0
4.307 * * [simplify]: Extracting #2: cost 125 inf + 1
4.307 * * [simplify]: Extracting #3: cost 192 inf + 3056
4.308 * * [simplify]: Extracting #4: cost 252 inf + 8914
4.311 * * [simplify]: Extracting #5: cost 288 inf + 55001
4.325 * * [simplify]: Extracting #6: cost 174 inf + 365952
4.351 * * [simplify]: Extracting #7: cost 7 inf + 676616
4.407 * * [simplify]: Extracting #8: cost 0 inf + 688601
4.458 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
4.458 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
4.458 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
4.458 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
4.458 * * [simplify]: iters left: 6 (15 enodes)
4.462 * * [simplify]: iters left: 5 (43 enodes)
4.470 * * [simplify]: iters left: 4 (88 enodes)
4.502 * * [simplify]: iters left: 3 (308 enodes)
4.697 * * [simplify]: Extracting #0: cost 1 inf + 0
4.697 * * [simplify]: Extracting #1: cost 31 inf + 0
4.697 * * [simplify]: Extracting #2: cost 125 inf + 1
4.699 * * [simplify]: Extracting #3: cost 192 inf + 3056
4.701 * * [simplify]: Extracting #4: cost 252 inf + 8914
4.705 * * [simplify]: Extracting #5: cost 288 inf + 55001
4.730 * * [simplify]: Extracting #6: cost 174 inf + 365952
4.758 * * [simplify]: Extracting #7: cost 7 inf + 676616
4.793 * * [simplify]: Extracting #8: cost 0 inf + 688601
4.837 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
4.838 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
4.838 * * * [progress]: adding candidates to table
5.209 * * [progress]: iteration 2 / 4
5.209 * * * [progress]: picking best candidate
5.293 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
5.293 * * * [progress]: localizing error
5.567 * * * [progress]: generating rewritten candidates
5.567 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
5.571 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1)
5.591 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
5.592 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 1 2)
5.599 * * * [progress]: generating series expansions
5.599 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
5.599 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1)
5.599 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
5.599 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 1 2)
5.599 * * * [progress]: simplifying candidates
5.599 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (real->posit16 2)) a))>
5.600 * [simplify]: Simplifying (neg.p16 b)
5.600 * * [simplify]: iters left: 1 (2 enodes)
5.601 * * [simplify]: Extracting #0: cost 1 inf + 0
5.601 * * [simplify]: Extracting #1: cost 2 inf + 0
5.601 * * [simplify]: Extracting #2: cost 1 inf + 1
5.601 * * [simplify]: Extracting #3: cost 0 inf + 82
5.601 * [simplify]: Simplified to (neg.p16 b)
5.601 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (real->posit16 2)) a))
5.601 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
5.601 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))
5.601 * * [simplify]: iters left: 6 (12 enodes)
5.609 * * [simplify]: iters left: 5 (39 enodes)
5.624 * * [simplify]: iters left: 4 (111 enodes)
5.679 * * [simplify]: iters left: 3 (422 enodes)
6.009 * * [simplify]: Extracting #0: cost 1 inf + 0
6.009 * * [simplify]: Extracting #1: cost 45 inf + 0
6.010 * * [simplify]: Extracting #2: cost 218 inf + 0
6.011 * * [simplify]: Extracting #3: cost 370 inf + 2894
6.017 * * [simplify]: Extracting #4: cost 452 inf + 174728
6.056 * * [simplify]: Extracting #5: cost 194 inf + 773405
6.133 * * [simplify]: Extracting #6: cost 9 inf + 1160355
6.226 * * [simplify]: Extracting #7: cost 0 inf + 1181311
6.307 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4)))
6.307 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))
6.307 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
6.307 * * [simplify]: iters left: 5 (11 enodes)
6.313 * * [simplify]: iters left: 4 (30 enodes)
6.325 * * [simplify]: iters left: 3 (62 enodes)
6.350 * * [simplify]: iters left: 2 (181 enodes)
6.453 * * [simplify]: Extracting #0: cost 1 inf + 0
6.453 * * [simplify]: Extracting #1: cost 3 inf + 0
6.453 * * [simplify]: Extracting #2: cost 3 inf + 1
6.453 * * [simplify]: Extracting #3: cost 17 inf + 1
6.453 * * [simplify]: Extracting #4: cost 59 inf + 322
6.453 * * [simplify]: Extracting #5: cost 140 inf + 1287
6.454 * * [simplify]: Extracting #6: cost 197 inf + 13674
6.457 * * [simplify]: Extracting #7: cost 148 inf + 70160
6.466 * * [simplify]: Extracting #8: cost 22 inf + 301653
6.479 * * [simplify]: Extracting #9: cost 0 inf + 348970
6.493 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
6.493 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))) (real->posit16 2)) a))
6.493 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))>
6.493 * [simplify]: Simplifying (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
6.493 * * [simplify]: iters left: 3 (7 enodes)
6.495 * * [simplify]: iters left: 2 (16 enodes)
6.497 * * [simplify]: iters left: 1 (22 enodes)
6.501 * * [simplify]: Extracting #0: cost 1 inf + 0
6.501 * * [simplify]: Extracting #1: cost 2 inf + 0
6.501 * * [simplify]: Extracting #2: cost 8 inf + 0
6.501 * * [simplify]: Extracting #3: cost 7 inf + 2
6.501 * * [simplify]: Extracting #4: cost 0 inf + 2336
6.501 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 a c) (real->posit16 4)))
6.501 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 a c) (real->posit16 4))))) b) (real->posit16 2)) a))
6.502 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))>
6.502 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4))))
6.502 * * [simplify]: iters left: 4 (11 enodes)
6.511 * * [simplify]: iters left: 3 (40 enodes)
6.526 * * [simplify]: iters left: 2 (100 enodes)
6.574 * * [simplify]: iters left: 1 (362 enodes)
6.880 * * [simplify]: Extracting #0: cost 1 inf + 0
6.880 * * [simplify]: Extracting #1: cost 32 inf + 0
6.881 * * [simplify]: Extracting #2: cost 201 inf + 0
6.883 * * [simplify]: Extracting #3: cost 322 inf + 3534
6.893 * * [simplify]: Extracting #4: cost 446 inf + 85826
6.946 * * [simplify]: Extracting #5: cost 150 inf + 651907
7.026 * * [simplify]: Extracting #6: cost 18 inf + 952407
7.090 * * [simplify]: Extracting #7: cost 0 inf + 997559
7.155 * * [simplify]: Extracting #8: cost 0 inf + 994839
7.200 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))
7.200 * [simplify]: Simplified (2 1 1 1 1 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))
7.201 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))
7.201 * * [simplify]: iters left: 3 (9 enodes)
7.205 * * [simplify]: iters left: 2 (21 enodes)
7.214 * * [simplify]: iters left: 1 (27 enodes)
7.222 * * [simplify]: Extracting #0: cost 1 inf + 0
7.222 * * [simplify]: Extracting #1: cost 3 inf + 0
7.222 * * [simplify]: Extracting #2: cost 10 inf + 0
7.222 * * [simplify]: Extracting #3: cost 7 inf + 325
7.222 * * [simplify]: Extracting #4: cost 5 inf + 647
7.223 * * [simplify]: Extracting #5: cost 1 inf + 2617
7.223 * * [simplify]: Extracting #6: cost 0 inf + 2939
7.223 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
7.223 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)))) b) (real->posit16 2)) a))
7.223 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
7.224 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
7.224 * * [simplify]: iters left: 2 (4 enodes)
7.226 * * [simplify]: iters left: 1 (8 enodes)
7.229 * * [simplify]: Extracting #0: cost 1 inf + 0
7.229 * * [simplify]: Extracting #1: cost 3 inf + 0
7.229 * * [simplify]: Extracting #2: cost 3 inf + 1
7.229 * * [simplify]: Extracting #3: cost 0 inf + 325
7.229 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
7.229 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
7.229 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (real->posit16 2)) a))>
7.230 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
7.230 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
7.230 * * [simplify]: iters left: 6 (14 enodes)
7.237 * * [simplify]: iters left: 5 (39 enodes)
7.252 * * [simplify]: iters left: 4 (82 enodes)
7.272 * * [simplify]: iters left: 3 (290 enodes)
7.408 * * [simplify]: Extracting #0: cost 1 inf + 0
7.408 * * [simplify]: Extracting #1: cost 20 inf + 0
7.408 * * [simplify]: Extracting #2: cost 96 inf + 0
7.408 * * [simplify]: Extracting #3: cost 169 inf + 1046
7.409 * * [simplify]: Extracting #4: cost 227 inf + 7305
7.412 * * [simplify]: Extracting #5: cost 249 inf + 62943
7.437 * * [simplify]: Extracting #6: cost 153 inf + 344310
7.464 * * [simplify]: Extracting #7: cost 8 inf + 619712
7.507 * * [simplify]: Extracting #8: cost 0 inf + 637660
7.556 * * [simplify]: Extracting #9: cost 0 inf + 637340
7.598 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
7.599 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2)) a))
7.599 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
7.599 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
7.599 * * [simplify]: iters left: 6 (14 enodes)
7.606 * * [simplify]: iters left: 5 (39 enodes)
7.620 * * [simplify]: iters left: 4 (82 enodes)
7.656 * * [simplify]: iters left: 3 (290 enodes)
7.808 * * [simplify]: Extracting #0: cost 1 inf + 0
7.808 * * [simplify]: Extracting #1: cost 20 inf + 0
7.808 * * [simplify]: Extracting #2: cost 96 inf + 0
7.809 * * [simplify]: Extracting #3: cost 169 inf + 1046
7.811 * * [simplify]: Extracting #4: cost 227 inf + 7305
7.814 * * [simplify]: Extracting #5: cost 249 inf + 62943
7.827 * * [simplify]: Extracting #6: cost 153 inf + 344310
7.852 * * [simplify]: Extracting #7: cost 8 inf + 619712
7.910 * * [simplify]: Extracting #8: cost 0 inf + 637660
7.964 * * [simplify]: Extracting #9: cost 0 inf + 637340
8.018 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
8.019 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2)) a))
8.019 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
8.019 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
8.019 * * [simplify]: iters left: 6 (14 enodes)
8.026 * * [simplify]: iters left: 5 (39 enodes)
8.042 * * [simplify]: iters left: 4 (82 enodes)
8.075 * * [simplify]: iters left: 3 (290 enodes)
8.198 * * [simplify]: Extracting #0: cost 1 inf + 0
8.198 * * [simplify]: Extracting #1: cost 20 inf + 0
8.198 * * [simplify]: Extracting #2: cost 96 inf + 0
8.198 * * [simplify]: Extracting #3: cost 169 inf + 1046
8.199 * * [simplify]: Extracting #4: cost 227 inf + 7305
8.202 * * [simplify]: Extracting #5: cost 249 inf + 62943
8.214 * * [simplify]: Extracting #6: cost 153 inf + 344310
8.249 * * [simplify]: Extracting #7: cost 8 inf + 619712
8.285 * * [simplify]: Extracting #8: cost 0 inf + 637660
8.326 * * [simplify]: Extracting #9: cost 0 inf + 637340
8.370 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
8.370 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2)) a))
8.370 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
8.371 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
8.371 * * [simplify]: iters left: 6 (14 enodes)
8.378 * * [simplify]: iters left: 5 (39 enodes)
8.393 * * [simplify]: iters left: 4 (82 enodes)
8.429 * * [simplify]: iters left: 3 (290 enodes)
8.584 * * [simplify]: Extracting #0: cost 1 inf + 0
8.584 * * [simplify]: Extracting #1: cost 20 inf + 0
8.585 * * [simplify]: Extracting #2: cost 96 inf + 0
8.586 * * [simplify]: Extracting #3: cost 169 inf + 1046
8.587 * * [simplify]: Extracting #4: cost 227 inf + 7305
8.592 * * [simplify]: Extracting #5: cost 249 inf + 62943
8.605 * * [simplify]: Extracting #6: cost 153 inf + 344310
8.636 * * [simplify]: Extracting #7: cost 8 inf + 619712
8.675 * * [simplify]: Extracting #8: cost 0 inf + 637660
8.717 * * [simplify]: Extracting #9: cost 0 inf + 637340
8.755 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
8.755 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2)) a))
8.755 * * * [progress]: adding candidates to table
9.093 * * [progress]: iteration 3 / 4
9.093 * * * [progress]: picking best candidate
9.193 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
9.194 * * * [progress]: localizing error
9.479 * * * [progress]: generating rewritten candidates
9.479 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
9.482 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1)
9.492 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
9.492 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
9.499 * * * [progress]: generating series expansions
9.499 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
9.499 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1)
9.499 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
9.499 * * * * [progress]: [ 4 / 4 ] generating series at (2)
9.499 * * * [progress]: simplifying candidates
9.499 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (real->posit16 2)) a))>
9.500 * [simplify]: Simplifying (neg.p16 b)
9.500 * * [simplify]: iters left: 1 (2 enodes)
9.501 * * [simplify]: Extracting #0: cost 1 inf + 0
9.501 * * [simplify]: Extracting #1: cost 2 inf + 0
9.501 * * [simplify]: Extracting #2: cost 1 inf + 1
9.501 * * [simplify]: Extracting #3: cost 0 inf + 82
9.501 * [simplify]: Simplified to (neg.p16 b)
9.501 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (real->posit16 2)) a))
9.501 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.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)) (real->posit16 2)) a))>
9.501 * [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))
9.501 * * [simplify]: iters left: 6 (12 enodes)
9.508 * * [simplify]: iters left: 5 (39 enodes)
9.516 * * [simplify]: iters left: 4 (111 enodes)
9.561 * * [simplify]: iters left: 3 (419 enodes)
9.851 * * [simplify]: Extracting #0: cost 1 inf + 0
9.851 * * [simplify]: Extracting #1: cost 45 inf + 0
9.852 * * [simplify]: Extracting #2: cost 218 inf + 0
9.855 * * [simplify]: Extracting #3: cost 372 inf + 3054
9.869 * * [simplify]: Extracting #4: cost 447 inf + 176392
9.935 * * [simplify]: Extracting #5: cost 180 inf + 817643
10.046 * * [simplify]: Extracting #6: cost 4 inf + 1166833
10.155 * * [simplify]: Extracting #7: cost 0 inf + 1177411
10.267 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c))
10.267 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.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)) (real->posit16 2)) a))
10.267 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)
10.267 * * [simplify]: iters left: 6 (11 enodes)
10.273 * * [simplify]: iters left: 5 (30 enodes)
10.284 * * [simplify]: iters left: 4 (62 enodes)
10.310 * * [simplify]: iters left: 3 (175 enodes)
10.402 * * [simplify]: Extracting #0: cost 1 inf + 0
10.403 * * [simplify]: Extracting #1: cost 3 inf + 0
10.403 * * [simplify]: Extracting #2: cost 3 inf + 1
10.403 * * [simplify]: Extracting #3: cost 17 inf + 1
10.403 * * [simplify]: Extracting #4: cost 59 inf + 322
10.404 * * [simplify]: Extracting #5: cost 133 inf + 1287
10.406 * * [simplify]: Extracting #6: cost 197 inf + 12718
10.412 * * [simplify]: Extracting #7: cost 127 inf + 114668
10.436 * * [simplify]: Extracting #8: cost 13 inf + 318519
10.460 * * [simplify]: Extracting #9: cost 0 inf + 342366
10.486 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
10.486 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.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))))) (real->posit16 2)) a))
10.486 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))>
10.487 * [simplify]: Simplifying (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
10.487 * * [simplify]: iters left: 4 (7 enodes)
10.490 * * [simplify]: iters left: 3 (16 enodes)
10.494 * * [simplify]: iters left: 2 (22 enodes)
10.497 * * [simplify]: iters left: 1 (23 enodes)
10.501 * * [simplify]: Extracting #0: cost 1 inf + 0
10.501 * * [simplify]: Extracting #1: cost 2 inf + 0
10.501 * * [simplify]: Extracting #2: cost 8 inf + 0
10.501 * * [simplify]: Extracting #3: cost 7 inf + 2
10.501 * * [simplify]: Extracting #4: cost 5 inf + 325
10.501 * * [simplify]: Extracting #5: cost 1 inf + 2014
10.501 * * [simplify]: Extracting #6: cost 0 inf + 2336
10.501 * [simplify]: Simplified to (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
10.501 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))
10.501 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.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) (real->posit16 2)) a))>
10.502 * [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)))))
10.502 * * [simplify]: iters left: 5 (11 enodes)
10.505 * * [simplify]: iters left: 4 (40 enodes)
10.513 * * [simplify]: iters left: 3 (105 enodes)
10.554 * * [simplify]: iters left: 2 (407 enodes)
10.905 * * [simplify]: Extracting #0: cost 1 inf + 0
10.906 * * [simplify]: Extracting #1: cost 32 inf + 0
10.906 * * [simplify]: Extracting #2: cost 198 inf + 0
10.907 * * [simplify]: Extracting #3: cost 346 inf + 2571
10.917 * * [simplify]: Extracting #4: cost 496 inf + 91867
10.955 * * [simplify]: Extracting #5: cost 168 inf + 732046
11.022 * * [simplify]: Extracting #6: cost 9 inf + 1087233
11.085 * * [simplify]: Extracting #7: cost 0 inf + 1112349
11.156 * [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))))
11.156 * [simplify]: Simplified (2 1 1 1 1 1) to (λ (a b c) (/.p16 (/.p16 (-.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) (real->posit16 2)) a))
11.157 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))
11.157 * * [simplify]: iters left: 4 (9 enodes)
11.161 * * [simplify]: iters left: 3 (21 enodes)
11.170 * * [simplify]: iters left: 2 (27 enodes)
11.178 * * [simplify]: iters left: 1 (28 enodes)
11.187 * * [simplify]: Extracting #0: cost 1 inf + 0
11.187 * * [simplify]: Extracting #1: cost 3 inf + 0
11.187 * * [simplify]: Extracting #2: cost 10 inf + 0
11.187 * * [simplify]: Extracting #3: cost 7 inf + 325
11.187 * * [simplify]: Extracting #4: cost 1 inf + 1935
11.188 * * [simplify]: Extracting #5: cost 0 inf + 2939
11.188 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b))
11.188 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (-.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) (real->posit16 2)) a))
11.188 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
11.189 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
11.189 * * [simplify]: iters left: 2 (4 enodes)
11.191 * * [simplify]: iters left: 1 (8 enodes)
11.193 * * [simplify]: Extracting #0: cost 1 inf + 0
11.194 * * [simplify]: Extracting #1: cost 3 inf + 0
11.194 * * [simplify]: Extracting #2: cost 3 inf + 1
11.194 * * [simplify]: Extracting #3: cost 0 inf + 325
11.194 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
11.194 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
11.194 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
11.194 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
11.194 * * [simplify]: iters left: 2 (4 enodes)
11.196 * * [simplify]: iters left: 1 (8 enodes)
11.199 * * [simplify]: Extracting #0: cost 1 inf + 0
11.199 * * [simplify]: Extracting #1: cost 3 inf + 0
11.199 * * [simplify]: Extracting #2: cost 3 inf + 1
11.199 * * [simplify]: Extracting #3: cost 0 inf + 325
11.199 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.199 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
11.199 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
11.200 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
11.200 * * [simplify]: iters left: 2 (4 enodes)
11.202 * * [simplify]: iters left: 1 (8 enodes)
11.204 * * [simplify]: Extracting #0: cost 1 inf + 0
11.204 * * [simplify]: Extracting #1: cost 3 inf + 0
11.205 * * [simplify]: Extracting #2: cost 3 inf + 1
11.205 * * [simplify]: Extracting #3: cost 0 inf + 325
11.205 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.205 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
11.205 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
11.205 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
11.205 * * [simplify]: iters left: 2 (4 enodes)
11.207 * * [simplify]: iters left: 1 (8 enodes)
11.210 * * [simplify]: Extracting #0: cost 1 inf + 0
11.210 * * [simplify]: Extracting #1: cost 3 inf + 0
11.210 * * [simplify]: Extracting #2: cost 3 inf + 1
11.210 * * [simplify]: Extracting #3: cost 0 inf + 325
11.210 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.210 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
11.210 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
11.211 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
11.211 * * [simplify]: iters left: 2 (4 enodes)
11.213 * * [simplify]: iters left: 1 (8 enodes)
11.216 * * [simplify]: Extracting #0: cost 1 inf + 0
11.216 * * [simplify]: Extracting #1: cost 3 inf + 0
11.216 * * [simplify]: Extracting #2: cost 3 inf + 1
11.216 * * [simplify]: Extracting #3: cost 0 inf + 325
11.216 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.216 * [simplify]: Simplified (2 1 1 1 1 2 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))
11.216 * * * [progress]: adding candidates to table
11.553 * * [progress]: iteration 4 / 4
11.553 * * * [progress]: picking best candidate
11.686 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
11.686 * * * [progress]: localizing error
11.906 * * * [progress]: generating rewritten candidates
11.906 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
11.908 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
11.911 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
11.917 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
11.917 * * * [progress]: generating series expansions
11.917 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
11.917 * * * * [progress]: [ 2 / 4 ] generating series at (2)
11.917 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
11.917 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
11.917 * * * [progress]: simplifying candidates
11.917 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (*.p16 a (real->posit16 2))))>
11.918 * [simplify]: Simplifying (neg.p16 b)
11.918 * * [simplify]: iters left: 1 (2 enodes)
11.918 * * [simplify]: Extracting #0: cost 1 inf + 0
11.918 * * [simplify]: Extracting #1: cost 2 inf + 0
11.918 * * [simplify]: Extracting #2: cost 1 inf + 1
11.918 * * [simplify]: Extracting #3: cost 0 inf + 82
11.918 * [simplify]: Simplified to (neg.p16 b)
11.918 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (*.p16 a (real->posit16 2))))
11.918 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.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)) (*.p16 a (real->posit16 2))))>
11.918 * [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.918 * * [simplify]: iters left: 6 (12 enodes)
11.922 * * [simplify]: iters left: 5 (39 enodes)
11.929 * * [simplify]: iters left: 4 (111 enodes)
11.965 * * [simplify]: iters left: 3 (419 enodes)
12.217 * * [simplify]: Extracting #0: cost 1 inf + 0
12.217 * * [simplify]: Extracting #1: cost 45 inf + 0
12.218 * * [simplify]: Extracting #2: cost 218 inf + 0
12.220 * * [simplify]: Extracting #3: cost 372 inf + 3054
12.234 * * [simplify]: Extracting #4: cost 447 inf + 176392
12.299 * * [simplify]: Extracting #5: cost 180 inf + 817643
12.410 * * [simplify]: Extracting #6: cost 4 inf + 1166833
12.520 * * [simplify]: Extracting #7: cost 0 inf + 1177411
12.633 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c))
12.633 * [simplify]: Simplified (2 1 1) to (λ (a b c) (/.p16 (/.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)) (*.p16 a (real->posit16 2))))
12.633 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)
12.633 * * [simplify]: iters left: 6 (11 enodes)
12.639 * * [simplify]: iters left: 5 (30 enodes)
12.650 * * [simplify]: iters left: 4 (62 enodes)
12.676 * * [simplify]: iters left: 3 (175 enodes)
12.739 * * [simplify]: Extracting #0: cost 1 inf + 0
12.739 * * [simplify]: Extracting #1: cost 3 inf + 0
12.740 * * [simplify]: Extracting #2: cost 3 inf + 1
12.740 * * [simplify]: Extracting #3: cost 17 inf + 1
12.740 * * [simplify]: Extracting #4: cost 59 inf + 322
12.740 * * [simplify]: Extracting #5: cost 133 inf + 1287
12.741 * * [simplify]: Extracting #6: cost 197 inf + 12718
12.745 * * [simplify]: Extracting #7: cost 127 inf + 114668
12.755 * * [simplify]: Extracting #8: cost 13 inf + 318519
12.773 * * [simplify]: Extracting #9: cost 0 inf + 342366
12.787 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
12.787 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (/.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))))) (*.p16 a (real->posit16 2))))
12.787 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))>
12.787 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a)
12.787 * * [simplify]: iters left: 6 (12 enodes)
12.790 * * [simplify]: iters left: 5 (36 enodes)
12.798 * * [simplify]: iters left: 4 (79 enodes)
12.815 * * [simplify]: iters left: 3 (280 enodes)
12.909 * * [simplify]: Extracting #0: cost 1 inf + 0
12.909 * * [simplify]: Extracting #1: cost 20 inf + 0
12.910 * * [simplify]: Extracting #2: cost 94 inf + 1
12.910 * * [simplify]: Extracting #3: cost 166 inf + 1768
12.911 * * [simplify]: Extracting #4: cost 226 inf + 6981
12.913 * * [simplify]: Extracting #5: cost 246 inf + 63504
12.927 * * [simplify]: Extracting #6: cost 139 inf + 360206
12.952 * * [simplify]: Extracting #7: cost 3 inf + 617210
12.979 * * [simplify]: Extracting #8: cost 0 inf + 625421
13.005 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) b) a)
13.006 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) b) a) (real->posit16 2)))
13.006 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.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 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
13.006 * [simplify]: Simplifying (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))
13.006 * * [simplify]: iters left: 6 (15 enodes)
13.010 * * [simplify]: iters left: 5 (45 enodes)
13.019 * * [simplify]: iters left: 4 (105 enodes)
13.050 * * [simplify]: iters left: 3 (235 enodes)
13.196 * * [simplify]: Extracting #0: cost 1 inf + 0
13.196 * * [simplify]: Extracting #1: cost 23 inf + 0
13.196 * * [simplify]: Extracting #2: cost 29 inf + 1
13.197 * * [simplify]: Extracting #3: cost 28 inf + 3
13.197 * * [simplify]: Extracting #4: cost 38 inf + 970
13.198 * * [simplify]: Extracting #5: cost 78 inf + 1934
13.199 * * [simplify]: Extracting #6: cost 156 inf + 2576
13.201 * * [simplify]: Extracting #7: cost 239 inf + 9312
13.213 * * [simplify]: Extracting #8: cost 124 inf + 200111
13.246 * * [simplify]: Extracting #9: cost 14 inf + 413653
13.275 * * [simplify]: Extracting #10: cost 0 inf + 408188
13.307 * * [simplify]: Extracting #11: cost 0 inf + 406268
13.338 * [simplify]: Simplified to (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2)))
13.338 * [simplify]: Simplified (2 2) to (λ (a b c) (/.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 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2)))))
13.339 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))>
13.339 * [simplify]: Simplifying (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
13.339 * * [simplify]: iters left: 4 (7 enodes)
13.342 * * [simplify]: iters left: 3 (16 enodes)
13.347 * * [simplify]: iters left: 2 (22 enodes)
13.353 * * [simplify]: iters left: 1 (23 enodes)
13.359 * * [simplify]: Extracting #0: cost 1 inf + 0
13.359 * * [simplify]: Extracting #1: cost 2 inf + 0
13.359 * * [simplify]: Extracting #2: cost 8 inf + 0
13.359 * * [simplify]: Extracting #3: cost 7 inf + 2
13.359 * * [simplify]: Extracting #4: cost 5 inf + 325
13.360 * * [simplify]: Extracting #5: cost 1 inf + 2014
13.360 * * [simplify]: Extracting #6: cost 0 inf + 2336
13.360 * [simplify]: Simplified to (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
13.360 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 a (real->posit16 2))))
13.360 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.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) (*.p16 a (real->posit16 2))))>
13.360 * [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)))))
13.361 * * [simplify]: iters left: 5 (11 enodes)
13.365 * * [simplify]: iters left: 4 (40 enodes)
13.380 * * [simplify]: iters left: 3 (105 enodes)
13.438 * * [simplify]: iters left: 2 (407 enodes)
13.771 * * [simplify]: Extracting #0: cost 1 inf + 0
13.772 * * [simplify]: Extracting #1: cost 32 inf + 0
13.772 * * [simplify]: Extracting #2: cost 198 inf + 0
13.773 * * [simplify]: Extracting #3: cost 346 inf + 2571
13.781 * * [simplify]: Extracting #4: cost 496 inf + 91867
13.842 * * [simplify]: Extracting #5: cost 168 inf + 732046
13.910 * * [simplify]: Extracting #6: cost 9 inf + 1087233
13.974 * * [simplify]: Extracting #7: cost 0 inf + 1112349
14.078 * [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.078 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b c) (/.p16 (-.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) (*.p16 a (real->posit16 2))))
14.078 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))
14.079 * * [simplify]: iters left: 4 (9 enodes)
14.083 * * [simplify]: iters left: 3 (21 enodes)
14.090 * * [simplify]: iters left: 2 (27 enodes)
14.098 * * [simplify]: iters left: 1 (28 enodes)
14.105 * * [simplify]: Extracting #0: cost 1 inf + 0
14.105 * * [simplify]: Extracting #1: cost 3 inf + 0
14.106 * * [simplify]: Extracting #2: cost 10 inf + 0
14.106 * * [simplify]: Extracting #3: cost 7 inf + 325
14.106 * * [simplify]: Extracting #4: cost 1 inf + 1935
14.106 * * [simplify]: Extracting #5: cost 0 inf + 2939
14.106 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b))
14.106 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (-.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) (*.p16 a (real->posit16 2))))
14.107 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
14.107 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
14.107 * * [simplify]: iters left: 2 (4 enodes)
14.109 * * [simplify]: iters left: 1 (8 enodes)
14.112 * * [simplify]: Extracting #0: cost 1 inf + 0
14.112 * * [simplify]: Extracting #1: cost 3 inf + 0
14.112 * * [simplify]: Extracting #2: cost 3 inf + 1
14.112 * * [simplify]: Extracting #3: cost 0 inf + 325
14.112 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
14.112 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
14.112 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
14.113 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
14.113 * * [simplify]: iters left: 2 (4 enodes)
14.115 * * [simplify]: iters left: 1 (8 enodes)
14.117 * * [simplify]: Extracting #0: cost 1 inf + 0
14.117 * * [simplify]: Extracting #1: cost 3 inf + 0
14.117 * * [simplify]: Extracting #2: cost 3 inf + 1
14.117 * * [simplify]: Extracting #3: cost 0 inf + 325
14.118 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
14.118 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
14.118 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
14.118 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
14.118 * * [simplify]: iters left: 2 (4 enodes)
14.120 * * [simplify]: iters left: 1 (8 enodes)
14.123 * * [simplify]: Extracting #0: cost 1 inf + 0
14.123 * * [simplify]: Extracting #1: cost 3 inf + 0
14.123 * * [simplify]: Extracting #2: cost 3 inf + 1
14.123 * * [simplify]: Extracting #3: cost 0 inf + 325
14.123 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
14.123 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
14.123 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
14.123 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
14.123 * * [simplify]: iters left: 2 (4 enodes)
14.125 * * [simplify]: iters left: 1 (8 enodes)
14.128 * * [simplify]: Extracting #0: cost 1 inf + 0
14.128 * * [simplify]: Extracting #1: cost 3 inf + 0
14.128 * * [simplify]: Extracting #2: cost 3 inf + 1
14.128 * * [simplify]: Extracting #3: cost 0 inf + 325
14.128 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
14.128 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))
14.129 * * * [progress]: adding candidates to table
14.540 * [progress]: [Phase 3 of 3] Extracting.
14.541 * * [regime]: Finding splitpoints for: (#<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.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 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.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)) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (-.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) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.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)) (real->posit16 2)) a))>)
14.546 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
14.547 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.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 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.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)) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (-.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) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.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)) (real->posit16 2)) a))>)
14.762 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.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 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.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)) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (-.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) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.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)) (real->posit16 2)) a))>)
14.970 * * * * [regimes]: Trying to branch on b from (#<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.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 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.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)) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (-.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) (*.p16 a (real->posit16 2))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.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)) (real->posit16 2)) a))>)
15.225 * * * [regime]: Found split indices: #<option (#s(si 3 256))>
15.225 * [simplify]: Simplifying (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2))
15.225 * * [simplify]: iters left: 6 (15 enodes)
15.227 * * [simplify]: Extracting #0: cost 1 inf + 0
15.227 * * [simplify]: Extracting #1: cost 3 inf + 0
15.227 * * [simplify]: Extracting #2: cost 6 inf + 0
15.227 * * [simplify]: Extracting #3: cost 5 inf + 3
15.227 * * [simplify]: Extracting #4: cost 5 inf + 4
15.227 * * [simplify]: Extracting #5: cost 7 inf + 4
15.227 * * [simplify]: Extracting #6: cost 8 inf + 325
15.227 * * [simplify]: Extracting #7: cost 8 inf + 326
15.227 * * [simplify]: Extracting #8: cost 9 inf + 326
15.227 * * [simplify]: Extracting #9: cost 7 inf + 328
15.227 * * [simplify]: Extracting #10: cost 5 inf + 1293
15.227 * * [simplify]: Extracting #11: cost 3 inf + 3421
15.227 * * [simplify]: Extracting #12: cost 1 inf + 6189
15.227 * * [simplify]: Extracting #13: cost 0 inf + 8234
15.228 * [simplify]: Simplified to (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2))
15.228 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
15.261 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
15.266 * * * * [points]: Setting MPFR precision to 64
15.268 * * * * [points]: Setting MPFR precision to 320
15.270 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
15.274 * * * * [points]: Setting MPFR precision to 64
15.278 * * * * [points]: Setting MPFR precision to 320
15.282 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
15.287 * * * * [points]: Setting MPFR precision to 64
15.295 * * * * [points]: Setting MPFR precision to 320
15.302 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
15.305 * * * * [points]: Setting MPFR precision to 64
15.314 * * * * [points]: Setting MPFR precision to 320
15.323 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
15.326 * * * * [points]: Setting MPFR precision to 64
15.358 * * * * [points]: Setting MPFR precision to 320
15.378 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
15.384 * * * * [points]: Setting MPFR precision to 64
15.446 * * * * [points]: Setting MPFR precision to 320
15.485 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
15.488 * * * * [points]: Setting MPFR precision to 64
15.652 * * * * [points]: Setting MPFR precision to 320
15.811 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
15.814 * * * * [points]: Setting MPFR precision to 64
16.029 * * * * [points]: Setting MPFR precision to 320
16.239 * * * * [points]: Computing exacts for 8000 points
16.244 * * * * [points]: Setting MPFR precision to 64
17.288 * * * * [points]: Setting MPFR precision to 320
18.373 * * * * [points]: Filtering points with unrepresentable outputs
18.443 * * * * [points]: Sampled 8000 points with exact outputs
25.724 * [regime-testing]: Baseline error score: 64.0
25.730 * [regime-testing]: Oracle error score: 64.0
25.743 * [regime-testing]: End program error score: 1.53861151671579