0.002 * [progress]: [Phase 1 of 3] Setting up.
0.003 * * * [progress]: [1/2] Preparing points
0.004 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.006 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.079 * * * * [points]: Setting MPFR precision to 64
0.082 * * * * [points]: Setting MPFR precision to 320
0.084 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.086 * * * * [points]: Setting MPFR precision to 64
0.088 * * * * [points]: Setting MPFR precision to 320
0.090 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.093 * * * * [points]: Setting MPFR precision to 64
0.099 * * * * [points]: Setting MPFR precision to 320
0.106 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.111 * * * * [points]: Setting MPFR precision to 64
0.122 * * * * [points]: Setting MPFR precision to 320
0.133 * * * * [points]: Computing exacts for 256 points
0.138 * * * * [points]: Setting MPFR precision to 64
0.170 * * * * [points]: Setting MPFR precision to 320
0.204 * * * * [points]: Filtering points with unrepresentable outputs
0.206 * * * * [points]: Sampled 256 points with exact outputs
0.256 * * * [progress]: [2/2] Setting up program.
0.276 * [progress]: [Phase 2 of 3] Improving.
0.276 * * * * [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.277 * [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.278 * * [simplify]: iters left: 6 (16 enodes)
0.287 * * [simplify]: iters left: 5 (45 enodes)
0.296 * * [simplify]: iters left: 4 (91 enodes)
0.315 * * [simplify]: iters left: 3 (310 enodes)
0.478 * * [simplify]: Extracting #0: cost 1 inf + 0
0.478 * * [simplify]: Extracting #1: cost 31 inf + 0
0.479 * * [simplify]: Extracting #2: cost 123 inf + 1
0.479 * * [simplify]: Extracting #3: cost 200 inf + 1531
0.480 * * [simplify]: Extracting #4: cost 265 inf + 7949
0.482 * * [simplify]: Extracting #5: cost 321 inf + 21683
0.486 * * [simplify]: Extracting #6: cost 355 inf + 88776
0.503 * * [simplify]: Extracting #7: cost 146 inf + 448651
0.540 * * [simplify]: Extracting #8: cost 8 inf + 713461
0.593 * * [simplify]: Extracting #9: cost 0 inf + 728055
0.634 * [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.634 * [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.668 * * [progress]: iteration 1 / 4
0.668 * * * [progress]: picking best candidate
0.698 * * * * [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.699 * * * [progress]: localizing error
0.957 * * * [progress]: generating rewritten candidates
0.957 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.960 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
0.963 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 1)
0.968 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2)
0.969 * * * [progress]: generating series expansions
0.970 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.970 * * * * [progress]: [ 2 / 4 ] generating series at (2)
0.970 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 1)
0.970 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2)
0.970 * * * [progress]: simplifying candidates
0.970 * * * * [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)))>
0.970 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
0.970 * * [simplify]: iters left: 5 (11 enodes)
0.973 * * [simplify]: iters left: 4 (29 enodes)
0.978 * * [simplify]: iters left: 3 (61 enodes)
0.992 * * [simplify]: iters left: 2 (176 enodes)
1.081 * * [simplify]: Extracting #0: cost 1 inf + 0
1.081 * * [simplify]: Extracting #1: cost 2 inf + 0
1.081 * * [simplify]: Extracting #2: cost 3 inf + 0
1.081 * * [simplify]: Extracting #3: cost 17 inf + 0
1.081 * * [simplify]: Extracting #4: cost 61 inf + 0
1.082 * * [simplify]: Extracting #5: cost 127 inf + 646
1.087 * * [simplify]: Extracting #6: cost 193 inf + 14402
1.094 * * [simplify]: Extracting #7: cost 126 inf + 105460
1.116 * * [simplify]: Extracting #8: cost 12 inf + 317072
1.142 * * [simplify]: Extracting #9: cost 0 inf + 340034
1.167 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
1.167 * [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.167 * * * * [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.168 * [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.168 * * [simplify]: iters left: 6 (14 enodes)
1.174 * * [simplify]: iters left: 5 (42 enodes)
1.190 * * [simplify]: iters left: 4 (117 enodes)
1.245 * * [simplify]: iters left: 3 (426 enodes)
1.528 * * [simplify]: Extracting #0: cost 1 inf + 0
1.529 * * [simplify]: Extracting #1: cost 51 inf + 0
1.530 * * [simplify]: Extracting #2: cost 242 inf + 0
1.532 * * [simplify]: Extracting #3: cost 412 inf + 4894
1.559 * * [simplify]: Extracting #4: cost 407 inf + 277787
1.622 * * [simplify]: Extracting #5: cost 129 inf + 1021325
1.699 * * [simplify]: Extracting #6: cost 1 inf + 1253728
1.789 * * [simplify]: Extracting #7: cost 0 inf + 1257332
1.878 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
1.878 * [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)))
1.878 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1.878 * * [simplify]: iters left: 5 (12 enodes)
1.884 * * [simplify]: iters left: 4 (31 enodes)
1.895 * * [simplify]: iters left: 3 (64 enodes)
1.920 * * [simplify]: iters left: 2 (183 enodes)
2.001 * * [simplify]: Extracting #0: cost 1 inf + 0
2.002 * * [simplify]: Extracting #1: cost 6 inf + 0
2.002 * * [simplify]: Extracting #2: cost 10 inf + 1
2.002 * * [simplify]: Extracting #3: cost 22 inf + 804
2.002 * * [simplify]: Extracting #4: cost 64 inf + 1445
2.003 * * [simplify]: Extracting #5: cost 138 inf + 3371
2.005 * * [simplify]: Extracting #6: cost 216 inf + 12754
2.013 * * [simplify]: Extracting #7: cost 138 inf + 118173
2.026 * * [simplify]: Extracting #8: cost 17 inf + 330365
2.041 * * [simplify]: Extracting #9: cost 0 inf + 369430
2.058 * * [simplify]: Extracting #10: cost 0 inf + 369110
2.075 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
2.075 * [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.075 * * * * [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.075 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
2.075 * * [simplify]: iters left: 6 (15 enodes)
2.082 * * [simplify]: iters left: 5 (41 enodes)
2.089 * * [simplify]: iters left: 4 (85 enodes)
2.108 * * [simplify]: iters left: 3 (287 enodes)
2.232 * * [simplify]: Extracting #0: cost 1 inf + 0
2.232 * * [simplify]: Extracting #1: cost 20 inf + 0
2.233 * * [simplify]: Extracting #2: cost 91 inf + 0
2.233 * * [simplify]: Extracting #3: cost 174 inf + 83
2.234 * * [simplify]: Extracting #4: cost 237 inf + 4418
2.236 * * [simplify]: Extracting #5: cost 262 inf + 55666
2.249 * * [simplify]: Extracting #6: cost 180 inf + 332251
2.291 * * [simplify]: Extracting #7: cost 12 inf + 639867
2.347 * * [simplify]: Extracting #8: cost 0 inf + 669631
2.391 * [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.391 * [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.392 * * * * [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.392 * [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.392 * * [simplify]: iters left: 6 (16 enodes)
2.396 * * [simplify]: iters left: 5 (46 enodes)
2.405 * * [simplify]: iters left: 4 (107 enodes)
2.449 * * [simplify]: iters left: 3 (238 enodes)
2.561 * * [simplify]: Extracting #0: cost 1 inf + 0
2.562 * * [simplify]: Extracting #1: cost 24 inf + 0
2.562 * * [simplify]: Extracting #2: cost 36 inf + 1
2.562 * * [simplify]: Extracting #3: cost 37 inf + 85
2.562 * * [simplify]: Extracting #4: cost 46 inf + 2656
2.563 * * [simplify]: Extracting #5: cost 87 inf + 3297
2.566 * * [simplify]: Extracting #6: cost 166 inf + 4900
2.569 * * [simplify]: Extracting #7: cost 230 inf + 13556
2.576 * * [simplify]: Extracting #8: cost 168 inf + 107441
2.598 * * [simplify]: Extracting #9: cost 37 inf + 337047
2.628 * * [simplify]: Extracting #10: cost 0 inf + 395102
2.647 * * [simplify]: Extracting #11: cost 0 inf + 394462
2.665 * [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.666 * [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.666 * * * * [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.666 * [simplify]: Simplifying (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c)))
2.666 * * [simplify]: iters left: 3 (7 enodes)
2.670 * * [simplify]: iters left: 2 (16 enodes)
2.675 * * [simplify]: iters left: 1 (22 enodes)
2.682 * * [simplify]: Extracting #0: cost 1 inf + 0
2.682 * * [simplify]: Extracting #1: cost 2 inf + 0
2.682 * * [simplify]: Extracting #2: cost 8 inf + 0
2.682 * * [simplify]: Extracting #3: cost 6 inf + 324
2.682 * * [simplify]: Extracting #4: cost 5 inf + 325
2.682 * * [simplify]: Extracting #5: cost 0 inf + 2336
2.682 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
2.682 * [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.683 * * * * [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.683 * [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.683 * * [simplify]: iters left: 4 (11 enodes)
2.689 * * [simplify]: iters left: 3 (40 enodes)
2.707 * * [simplify]: iters left: 2 (105 enodes)
2.762 * * [simplify]: iters left: 1 (409 enodes)
3.095 * * [simplify]: Extracting #0: cost 1 inf + 0
3.095 * * [simplify]: Extracting #1: cost 32 inf + 0
3.096 * * [simplify]: Extracting #2: cost 197 inf + 0
3.098 * * [simplify]: Extracting #3: cost 336 inf + 2893
3.108 * * [simplify]: Extracting #4: cost 467 inf + 105237
3.161 * * [simplify]: Extracting #5: cost 158 inf + 692584
3.241 * * [simplify]: Extracting #6: cost 14 inf + 1019119
3.307 * * [simplify]: Extracting #7: cost 0 inf + 1058774
3.374 * [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))))
3.375 * [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)))
3.375 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))
3.375 * * [simplify]: iters left: 3 (9 enodes)
3.377 * * [simplify]: iters left: 2 (21 enodes)
3.382 * * [simplify]: iters left: 1 (27 enodes)
3.386 * * [simplify]: Extracting #0: cost 1 inf + 0
3.386 * * [simplify]: Extracting #1: cost 3 inf + 0
3.386 * * [simplify]: Extracting #2: cost 10 inf + 0
3.387 * * [simplify]: Extracting #3: cost 7 inf + 325
3.387 * * [simplify]: Extracting #4: cost 0 inf + 2939
3.387 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
3.387 * [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)))
3.387 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
3.387 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
3.387 * * [simplify]: iters left: 6 (16 enodes)
3.391 * * [simplify]: iters left: 5 (45 enodes)
3.400 * * [simplify]: iters left: 4 (91 enodes)
3.438 * * [simplify]: iters left: 3 (310 enodes)
3.612 * * [simplify]: Extracting #0: cost 1 inf + 0
3.612 * * [simplify]: Extracting #1: cost 31 inf + 0
3.613 * * [simplify]: Extracting #2: cost 123 inf + 1
3.614 * * [simplify]: Extracting #3: cost 200 inf + 1531
3.616 * * [simplify]: Extracting #4: cost 265 inf + 7949
3.619 * * [simplify]: Extracting #5: cost 321 inf + 21683
3.627 * * [simplify]: Extracting #6: cost 355 inf + 88776
3.647 * * [simplify]: Extracting #7: cost 146 inf + 448651
3.677 * * [simplify]: Extracting #8: cost 8 inf + 713461
3.726 * * [simplify]: Extracting #9: cost 0 inf + 728055
3.787 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
3.787 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
3.787 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
3.787 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
3.788 * * [simplify]: iters left: 6 (16 enodes)
3.795 * * [simplify]: iters left: 5 (45 enodes)
3.811 * * [simplify]: iters left: 4 (91 enodes)
3.844 * * [simplify]: iters left: 3 (310 enodes)
3.985 * * [simplify]: Extracting #0: cost 1 inf + 0
3.985 * * [simplify]: Extracting #1: cost 31 inf + 0
3.986 * * [simplify]: Extracting #2: cost 123 inf + 1
3.987 * * [simplify]: Extracting #3: cost 200 inf + 1531
3.989 * * [simplify]: Extracting #4: cost 265 inf + 7949
3.992 * * [simplify]: Extracting #5: cost 321 inf + 21683
4.000 * * [simplify]: Extracting #6: cost 355 inf + 88776
4.030 * * [simplify]: Extracting #7: cost 146 inf + 448651
4.092 * * [simplify]: Extracting #8: cost 8 inf + 713461
4.141 * * [simplify]: Extracting #9: cost 0 inf + 728055
4.172 * [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.172 * [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.173 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
4.173 * [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.173 * * [simplify]: iters left: 6 (16 enodes)
4.177 * * [simplify]: iters left: 5 (45 enodes)
4.186 * * [simplify]: iters left: 4 (91 enodes)
4.217 * * [simplify]: iters left: 3 (310 enodes)
4.360 * * [simplify]: Extracting #0: cost 1 inf + 0
4.360 * * [simplify]: Extracting #1: cost 31 inf + 0
4.360 * * [simplify]: Extracting #2: cost 123 inf + 1
4.364 * * [simplify]: Extracting #3: cost 200 inf + 1531
4.365 * * [simplify]: Extracting #4: cost 265 inf + 7949
4.367 * * [simplify]: Extracting #5: cost 321 inf + 21683
4.371 * * [simplify]: Extracting #6: cost 355 inf + 88776
4.388 * * [simplify]: Extracting #7: cost 146 inf + 448651
4.438 * * [simplify]: Extracting #8: cost 8 inf + 713461
4.473 * * [simplify]: Extracting #9: cost 0 inf + 728055
4.505 * [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.505 * [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.506 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
4.506 * [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.506 * * [simplify]: iters left: 6 (16 enodes)
4.514 * * [simplify]: iters left: 5 (45 enodes)
4.531 * * [simplify]: iters left: 4 (91 enodes)
4.556 * * [simplify]: iters left: 3 (310 enodes)
4.709 * * [simplify]: Extracting #0: cost 1 inf + 0
4.709 * * [simplify]: Extracting #1: cost 31 inf + 0
4.709 * * [simplify]: Extracting #2: cost 123 inf + 1
4.711 * * [simplify]: Extracting #3: cost 200 inf + 1531
4.713 * * [simplify]: Extracting #4: cost 265 inf + 7949
4.716 * * [simplify]: Extracting #5: cost 321 inf + 21683
4.724 * * [simplify]: Extracting #6: cost 355 inf + 88776
4.741 * * [simplify]: Extracting #7: cost 146 inf + 448651
4.787 * * [simplify]: Extracting #8: cost 8 inf + 713461
4.849 * * [simplify]: Extracting #9: cost 0 inf + 728055
4.896 * [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.896 * [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.896 * * * [progress]: adding candidates to table
5.298 * * [progress]: iteration 2 / 4
5.298 * * * [progress]: picking best candidate
5.426 * * * * [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))>
5.426 * * * [progress]: localizing error
5.752 * * * [progress]: generating rewritten candidates
5.752 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
5.756 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2 1)
5.765 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
5.766 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 1 2)
5.773 * * * [progress]: generating series expansions
5.773 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
5.774 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2 1)
5.774 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
5.774 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 1 2)
5.774 * * * [progress]: simplifying candidates
5.774 * * * * [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))>
5.774 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
5.774 * * [simplify]: iters left: 5 (11 enodes)
5.779 * * [simplify]: iters left: 4 (29 enodes)
5.799 * * [simplify]: iters left: 3 (61 enodes)
5.824 * * [simplify]: iters left: 2 (176 enodes)
5.908 * * [simplify]: Extracting #0: cost 1 inf + 0
5.908 * * [simplify]: Extracting #1: cost 2 inf + 0
5.908 * * [simplify]: Extracting #2: cost 3 inf + 0
5.908 * * [simplify]: Extracting #3: cost 17 inf + 0
5.908 * * [simplify]: Extracting #4: cost 61 inf + 0
5.909 * * [simplify]: Extracting #5: cost 127 inf + 646
5.910 * * [simplify]: Extracting #6: cost 193 inf + 14402
5.914 * * [simplify]: Extracting #7: cost 126 inf + 105460
5.925 * * [simplify]: Extracting #8: cost 12 inf + 317072
5.939 * * [simplify]: Extracting #9: cost 0 inf + 340034
5.953 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
5.953 * [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))
5.953 * * * * [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))>
5.953 * [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))))))
5.953 * * [simplify]: iters left: 6 (14 enodes)
5.957 * * [simplify]: iters left: 5 (42 enodes)
5.966 * * [simplify]: iters left: 4 (117 enodes)
6.012 * * [simplify]: iters left: 3 (426 enodes)
6.282 * * [simplify]: Extracting #0: cost 1 inf + 0
6.283 * * [simplify]: Extracting #1: cost 51 inf + 0
6.284 * * [simplify]: Extracting #2: cost 242 inf + 0
6.286 * * [simplify]: Extracting #3: cost 412 inf + 4894
6.296 * * [simplify]: Extracting #4: cost 407 inf + 277787
6.349 * * [simplify]: Extracting #5: cost 129 inf + 1021325
6.452 * * [simplify]: Extracting #6: cost 1 inf + 1253728
6.556 * * [simplify]: Extracting #7: cost 0 inf + 1257332
6.644 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
6.645 * [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))
6.645 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
6.645 * * [simplify]: iters left: 5 (12 enodes)
6.651 * * [simplify]: iters left: 4 (31 enodes)
6.662 * * [simplify]: iters left: 3 (64 enodes)
6.690 * * [simplify]: iters left: 2 (183 enodes)
6.782 * * [simplify]: Extracting #0: cost 1 inf + 0
6.782 * * [simplify]: Extracting #1: cost 6 inf + 0
6.782 * * [simplify]: Extracting #2: cost 10 inf + 1
6.782 * * [simplify]: Extracting #3: cost 22 inf + 804
6.783 * * [simplify]: Extracting #4: cost 64 inf + 1445
6.783 * * [simplify]: Extracting #5: cost 138 inf + 3371
6.786 * * [simplify]: Extracting #6: cost 216 inf + 12754
6.794 * * [simplify]: Extracting #7: cost 138 inf + 118173
6.812 * * [simplify]: Extracting #8: cost 17 inf + 330365
6.826 * * [simplify]: Extracting #9: cost 0 inf + 369430
6.841 * * [simplify]: Extracting #10: cost 0 inf + 369110
6.861 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
6.861 * [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))
6.861 * * * * [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))>
6.861 * [simplify]: Simplifying (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c)))
6.861 * * [simplify]: iters left: 3 (7 enodes)
6.863 * * [simplify]: iters left: 2 (16 enodes)
6.866 * * [simplify]: iters left: 1 (22 enodes)
6.869 * * [simplify]: Extracting #0: cost 1 inf + 0
6.869 * * [simplify]: Extracting #1: cost 2 inf + 0
6.869 * * [simplify]: Extracting #2: cost 8 inf + 0
6.870 * * [simplify]: Extracting #3: cost 6 inf + 324
6.870 * * [simplify]: Extracting #4: cost 5 inf + 325
6.870 * * [simplify]: Extracting #5: cost 0 inf + 2336
6.870 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
6.870 * [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))
6.870 * * * * [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))>
6.870 * [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))))
6.870 * * [simplify]: iters left: 4 (11 enodes)
6.873 * * [simplify]: iters left: 3 (40 enodes)
6.881 * * [simplify]: iters left: 2 (105 enodes)
6.917 * * [simplify]: iters left: 1 (409 enodes)
7.678 * * [simplify]: Extracting #0: cost 1 inf + 0
7.678 * * [simplify]: Extracting #1: cost 32 inf + 0
7.679 * * [simplify]: Extracting #2: cost 197 inf + 0
7.680 * * [simplify]: Extracting #3: cost 336 inf + 2893
7.688 * * [simplify]: Extracting #4: cost 467 inf + 105237
7.741 * * [simplify]: Extracting #5: cost 158 inf + 692584
7.803 * * [simplify]: Extracting #6: cost 14 inf + 1019119
7.877 * * [simplify]: Extracting #7: cost 0 inf + 1058774
7.967 * [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))))
7.967 * [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))
7.967 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))
7.967 * * [simplify]: iters left: 3 (9 enodes)
7.972 * * [simplify]: iters left: 2 (21 enodes)
7.978 * * [simplify]: iters left: 1 (27 enodes)
7.986 * * [simplify]: Extracting #0: cost 1 inf + 0
7.986 * * [simplify]: Extracting #1: cost 3 inf + 0
7.986 * * [simplify]: Extracting #2: cost 10 inf + 0
7.986 * * [simplify]: Extracting #3: cost 7 inf + 325
7.987 * * [simplify]: Extracting #4: cost 0 inf + 2939
7.987 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
7.987 * [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))
7.987 * * * * [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))>
7.988 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
7.988 * * [simplify]: iters left: 2 (4 enodes)
7.990 * * [simplify]: iters left: 1 (8 enodes)
7.993 * * [simplify]: Extracting #0: cost 1 inf + 0
7.994 * * [simplify]: Extracting #1: cost 3 inf + 0
7.994 * * [simplify]: Extracting #2: cost 3 inf + 1
7.994 * * [simplify]: Extracting #3: cost 2 inf + 2
7.994 * * [simplify]: Extracting #4: cost 0 inf + 325
7.994 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
7.994 * [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))
7.994 * * * * [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))>
7.994 * * * * [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))>
7.995 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
7.995 * * [simplify]: iters left: 6 (15 enodes)
8.002 * * [simplify]: iters left: 5 (41 enodes)
8.011 * * [simplify]: iters left: 4 (85 enodes)
8.030 * * [simplify]: iters left: 3 (287 enodes)
8.203 * * [simplify]: Extracting #0: cost 1 inf + 0
8.203 * * [simplify]: Extracting #1: cost 20 inf + 0
8.204 * * [simplify]: Extracting #2: cost 91 inf + 0
8.204 * * [simplify]: Extracting #3: cost 174 inf + 83
8.206 * * [simplify]: Extracting #4: cost 237 inf + 4418
8.211 * * [simplify]: Extracting #5: cost 262 inf + 55666
8.235 * * [simplify]: Extracting #6: cost 180 inf + 332251
8.260 * * [simplify]: Extracting #7: cost 12 inf + 639867
8.289 * * [simplify]: Extracting #8: cost 0 inf + 669631
8.318 * [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.318 * [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.318 * * * * [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.319 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
8.319 * * [simplify]: iters left: 6 (15 enodes)
8.322 * * [simplify]: iters left: 5 (41 enodes)
8.330 * * [simplify]: iters left: 4 (85 enodes)
8.351 * * [simplify]: iters left: 3 (287 enodes)
8.540 * * [simplify]: Extracting #0: cost 1 inf + 0
8.540 * * [simplify]: Extracting #1: cost 20 inf + 0
8.540 * * [simplify]: Extracting #2: cost 91 inf + 0
8.541 * * [simplify]: Extracting #3: cost 174 inf + 83
8.543 * * [simplify]: Extracting #4: cost 237 inf + 4418
8.547 * * [simplify]: Extracting #5: cost 262 inf + 55666
8.576 * * [simplify]: Extracting #6: cost 180 inf + 332251
8.625 * * [simplify]: Extracting #7: cost 12 inf + 639867
8.657 * * [simplify]: Extracting #8: cost 0 inf + 669631
8.709 * [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.710 * [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.710 * * * * [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))>
8.710 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
8.710 * * [simplify]: iters left: 6 (15 enodes)
8.715 * * [simplify]: iters left: 5 (41 enodes)
8.723 * * [simplify]: iters left: 4 (85 enodes)
8.743 * * [simplify]: iters left: 3 (287 enodes)
8.897 * * [simplify]: Extracting #0: cost 1 inf + 0
8.897 * * [simplify]: Extracting #1: cost 20 inf + 0
8.898 * * [simplify]: Extracting #2: cost 91 inf + 0
8.898 * * [simplify]: Extracting #3: cost 174 inf + 83
8.900 * * [simplify]: Extracting #4: cost 237 inf + 4418
8.905 * * [simplify]: Extracting #5: cost 262 inf + 55666
8.935 * * [simplify]: Extracting #6: cost 180 inf + 332251
8.984 * * [simplify]: Extracting #7: cost 12 inf + 639867
9.030 * * [simplify]: Extracting #8: cost 0 inf + 669631
9.072 * [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.073 * [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.073 * * * * [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.073 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2))
9.073 * * [simplify]: iters left: 6 (15 enodes)
9.080 * * [simplify]: iters left: 5 (41 enodes)
9.096 * * [simplify]: iters left: 4 (85 enodes)
9.117 * * [simplify]: iters left: 3 (287 enodes)
9.248 * * [simplify]: Extracting #0: cost 1 inf + 0
9.248 * * [simplify]: Extracting #1: cost 20 inf + 0
9.248 * * [simplify]: Extracting #2: cost 91 inf + 0
9.249 * * [simplify]: Extracting #3: cost 174 inf + 83
9.251 * * [simplify]: Extracting #4: cost 237 inf + 4418
9.255 * * [simplify]: Extracting #5: cost 262 inf + 55666
9.281 * * [simplify]: Extracting #6: cost 180 inf + 332251
9.330 * * [simplify]: Extracting #7: cost 12 inf + 639867
9.375 * * [simplify]: Extracting #8: cost 0 inf + 669631
9.422 * [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.422 * [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.422 * * * [progress]: adding candidates to table
9.738 * * [progress]: iteration 3 / 4
9.738 * * * [progress]: picking best candidate
9.891 * * * * [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))>
9.891 * * * [progress]: localizing error
10.138 * * * [progress]: generating rewritten candidates
10.138 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
10.140 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2 1)
10.144 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
10.144 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
10.147 * * * [progress]: generating series expansions
10.147 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
10.147 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2 1)
10.147 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
10.147 * * * * [progress]: [ 4 / 4 ] generating series at (2)
10.147 * * * [progress]: simplifying candidates
10.147 * * * * [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.147 * [simplify]: Simplifying (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
10.147 * * [simplify]: iters left: 6 (11 enodes)
10.150 * * [simplify]: iters left: 5 (29 enodes)
10.155 * * [simplify]: iters left: 4 (61 enodes)
10.169 * * [simplify]: iters left: 3 (181 enodes)
10.237 * * [simplify]: Extracting #0: cost 1 inf + 0
10.237 * * [simplify]: Extracting #1: cost 2 inf + 0
10.237 * * [simplify]: Extracting #2: cost 3 inf + 0
10.237 * * [simplify]: Extracting #3: cost 17 inf + 0
10.237 * * [simplify]: Extracting #4: cost 61 inf + 0
10.238 * * [simplify]: Extracting #5: cost 136 inf + 324
10.239 * * [simplify]: Extracting #6: cost 193 inf + 16244
10.244 * * [simplify]: Extracting #7: cost 123 inf + 104476
10.259 * * [simplify]: Extracting #8: cost 8 inf + 322378
10.274 * * [simplify]: Extracting #9: cost 0 inf + 339405
10.288 * [simplify]: Simplified to (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))))
10.289 * [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))
10.289 * * * * [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))>
10.289 * [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)))))
10.289 * * [simplify]: iters left: 6 (14 enodes)
10.296 * * [simplify]: iters left: 5 (42 enodes)
10.312 * * [simplify]: iters left: 4 (117 enodes)
10.368 * * [simplify]: iters left: 3 (432 enodes)
10.600 * * [simplify]: Extracting #0: cost 1 inf + 0
10.600 * * [simplify]: Extracting #1: cost 51 inf + 0
10.601 * * [simplify]: Extracting #2: cost 242 inf + 0
10.602 * * [simplify]: Extracting #3: cost 411 inf + 3092
10.612 * * [simplify]: Extracting #4: cost 417 inf + 266776
10.680 * * [simplify]: Extracting #5: cost 155 inf + 959244
10.755 * * [simplify]: Extracting #6: cost 2 inf + 1266055
10.851 * * [simplify]: Extracting #7: cost 0 inf + 1272103
10.933 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4))))
10.933 * [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))
10.933 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
10.933 * * [simplify]: iters left: 6 (12 enodes)
10.936 * * [simplify]: iters left: 5 (31 enodes)
10.942 * * [simplify]: iters left: 4 (64 enodes)
10.962 * * [simplify]: iters left: 3 (187 enodes)
11.048 * * [simplify]: Extracting #0: cost 1 inf + 0
11.048 * * [simplify]: Extracting #1: cost 6 inf + 0
11.048 * * [simplify]: Extracting #2: cost 10 inf + 1
11.048 * * [simplify]: Extracting #3: cost 22 inf + 804
11.048 * * [simplify]: Extracting #4: cost 64 inf + 1445
11.049 * * [simplify]: Extracting #5: cost 135 inf + 3049
11.050 * * [simplify]: Extracting #6: cost 191 inf + 13398
11.054 * * [simplify]: Extracting #7: cost 127 inf + 98415
11.066 * * [simplify]: Extracting #8: cost 10 inf + 313726
11.093 * * [simplify]: Extracting #9: cost 0 inf + 337284
11.108 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) b)
11.108 * [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))
11.108 * * * * [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))>
11.108 * [simplify]: Simplifying (neg.p16 (*.p16 (*.p16 (real->posit16 4) a) c))
11.109 * * [simplify]: iters left: 4 (7 enodes)
11.112 * * [simplify]: iters left: 3 (16 enodes)
11.115 * * [simplify]: iters left: 2 (22 enodes)
11.118 * * [simplify]: iters left: 1 (23 enodes)
11.121 * * [simplify]: Extracting #0: cost 1 inf + 0
11.121 * * [simplify]: Extracting #1: cost 2 inf + 0
11.121 * * [simplify]: Extracting #2: cost 8 inf + 0
11.121 * * [simplify]: Extracting #3: cost 6 inf + 324
11.121 * * [simplify]: Extracting #4: cost 5 inf + 325
11.122 * * [simplify]: Extracting #5: cost 0 inf + 2336
11.122 * [simplify]: Simplified to (neg.p16 (*.p16 c (*.p16 a (real->posit16 4))))
11.122 * [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))
11.122 * * * * [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))>
11.122 * [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)))
11.122 * * [simplify]: iters left: 5 (11 enodes)
11.125 * * [simplify]: iters left: 4 (40 enodes)
11.132 * * [simplify]: iters left: 3 (100 enodes)
11.176 * * [simplify]: iters left: 2 (360 enodes)
11.425 * * [simplify]: Extracting #0: cost 1 inf + 0
11.425 * * [simplify]: Extracting #1: cost 32 inf + 0
11.426 * * [simplify]: Extracting #2: cost 200 inf + 0
11.427 * * [simplify]: Extracting #3: cost 325 inf + 3535
11.431 * * [simplify]: Extracting #4: cost 456 inf + 67717
11.468 * * [simplify]: Extracting #5: cost 170 inf + 641860
11.553 * * [simplify]: Extracting #6: cost 19 inf + 997414
11.615 * * [simplify]: Extracting #7: cost 0 inf + 1027370
11.677 * * [simplify]: Extracting #8: cost 0 inf + 1020770
11.739 * [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))))
11.739 * [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))
11.740 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))
11.740 * * [simplify]: iters left: 4 (9 enodes)
11.745 * * [simplify]: iters left: 3 (21 enodes)
11.752 * * [simplify]: iters left: 2 (27 enodes)
11.762 * * [simplify]: iters left: 1 (29 enodes)
11.770 * * [simplify]: Extracting #0: cost 1 inf + 0
11.770 * * [simplify]: Extracting #1: cost 3 inf + 0
11.770 * * [simplify]: Extracting #2: cost 10 inf + 0
11.770 * * [simplify]: Extracting #3: cost 7 inf + 325
11.771 * * [simplify]: Extracting #4: cost 0 inf + 2939
11.771 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 c (real->posit16 4)) a) (*.p16 b b))
11.771 * [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))
11.771 * * * * [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))))>
11.772 * [simplify]: Simplifying (*.p16 a (real->posit16 2))
11.772 * * [simplify]: iters left: 2 (4 enodes)
11.774 * * [simplify]: iters left: 1 (8 enodes)
11.776 * * [simplify]: Extracting #0: cost 1 inf + 0
11.777 * * [simplify]: Extracting #1: cost 3 inf + 0
11.777 * * [simplify]: Extracting #2: cost 3 inf + 1
11.777 * * [simplify]: Extracting #3: cost 0 inf + 325
11.777 * [simplify]: Simplified to (*.p16 a (real->posit16 2))
11.777 * [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))))
11.777 * * * * [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))>
11.777 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
11.777 * * [simplify]: iters left: 2 (4 enodes)
11.778 * * [simplify]: iters left: 1 (8 enodes)
11.780 * * [simplify]: Extracting #0: cost 1 inf + 0
11.780 * * [simplify]: Extracting #1: cost 3 inf + 0
11.780 * * [simplify]: Extracting #2: cost 3 inf + 1
11.780 * * [simplify]: Extracting #3: cost 2 inf + 2
11.780 * * [simplify]: Extracting #4: cost 0 inf + 325
11.780 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.780 * [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))
11.780 * * * * [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))>
11.780 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
11.780 * * [simplify]: iters left: 2 (4 enodes)
11.781 * * [simplify]: iters left: 1 (8 enodes)
11.783 * * [simplify]: Extracting #0: cost 1 inf + 0
11.783 * * [simplify]: Extracting #1: cost 3 inf + 0
11.783 * * [simplify]: Extracting #2: cost 3 inf + 1
11.783 * * [simplify]: Extracting #3: cost 2 inf + 2
11.783 * * [simplify]: Extracting #4: cost 0 inf + 325
11.783 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.783 * [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))
11.783 * * * * [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))>
11.783 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
11.783 * * [simplify]: iters left: 2 (4 enodes)
11.784 * * [simplify]: iters left: 1 (8 enodes)
11.786 * * [simplify]: Extracting #0: cost 1 inf + 0
11.786 * * [simplify]: Extracting #1: cost 3 inf + 0
11.786 * * [simplify]: Extracting #2: cost 3 inf + 1
11.786 * * [simplify]: Extracting #3: cost 2 inf + 2
11.786 * * [simplify]: Extracting #4: cost 0 inf + 325
11.786 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.786 * [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))
11.786 * * * * [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))>
11.786 * [simplify]: Simplifying (*.p16 (real->posit16 4) a)
11.786 * * [simplify]: iters left: 2 (4 enodes)
11.788 * * [simplify]: iters left: 1 (8 enodes)
11.789 * * [simplify]: Extracting #0: cost 1 inf + 0
11.789 * * [simplify]: Extracting #1: cost 3 inf + 0
11.789 * * [simplify]: Extracting #2: cost 3 inf + 1
11.789 * * [simplify]: Extracting #3: cost 2 inf + 2
11.789 * * [simplify]: Extracting #4: cost 0 inf + 325
11.789 * [simplify]: Simplified to (*.p16 a (real->posit16 4))
11.790 * [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))
11.790 * * * [progress]: adding candidates to table
12.097 * * [progress]: iteration 4 / 4
12.097 * * * [progress]: picking best candidate
12.270 * * * * [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)))>
12.270 * * * [progress]: localizing error
12.617 * * * [progress]: generating rewritten candidates
12.617 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
12.623 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
12.629 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
12.635 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2 1)
12.644 * * * [progress]: generating series expansions
12.644 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
12.644 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
12.644 * * * * [progress]: [ 3 / 4 ] generating series at (2)
12.644 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2 1)
12.644 * * * [progress]: simplifying candidates
12.644 * * * * [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)))>
12.645 * * * * [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))>
12.645 * [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))
12.645 * * [simplify]: iters left: 6 (20 enodes)
12.655 * * [simplify]: iters left: 5 (50 enodes)
12.675 * * [simplify]: iters left: 4 (122 enodes)
12.727 * * [simplify]: iters left: 3 (328 enodes)
12.972 * * [simplify]: Extracting #0: cost 1 inf + 0
12.972 * * [simplify]: Extracting #1: cost 9 inf + 0
12.972 * * [simplify]: Extracting #2: cost 36 inf + 0
12.972 * * [simplify]: Extracting #3: cost 91 inf + 525
12.973 * * [simplify]: Extracting #4: cost 103 inf + 15440
12.975 * * [simplify]: Extracting #5: cost 157 inf + 31956
12.980 * * [simplify]: Extracting #6: cost 194 inf + 98726
12.996 * * [simplify]: Extracting #7: cost 16 inf + 431933
13.032 * * [simplify]: Extracting #8: cost 0 inf + 419397
13.050 * * [simplify]: Extracting #9: cost 0 inf + 417437
13.067 * [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)))
13.067 * [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))
13.067 * * * * [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))))))))>
13.068 * [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))))))
13.068 * * [simplify]: iters left: 6 (16 enodes)
13.075 * * [simplify]: iters left: 5 (46 enodes)
13.092 * * [simplify]: iters left: 4 (107 enodes)
13.134 * * [simplify]: iters left: 3 (238 enodes)
13.218 * * [simplify]: Extracting #0: cost 1 inf + 0
13.218 * * [simplify]: Extracting #1: cost 24 inf + 0
13.218 * * [simplify]: Extracting #2: cost 36 inf + 1
13.219 * * [simplify]: Extracting #3: cost 37 inf + 85
13.219 * * [simplify]: Extracting #4: cost 46 inf + 2656
13.219 * * [simplify]: Extracting #5: cost 87 inf + 3297
13.220 * * [simplify]: Extracting #6: cost 166 inf + 4900
13.222 * * [simplify]: Extracting #7: cost 230 inf + 13556
13.229 * * [simplify]: Extracting #8: cost 168 inf + 107441
13.252 * * [simplify]: Extracting #9: cost 37 inf + 337047
13.283 * * [simplify]: Extracting #10: cost 0 inf + 395102
13.315 * * [simplify]: Extracting #11: cost 0 inf + 394462
13.341 * [simplify]: Simplified to (*.p16 (*.p16 a (real->posit16 2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) c) a))) b))
13.342 * [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))))
13.342 * * * * [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)))>
13.342 * [simplify]: Simplifying (neg.p16 (*.p16 (real->posit16 4) (*.p16 a c)))
13.342 * * [simplify]: iters left: 3 (7 enodes)
13.344 * * [simplify]: iters left: 2 (16 enodes)
13.350 * * [simplify]: iters left: 1 (22 enodes)
13.353 * * [simplify]: Extracting #0: cost 1 inf + 0
13.353 * * [simplify]: Extracting #1: cost 2 inf + 0
13.353 * * [simplify]: Extracting #2: cost 8 inf + 0
13.353 * * [simplify]: Extracting #3: cost 6 inf + 324
13.353 * * [simplify]: Extracting #4: cost 5 inf + 325
13.354 * * [simplify]: Extracting #5: cost 0 inf + 2336
13.354 * [simplify]: Simplified to (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4)))
13.354 * [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)))
13.354 * * * * [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)))>
13.354 * [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))))
13.354 * * [simplify]: iters left: 4 (11 enodes)
13.357 * * [simplify]: iters left: 3 (40 enodes)
13.365 * * [simplify]: iters left: 2 (105 enodes)
13.407 * * [simplify]: iters left: 1 (409 enodes)
13.746 * * [simplify]: Extracting #0: cost 1 inf + 0
13.746 * * [simplify]: Extracting #1: cost 32 inf + 0
13.747 * * [simplify]: Extracting #2: cost 197 inf + 0
13.749 * * [simplify]: Extracting #3: cost 336 inf + 2893
13.759 * * [simplify]: Extracting #4: cost 467 inf + 105237
13.813 * * [simplify]: Extracting #5: cost 158 inf + 692584
13.907 * * [simplify]: Extracting #6: cost 14 inf + 1019119
14.003 * * [simplify]: Extracting #7: cost 0 inf + 1058774
14.064 * [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))))
14.064 * [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)))
14.064 * [simplify]: Simplifying (+.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))
14.064 * * [simplify]: iters left: 3 (9 enodes)
14.068 * * [simplify]: iters left: 2 (21 enodes)
14.075 * * [simplify]: iters left: 1 (27 enodes)
14.083 * * [simplify]: Extracting #0: cost 1 inf + 0
14.083 * * [simplify]: Extracting #1: cost 3 inf + 0
14.083 * * [simplify]: Extracting #2: cost 10 inf + 0
14.083 * * [simplify]: Extracting #3: cost 7 inf + 325
14.084 * * [simplify]: Extracting #4: cost 0 inf + 2939
14.084 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))
14.084 * [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)))
14.085 * * * * [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)))>
14.085 * [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))
14.085 * * [simplify]: iters left: 6 (21 enodes)
14.095 * * [simplify]: iters left: 5 (54 enodes)
14.115 * * [simplify]: iters left: 4 (133 enodes)
14.151 * * [simplify]: iters left: 3 (370 enodes)
14.370 * * [simplify]: Extracting #0: cost 1 inf + 0
14.370 * * [simplify]: Extracting #1: cost 13 inf + 0
14.371 * * [simplify]: Extracting #2: cost 47 inf + 1
14.371 * * [simplify]: Extracting #3: cost 111 inf + 84
14.372 * * [simplify]: Extracting #4: cost 134 inf + 8949
14.374 * * [simplify]: Extracting #5: cost 180 inf + 29874
14.378 * * [simplify]: Extracting #6: cost 220 inf + 71010
14.392 * * [simplify]: Extracting #7: cost 61 inf + 372007
14.423 * * [simplify]: Extracting #8: cost 3 inf + 443221
14.444 * * [simplify]: Extracting #9: cost 0 inf + 440433
14.463 * [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)))
14.463 * [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))))
14.463 * * * * [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)))>
14.464 * [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))
14.464 * * [simplify]: iters left: 6 (21 enodes)
14.469 * * [simplify]: iters left: 5 (54 enodes)
14.480 * * [simplify]: iters left: 4 (133 enodes)
14.527 * * [simplify]: iters left: 3 (370 enodes)
14.714 * * [simplify]: Extracting #0: cost 1 inf + 0
14.714 * * [simplify]: Extracting #1: cost 13 inf + 0
14.715 * * [simplify]: Extracting #2: cost 47 inf + 1
14.715 * * [simplify]: Extracting #3: cost 111 inf + 84
14.717 * * [simplify]: Extracting #4: cost 134 inf + 8949
14.721 * * [simplify]: Extracting #5: cost 180 inf + 29874
14.729 * * [simplify]: Extracting #6: cost 220 inf + 71010
14.762 * * [simplify]: Extracting #7: cost 61 inf + 372007
14.799 * * [simplify]: Extracting #8: cost 3 inf + 443221
14.837 * * [simplify]: Extracting #9: cost 0 inf + 440433
14.867 * [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)))
14.867 * [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))))
14.867 * * * * [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)))>
14.868 * [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))
14.868 * * [simplify]: iters left: 6 (21 enodes)
14.873 * * [simplify]: iters left: 5 (54 enodes)
14.883 * * [simplify]: iters left: 4 (133 enodes)
14.917 * * [simplify]: iters left: 3 (370 enodes)
15.171 * * [simplify]: Extracting #0: cost 1 inf + 0
15.171 * * [simplify]: Extracting #1: cost 13 inf + 0
15.171 * * [simplify]: Extracting #2: cost 47 inf + 1
15.172 * * [simplify]: Extracting #3: cost 111 inf + 84
15.172 * * [simplify]: Extracting #4: cost 134 inf + 8949
15.174 * * [simplify]: Extracting #5: cost 180 inf + 29874
15.179 * * [simplify]: Extracting #6: cost 220 inf + 71010
15.207 * * [simplify]: Extracting #7: cost 61 inf + 372007
15.246 * * [simplify]: Extracting #8: cost 3 inf + 443221
15.283 * * [simplify]: Extracting #9: cost 0 inf + 440433
15.320 * [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.321 * [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.321 * * * * [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)))>
15.321 * [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.321 * * [simplify]: iters left: 6 (21 enodes)
15.335 * * [simplify]: iters left: 5 (54 enodes)
15.356 * * [simplify]: iters left: 4 (133 enodes)
15.413 * * [simplify]: iters left: 3 (370 enodes)
15.598 * * [simplify]: Extracting #0: cost 1 inf + 0
15.598 * * [simplify]: Extracting #1: cost 13 inf + 0
15.598 * * [simplify]: Extracting #2: cost 47 inf + 1
15.598 * * [simplify]: Extracting #3: cost 111 inf + 84
15.599 * * [simplify]: Extracting #4: cost 134 inf + 8949
15.601 * * [simplify]: Extracting #5: cost 180 inf + 29874
15.605 * * [simplify]: Extracting #6: cost 220 inf + 71010
15.619 * * [simplify]: Extracting #7: cost 61 inf + 372007
15.637 * * [simplify]: Extracting #8: cost 3 inf + 443221
15.657 * * [simplify]: Extracting #9: cost 0 inf + 440433
15.680 * [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.680 * [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.680 * * * [progress]: adding candidates to table
16.044 * [progress]: [Phase 3 of 3] Extracting.
16.044 * * [regime]: Finding splitpoints for: (#<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 (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 (*.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 (+.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 (+.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) (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 (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 (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 (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) (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 (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.048 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
16.049 * * * * [regimes]: Trying to branch on c from (#<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 (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 (*.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 (+.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 (+.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) (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 (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 (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 (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) (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 (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.453 * * * * [regimes]: Trying to branch on a from (#<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 (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 (*.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 (+.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 (+.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) (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 (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 (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 (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) (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 (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.829 * * * * [regimes]: Trying to branch on b from (#<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 (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 (*.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 (+.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 (+.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) (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 (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 (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 (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) (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 (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.133 * * * [regime]: Found split indices: #<option (#s(si 8 256))>
17.133 * [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)
17.133 * * [simplify]: iters left: 6 (16 enodes)
17.135 * * [simplify]: Extracting #0: cost 1 inf + 0
17.135 * * [simplify]: Extracting #1: cost 3 inf + 0
17.135 * * [simplify]: Extracting #2: cost 4 inf + 1
17.135 * * [simplify]: Extracting #3: cost 7 inf + 1
17.135 * * [simplify]: Extracting #4: cost 7 inf + 3
17.135 * * [simplify]: Extracting #5: cost 8 inf + 4
17.135 * * [simplify]: Extracting #6: cost 8 inf + 406
17.135 * * [simplify]: Extracting #7: cost 8 inf + 407
17.135 * * [simplify]: Extracting #8: cost 9 inf + 407
17.135 * * [simplify]: Extracting #9: cost 8 inf + 408
17.135 * * [simplify]: Extracting #10: cost 4 inf + 2418
17.135 * * [simplify]: Extracting #11: cost 2 inf + 4746
17.136 * * [simplify]: Extracting #12: cost 0 inf + 8556
17.136 * [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)
17.136 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
17.178 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
17.180 * * * * [points]: Setting MPFR precision to 64
17.182 * * * * [points]: Setting MPFR precision to 320
17.183 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
17.185 * * * * [points]: Setting MPFR precision to 64
17.187 * * * * [points]: Setting MPFR precision to 320
17.190 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
17.192 * * * * [points]: Setting MPFR precision to 64
17.197 * * * * [points]: Setting MPFR precision to 320
17.201 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
17.204 * * * * [points]: Setting MPFR precision to 64
17.213 * * * * [points]: Setting MPFR precision to 320
17.222 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
17.224 * * * * [points]: Setting MPFR precision to 64
17.241 * * * * [points]: Setting MPFR precision to 320
17.258 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
17.260 * * * * [points]: Setting MPFR precision to 64
17.326 * * * * [points]: Setting MPFR precision to 320
17.360 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
17.363 * * * * [points]: Setting MPFR precision to 64
17.461 * * * * [points]: Setting MPFR precision to 320
17.540 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
17.543 * * * * [points]: Setting MPFR precision to 64
17.714 * * * * [points]: Setting MPFR precision to 320
17.925 * * * * [points]: Computing exacts for 8000 points
17.928 * * * * [points]: Setting MPFR precision to 64
19.172 * * * * [points]: Setting MPFR precision to 320
20.334 * * * * [points]: Filtering points with unrepresentable outputs
20.375 * * * * [points]: Sampled 8000 points with exact outputs
29.920 * [regime-testing]: Baseline error score: 64.0
29.926 * [regime-testing]: Oracle error score: 64.0
29.939 * [regime-testing]: End program error score: 1.5419624136882608