0.002 * [progress]: [Phase 1 of 3] Setting up.
0.003 * * * [progress]: [1/2] Preparing points
0.005 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.008 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.215 * * * * [points]: Setting MPFR precision to 64
0.220 * * * * [points]: Setting MPFR precision to 320
0.224 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.264 * * * * [points]: Setting MPFR precision to 64
0.269 * * * * [points]: Setting MPFR precision to 320
0.275 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.283 * * * * [points]: Setting MPFR precision to 64
0.290 * * * * [points]: Setting MPFR precision to 320
0.297 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.303 * * * * [points]: Setting MPFR precision to 64
0.348 * * * * [points]: Setting MPFR precision to 320
0.364 * * * * [points]: Computing exacts for 256 points
0.372 * * * * [points]: Setting MPFR precision to 64
0.439 * * * * [points]: Setting MPFR precision to 320
0.470 * * * * [points]: Filtering points with unrepresentable outputs
0.472 * * * * [points]: Sampled 256 points with exact outputs
0.472 * * * [progress]: [2/2] Setting up program.
0.602 * [progress]: [Phase 2 of 3] Improving.
0.602 * * * * [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.604 * [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.641 * * [simplify]: iters left: 6 (16 enodes)
0.653 * * [simplify]: iters left: 5 (39 enodes)
0.666 * * [simplify]: iters left: 4 (72 enodes)
0.688 * * [simplify]: iters left: 3 (196 enodes)
0.906 * * [simplify]: Extracting #0: cost 1 inf + 0
0.906 * * [simplify]: Extracting #1: cost 5 inf + 0
0.907 * * [simplify]: Extracting #2: cost 11 inf + 1
0.907 * * [simplify]: Extracting #3: cost 16 inf + 2
0.907 * * [simplify]: Extracting #4: cost 26 inf + 807
0.907 * * [simplify]: Extracting #5: cost 66 inf + 1770
0.908 * * [simplify]: Extracting #6: cost 134 inf + 3695
0.909 * * [simplify]: Extracting #7: cost 206 inf + 14082
0.913 * * [simplify]: Extracting #8: cost 137 inf + 107885
0.924 * * [simplify]: Extracting #9: cost 38 inf + 285888
0.943 * * [simplify]: Extracting #10: cost 3 inf + 348921
0.958 * * [simplify]: Extracting #11: cost 0 inf + 357092
0.975 * [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.976 * [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)))
1.023 * * [progress]: iteration 1 / 4
1.023 * * * [progress]: picking best candidate
1.048 * * * * [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)))>
1.048 * * * [progress]: localizing error
1.294 * * * [progress]: generating rewritten candidates
1.294 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.297 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
1.309 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
1.317 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
1.320 * * * [progress]: generating series expansions
1.320 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.320 * * * * [progress]: [ 2 / 4 ] generating series at (2)
1.320 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
1.320 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
1.320 * * * [progress]: simplifying candidates
1.321 * * * * [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)))>
1.321 * [simplify]: Simplifying (neg.p16 b)
1.321 * * [simplify]: iters left: 1 (2 enodes)
1.321 * * [simplify]: Extracting #0: cost 1 inf + 0
1.321 * * [simplify]: Extracting #1: cost 2 inf + 0
1.322 * * [simplify]: Extracting #2: cost 1 inf + 1
1.322 * * [simplify]: Extracting #3: cost 0 inf + 82
1.322 * [simplify]: Simplified to (neg.p16 b)
1.322 * [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)))
1.322 * * * * [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)))>
1.322 * [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))
1.323 * * [simplify]: iters left: 6 (12 enodes)
1.326 * * [simplify]: iters left: 5 (39 enodes)
1.333 * * [simplify]: iters left: 4 (111 enodes)
1.359 * * [simplify]: iters left: 3 (422 enodes)
1.626 * * [simplify]: Extracting #0: cost 1 inf + 0
1.626 * * [simplify]: Extracting #1: cost 45 inf + 0
1.627 * * [simplify]: Extracting #2: cost 218 inf + 0
1.629 * * [simplify]: Extracting #3: cost 370 inf + 2894
1.642 * * [simplify]: Extracting #4: cost 452 inf + 174728
1.686 * * [simplify]: Extracting #5: cost 194 inf + 773405
1.751 * * [simplify]: Extracting #6: cost 9 inf + 1160355
1.851 * * [simplify]: Extracting #7: cost 0 inf + 1181311
1.923 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4)))
1.923 * [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.923 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1.923 * * [simplify]: iters left: 5 (11 enodes)
1.926 * * [simplify]: iters left: 4 (30 enodes)
1.932 * * [simplify]: iters left: 3 (62 enodes)
1.952 * * [simplify]: iters left: 2 (181 enodes)
2.044 * * [simplify]: Extracting #0: cost 1 inf + 0
2.044 * * [simplify]: Extracting #1: cost 3 inf + 0
2.044 * * [simplify]: Extracting #2: cost 3 inf + 1
2.044 * * [simplify]: Extracting #3: cost 17 inf + 1
2.044 * * [simplify]: Extracting #4: cost 59 inf + 322
2.045 * * [simplify]: Extracting #5: cost 140 inf + 1287
2.047 * * [simplify]: Extracting #6: cost 197 inf + 13674
2.052 * * [simplify]: Extracting #7: cost 148 inf + 70160
2.070 * * [simplify]: Extracting #8: cost 22 inf + 301653
2.097 * * [simplify]: Extracting #9: cost 0 inf + 348970
2.123 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
2.123 * [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)))
2.123 * * * * [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))>
2.124 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
2.124 * * [simplify]: iters left: 6 (14 enodes)
2.130 * * [simplify]: iters left: 5 (39 enodes)
2.148 * * [simplify]: iters left: 4 (82 enodes)
2.183 * * [simplify]: iters left: 3 (290 enodes)
2.315 * * [simplify]: Extracting #0: cost 1 inf + 0
2.315 * * [simplify]: Extracting #1: cost 20 inf + 0
2.315 * * [simplify]: Extracting #2: cost 96 inf + 0
2.315 * * [simplify]: Extracting #3: cost 169 inf + 1046
2.316 * * [simplify]: Extracting #4: cost 227 inf + 7305
2.319 * * [simplify]: Extracting #5: cost 249 inf + 62943
2.342 * * [simplify]: Extracting #6: cost 153 inf + 344310
2.364 * * [simplify]: Extracting #7: cost 8 inf + 619712
2.398 * * [simplify]: Extracting #8: cost 0 inf + 637660
2.425 * * [simplify]: Extracting #9: cost 0 inf + 637340
2.452 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
2.452 * [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.452 * * * * [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.453 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))
2.453 * * [simplify]: iters left: 6 (15 enodes)
2.457 * * [simplify]: iters left: 5 (45 enodes)
2.466 * * [simplify]: iters left: 4 (105 enodes)
2.487 * * [simplify]: iters left: 3 (240 enodes)
2.585 * * [simplify]: Extracting #0: cost 1 inf + 0
2.585 * * [simplify]: Extracting #1: cost 21 inf + 0
2.585 * * [simplify]: Extracting #2: cost 27 inf + 1
2.585 * * [simplify]: Extracting #3: cost 24 inf + 326
2.587 * * [simplify]: Extracting #4: cost 35 inf + 1613
2.588 * * [simplify]: Extracting #5: cost 76 inf + 1934
2.588 * * [simplify]: Extracting #6: cost 154 inf + 3859
2.589 * * [simplify]: Extracting #7: cost 223 inf + 10912
2.592 * * [simplify]: Extracting #8: cost 165 inf + 84380
2.603 * * [simplify]: Extracting #9: cost 51 inf + 283434
2.617 * * [simplify]: Extracting #10: cost 3 inf + 373922
2.646 * * [simplify]: Extracting #11: cost 0 inf + 380294
2.661 * [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.661 * [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.661 * * * * [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.661 * [simplify]: Simplifying (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
2.661 * * [simplify]: iters left: 3 (7 enodes)
2.663 * * [simplify]: iters left: 2 (16 enodes)
2.666 * * [simplify]: iters left: 1 (22 enodes)
2.669 * * [simplify]: Extracting #0: cost 1 inf + 0
2.669 * * [simplify]: Extracting #1: cost 2 inf + 0
2.669 * * [simplify]: Extracting #2: cost 8 inf + 0
2.669 * * [simplify]: Extracting #3: cost 7 inf + 2
2.669 * * [simplify]: Extracting #4: cost 0 inf + 2336
2.669 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 a c) (real->posit16 4)))
2.669 * [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.669 * * * * [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.669 * [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.669 * * [simplify]: iters left: 4 (11 enodes)
2.672 * * [simplify]: iters left: 3 (40 enodes)
2.680 * * [simplify]: iters left: 2 (100 enodes)
2.704 * * [simplify]: iters left: 1 (362 enodes)
3.014 * * [simplify]: Extracting #0: cost 1 inf + 0
3.014 * * [simplify]: Extracting #1: cost 32 inf + 0
3.015 * * [simplify]: Extracting #2: cost 201 inf + 0
3.017 * * [simplify]: Extracting #3: cost 322 inf + 3534
3.026 * * [simplify]: Extracting #4: cost 446 inf + 85826
3.060 * * [simplify]: Extracting #5: cost 150 inf + 651907
3.103 * * [simplify]: Extracting #6: cost 18 inf + 952407
3.157 * * [simplify]: Extracting #7: cost 0 inf + 997559
3.227 * * [simplify]: Extracting #8: cost 0 inf + 994839
3.289 * [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))))
3.289 * [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)))
3.289 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))
3.290 * * [simplify]: iters left: 3 (9 enodes)
3.294 * * [simplify]: iters left: 2 (21 enodes)
3.301 * * [simplify]: iters left: 1 (27 enodes)
3.309 * * [simplify]: Extracting #0: cost 1 inf + 0
3.309 * * [simplify]: Extracting #1: cost 3 inf + 0
3.310 * * [simplify]: Extracting #2: cost 10 inf + 0
3.310 * * [simplify]: Extracting #3: cost 7 inf + 325
3.310 * * [simplify]: Extracting #4: cost 5 inf + 647
3.310 * * [simplify]: Extracting #5: cost 1 inf + 2617
3.310 * * [simplify]: Extracting #6: cost 0 inf + 2939
3.311 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
3.311 * [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)))
3.311 * * * * [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)))>
3.311 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
3.311 * * [simplify]: iters left: 6 (15 enodes)
3.319 * * [simplify]: iters left: 5 (43 enodes)
3.333 * * [simplify]: iters left: 4 (88 enodes)
3.352 * * [simplify]: iters left: 3 (308 enodes)
3.513 * * [simplify]: Extracting #0: cost 1 inf + 0
3.513 * * [simplify]: Extracting #1: cost 31 inf + 0
3.513 * * [simplify]: Extracting #2: cost 125 inf + 1
3.514 * * [simplify]: Extracting #3: cost 192 inf + 3056
3.515 * * [simplify]: Extracting #4: cost 252 inf + 8914
3.517 * * [simplify]: Extracting #5: cost 288 inf + 55001
3.531 * * [simplify]: Extracting #6: cost 174 inf + 365952
3.565 * * [simplify]: Extracting #7: cost 7 inf + 676616
3.620 * * [simplify]: Extracting #8: cost 0 inf + 688601
3.681 * [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.681 * [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.681 * * * * [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.681 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
3.682 * * [simplify]: iters left: 6 (15 enodes)
3.689 * * [simplify]: iters left: 5 (43 enodes)
3.701 * * [simplify]: iters left: 4 (88 enodes)
3.720 * * [simplify]: iters left: 3 (308 enodes)
3.878 * * [simplify]: Extracting #0: cost 1 inf + 0
3.878 * * [simplify]: Extracting #1: cost 31 inf + 0
3.878 * * [simplify]: Extracting #2: cost 125 inf + 1
3.880 * * [simplify]: Extracting #3: cost 192 inf + 3056
3.882 * * [simplify]: Extracting #4: cost 252 inf + 8914
3.887 * * [simplify]: Extracting #5: cost 288 inf + 55001
3.912 * * [simplify]: Extracting #6: cost 174 inf + 365952
3.943 * * [simplify]: Extracting #7: cost 7 inf + 676616
3.999 * * [simplify]: Extracting #8: cost 0 inf + 688601
4.058 * [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.058 * [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.059 * * * * [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.059 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
4.059 * * [simplify]: iters left: 6 (15 enodes)
4.066 * * [simplify]: iters left: 5 (43 enodes)
4.081 * * [simplify]: iters left: 4 (88 enodes)
4.119 * * [simplify]: iters left: 3 (308 enodes)
4.248 * * [simplify]: Extracting #0: cost 1 inf + 0
4.249 * * [simplify]: Extracting #1: cost 31 inf + 0
4.249 * * [simplify]: Extracting #2: cost 125 inf + 1
4.250 * * [simplify]: Extracting #3: cost 192 inf + 3056
4.251 * * [simplify]: Extracting #4: cost 252 inf + 8914
4.253 * * [simplify]: Extracting #5: cost 288 inf + 55001
4.277 * * [simplify]: Extracting #6: cost 174 inf + 365952
4.322 * * [simplify]: Extracting #7: cost 7 inf + 676616
4.361 * * [simplify]: Extracting #8: cost 0 inf + 688601
4.392 * [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.392 * [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.392 * * * * [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.392 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
4.392 * * [simplify]: iters left: 6 (15 enodes)
4.399 * * [simplify]: iters left: 5 (43 enodes)
4.415 * * [simplify]: iters left: 4 (88 enodes)
4.453 * * [simplify]: iters left: 3 (308 enodes)
4.590 * * [simplify]: Extracting #0: cost 1 inf + 0
4.590 * * [simplify]: Extracting #1: cost 31 inf + 0
4.590 * * [simplify]: Extracting #2: cost 125 inf + 1
4.591 * * [simplify]: Extracting #3: cost 192 inf + 3056
4.592 * * [simplify]: Extracting #4: cost 252 inf + 8914
4.594 * * [simplify]: Extracting #5: cost 288 inf + 55001
4.608 * * [simplify]: Extracting #6: cost 174 inf + 365952
4.653 * * [simplify]: Extracting #7: cost 7 inf + 676616
4.685 * * [simplify]: Extracting #8: cost 0 inf + 688601
4.724 * [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.724 * [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.724 * * * [progress]: adding candidates to table
5.081 * * [progress]: iteration 2 / 4
5.081 * * * [progress]: picking best candidate
5.168 * * * * [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.168 * * * [progress]: localizing error
5.424 * * * [progress]: generating rewritten candidates
5.424 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
5.427 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1)
5.435 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
5.436 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 1 2)
5.442 * * * [progress]: generating series expansions
5.442 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
5.443 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1)
5.443 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
5.443 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 1 2)
5.443 * * * [progress]: simplifying candidates
5.443 * * * * [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.443 * [simplify]: Simplifying (neg.p16 b)
5.443 * * [simplify]: iters left: 1 (2 enodes)
5.444 * * [simplify]: Extracting #0: cost 1 inf + 0
5.444 * * [simplify]: Extracting #1: cost 2 inf + 0
5.444 * * [simplify]: Extracting #2: cost 1 inf + 1
5.444 * * [simplify]: Extracting #3: cost 0 inf + 82
5.444 * [simplify]: Simplified to (neg.p16 b)
5.444 * [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.444 * * * * [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.445 * [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.445 * * [simplify]: iters left: 6 (12 enodes)
5.451 * * [simplify]: iters left: 5 (39 enodes)
5.473 * * [simplify]: iters left: 4 (111 enodes)
5.505 * * [simplify]: iters left: 3 (422 enodes)
5.775 * * [simplify]: Extracting #0: cost 1 inf + 0
5.776 * * [simplify]: Extracting #1: cost 45 inf + 0
5.777 * * [simplify]: Extracting #2: cost 218 inf + 0
5.779 * * [simplify]: Extracting #3: cost 370 inf + 2894
5.791 * * [simplify]: Extracting #4: cost 452 inf + 174728
5.839 * * [simplify]: Extracting #5: cost 194 inf + 773405
5.901 * * [simplify]: Extracting #6: cost 9 inf + 1160355
5.984 * * [simplify]: Extracting #7: cost 0 inf + 1181311
6.042 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4)))
6.042 * [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.042 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
6.042 * * [simplify]: iters left: 5 (11 enodes)
6.045 * * [simplify]: iters left: 4 (30 enodes)
6.050 * * [simplify]: iters left: 3 (62 enodes)
6.075 * * [simplify]: iters left: 2 (181 enodes)
6.204 * * [simplify]: Extracting #0: cost 1 inf + 0
6.204 * * [simplify]: Extracting #1: cost 3 inf + 0
6.204 * * [simplify]: Extracting #2: cost 3 inf + 1
6.204 * * [simplify]: Extracting #3: cost 17 inf + 1
6.205 * * [simplify]: Extracting #4: cost 59 inf + 322
6.205 * * [simplify]: Extracting #5: cost 140 inf + 1287
6.207 * * [simplify]: Extracting #6: cost 197 inf + 13674
6.213 * * [simplify]: Extracting #7: cost 148 inf + 70160
6.230 * * [simplify]: Extracting #8: cost 22 inf + 301653
6.255 * * [simplify]: Extracting #9: cost 0 inf + 348970
6.282 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
6.282 * [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.282 * * * * [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.282 * [simplify]: Simplifying (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
6.282 * * [simplify]: iters left: 3 (7 enodes)
6.284 * * [simplify]: iters left: 2 (16 enodes)
6.287 * * [simplify]: iters left: 1 (22 enodes)
6.290 * * [simplify]: Extracting #0: cost 1 inf + 0
6.290 * * [simplify]: Extracting #1: cost 2 inf + 0
6.290 * * [simplify]: Extracting #2: cost 8 inf + 0
6.290 * * [simplify]: Extracting #3: cost 7 inf + 2
6.291 * * [simplify]: Extracting #4: cost 0 inf + 2336
6.291 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 a c) (real->posit16 4)))
6.291 * [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.291 * * * * [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.291 * [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.291 * * [simplify]: iters left: 4 (11 enodes)
6.294 * * [simplify]: iters left: 3 (40 enodes)
6.301 * * [simplify]: iters left: 2 (100 enodes)
6.343 * * [simplify]: iters left: 1 (362 enodes)
6.599 * * [simplify]: Extracting #0: cost 1 inf + 0
6.599 * * [simplify]: Extracting #1: cost 32 inf + 0
6.600 * * [simplify]: Extracting #2: cost 201 inf + 0
6.601 * * [simplify]: Extracting #3: cost 322 inf + 3534
6.606 * * [simplify]: Extracting #4: cost 446 inf + 85826
6.631 * * [simplify]: Extracting #5: cost 150 inf + 651907
6.675 * * [simplify]: Extracting #6: cost 18 inf + 952407
6.741 * * [simplify]: Extracting #7: cost 0 inf + 997559
6.789 * * [simplify]: Extracting #8: cost 0 inf + 994839
6.833 * [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))))
6.833 * [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))
6.833 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))
6.834 * * [simplify]: iters left: 3 (9 enodes)
6.836 * * [simplify]: iters left: 2 (21 enodes)
6.839 * * [simplify]: iters left: 1 (27 enodes)
6.843 * * [simplify]: Extracting #0: cost 1 inf + 0
6.843 * * [simplify]: Extracting #1: cost 3 inf + 0
6.843 * * [simplify]: Extracting #2: cost 10 inf + 0
6.843 * * [simplify]: Extracting #3: cost 7 inf + 325
6.843 * * [simplify]: Extracting #4: cost 5 inf + 647
6.844 * * [simplify]: Extracting #5: cost 1 inf + 2617
6.844 * * [simplify]: Extracting #6: cost 0 inf + 2939
6.844 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
6.844 * [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))
6.844 * * * * [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))>
6.844 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
6.844 * * [simplify]: iters left: 2 (4 enodes)
6.845 * * [simplify]: iters left: 1 (8 enodes)
6.848 * * [simplify]: Extracting #0: cost 1 inf + 0
6.848 * * [simplify]: Extracting #1: cost 3 inf + 0
6.848 * * [simplify]: Extracting #2: cost 3 inf + 1
6.848 * * [simplify]: Extracting #3: cost 0 inf + 325
6.848 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
6.848 * [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))
6.848 * * * * [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))>
6.848 * * * * [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))>
6.848 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
6.849 * * [simplify]: iters left: 6 (14 enodes)
6.855 * * [simplify]: iters left: 5 (39 enodes)
6.871 * * [simplify]: iters left: 4 (82 enodes)
6.906 * * [simplify]: iters left: 3 (290 enodes)
7.095 * * [simplify]: Extracting #0: cost 1 inf + 0
7.095 * * [simplify]: Extracting #1: cost 20 inf + 0
7.096 * * [simplify]: Extracting #2: cost 96 inf + 0
7.097 * * [simplify]: Extracting #3: cost 169 inf + 1046
7.098 * * [simplify]: Extracting #4: cost 227 inf + 7305
7.104 * * [simplify]: Extracting #5: cost 249 inf + 62943
7.133 * * [simplify]: Extracting #6: cost 153 inf + 344310
7.164 * * [simplify]: Extracting #7: cost 8 inf + 619712
7.199 * * [simplify]: Extracting #8: cost 0 inf + 637660
7.233 * * [simplify]: Extracting #9: cost 0 inf + 637340
7.260 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
7.260 * [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.260 * * * * [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.260 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
7.261 * * [simplify]: iters left: 6 (14 enodes)
7.265 * * [simplify]: iters left: 5 (39 enodes)
7.273 * * [simplify]: iters left: 4 (82 enodes)
7.290 * * [simplify]: iters left: 3 (290 enodes)
7.439 * * [simplify]: Extracting #0: cost 1 inf + 0
7.439 * * [simplify]: Extracting #1: cost 20 inf + 0
7.439 * * [simplify]: Extracting #2: cost 96 inf + 0
7.440 * * [simplify]: Extracting #3: cost 169 inf + 1046
7.440 * * [simplify]: Extracting #4: cost 227 inf + 7305
7.443 * * [simplify]: Extracting #5: cost 249 inf + 62943
7.455 * * [simplify]: Extracting #6: cost 153 inf + 344310
7.498 * * [simplify]: Extracting #7: cost 8 inf + 619712
7.539 * * [simplify]: Extracting #8: cost 0 inf + 637660
7.567 * * [simplify]: Extracting #9: cost 0 inf + 637340
7.615 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
7.615 * [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.616 * * * * [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))>
7.616 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
7.616 * * [simplify]: iters left: 6 (14 enodes)
7.619 * * [simplify]: iters left: 5 (39 enodes)
7.626 * * [simplify]: iters left: 4 (82 enodes)
7.644 * * [simplify]: iters left: 3 (290 enodes)
7.772 * * [simplify]: Extracting #0: cost 1 inf + 0
7.772 * * [simplify]: Extracting #1: cost 20 inf + 0
7.772 * * [simplify]: Extracting #2: cost 96 inf + 0
7.773 * * [simplify]: Extracting #3: cost 169 inf + 1046
7.774 * * [simplify]: Extracting #4: cost 227 inf + 7305
7.776 * * [simplify]: Extracting #5: cost 249 inf + 62943
7.794 * * [simplify]: Extracting #6: cost 153 inf + 344310
7.836 * * [simplify]: Extracting #7: cost 8 inf + 619712
8.256 * * [simplify]: Extracting #8: cost 0 inf + 637660
8.305 * * [simplify]: Extracting #9: cost 0 inf + 637340
8.359 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
8.359 * [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.359 * * * * [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.360 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2))
8.360 * * [simplify]: iters left: 6 (14 enodes)
8.366 * * [simplify]: iters left: 5 (39 enodes)
8.382 * * [simplify]: iters left: 4 (82 enodes)
8.408 * * [simplify]: iters left: 3 (290 enodes)
8.566 * * [simplify]: Extracting #0: cost 1 inf + 0
8.566 * * [simplify]: Extracting #1: cost 20 inf + 0
8.566 * * [simplify]: Extracting #2: cost 96 inf + 0
8.566 * * [simplify]: Extracting #3: cost 169 inf + 1046
8.567 * * [simplify]: Extracting #4: cost 227 inf + 7305
8.570 * * [simplify]: Extracting #5: cost 249 inf + 62943
8.586 * * [simplify]: Extracting #6: cost 153 inf + 344310
8.632 * * [simplify]: Extracting #7: cost 8 inf + 619712
8.685 * * [simplify]: Extracting #8: cost 0 inf + 637660
8.735 * * [simplify]: Extracting #9: cost 0 inf + 637340
8.773 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (real->posit16 2))
8.774 * [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.774 * * * [progress]: adding candidates to table
9.198 * * [progress]: iteration 3 / 4
9.198 * * * [progress]: picking best candidate
9.277 * * * * [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.277 * * * [progress]: localizing error
9.524 * * * [progress]: generating rewritten candidates
9.524 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
9.525 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1)
9.530 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
9.530 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
9.533 * * * [progress]: generating series expansions
9.533 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
9.533 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1)
9.533 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
9.533 * * * * [progress]: [ 4 / 4 ] generating series at (2)
9.533 * * * [progress]: simplifying candidates
9.533 * * * * [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.534 * [simplify]: Simplifying (neg.p16 b)
9.534 * * [simplify]: iters left: 1 (2 enodes)
9.534 * * [simplify]: Extracting #0: cost 1 inf + 0
9.534 * * [simplify]: Extracting #1: cost 2 inf + 0
9.534 * * [simplify]: Extracting #2: cost 1 inf + 1
9.534 * * [simplify]: Extracting #3: cost 0 inf + 82
9.534 * [simplify]: Simplified to (neg.p16 b)
9.534 * [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.534 * * * * [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.534 * [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.534 * * [simplify]: iters left: 6 (12 enodes)
9.537 * * [simplify]: iters left: 5 (39 enodes)
9.545 * * [simplify]: iters left: 4 (111 enodes)
9.572 * * [simplify]: iters left: 3 (419 enodes)
9.831 * * [simplify]: Extracting #0: cost 1 inf + 0
9.831 * * [simplify]: Extracting #1: cost 45 inf + 0
9.837 * * [simplify]: Extracting #2: cost 218 inf + 0
9.839 * * [simplify]: Extracting #3: cost 372 inf + 3054
9.853 * * [simplify]: Extracting #4: cost 447 inf + 176392
9.919 * * [simplify]: Extracting #5: cost 180 inf + 817643
9.998 * * [simplify]: Extracting #6: cost 4 inf + 1166833
10.054 * * [simplify]: Extracting #7: cost 0 inf + 1177411
10.164 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c))
10.164 * [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.164 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)
10.164 * * [simplify]: iters left: 6 (11 enodes)
10.167 * * [simplify]: iters left: 5 (30 enodes)
10.172 * * [simplify]: iters left: 4 (62 enodes)
10.184 * * [simplify]: iters left: 3 (175 enodes)
10.263 * * [simplify]: Extracting #0: cost 1 inf + 0
10.263 * * [simplify]: Extracting #1: cost 3 inf + 0
10.263 * * [simplify]: Extracting #2: cost 3 inf + 1
10.263 * * [simplify]: Extracting #3: cost 17 inf + 1
10.263 * * [simplify]: Extracting #4: cost 59 inf + 322
10.264 * * [simplify]: Extracting #5: cost 133 inf + 1287
10.266 * * [simplify]: Extracting #6: cost 197 inf + 12718
10.274 * * [simplify]: Extracting #7: cost 127 inf + 114668
10.296 * * [simplify]: Extracting #8: cost 13 inf + 318519
10.322 * * [simplify]: Extracting #9: cost 0 inf + 342366
10.344 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
10.344 * [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.344 * * * * [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.344 * [simplify]: Simplifying (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
10.344 * * [simplify]: iters left: 4 (7 enodes)
10.346 * * [simplify]: iters left: 3 (16 enodes)
10.349 * * [simplify]: iters left: 2 (22 enodes)
10.352 * * [simplify]: iters left: 1 (23 enodes)
10.355 * * [simplify]: Extracting #0: cost 1 inf + 0
10.355 * * [simplify]: Extracting #1: cost 2 inf + 0
10.355 * * [simplify]: Extracting #2: cost 8 inf + 0
10.355 * * [simplify]: Extracting #3: cost 7 inf + 2
10.355 * * [simplify]: Extracting #4: cost 5 inf + 325
10.355 * * [simplify]: Extracting #5: cost 1 inf + 2014
10.355 * * [simplify]: Extracting #6: cost 0 inf + 2336
10.355 * [simplify]: Simplified to (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
10.355 * [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.355 * * * * [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.356 * [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.356 * * [simplify]: iters left: 5 (11 enodes)
10.358 * * [simplify]: iters left: 4 (40 enodes)
10.370 * * [simplify]: iters left: 3 (105 enodes)
10.398 * * [simplify]: iters left: 2 (407 enodes)
10.820 * * [simplify]: Extracting #0: cost 1 inf + 0
10.820 * * [simplify]: Extracting #1: cost 32 inf + 0
10.821 * * [simplify]: Extracting #2: cost 198 inf + 0
10.823 * * [simplify]: Extracting #3: cost 346 inf + 2571
10.833 * * [simplify]: Extracting #4: cost 496 inf + 91867
10.897 * * [simplify]: Extracting #5: cost 168 inf + 732046
10.996 * * [simplify]: Extracting #6: cost 9 inf + 1087233
11.103 * * [simplify]: Extracting #7: cost 0 inf + 1112349
11.188 * [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.188 * [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.189 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))
11.189 * * [simplify]: iters left: 4 (9 enodes)
11.191 * * [simplify]: iters left: 3 (21 enodes)
11.194 * * [simplify]: iters left: 2 (27 enodes)
11.198 * * [simplify]: iters left: 1 (28 enodes)
11.202 * * [simplify]: Extracting #0: cost 1 inf + 0
11.202 * * [simplify]: Extracting #1: cost 3 inf + 0
11.202 * * [simplify]: Extracting #2: cost 10 inf + 0
11.202 * * [simplify]: Extracting #3: cost 7 inf + 325
11.202 * * [simplify]: Extracting #4: cost 1 inf + 1935
11.203 * * [simplify]: Extracting #5: cost 0 inf + 2939
11.203 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b))
11.203 * [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.203 * * * * [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.203 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
11.203 * * [simplify]: iters left: 2 (4 enodes)
11.204 * * [simplify]: iters left: 1 (8 enodes)
11.205 * * [simplify]: Extracting #0: cost 1 inf + 0
11.205 * * [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.206 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
11.206 * [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.206 * * * * [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.206 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
11.206 * * [simplify]: iters left: 2 (4 enodes)
11.207 * * [simplify]: iters left: 1 (8 enodes)
11.208 * * [simplify]: Extracting #0: cost 1 inf + 0
11.208 * * [simplify]: Extracting #1: cost 3 inf + 0
11.208 * * [simplify]: Extracting #2: cost 3 inf + 1
11.208 * * [simplify]: Extracting #3: cost 0 inf + 325
11.208 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.208 * [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.208 * * * * [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.208 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
11.208 * * [simplify]: iters left: 2 (4 enodes)
11.209 * * [simplify]: iters left: 1 (8 enodes)
11.211 * * [simplify]: Extracting #0: cost 1 inf + 0
11.211 * * [simplify]: Extracting #1: cost 3 inf + 0
11.211 * * [simplify]: Extracting #2: cost 3 inf + 1
11.211 * * [simplify]: Extracting #3: cost 0 inf + 325
11.211 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.211 * [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.211 * * * * [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.211 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
11.211 * * [simplify]: iters left: 2 (4 enodes)
11.212 * * [simplify]: iters left: 1 (8 enodes)
11.213 * * [simplify]: Extracting #0: cost 1 inf + 0
11.213 * * [simplify]: Extracting #1: cost 3 inf + 0
11.213 * * [simplify]: Extracting #2: cost 3 inf + 1
11.213 * * [simplify]: Extracting #3: cost 0 inf + 325
11.213 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.213 * [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.214 * * * * [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.214 * [simplify]: Simplifying (*.p16 a (real->posit16 4))
11.214 * * [simplify]: iters left: 2 (4 enodes)
11.215 * * [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.493 * * [progress]: iteration 4 / 4
11.493 * * * [progress]: picking best candidate
11.609 * * * * [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.609 * * * [progress]: localizing error
11.921 * * * [progress]: generating rewritten candidates
11.921 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
11.924 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
11.930 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
11.940 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
11.940 * * * [progress]: generating series expansions
11.940 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
11.940 * * * * [progress]: [ 2 / 4 ] generating series at (2)
11.941 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
11.941 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
11.941 * * * [progress]: simplifying candidates
11.941 * * * * [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.941 * [simplify]: Simplifying (neg.p16 b)
11.941 * * [simplify]: iters left: 1 (2 enodes)
11.942 * * [simplify]: Extracting #0: cost 1 inf + 0
11.942 * * [simplify]: Extracting #1: cost 2 inf + 0
11.942 * * [simplify]: Extracting #2: cost 1 inf + 1
11.942 * * [simplify]: Extracting #3: cost 0 inf + 82
11.942 * [simplify]: Simplified to (neg.p16 b)
11.942 * [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.942 * * * * [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.942 * [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.943 * * [simplify]: iters left: 6 (12 enodes)
11.949 * * [simplify]: iters left: 5 (39 enodes)
11.961 * * [simplify]: iters left: 4 (111 enodes)
11.987 * * [simplify]: iters left: 3 (419 enodes)
12.291 * * [simplify]: Extracting #0: cost 1 inf + 0
12.291 * * [simplify]: Extracting #1: cost 45 inf + 0
12.292 * * [simplify]: Extracting #2: cost 218 inf + 0
12.294 * * [simplify]: Extracting #3: cost 372 inf + 3054
12.309 * * [simplify]: Extracting #4: cost 447 inf + 176392
12.384 * * [simplify]: Extracting #5: cost 180 inf + 817643
12.489 * * [simplify]: Extracting #6: cost 4 inf + 1166833
12.602 * * [simplify]: Extracting #7: cost 0 inf + 1177411
12.664 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c))
12.664 * [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.665 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)
12.665 * * [simplify]: iters left: 6 (11 enodes)
12.671 * * [simplify]: iters left: 5 (30 enodes)
12.681 * * [simplify]: iters left: 4 (62 enodes)
12.706 * * [simplify]: iters left: 3 (175 enodes)
12.795 * * [simplify]: Extracting #0: cost 1 inf + 0
12.796 * * [simplify]: Extracting #1: cost 3 inf + 0
12.796 * * [simplify]: Extracting #2: cost 3 inf + 1
12.796 * * [simplify]: Extracting #3: cost 17 inf + 1
12.796 * * [simplify]: Extracting #4: cost 59 inf + 322
12.796 * * [simplify]: Extracting #5: cost 133 inf + 1287
12.797 * * [simplify]: Extracting #6: cost 197 inf + 12718
12.801 * * [simplify]: Extracting #7: cost 127 inf + 114668
12.811 * * [simplify]: Extracting #8: cost 13 inf + 318519
12.828 * * [simplify]: Extracting #9: cost 0 inf + 342366
12.854 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
12.854 * [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.854 * * * * [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.854 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a)
12.855 * * [simplify]: iters left: 6 (12 enodes)
12.860 * * [simplify]: iters left: 5 (36 enodes)
12.872 * * [simplify]: iters left: 4 (79 enodes)
12.908 * * [simplify]: iters left: 3 (280 enodes)
13.012 * * [simplify]: Extracting #0: cost 1 inf + 0
13.012 * * [simplify]: Extracting #1: cost 20 inf + 0
13.012 * * [simplify]: Extracting #2: cost 94 inf + 1
13.013 * * [simplify]: Extracting #3: cost 166 inf + 1768
13.014 * * [simplify]: Extracting #4: cost 226 inf + 6981
13.016 * * [simplify]: Extracting #5: cost 246 inf + 63504
13.030 * * [simplify]: Extracting #6: cost 139 inf + 360206
13.058 * * [simplify]: Extracting #7: cost 3 inf + 617210
13.089 * * [simplify]: Extracting #8: cost 0 inf + 625421
13.143 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) b) a)
13.143 * [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.143 * * * * [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.144 * [simplify]: Simplifying (*.p16 (*.p16 a (real->posit16 2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))
13.144 * * [simplify]: iters left: 6 (15 enodes)
13.152 * * [simplify]: iters left: 5 (45 enodes)
13.168 * * [simplify]: iters left: 4 (105 enodes)
13.213 * * [simplify]: iters left: 3 (235 enodes)
13.355 * * [simplify]: Extracting #0: cost 1 inf + 0
13.355 * * [simplify]: Extracting #1: cost 23 inf + 0
13.355 * * [simplify]: Extracting #2: cost 29 inf + 1
13.355 * * [simplify]: Extracting #3: cost 28 inf + 3
13.355 * * [simplify]: Extracting #4: cost 38 inf + 970
13.356 * * [simplify]: Extracting #5: cost 78 inf + 1934
13.357 * * [simplify]: Extracting #6: cost 156 inf + 2576
13.359 * * [simplify]: Extracting #7: cost 239 inf + 9312
13.370 * * [simplify]: Extracting #8: cost 124 inf + 200111
13.400 * * [simplify]: Extracting #9: cost 14 inf + 413653
13.434 * * [simplify]: Extracting #10: cost 0 inf + 408188
13.469 * * [simplify]: Extracting #11: cost 0 inf + 406268
13.502 * [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.502 * [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.503 * * * * [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.503 * [simplify]: Simplifying (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
13.503 * * [simplify]: iters left: 4 (7 enodes)
13.506 * * [simplify]: iters left: 3 (16 enodes)
13.512 * * [simplify]: iters left: 2 (22 enodes)
13.518 * * [simplify]: iters left: 1 (23 enodes)
13.524 * * [simplify]: Extracting #0: cost 1 inf + 0
13.524 * * [simplify]: Extracting #1: cost 2 inf + 0
13.524 * * [simplify]: Extracting #2: cost 8 inf + 0
13.524 * * [simplify]: Extracting #3: cost 7 inf + 2
13.524 * * [simplify]: Extracting #4: cost 5 inf + 325
13.524 * * [simplify]: Extracting #5: cost 1 inf + 2014
13.525 * * [simplify]: Extracting #6: cost 0 inf + 2336
13.525 * [simplify]: Simplified to (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
13.525 * [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.525 * * * * [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.525 * [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.526 * * [simplify]: iters left: 5 (11 enodes)
13.531 * * [simplify]: iters left: 4 (40 enodes)
13.546 * * [simplify]: iters left: 3 (105 enodes)
13.599 * * [simplify]: iters left: 2 (407 enodes)
13.883 * * [simplify]: Extracting #0: cost 1 inf + 0
13.883 * * [simplify]: Extracting #1: cost 32 inf + 0
13.883 * * [simplify]: Extracting #2: cost 198 inf + 0
13.884 * * [simplify]: Extracting #3: cost 346 inf + 2571
13.890 * * [simplify]: Extracting #4: cost 496 inf + 91867
13.950 * * [simplify]: Extracting #5: cost 168 inf + 732046
14.043 * * [simplify]: Extracting #6: cost 9 inf + 1087233
14.107 * * [simplify]: Extracting #7: cost 0 inf + 1112349
14.172 * [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.172 * [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.173 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))
14.173 * * [simplify]: iters left: 4 (9 enodes)
14.178 * * [simplify]: iters left: 3 (21 enodes)
14.185 * * [simplify]: iters left: 2 (27 enodes)
14.194 * * [simplify]: iters left: 1 (28 enodes)
14.203 * * [simplify]: Extracting #0: cost 1 inf + 0
14.203 * * [simplify]: Extracting #1: cost 3 inf + 0
14.203 * * [simplify]: Extracting #2: cost 10 inf + 0
14.203 * * [simplify]: Extracting #3: cost 7 inf + 325
14.204 * * [simplify]: Extracting #4: cost 1 inf + 1935
14.204 * * [simplify]: Extracting #5: cost 0 inf + 2939
14.204 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b))
14.204 * [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.205 * * * * [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.205 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
14.205 * * [simplify]: iters left: 2 (4 enodes)
14.207 * * [simplify]: iters left: 1 (8 enodes)
14.210 * * [simplify]: Extracting #0: cost 1 inf + 0
14.210 * * [simplify]: Extracting #1: cost 3 inf + 0
14.210 * * [simplify]: Extracting #2: cost 3 inf + 1
14.210 * * [simplify]: Extracting #3: cost 0 inf + 325
14.210 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
14.210 * [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.211 * * * * [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.211 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
14.211 * * [simplify]: iters left: 2 (4 enodes)
14.213 * * [simplify]: iters left: 1 (8 enodes)
14.215 * * [simplify]: Extracting #0: cost 1 inf + 0
14.216 * * [simplify]: Extracting #1: cost 3 inf + 0
14.216 * * [simplify]: Extracting #2: cost 3 inf + 1
14.216 * * [simplify]: Extracting #3: cost 0 inf + 325
14.216 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
14.216 * [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.216 * * * * [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.216 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
14.216 * * [simplify]: iters left: 2 (4 enodes)
14.220 * * [simplify]: iters left: 1 (8 enodes)
14.222 * * [simplify]: Extracting #0: cost 1 inf + 0
14.222 * * [simplify]: Extracting #1: cost 3 inf + 0
14.223 * * [simplify]: Extracting #2: cost 3 inf + 1
14.223 * * [simplify]: Extracting #3: cost 0 inf + 325
14.223 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
14.223 * [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.223 * * * * [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.223 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
14.223 * * [simplify]: iters left: 2 (4 enodes)
14.225 * * [simplify]: iters left: 1 (8 enodes)
14.227 * * [simplify]: Extracting #0: cost 1 inf + 0
14.227 * * [simplify]: Extracting #1: cost 3 inf + 0
14.227 * * [simplify]: Extracting #2: cost 3 inf + 1
14.227 * * [simplify]: Extracting #3: cost 0 inf + 325
14.227 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
14.227 * [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.227 * * * [progress]: adding candidates to table
14.606 * [progress]: [Phase 3 of 3] Extracting.
14.607 * * [regime]: Finding splitpoints for: (#<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 (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 (*.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))> #<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 (*.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 (*.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 (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))))) b) a) (real->posit16 2)))>)
14.613 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
14.613 * * * * [regimes]: Trying to branch on c from (#<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 (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 (*.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))> #<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 (*.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 (*.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 (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))))) b) a) (real->posit16 2)))>)
14.917 * * * * [regimes]: Trying to branch on a from (#<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 (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 (*.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))> #<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 (*.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 (*.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 (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))))) b) a) (real->posit16 2)))>)
15.221 * * * * [regimes]: Trying to branch on b from (#<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 (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 (*.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))> #<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 (*.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 (*.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 (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))))) b) a) (real->posit16 2)))>)
15.440 * * * [regime]: Found split indices: #<option (#s(si 7 256))>
15.441 * [simplify]: Simplifying (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) a) (real->posit16 2))
15.441 * * [simplify]: iters left: 6 (15 enodes)
15.443 * * [simplify]: Extracting #0: cost 1 inf + 0
15.443 * * [simplify]: Extracting #1: cost 3 inf + 0
15.443 * * [simplify]: Extracting #2: cost 6 inf + 0
15.443 * * [simplify]: Extracting #3: cost 5 inf + 3
15.443 * * [simplify]: Extracting #4: cost 5 inf + 4
15.443 * * [simplify]: Extracting #5: cost 7 inf + 4
15.444 * * [simplify]: Extracting #6: cost 8 inf + 325
15.444 * * [simplify]: Extracting #7: cost 8 inf + 326
15.444 * * [simplify]: Extracting #8: cost 9 inf + 326
15.444 * * [simplify]: Extracting #9: cost 7 inf + 328
15.444 * * [simplify]: Extracting #10: cost 5 inf + 1293
15.444 * * [simplify]: Extracting #11: cost 3 inf + 3421
15.444 * * [simplify]: Extracting #12: cost 1 inf + 6189
15.445 * * [simplify]: Extracting #13: cost 0 inf + 8234
15.445 * [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.445 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
15.487 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
15.489 * * * * [points]: Setting MPFR precision to 64
15.491 * * * * [points]: Setting MPFR precision to 320
15.492 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
15.495 * * * * [points]: Setting MPFR precision to 64
15.497 * * * * [points]: Setting MPFR precision to 320
15.499 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
15.502 * * * * [points]: Setting MPFR precision to 64
15.506 * * * * [points]: Setting MPFR precision to 320
15.511 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
15.513 * * * * [points]: Setting MPFR precision to 64
15.522 * * * * [points]: Setting MPFR precision to 320
15.530 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
15.533 * * * * [points]: Setting MPFR precision to 64
15.556 * * * * [points]: Setting MPFR precision to 320
15.587 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
15.592 * * * * [points]: Setting MPFR precision to 64
15.701 * * * * [points]: Setting MPFR precision to 320
15.762 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
15.767 * * * * [points]: Setting MPFR precision to 64
15.936 * * * * [points]: Setting MPFR precision to 320
16.009 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
16.015 * * * * [points]: Setting MPFR precision to 64
16.277 * * * * [points]: Setting MPFR precision to 320
16.530 * * * * [points]: Computing exacts for 8000 points
16.536 * * * * [points]: Setting MPFR precision to 64
17.929 * * * * [points]: Setting MPFR precision to 320
19.044 * * * * [points]: Filtering points with unrepresentable outputs
19.087 * * * * [points]: Sampled 8000 points with exact outputs
24.000 * [regime-testing]: Baseline error score: 64.0
24.003 * [regime-testing]: Oracle error score: 64.0
24.010 * [regime-testing]: End program error score: 1.53861151671579