0.037 * [progress]: [Phase 1 of 3] Setting up.
0.040 * * * [progress]: [1/2] Preparing points
0.044 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.049 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.236 * * * * [points]: Setting MPFR precision to 64
0.239 * * * * [points]: Setting MPFR precision to 320
0.241 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.247 * * * * [points]: Setting MPFR precision to 64
0.251 * * * * [points]: Setting MPFR precision to 320
0.255 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.260 * * * * [points]: Setting MPFR precision to 64
0.267 * * * * [points]: Setting MPFR precision to 320
0.273 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.275 * * * * [points]: Setting MPFR precision to 64
0.282 * * * * [points]: Setting MPFR precision to 320
0.289 * * * * [points]: Computing exacts for 256 points
0.291 * * * * [points]: Setting MPFR precision to 64
0.310 * * * * [points]: Setting MPFR precision to 320
0.330 * * * * [points]: Filtering points with unrepresentable outputs
0.332 * * * * [points]: Sampled 256 points with exact outputs
0.332 * * * [progress]: [2/2] Setting up program.
0.354 * [progress]: [Phase 2 of 3] Improving.
0.355 * * * * [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.356 * [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.358 * * [simplify]: iters left: 6 (16 enodes)
0.396 * * [simplify]: iters left: 5 (45 enodes)
0.406 * * [simplify]: iters left: 4 (91 enodes)
0.445 * * [simplify]: iters left: 3 (310 enodes)
0.662 * * [simplify]: Extracting #0: cost 1 inf + 0
0.663 * * [simplify]: Extracting #1: cost 31 inf + 0
0.664 * * [simplify]: Extracting #2: cost 123 inf + 1
0.666 * * [simplify]: Extracting #3: cost 200 inf + 1531
0.668 * * [simplify]: Extracting #4: cost 265 inf + 7949
0.671 * * [simplify]: Extracting #5: cost 321 inf + 21683
0.679 * * [simplify]: Extracting #6: cost 355 inf + 88776
0.709 * * [simplify]: Extracting #7: cost 146 inf + 448651
0.755 * * [simplify]: Extracting #8: cost 8 inf + 713461
0.807 * * [simplify]: Extracting #9: cost 0 inf + 728055
0.851 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
0.852 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
0.874 * * [progress]: iteration 1 / 4
0.874 * * * [progress]: picking best candidate
0.908 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
0.908 * * * [progress]: localizing error
1.199 * * * [progress]: generating rewritten candidates
1.200 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.203 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
1.207 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 1)
1.211 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2)
1.213 * * * [progress]: generating series expansions
1.213 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.213 * * * * [progress]: [ 2 / 4 ] generating series at (2)
1.213 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 1)
1.213 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2)
1.213 * * * [progress]: simplifying candidates
1.213 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
1.213 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1.214 * * [simplify]: iters left: 5 (11 enodes)
1.216 * * [simplify]: iters left: 4 (29 enodes)
1.221 * * [simplify]: iters left: 3 (61 enodes)
1.241 * * [simplify]: iters left: 2 (176 enodes)
1.323 * * [simplify]: Extracting #0: cost 1 inf + 0
1.323 * * [simplify]: Extracting #1: cost 2 inf + 0
1.323 * * [simplify]: Extracting #2: cost 3 inf + 0
1.323 * * [simplify]: Extracting #3: cost 17 inf + 0
1.323 * * [simplify]: Extracting #4: cost 61 inf + 0
1.324 * * [simplify]: Extracting #5: cost 127 inf + 646
1.325 * * [simplify]: Extracting #6: cost 193 inf + 14402
1.328 * * [simplify]: Extracting #7: cost 126 inf + 105460
1.342 * * [simplify]: Extracting #8: cost 12 inf + 317072
1.366 * * [simplify]: Extracting #9: cost 0 inf + 340034
1.393 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
1.393 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))) (*.p16 (real->posit16 2) a)))
1.393 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
1.393 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))
1.394 * * [simplify]: iters left: 6 (14 enodes)
1.400 * * [simplify]: iters left: 5 (42 enodes)
1.414 * * [simplify]: iters left: 4 (117 enodes)
1.465 * * [simplify]: iters left: 3 (426 enodes)
1.701 * * [simplify]: Extracting #0: cost 1 inf + 0
1.701 * * [simplify]: Extracting #1: cost 51 inf + 0
1.701 * * [simplify]: Extracting #2: cost 242 inf + 0
1.702 * * [simplify]: Extracting #3: cost 412 inf + 4894
1.721 * * [simplify]: Extracting #4: cost 407 inf + 277787
1.803 * * [simplify]: Extracting #5: cost 129 inf + 1021325
1.894 * * [simplify]: Extracting #6: cost 1 inf + 1253728
1.985 * * [simplify]: Extracting #7: cost 0 inf + 1257332
2.104 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
2.104 * [simplify]: Simplified (2 1 1) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))
2.105 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
2.105 * * [simplify]: iters left: 5 (12 enodes)
2.111 * * [simplify]: iters left: 4 (31 enodes)
2.122 * * [simplify]: iters left: 3 (64 enodes)
2.149 * * [simplify]: iters left: 2 (183 enodes)
2.269 * * [simplify]: Extracting #0: cost 1 inf + 0
2.269 * * [simplify]: Extracting #1: cost 6 inf + 0
2.269 * * [simplify]: Extracting #2: cost 10 inf + 1
2.269 * * [simplify]: Extracting #3: cost 22 inf + 804
2.270 * * [simplify]: Extracting #4: cost 64 inf + 1445
2.270 * * [simplify]: Extracting #5: cost 138 inf + 3371
2.272 * * [simplify]: Extracting #6: cost 216 inf + 12754
2.280 * * [simplify]: Extracting #7: cost 138 inf + 118173
2.302 * * [simplify]: Extracting #8: cost 17 inf + 330365
2.323 * * [simplify]: Extracting #9: cost 0 inf + 369430
2.338 * * [simplify]: Extracting #10: cost 0 inf + 369110
2.354 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
2.354 * [simplify]: Simplified (2 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))
2.354 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
2.354 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
2.354 * * [simplify]: iters left: 6 (15 enodes)
2.358 * * [simplify]: iters left: 5 (41 enodes)
2.366 * * [simplify]: iters left: 4 (85 enodes)
2.384 * * [simplify]: iters left: 3 (287 enodes)
2.506 * * [simplify]: Extracting #0: cost 1 inf + 0
2.506 * * [simplify]: Extracting #1: cost 20 inf + 0
2.507 * * [simplify]: Extracting #2: cost 91 inf + 0
2.507 * * [simplify]: Extracting #3: cost 174 inf + 83
2.508 * * [simplify]: Extracting #4: cost 237 inf + 4418
2.510 * * [simplify]: Extracting #5: cost 262 inf + 55666
2.522 * * [simplify]: Extracting #6: cost 180 inf + 332251
2.560 * * [simplify]: Extracting #7: cost 12 inf + 639867
2.616 * * [simplify]: Extracting #8: cost 0 inf + 669631
2.646 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2))
2.646 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2)) a))
2.646 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
2.646 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))
2.647 * * [simplify]: iters left: 6 (16 enodes)
2.651 * * [simplify]: iters left: 5 (46 enodes)
2.660 * * [simplify]: iters left: 4 (107 enodes)
2.701 * * [simplify]: iters left: 3 (238 enodes)
2.838 * * [simplify]: Extracting #0: cost 1 inf + 0
2.838 * * [simplify]: Extracting #1: cost 24 inf + 0
2.839 * * [simplify]: Extracting #2: cost 36 inf + 1
2.839 * * [simplify]: Extracting #3: cost 37 inf + 85
2.839 * * [simplify]: Extracting #4: cost 46 inf + 2656
2.840 * * [simplify]: Extracting #5: cost 87 inf + 3297
2.841 * * [simplify]: Extracting #6: cost 166 inf + 4900
2.844 * * [simplify]: Extracting #7: cost 230 inf + 13556
2.851 * * [simplify]: Extracting #8: cost 168 inf + 107441
2.876 * * [simplify]: Extracting #9: cost 37 inf + 337047
2.905 * * [simplify]: Extracting #10: cost 0 inf + 395102
2.935 * * [simplify]: Extracting #11: cost 0 inf + 394462
2.965 * [simplify]: Simplified to (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))
2.965 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))))
2.965 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
2.966 * [simplify]: Simplifying (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c)))
2.966 * * [simplify]: iters left: 3 (7 enodes)
2.969 * * [simplify]: iters left: 2 (16 enodes)
2.974 * * [simplify]: iters left: 1 (22 enodes)
2.980 * * [simplify]: Extracting #0: cost 1 inf + 0
2.981 * * [simplify]: Extracting #1: cost 2 inf + 0
2.981 * * [simplify]: Extracting #2: cost 8 inf + 0
2.981 * * [simplify]: Extracting #3: cost 6 inf + 324
2.981 * * [simplify]: Extracting #4: cost 5 inf + 325
2.981 * * [simplify]: Extracting #5: cost 0 inf + 2336
2.981 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
2.981 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (real->posit16 2) a)))
2.981 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
2.982 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c))))
2.982 * * [simplify]: iters left: 4 (11 enodes)
2.987 * * [simplify]: iters left: 3 (40 enodes)
3.002 * * [simplify]: iters left: 2 (105 enodes)
3.057 * * [simplify]: iters left: 1 (409 enodes)
3.937 * * [simplify]: Extracting #0: cost 1 inf + 0
3.937 * * [simplify]: Extracting #1: cost 32 inf + 0
3.938 * * [simplify]: Extracting #2: cost 197 inf + 0
3.940 * * [simplify]: Extracting #3: cost 336 inf + 2893
3.950 * * [simplify]: Extracting #4: cost 467 inf + 105237
4.003 * * [simplify]: Extracting #5: cost 158 inf + 692584
4.076 * * [simplify]: Extracting #6: cost 14 inf + 1019119
4.164 * * [simplify]: Extracting #7: cost 0 inf + 1058774
4.249 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))
4.249 * [simplify]: Simplified (2 1 2 1 1) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))
4.250 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))
4.250 * * [simplify]: iters left: 3 (9 enodes)
4.252 * * [simplify]: iters left: 2 (21 enodes)
4.256 * * [simplify]: iters left: 1 (27 enodes)
4.261 * * [simplify]: Extracting #0: cost 1 inf + 0
4.261 * * [simplify]: Extracting #1: cost 3 inf + 0
4.261 * * [simplify]: Extracting #2: cost 10 inf + 0
4.261 * * [simplify]: Extracting #3: cost 7 inf + 325
4.261 * * [simplify]: Extracting #4: cost 0 inf + 2939
4.261 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
4.261 * [simplify]: Simplified (2 1 2 1 2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))))) (*.p16 (real->posit16 2) a)))
4.261 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
4.261 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
4.262 * * [simplify]: iters left: 6 (16 enodes)
4.265 * * [simplify]: iters left: 5 (45 enodes)
4.279 * * [simplify]: iters left: 4 (91 enodes)
4.316 * * [simplify]: iters left: 3 (310 enodes)
4.469 * * [simplify]: Extracting #0: cost 1 inf + 0
4.469 * * [simplify]: Extracting #1: cost 31 inf + 0
4.469 * * [simplify]: Extracting #2: cost 123 inf + 1
4.471 * * [simplify]: Extracting #3: cost 200 inf + 1531
4.472 * * [simplify]: Extracting #4: cost 265 inf + 7949
4.475 * * [simplify]: Extracting #5: cost 321 inf + 21683
4.483 * * [simplify]: Extracting #6: cost 355 inf + 88776
4.511 * * [simplify]: Extracting #7: cost 146 inf + 448651
4.559 * * [simplify]: Extracting #8: cost 8 inf + 713461
4.622 * * [simplify]: Extracting #9: cost 0 inf + 728055
4.657 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
4.657 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
4.657 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
4.658 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
4.658 * * [simplify]: iters left: 6 (16 enodes)
4.662 * * [simplify]: iters left: 5 (45 enodes)
4.676 * * [simplify]: iters left: 4 (91 enodes)
4.714 * * [simplify]: iters left: 3 (310 enodes)
4.917 * * [simplify]: Extracting #0: cost 1 inf + 0
4.917 * * [simplify]: Extracting #1: cost 31 inf + 0
4.917 * * [simplify]: Extracting #2: cost 123 inf + 1
4.918 * * [simplify]: Extracting #3: cost 200 inf + 1531
4.920 * * [simplify]: Extracting #4: cost 265 inf + 7949
4.923 * * [simplify]: Extracting #5: cost 321 inf + 21683
4.930 * * [simplify]: Extracting #6: cost 355 inf + 88776
4.960 * * [simplify]: Extracting #7: cost 146 inf + 448651
5.010 * * [simplify]: Extracting #8: cost 8 inf + 713461
5.045 * * [simplify]: Extracting #9: cost 0 inf + 728055
5.107 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
5.107 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
5.107 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
5.107 * [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))
5.107 * * [simplify]: iters left: 6 (16 enodes)
5.115 * * [simplify]: iters left: 5 (45 enodes)
5.132 * * [simplify]: iters left: 4 (91 enodes)
5.170 * * [simplify]: iters left: 3 (310 enodes)
5.325 * * [simplify]: Extracting #0: cost 1 inf + 0
5.326 * * [simplify]: Extracting #1: cost 31 inf + 0
5.326 * * [simplify]: Extracting #2: cost 123 inf + 1
5.330 * * [simplify]: Extracting #3: cost 200 inf + 1531
5.331 * * [simplify]: Extracting #4: cost 265 inf + 7949
5.333 * * [simplify]: Extracting #5: cost 321 inf + 21683
5.338 * * [simplify]: Extracting #6: cost 355 inf + 88776
5.368 * * [simplify]: Extracting #7: cost 146 inf + 448651
5.405 * * [simplify]: Extracting #8: cost 8 inf + 713461
5.452 * * [simplify]: Extracting #9: cost 0 inf + 728055
5.514 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
5.515 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
5.515 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
5.515 * [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))
5.515 * * [simplify]: iters left: 6 (16 enodes)
5.522 * * [simplify]: iters left: 5 (45 enodes)
5.531 * * [simplify]: iters left: 4 (91 enodes)
5.550 * * [simplify]: iters left: 3 (310 enodes)
5.720 * * [simplify]: Extracting #0: cost 1 inf + 0
5.721 * * [simplify]: Extracting #1: cost 31 inf + 0
5.721 * * [simplify]: Extracting #2: cost 123 inf + 1
5.723 * * [simplify]: Extracting #3: cost 200 inf + 1531
5.725 * * [simplify]: Extracting #4: cost 265 inf + 7949
5.728 * * [simplify]: Extracting #5: cost 321 inf + 21683
5.735 * * [simplify]: Extracting #6: cost 355 inf + 88776
5.765 * * [simplify]: Extracting #7: cost 146 inf + 448651
5.827 * * [simplify]: Extracting #8: cost 8 inf + 713461
5.888 * * [simplify]: Extracting #9: cost 0 inf + 728055
5.950 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
5.951 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
5.951 * * * [progress]: adding candidates to table
6.356 * * [progress]: iteration 2 / 4
6.356 * * * [progress]: picking best candidate
6.432 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
6.432 * * * [progress]: localizing error
6.684 * * * [progress]: generating rewritten candidates
6.684 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
6.688 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2 1)
6.698 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
6.698 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 1 2)
6.707 * * * [progress]: generating series expansions
6.707 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
6.707 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2 1)
6.707 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
6.707 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 1 2)
6.707 * * * [progress]: simplifying candidates
6.707 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))>
6.707 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
6.707 * * [simplify]: iters left: 5 (11 enodes)
6.722 * * [simplify]: iters left: 4 (29 enodes)
6.732 * * [simplify]: iters left: 3 (61 enodes)
6.745 * * [simplify]: iters left: 2 (176 enodes)
6.849 * * [simplify]: Extracting #0: cost 1 inf + 0
6.849 * * [simplify]: Extracting #1: cost 2 inf + 0
6.849 * * [simplify]: Extracting #2: cost 3 inf + 0
6.850 * * [simplify]: Extracting #3: cost 17 inf + 0
6.850 * * [simplify]: Extracting #4: cost 61 inf + 0
6.850 * * [simplify]: Extracting #5: cost 127 inf + 646
6.852 * * [simplify]: Extracting #6: cost 193 inf + 14402
6.859 * * [simplify]: Extracting #7: cost 126 inf + 105460
6.881 * * [simplify]: Extracting #8: cost 12 inf + 317072
6.907 * * [simplify]: Extracting #9: cost 0 inf + 340034
6.933 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
6.933 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))) (real->posit16 2)) a))
6.933 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))>
6.933 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))
6.934 * * [simplify]: iters left: 6 (14 enodes)
6.940 * * [simplify]: iters left: 5 (42 enodes)
6.959 * * [simplify]: iters left: 4 (117 enodes)
7.012 * * [simplify]: iters left: 3 (426 enodes)
7.300 * * [simplify]: Extracting #0: cost 1 inf + 0
7.300 * * [simplify]: Extracting #1: cost 51 inf + 0
7.301 * * [simplify]: Extracting #2: cost 242 inf + 0
7.302 * * [simplify]: Extracting #3: cost 412 inf + 4894
7.312 * * [simplify]: Extracting #4: cost 407 inf + 277787
7.395 * * [simplify]: Extracting #5: cost 129 inf + 1021325
7.506 * * [simplify]: Extracting #6: cost 1 inf + 1253728
7.588 * * [simplify]: Extracting #7: cost 0 inf + 1257332
7.656 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
7.656 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))
7.657 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
7.657 * * [simplify]: iters left: 5 (12 enodes)
7.660 * * [simplify]: iters left: 4 (31 enodes)
7.666 * * [simplify]: iters left: 3 (64 enodes)
7.683 * * [simplify]: iters left: 2 (183 enodes)
7.776 * * [simplify]: Extracting #0: cost 1 inf + 0
7.776 * * [simplify]: Extracting #1: cost 6 inf + 0
7.776 * * [simplify]: Extracting #2: cost 10 inf + 1
7.776 * * [simplify]: Extracting #3: cost 22 inf + 804
7.777 * * [simplify]: Extracting #4: cost 64 inf + 1445
7.778 * * [simplify]: Extracting #5: cost 138 inf + 3371
7.785 * * [simplify]: Extracting #6: cost 216 inf + 12754
7.792 * * [simplify]: Extracting #7: cost 138 inf + 118173
7.814 * * [simplify]: Extracting #8: cost 17 inf + 330365
7.841 * * [simplify]: Extracting #9: cost 0 inf + 369430
7.869 * * [simplify]: Extracting #10: cost 0 inf + 369110
7.897 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
7.897 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))
7.898 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))>
7.898 * [simplify]: Simplifying (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c)))
7.898 * * [simplify]: iters left: 3 (7 enodes)
7.902 * * [simplify]: iters left: 2 (16 enodes)
7.909 * * [simplify]: iters left: 1 (22 enodes)
7.916 * * [simplify]: Extracting #0: cost 1 inf + 0
7.916 * * [simplify]: Extracting #1: cost 2 inf + 0
7.916 * * [simplify]: Extracting #2: cost 8 inf + 0
7.916 * * [simplify]: Extracting #3: cost 6 inf + 324
7.916 * * [simplify]: Extracting #4: cost 5 inf + 325
7.916 * * [simplify]: Extracting #5: cost 0 inf + 2336
7.917 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
7.917 * [simplify]: Simplified (2 1 1 2 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))))) (real->posit16 2)) a))
7.917 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))>
7.917 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c))))
7.917 * * [simplify]: iters left: 4 (11 enodes)
7.923 * * [simplify]: iters left: 3 (40 enodes)
7.939 * * [simplify]: iters left: 2 (105 enodes)
7.983 * * [simplify]: iters left: 1 (409 enodes)
8.335 * * [simplify]: Extracting #0: cost 1 inf + 0
8.335 * * [simplify]: Extracting #1: cost 32 inf + 0
8.335 * * [simplify]: Extracting #2: cost 197 inf + 0
8.337 * * [simplify]: Extracting #3: cost 336 inf + 2893
8.343 * * [simplify]: Extracting #4: cost 467 inf + 105237
8.379 * * [simplify]: Extracting #5: cost 158 inf + 692584
8.423 * * [simplify]: Extracting #6: cost 14 inf + 1019119
8.495 * * [simplify]: Extracting #7: cost 0 inf + 1058774
8.561 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))
8.561 * [simplify]: Simplified (2 1 1 2 1 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))
8.561 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))
8.562 * * [simplify]: iters left: 3 (9 enodes)
8.566 * * [simplify]: iters left: 2 (21 enodes)
8.574 * * [simplify]: iters left: 1 (27 enodes)
8.581 * * [simplify]: Extracting #0: cost 1 inf + 0
8.581 * * [simplify]: Extracting #1: cost 3 inf + 0
8.581 * * [simplify]: Extracting #2: cost 10 inf + 0
8.581 * * [simplify]: Extracting #3: cost 7 inf + 325
8.581 * * [simplify]: Extracting #4: cost 0 inf + 2939
8.582 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
8.582 * [simplify]: Simplified (2 1 1 2 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))))) (real->posit16 2)) a))
8.582 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
8.582 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
8.582 * * [simplify]: iters left: 2 (4 enodes)
8.583 * * [simplify]: iters left: 1 (8 enodes)
8.585 * * [simplify]: Extracting #0: cost 1 inf + 0
8.585 * * [simplify]: Extracting #1: cost 3 inf + 0
8.585 * * [simplify]: Extracting #2: cost 3 inf + 1
8.585 * * [simplify]: Extracting #3: cost 2 inf + 2
8.585 * * [simplify]: Extracting #4: cost 0 inf + 325
8.585 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
8.585 * [simplify]: Simplified (2 1 1 2 1 2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c)))) (real->posit16 2)) a))
8.585 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (real->posit16 2)) a))>
8.585 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
8.585 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
8.585 * * [simplify]: iters left: 6 (15 enodes)
8.589 * * [simplify]: iters left: 5 (41 enodes)
8.596 * * [simplify]: iters left: 4 (85 enodes)
8.614 * * [simplify]: iters left: 3 (287 enodes)
8.765 * * [simplify]: Extracting #0: cost 1 inf + 0
8.766 * * [simplify]: Extracting #1: cost 20 inf + 0
8.766 * * [simplify]: Extracting #2: cost 91 inf + 0
8.775 * * [simplify]: Extracting #3: cost 174 inf + 83
8.776 * * [simplify]: Extracting #4: cost 237 inf + 4418
8.781 * * [simplify]: Extracting #5: cost 262 inf + 55666
8.804 * * [simplify]: Extracting #6: cost 180 inf + 332251
8.852 * * [simplify]: Extracting #7: cost 12 inf + 639867
8.908 * * [simplify]: Extracting #8: cost 0 inf + 669631
8.961 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2))
8.961 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2)) a))
8.961 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
8.961 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
8.961 * * [simplify]: iters left: 6 (15 enodes)
8.965 * * [simplify]: iters left: 5 (41 enodes)
8.973 * * [simplify]: iters left: 4 (85 enodes)
8.996 * * [simplify]: iters left: 3 (287 enodes)
9.126 * * [simplify]: Extracting #0: cost 1 inf + 0
9.126 * * [simplify]: Extracting #1: cost 20 inf + 0
9.127 * * [simplify]: Extracting #2: cost 91 inf + 0
9.128 * * [simplify]: Extracting #3: cost 174 inf + 83
9.129 * * [simplify]: Extracting #4: cost 237 inf + 4418
9.134 * * [simplify]: Extracting #5: cost 262 inf + 55666
9.155 * * [simplify]: Extracting #6: cost 180 inf + 332251
9.179 * * [simplify]: Extracting #7: cost 12 inf + 639867
9.213 * * [simplify]: Extracting #8: cost 0 inf + 669631
9.252 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2))
9.252 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2)) a))
9.252 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
9.252 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
9.252 * * [simplify]: iters left: 6 (15 enodes)
9.256 * * [simplify]: iters left: 5 (41 enodes)
9.264 * * [simplify]: iters left: 4 (85 enodes)
9.296 * * [simplify]: iters left: 3 (287 enodes)
9.432 * * [simplify]: Extracting #0: cost 1 inf + 0
9.432 * * [simplify]: Extracting #1: cost 20 inf + 0
9.432 * * [simplify]: Extracting #2: cost 91 inf + 0
9.433 * * [simplify]: Extracting #3: cost 174 inf + 83
9.435 * * [simplify]: Extracting #4: cost 237 inf + 4418
9.439 * * [simplify]: Extracting #5: cost 262 inf + 55666
9.459 * * [simplify]: Extracting #6: cost 180 inf + 332251
9.487 * * [simplify]: Extracting #7: cost 12 inf + 639867
9.526 * * [simplify]: Extracting #8: cost 0 inf + 669631
9.584 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2))
9.584 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2)) a))
9.584 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
9.585 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
9.585 * * [simplify]: iters left: 6 (15 enodes)
9.592 * * [simplify]: iters left: 5 (41 enodes)
9.607 * * [simplify]: iters left: 4 (85 enodes)
9.643 * * [simplify]: iters left: 3 (287 enodes)
9.800 * * [simplify]: Extracting #0: cost 1 inf + 0
9.800 * * [simplify]: Extracting #1: cost 20 inf + 0
9.800 * * [simplify]: Extracting #2: cost 91 inf + 0
9.801 * * [simplify]: Extracting #3: cost 174 inf + 83
9.802 * * [simplify]: Extracting #4: cost 237 inf + 4418
9.804 * * [simplify]: Extracting #5: cost 262 inf + 55666
9.816 * * [simplify]: Extracting #6: cost 180 inf + 332251
9.852 * * [simplify]: Extracting #7: cost 12 inf + 639867
9.908 * * [simplify]: Extracting #8: cost 0 inf + 669631
9.951 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2))
9.951 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (real->posit16 2)) a))
9.951 * * * [progress]: adding candidates to table
10.516 * * [progress]: iteration 3 / 4
10.516 * * * [progress]: picking best candidate
10.633 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
10.634 * * * [progress]: localizing error
10.948 * * * [progress]: generating rewritten candidates
10.948 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
10.952 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2 1)
10.962 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
10.963 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
10.969 * * * [progress]: generating series expansions
10.969 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
10.970 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2 1)
10.970 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
10.970 * * * * [progress]: [ 4 / 4 ] generating series at (2)
10.970 * * * [progress]: simplifying candidates
10.970 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))>
10.970 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
10.970 * * [simplify]: iters left: 6 (11 enodes)
10.975 * * [simplify]: iters left: 5 (29 enodes)
10.986 * * [simplify]: iters left: 4 (61 enodes)
11.012 * * [simplify]: iters left: 3 (181 enodes)
11.114 * * [simplify]: Extracting #0: cost 1 inf + 0
11.114 * * [simplify]: Extracting #1: cost 2 inf + 0
11.114 * * [simplify]: Extracting #2: cost 3 inf + 0
11.114 * * [simplify]: Extracting #3: cost 17 inf + 0
11.114 * * [simplify]: Extracting #4: cost 61 inf + 0
11.115 * * [simplify]: Extracting #5: cost 136 inf + 324
11.117 * * [simplify]: Extracting #6: cost 193 inf + 16244
11.126 * * [simplify]: Extracting #7: cost 123 inf + 104476
11.150 * * [simplify]: Extracting #8: cost 8 inf + 322378
11.178 * * [simplify]: Extracting #9: cost 0 inf + 339405
11.206 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))
11.206 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))) (real->posit16 2)) a))
11.206 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))>
11.207 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))
11.207 * * [simplify]: iters left: 6 (14 enodes)
11.214 * * [simplify]: iters left: 5 (42 enodes)
11.229 * * [simplify]: iters left: 4 (117 enodes)
11.284 * * [simplify]: iters left: 3 (432 enodes)
11.502 * * [simplify]: Extracting #0: cost 1 inf + 0
11.502 * * [simplify]: Extracting #1: cost 51 inf + 0
11.503 * * [simplify]: Extracting #2: cost 242 inf + 0
11.511 * * [simplify]: Extracting #3: cost 411 inf + 3092
11.531 * * [simplify]: Extracting #4: cost 417 inf + 266776
11.613 * * [simplify]: Extracting #5: cost 155 inf + 959244
11.705 * * [simplify]: Extracting #6: cost 2 inf + 1266055
11.781 * * [simplify]: Extracting #7: cost 0 inf + 1272103
11.903 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4))))
11.904 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4)))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))
11.904 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
11.904 * * [simplify]: iters left: 6 (12 enodes)
11.910 * * [simplify]: iters left: 5 (31 enodes)
11.922 * * [simplify]: iters left: 4 (64 enodes)
11.950 * * [simplify]: iters left: 3 (187 enodes)
12.065 * * [simplify]: Extracting #0: cost 1 inf + 0
12.065 * * [simplify]: Extracting #1: cost 6 inf + 0
12.065 * * [simplify]: Extracting #2: cost 10 inf + 1
12.066 * * [simplify]: Extracting #3: cost 22 inf + 804
12.066 * * [simplify]: Extracting #4: cost 64 inf + 1445
12.067 * * [simplify]: Extracting #5: cost 135 inf + 3049
12.069 * * [simplify]: Extracting #6: cost 191 inf + 13398
12.078 * * [simplify]: Extracting #7: cost 127 inf + 98415
12.100 * * [simplify]: Extracting #8: cost 10 inf + 313726
12.131 * * [simplify]: Extracting #9: cost 0 inf + 337284
12.155 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) b)
12.155 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) b)) (real->posit16 2)) a))
12.156 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))>
12.156 * [simplify]: Simplifying (neg.p16 (*.p16 (*.p16 (real->posit16 4) a) c))
12.156 * * [simplify]: iters left: 4 (7 enodes)
12.159 * * [simplify]: iters left: 3 (16 enodes)
12.164 * * [simplify]: iters left: 2 (22 enodes)
12.171 * * [simplify]: iters left: 1 (23 enodes)
12.177 * * [simplify]: Extracting #0: cost 1 inf + 0
12.178 * * [simplify]: Extracting #1: cost 2 inf + 0
12.178 * * [simplify]: Extracting #2: cost 8 inf + 0
12.178 * * [simplify]: Extracting #3: cost 6 inf + 324
12.178 * * [simplify]: Extracting #4: cost 5 inf + 325
12.178 * * [simplify]: Extracting #5: cost 0 inf + 2336
12.178 * [simplify]: Simplified to (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
12.178 * [simplify]: Simplified (2 1 1 2 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))))) (real->posit16 2)) a))
12.179 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))>
12.179 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c)))
12.179 * * [simplify]: iters left: 5 (11 enodes)
12.184 * * [simplify]: iters left: 4 (40 enodes)
12.200 * * [simplify]: iters left: 3 (100 enodes)
12.249 * * [simplify]: iters left: 2 (360 enodes)
12.576 * * [simplify]: Extracting #0: cost 1 inf + 0
12.576 * * [simplify]: Extracting #1: cost 32 inf + 0
12.576 * * [simplify]: Extracting #2: cost 200 inf + 0
12.577 * * [simplify]: Extracting #3: cost 325 inf + 3535
12.581 * * [simplify]: Extracting #4: cost 456 inf + 67717
12.611 * * [simplify]: Extracting #5: cost 170 inf + 641860
12.659 * * [simplify]: Extracting #6: cost 19 inf + 997414
12.751 * * [simplify]: Extracting #7: cost 0 inf + 1027370
12.800 * * [simplify]: Extracting #8: cost 0 inf + 1020770
12.846 * [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))))
12.847 * [simplify]: Simplified (2 1 1 2 1 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (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 (real->posit16 4) a) c))))) (real->posit16 2)) a))
12.847 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))
12.847 * * [simplify]: iters left: 4 (9 enodes)
12.849 * * [simplify]: iters left: 3 (21 enodes)
12.852 * * [simplify]: iters left: 2 (27 enodes)
12.856 * * [simplify]: iters left: 1 (29 enodes)
12.860 * * [simplify]: Extracting #0: cost 1 inf + 0
12.860 * * [simplify]: Extracting #1: cost 3 inf + 0
12.860 * * [simplify]: Extracting #2: cost 10 inf + 0
12.860 * * [simplify]: Extracting #3: cost 7 inf + 325
12.860 * * [simplify]: Extracting #4: cost 0 inf + 2939
12.861 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b))
12.861 * [simplify]: Simplified (2 1 1 2 1 2) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b))))) (real->posit16 2)) a))
12.861 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 a (real->posit16 2))))>
12.861 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
12.861 * * [simplify]: iters left: 2 (4 enodes)
12.862 * * [simplify]: iters left: 1 (8 enodes)
12.863 * * [simplify]: Extracting #0: cost 1 inf + 0
12.863 * * [simplify]: Extracting #1: cost 3 inf + 0
12.864 * * [simplify]: Extracting #2: cost 3 inf + 1
12.864 * * [simplify]: Extracting #3: cost 0 inf + 325
12.864 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
12.864 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 a (real->posit16 2))))
12.864 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
12.864 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
12.864 * * [simplify]: iters left: 2 (4 enodes)
12.865 * * [simplify]: iters left: 1 (8 enodes)
12.866 * * [simplify]: Extracting #0: cost 1 inf + 0
12.866 * * [simplify]: Extracting #1: cost 3 inf + 0
12.866 * * [simplify]: Extracting #2: cost 3 inf + 1
12.866 * * [simplify]: Extracting #3: cost 2 inf + 2
12.866 * * [simplify]: Extracting #4: cost 0 inf + 325
12.866 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
12.866 * [simplify]: Simplified (2 1 1 2 1 2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c)))) (real->posit16 2)) a))
12.866 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
12.867 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
12.867 * * [simplify]: iters left: 2 (4 enodes)
12.868 * * [simplify]: iters left: 1 (8 enodes)
12.870 * * [simplify]: Extracting #0: cost 1 inf + 0
12.870 * * [simplify]: Extracting #1: cost 3 inf + 0
12.870 * * [simplify]: Extracting #2: cost 3 inf + 1
12.870 * * [simplify]: Extracting #3: cost 2 inf + 2
12.870 * * [simplify]: Extracting #4: cost 0 inf + 325
12.870 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
12.870 * [simplify]: Simplified (2 1 1 2 1 2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c)))) (real->posit16 2)) a))
12.871 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
12.871 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
12.871 * * [simplify]: iters left: 2 (4 enodes)
12.873 * * [simplify]: iters left: 1 (8 enodes)
12.875 * * [simplify]: Extracting #0: cost 1 inf + 0
12.875 * * [simplify]: Extracting #1: cost 3 inf + 0
12.875 * * [simplify]: Extracting #2: cost 3 inf + 1
12.875 * * [simplify]: Extracting #3: cost 2 inf + 2
12.875 * * [simplify]: Extracting #4: cost 0 inf + 325
12.876 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
12.876 * [simplify]: Simplified (2 1 1 2 1 2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c)))) (real->posit16 2)) a))
12.876 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
12.876 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
12.876 * * [simplify]: iters left: 2 (4 enodes)
12.878 * * [simplify]: iters left: 1 (8 enodes)
12.880 * * [simplify]: Extracting #0: cost 1 inf + 0
12.881 * * [simplify]: Extracting #1: cost 3 inf + 0
12.882 * * [simplify]: Extracting #2: cost 3 inf + 1
12.882 * * [simplify]: Extracting #3: cost 2 inf + 2
12.882 * * [simplify]: Extracting #4: cost 0 inf + 325
12.882 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
12.882 * [simplify]: Simplified (2 1 1 2 1 2 1) to (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a (real->posit16 4)) c)))) (real->posit16 2)) a))
12.882 * * * [progress]: adding candidates to table
13.366 * * [progress]: iteration 4 / 4
13.366 * * * [progress]: picking best candidate
13.539 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
13.539 * * * [progress]: localizing error
13.911 * * * [progress]: generating rewritten candidates
13.911 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
13.916 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
13.922 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
13.928 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2 1)
13.938 * * * [progress]: generating series expansions
13.938 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
13.938 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
13.938 * * * * [progress]: [ 3 / 4 ] generating series at (2)
13.938 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2 1)
13.938 * * * [progress]: simplifying candidates
13.938 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (neg.p16 b))) (*.p16 (real->posit16 2) a)))>
13.938 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))>
13.939 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2))
13.939 * * [simplify]: iters left: 6 (20 enodes)
13.949 * * [simplify]: iters left: 5 (50 enodes)
13.969 * * [simplify]: iters left: 4 (122 enodes)
14.015 * * [simplify]: iters left: 3 (328 enodes)
14.208 * * [simplify]: Extracting #0: cost 1 inf + 0
14.208 * * [simplify]: Extracting #1: cost 9 inf + 0
14.208 * * [simplify]: Extracting #2: cost 36 inf + 0
14.209 * * [simplify]: Extracting #3: cost 91 inf + 525
14.209 * * [simplify]: Extracting #4: cost 103 inf + 15440
14.211 * * [simplify]: Extracting #5: cost 157 inf + 31956
14.215 * * [simplify]: Extracting #6: cost 194 inf + 98726
14.243 * * [simplify]: Extracting #7: cost 16 inf + 431933
14.276 * * [simplify]: Extracting #8: cost 0 inf + 419397
14.306 * * [simplify]: Extracting #9: cost 0 inf + 417437
14.323 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b)))
14.323 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))
14.323 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
14.323 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))
14.324 * * [simplify]: iters left: 6 (16 enodes)
14.328 * * [simplify]: iters left: 5 (46 enodes)
14.337 * * [simplify]: iters left: 4 (107 enodes)
14.359 * * [simplify]: iters left: 3 (238 enodes)
14.432 * * [simplify]: Extracting #0: cost 1 inf + 0
14.432 * * [simplify]: Extracting #1: cost 24 inf + 0
14.432 * * [simplify]: Extracting #2: cost 36 inf + 1
14.432 * * [simplify]: Extracting #3: cost 37 inf + 85
14.433 * * [simplify]: Extracting #4: cost 46 inf + 2656
14.433 * * [simplify]: Extracting #5: cost 87 inf + 3297
14.434 * * [simplify]: Extracting #6: cost 166 inf + 4900
14.435 * * [simplify]: Extracting #7: cost 230 inf + 13556
14.438 * * [simplify]: Extracting #8: cost 168 inf + 107441
14.450 * * [simplify]: Extracting #9: cost 37 inf + 337047
14.465 * * [simplify]: Extracting #10: cost 0 inf + 395102
14.484 * * [simplify]: Extracting #11: cost 0 inf + 394462
14.500 * [simplify]: Simplified to (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))
14.500 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))))
14.500 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c))))))) (*.p16 (real->posit16 2) a)))>
14.500 * [simplify]: Simplifying (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c)))
14.500 * * [simplify]: iters left: 3 (7 enodes)
14.502 * * [simplify]: iters left: 2 (16 enodes)
14.505 * * [simplify]: iters left: 1 (22 enodes)
14.511 * * [simplify]: Extracting #0: cost 1 inf + 0
14.511 * * [simplify]: Extracting #1: cost 2 inf + 0
14.511 * * [simplify]: Extracting #2: cost 8 inf + 0
14.511 * * [simplify]: Extracting #3: cost 6 inf + 324
14.511 * * [simplify]: Extracting #4: cost 5 inf + 325
14.511 * * [simplify]: Extracting #5: cost 0 inf + 2336
14.512 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
14.512 * [simplify]: Simplified (2 1 2 2 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))))) (*.p16 (real->posit16 2) a)))
14.512 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) (*.p16 (real->posit16 2) a)))>
14.512 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c))))
14.513 * * [simplify]: iters left: 4 (11 enodes)
14.518 * * [simplify]: iters left: 3 (40 enodes)
14.533 * * [simplify]: iters left: 2 (105 enodes)
14.587 * * [simplify]: iters left: 1 (409 enodes)
14.983 * * [simplify]: Extracting #0: cost 1 inf + 0
14.983 * * [simplify]: Extracting #1: cost 32 inf + 0
14.983 * * [simplify]: Extracting #2: cost 197 inf + 0
14.984 * * [simplify]: Extracting #3: cost 336 inf + 2893
14.989 * * [simplify]: Extracting #4: cost 467 inf + 105237
15.030 * * [simplify]: Extracting #5: cost 158 inf + 692584
15.085 * * [simplify]: Extracting #6: cost 14 inf + 1019119
15.155 * * [simplify]: Extracting #7: cost 0 inf + 1058774
15.219 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))
15.219 * [simplify]: Simplified (2 1 2 2 1 1) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 b b)) (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) (*.p16 (real->posit16 2) a)))
15.219 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))
15.219 * * [simplify]: iters left: 3 (9 enodes)
15.223 * * [simplify]: iters left: 2 (21 enodes)
15.230 * * [simplify]: iters left: 1 (27 enodes)
15.238 * * [simplify]: Extracting #0: cost 1 inf + 0
15.238 * * [simplify]: Extracting #1: cost 3 inf + 0
15.238 * * [simplify]: Extracting #2: cost 10 inf + 0
15.238 * * [simplify]: Extracting #3: cost 7 inf + 325
15.238 * * [simplify]: Extracting #4: cost 0 inf + 2939
15.238 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
15.238 * [simplify]: Simplified (2 1 2 2 1 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b)))))) (*.p16 (real->posit16 2) a)))
15.239 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
15.239 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a))
15.239 * * [simplify]: iters left: 6 (21 enodes)
15.248 * * [simplify]: iters left: 5 (54 enodes)
15.258 * * [simplify]: iters left: 4 (133 enodes)
15.289 * * [simplify]: iters left: 3 (370 enodes)
15.473 * * [simplify]: Extracting #0: cost 1 inf + 0
15.473 * * [simplify]: Extracting #1: cost 13 inf + 0
15.473 * * [simplify]: Extracting #2: cost 47 inf + 1
15.473 * * [simplify]: Extracting #3: cost 111 inf + 84
15.474 * * [simplify]: Extracting #4: cost 134 inf + 8949
15.476 * * [simplify]: Extracting #5: cost 180 inf + 29874
15.482 * * [simplify]: Extracting #6: cost 220 inf + 71010
15.495 * * [simplify]: Extracting #7: cost 61 inf + 372007
15.514 * * [simplify]: Extracting #8: cost 3 inf + 443221
15.532 * * [simplify]: Extracting #9: cost 0 inf + 440433
15.559 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))
15.559 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))
15.559 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
15.559 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a))
15.560 * * [simplify]: iters left: 6 (21 enodes)
15.569 * * [simplify]: iters left: 5 (54 enodes)
15.591 * * [simplify]: iters left: 4 (133 enodes)
15.647 * * [simplify]: iters left: 3 (370 enodes)
15.841 * * [simplify]: Extracting #0: cost 1 inf + 0
15.841 * * [simplify]: Extracting #1: cost 13 inf + 0
15.841 * * [simplify]: Extracting #2: cost 47 inf + 1
15.841 * * [simplify]: Extracting #3: cost 111 inf + 84
15.842 * * [simplify]: Extracting #4: cost 134 inf + 8949
15.844 * * [simplify]: Extracting #5: cost 180 inf + 29874
15.847 * * [simplify]: Extracting #6: cost 220 inf + 71010
15.861 * * [simplify]: Extracting #7: cost 61 inf + 372007
15.879 * * [simplify]: Extracting #8: cost 3 inf + 443221
15.901 * * [simplify]: Extracting #9: cost 0 inf + 440433
15.941 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))
15.941 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))
15.941 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
15.941 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a))
15.942 * * [simplify]: iters left: 6 (21 enodes)
15.951 * * [simplify]: iters left: 5 (54 enodes)
15.970 * * [simplify]: iters left: 4 (133 enodes)
16.001 * * [simplify]: iters left: 3 (370 enodes)
16.248 * * [simplify]: Extracting #0: cost 1 inf + 0
16.248 * * [simplify]: Extracting #1: cost 13 inf + 0
16.249 * * [simplify]: Extracting #2: cost 47 inf + 1
16.249 * * [simplify]: Extracting #3: cost 111 inf + 84
16.251 * * [simplify]: Extracting #4: cost 134 inf + 8949
16.254 * * [simplify]: Extracting #5: cost 180 inf + 29874
16.262 * * [simplify]: Extracting #6: cost 220 inf + 71010
16.286 * * [simplify]: Extracting #7: cost 61 inf + 372007
16.304 * * [simplify]: Extracting #8: cost 3 inf + 443221
16.337 * * [simplify]: Extracting #9: cost 0 inf + 440433
16.374 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))
16.374 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))
16.374 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
16.374 * [simplify]: Simplifying (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a))
16.375 * * [simplify]: iters left: 6 (21 enodes)
16.379 * * [simplify]: iters left: 5 (54 enodes)
16.390 * * [simplify]: iters left: 4 (133 enodes)
16.428 * * [simplify]: iters left: 3 (370 enodes)
16.716 * * [simplify]: Extracting #0: cost 1 inf + 0
16.716 * * [simplify]: Extracting #1: cost 13 inf + 0
16.717 * * [simplify]: Extracting #2: cost 47 inf + 1
16.717 * * [simplify]: Extracting #3: cost 111 inf + 84
16.719 * * [simplify]: Extracting #4: cost 134 inf + 8949
16.723 * * [simplify]: Extracting #5: cost 180 inf + 29874
16.730 * * [simplify]: Extracting #6: cost 220 inf + 71010
16.757 * * [simplify]: Extracting #7: cost 61 inf + 372007
16.799 * * [simplify]: Extracting #8: cost 3 inf + 443221
16.837 * * [simplify]: Extracting #9: cost 0 inf + 440433
16.875 * [simplify]: Simplified to (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))
16.875 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))
16.875 * * * [progress]: adding candidates to table
17.573 * [progress]: [Phase 3 of 3] Extracting.
17.573 * * [regime]: Finding splitpoints for: (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))>)
17.582 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
17.583 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))>)
18.124 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))>)
18.615 * * * * [regimes]: Trying to branch on b from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 4) (*.p16 a c)) (*.p16 (real->posit16 4) (*.p16 a c)))) (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (real->posit16 2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b))) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (real->posit16 0.0) (*.p16 (real->posit16 4) (*.p16 c a))) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a))))>)
18.955 * * * [regime]: Found split indices: #<option (#s(si 6 256))>
18.956 * [simplify]: Simplifying (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a)
18.956 * * [simplify]: iters left: 6 (16 enodes)
18.960 * * [simplify]: Extracting #0: cost 1 inf + 0
18.960 * * [simplify]: Extracting #1: cost 3 inf + 0
18.960 * * [simplify]: Extracting #2: cost 4 inf + 1
18.960 * * [simplify]: Extracting #3: cost 7 inf + 1
18.960 * * [simplify]: Extracting #4: cost 7 inf + 3
18.960 * * [simplify]: Extracting #5: cost 8 inf + 4
18.960 * * [simplify]: Extracting #6: cost 8 inf + 406
18.960 * * [simplify]: Extracting #7: cost 8 inf + 407
18.961 * * [simplify]: Extracting #8: cost 9 inf + 407
18.961 * * [simplify]: Extracting #9: cost 8 inf + 408
18.961 * * [simplify]: Extracting #10: cost 4 inf + 2418
18.961 * * [simplify]: Extracting #11: cost 2 inf + 4746
18.962 * * [simplify]: Extracting #12: cost 0 inf + 8556
18.962 * [simplify]: Simplified to (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a)
18.962 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
19.025 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
19.030 * * * * [points]: Setting MPFR precision to 64
19.032 * * * * [points]: Setting MPFR precision to 320
19.035 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
19.041 * * * * [points]: Setting MPFR precision to 64
19.045 * * * * [points]: Setting MPFR precision to 320
19.049 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
19.054 * * * * [points]: Setting MPFR precision to 64
19.062 * * * * [points]: Setting MPFR precision to 320
19.070 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
19.075 * * * * [points]: Setting MPFR precision to 64
19.091 * * * * [points]: Setting MPFR precision to 320
19.107 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
19.112 * * * * [points]: Setting MPFR precision to 64
19.171 * * * * [points]: Setting MPFR precision to 320
19.205 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
19.211 * * * * [points]: Setting MPFR precision to 64
19.273 * * * * [points]: Setting MPFR precision to 320
19.333 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
19.339 * * * * [points]: Setting MPFR precision to 64
19.512 * * * * [points]: Setting MPFR precision to 320
19.696 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
19.702 * * * * [points]: Setting MPFR precision to 64
20.007 * * * * [points]: Setting MPFR precision to 320
20.655 * * * * [points]: Computing exacts for 8000 points
20.658 * * * * [points]: Setting MPFR precision to 64
21.554 * * * * [points]: Setting MPFR precision to 320
22.390 * * * * [points]: Filtering points with unrepresentable outputs
22.410 * * * * [points]: Sampled 8000 points with exact outputs
32.288 * [regime-testing]: Baseline error score: 64.0
32.291 * [regime-testing]: Oracle error score: 64.0
32.298 * [regime-testing]: End program error score: 1.5419624136882608