0.003 * [progress]: [Phase 1 of 3] Setting up.
0.005 * * * [progress]: [1/2] Preparing points
0.007 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.014 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.040 * * * * [points]: Setting MPFR precision to 64
0.042 * * * * [points]: Setting MPFR precision to 320
0.044 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.046 * * * * [points]: Setting MPFR precision to 64
0.047 * * * * [points]: Setting MPFR precision to 320
0.051 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.053 * * * * [points]: Setting MPFR precision to 64
0.059 * * * * [points]: Setting MPFR precision to 320
0.068 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.070 * * * * [points]: Setting MPFR precision to 64
0.080 * * * * [points]: Setting MPFR precision to 320
0.093 * * * * [points]: Computing exacts for 256 points
0.095 * * * * [points]: Setting MPFR precision to 64
0.126 * * * * [points]: Setting MPFR precision to 320
0.181 * * * * [points]: Filtering points with unrepresentable outputs
0.195 * * * * [points]: Sampling 63 additional inputs, on iter 1 have 193 / 256
0.195 * * * * [points]: Computing exacts on every 3 of 63 points to ramp up precision
0.196 * * * * [points]: Setting MPFR precision to 64
0.198 * * * * [points]: Setting MPFR precision to 320
0.199 * * * * [points]: Computing exacts for 63 points
0.200 * * * * [points]: Setting MPFR precision to 64
0.205 * * * * [points]: Setting MPFR precision to 320
0.210 * * * * [points]: Filtering points with unrepresentable outputs
0.213 * * * * [points]: Sampling 17 additional inputs, on iter 2 have 239 / 256
0.213 * * * * [points]: Computing exacts for 17 points
0.214 * * * * [points]: Setting MPFR precision to 64
0.215 * * * * [points]: Setting MPFR precision to 320
0.217 * * * * [points]: Filtering points with unrepresentable outputs
0.218 * * * * [points]: Sampling 5 additional inputs, on iter 3 have 251 / 256
0.218 * * * * [points]: Computing exacts for 5 points
0.219 * * * * [points]: Setting MPFR precision to 64
0.219 * * * * [points]: Setting MPFR precision to 320
0.220 * * * * [points]: Filtering points with unrepresentable outputs
0.220 * * * * [points]: Sampling 4 additional inputs, on iter 4 have 255 / 256
0.220 * * * * [points]: Computing exacts for 4 points
0.221 * * * * [points]: Setting MPFR precision to 64
0.221 * * * * [points]: Setting MPFR precision to 320
0.222 * * * * [points]: Filtering points with unrepresentable outputs
0.222 * * * * [points]: Sampled 258 points with exact outputs
0.222 * * * [progress]: [2/2] Setting up program.
0.242 * [progress]: [Phase 2 of 3] Improving.
0.243 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
0.244 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.245 * * [simplify]: iters left: 5 (10 enodes)
0.250 * * [simplify]: iters left: 4 (25 enodes)
0.255 * * [simplify]: iters left: 3 (48 enodes)
0.265 * * [simplify]: iters left: 2 (111 enodes)
0.311 * * [simplify]: iters left: 1 (392 enodes)
0.618 * * [simplify]: Extracting #0: cost 1 inf + 0
0.618 * * [simplify]: Extracting #1: cost 10 inf + 0
0.619 * * [simplify]: Extracting #2: cost 35 inf + 1
0.619 * * [simplify]: Extracting #3: cost 91 inf + 405
0.621 * * [simplify]: Extracting #4: cost 331 inf + 2291
0.628 * * [simplify]: Extracting #5: cost 455 inf + 80323
0.666 * * [simplify]: Extracting #6: cost 250 inf + 579968
0.713 * * [simplify]: Extracting #7: cost 28 inf + 1003440
0.788 * * [simplify]: Extracting #8: cost 0 inf + 1069311
0.834 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
0.834 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
0.870 * * [progress]: iteration 1 / 4
0.870 * * * [progress]: picking best candidate
0.885 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
0.885 * * * [progress]: localizing error
1.109 * * * [progress]: generating rewritten candidates
1.110 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.115 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1)
1.115 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1.121 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1.128 * * * [progress]: generating series expansions
1.129 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.129 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1)
1.129 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1.129 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1.129 * * * [progress]: simplifying candidates
1.129 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2)) a))>
1.129 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1.129 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
1.130 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
1.130 * * [simplify]: iters left: 5 (9 enodes)
1.134 * * [simplify]: iters left: 4 (32 enodes)
1.158 * * [simplify]: iters left: 3 (94 enodes)
1.202 * * [simplify]: iters left: 2 (340 enodes)
1.408 * * [simplify]: Extracting #0: cost 1 inf + 0
1.409 * * [simplify]: Extracting #1: cost 50 inf + 0
1.409 * * [simplify]: Extracting #2: cost 240 inf + 0
1.416 * * [simplify]: Extracting #3: cost 355 inf + 61800
1.431 * * [simplify]: Extracting #4: cost 246 inf + 415499
1.463 * * [simplify]: Extracting #5: cost 58 inf + 816216
1.522 * * [simplify]: Extracting #6: cost 1 inf + 911482
1.563 * * [simplify]: Extracting #7: cost 0 inf + 914765
1.630 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1.631 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
1.631 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))) b_2) a))>
1.631 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
1.631 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1.631 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.631 * * [simplify]: iters left: 5 (9 enodes)
1.635 * * [simplify]: iters left: 4 (29 enodes)
1.646 * * [simplify]: iters left: 3 (62 enodes)
1.666 * * [simplify]: iters left: 2 (199 enodes)
1.729 * * [simplify]: Extracting #0: cost 1 inf + 0
1.729 * * [simplify]: Extracting #1: cost 20 inf + 0
1.729 * * [simplify]: Extracting #2: cost 94 inf + 1
1.730 * * [simplify]: Extracting #3: cost 162 inf + 1046
1.731 * * [simplify]: Extracting #4: cost 208 inf + 17818
1.735 * * [simplify]: Extracting #5: cost 164 inf + 103714
1.758 * * [simplify]: Extracting #6: cost 47 inf + 336456
1.789 * * [simplify]: Extracting #7: cost 0 inf + 409081
1.821 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1.821 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1.821 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1.821 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.821 * * [simplify]: iters left: 5 (9 enodes)
1.825 * * [simplify]: iters left: 4 (29 enodes)
1.835 * * [simplify]: iters left: 3 (62 enodes)
1.860 * * [simplify]: iters left: 2 (199 enodes)
1.976 * * [simplify]: Extracting #0: cost 1 inf + 0
1.976 * * [simplify]: Extracting #1: cost 20 inf + 0
1.976 * * [simplify]: Extracting #2: cost 94 inf + 1
1.977 * * [simplify]: Extracting #3: cost 162 inf + 1046
1.979 * * [simplify]: Extracting #4: cost 208 inf + 17818
1.986 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.013 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.044 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.074 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.074 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
2.074 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
2.075 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.075 * * [simplify]: iters left: 5 (9 enodes)
2.078 * * [simplify]: iters left: 4 (29 enodes)
2.089 * * [simplify]: iters left: 3 (62 enodes)
2.113 * * [simplify]: iters left: 2 (199 enodes)
2.231 * * [simplify]: Extracting #0: cost 1 inf + 0
2.231 * * [simplify]: Extracting #1: cost 20 inf + 0
2.231 * * [simplify]: Extracting #2: cost 94 inf + 1
2.232 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.235 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.241 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.264 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.295 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.327 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.327 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
2.327 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
2.327 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.327 * * [simplify]: iters left: 5 (9 enodes)
2.329 * * [simplify]: iters left: 4 (29 enodes)
2.334 * * [simplify]: iters left: 3 (62 enodes)
2.346 * * [simplify]: iters left: 2 (199 enodes)
2.420 * * [simplify]: Extracting #0: cost 1 inf + 0
2.420 * * [simplify]: Extracting #1: cost 20 inf + 0
2.421 * * [simplify]: Extracting #2: cost 94 inf + 1
2.421 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.422 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.426 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.438 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.454 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.483 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.483 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
2.483 * * * [progress]: adding candidates to table
2.903 * * [progress]: iteration 2 / 4
2.903 * * * [progress]: picking best candidate
2.991 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
2.991 * * * [progress]: localizing error
3.319 * * * [progress]: generating rewritten candidates
3.320 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
3.328 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
3.329 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
3.330 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
3.332 * * * [progress]: generating series expansions
3.332 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
3.332 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
3.332 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
3.332 * * * * [progress]: [ 4 / 4 ] generating series at (2)
3.332 * * * [progress]: simplifying candidates
3.333 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
3.333 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
3.333 * * [simplify]: iters left: 2 (6 enodes)
3.334 * * [simplify]: iters left: 1 (14 enodes)
3.336 * * [simplify]: Extracting #0: cost 1 inf + 0
3.336 * * [simplify]: Extracting #1: cost 3 inf + 0
3.336 * * [simplify]: Extracting #2: cost 6 inf + 0
3.336 * * [simplify]: Extracting #3: cost 2 inf + 325
3.336 * * [simplify]: Extracting #4: cost 0 inf + 1329
3.336 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
3.336 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))
3.336 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>
3.336 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a))))
3.336 * * [simplify]: iters left: 4 (10 enodes)
3.339 * * [simplify]: iters left: 3 (43 enodes)
3.347 * * [simplify]: iters left: 2 (121 enodes)
3.386 * * [simplify]: iters left: 1 (429 enodes)
3.634 * * [simplify]: Extracting #0: cost 1 inf + 0
3.635 * * [simplify]: Extracting #1: cost 46 inf + 0
3.635 * * [simplify]: Extracting #2: cost 270 inf + 0
3.638 * * [simplify]: Extracting #3: cost 354 inf + 59003
3.651 * * [simplify]: Extracting #4: cost 345 inf + 369227
3.727 * * [simplify]: Extracting #5: cost 22 inf + 1102360
3.806 * * [simplify]: Extracting #6: cost 1 inf + 1150488
3.896 * * [simplify]: Extracting #7: cost 0 inf + 1155051
3.950 * [simplify]: Simplified to (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))))
3.950 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))
3.950 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 b_2)) a))>
3.950 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
3.950 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
3.951 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2))
3.951 * * [simplify]: iters left: 6 (13 enodes)
3.954 * * [simplify]: iters left: 5 (47 enodes)
3.962 * * [simplify]: iters left: 4 (118 enodes)
3.992 * * [simplify]: iters left: 3 (482 enodes)
4.404 * * [simplify]: Extracting #0: cost 1 inf + 0
4.404 * * [simplify]: Extracting #1: cost 39 inf + 0
4.405 * * [simplify]: Extracting #2: cost 255 inf + 0
4.408 * * [simplify]: Extracting #3: cost 532 inf + 10719
4.432 * * [simplify]: Extracting #4: cost 679 inf + 310118
4.536 * * [simplify]: Extracting #5: cost 214 inf + 1310578
4.688 * * [simplify]: Extracting #6: cost 5 inf + 1763746
4.849 * * [simplify]: Extracting #7: cost 0 inf + 1773035
5.012 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
5.012 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2))) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))
5.013 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
5.013 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
5.013 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
5.013 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
5.013 * * * [progress]: adding candidates to table
5.348 * * [progress]: iteration 3 / 4
5.348 * * * [progress]: picking best candidate
5.421 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
5.421 * * * [progress]: localizing error
5.785 * * * [progress]: generating rewritten candidates
5.785 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
5.788 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
5.791 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
5.796 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
5.796 * * * [progress]: generating series expansions
5.796 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
5.796 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
5.797 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
5.797 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
5.797 * * * [progress]: simplifying candidates
5.797 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
5.797 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.797 * * [simplify]: iters left: 4 (8 enodes)
5.798 * * [simplify]: iters left: 3 (23 enodes)
5.802 * * [simplify]: iters left: 2 (45 enodes)
5.811 * * [simplify]: iters left: 1 (108 enodes)
5.848 * * [simplify]: Extracting #0: cost 1 inf + 0
5.848 * * [simplify]: Extracting #1: cost 3 inf + 0
5.848 * * [simplify]: Extracting #2: cost 3 inf + 1
5.848 * * [simplify]: Extracting #3: cost 17 inf + 1
5.849 * * [simplify]: Extracting #4: cost 55 inf + 322
5.849 * * [simplify]: Extracting #5: cost 80 inf + 11197
5.851 * * [simplify]: Extracting #6: cost 84 inf + 56173
5.856 * * [simplify]: Extracting #7: cost 7 inf + 177856
5.867 * * [simplify]: Extracting #8: cost 0 inf + 193436
5.883 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.883 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
5.884 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.884 * * [simplify]: iters left: 4 (8 enodes)
5.886 * * [simplify]: iters left: 3 (28 enodes)
5.891 * * [simplify]: iters left: 2 (59 enodes)
5.902 * * [simplify]: iters left: 1 (178 enodes)
5.958 * * [simplify]: Extracting #0: cost 1 inf + 0
5.958 * * [simplify]: Extracting #1: cost 12 inf + 0
5.958 * * [simplify]: Extracting #2: cost 64 inf + 1
5.959 * * [simplify]: Extracting #3: cost 140 inf + 403
5.960 * * [simplify]: Extracting #4: cost 189 inf + 12881
5.964 * * [simplify]: Extracting #5: cost 149 inf + 112868
5.974 * * [simplify]: Extracting #6: cost 32 inf + 315911
5.988 * * [simplify]: Extracting #7: cost 1 inf + 362422
6.003 * * [simplify]: Extracting #8: cost 0 inf + 365106
6.016 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
6.017 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
6.017 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.017 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.017 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
6.017 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
6.017 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.017 * * [simplify]: iters left: 4 (8 enodes)
6.019 * * [simplify]: iters left: 3 (23 enodes)
6.022 * * [simplify]: iters left: 2 (45 enodes)
6.032 * * [simplify]: iters left: 1 (108 enodes)
6.059 * * [simplify]: Extracting #0: cost 1 inf + 0
6.059 * * [simplify]: Extracting #1: cost 3 inf + 0
6.059 * * [simplify]: Extracting #2: cost 3 inf + 1
6.060 * * [simplify]: Extracting #3: cost 17 inf + 1
6.060 * * [simplify]: Extracting #4: cost 55 inf + 322
6.060 * * [simplify]: Extracting #5: cost 80 inf + 11197
6.062 * * [simplify]: Extracting #6: cost 84 inf + 56173
6.067 * * [simplify]: Extracting #7: cost 7 inf + 177856
6.073 * * [simplify]: Extracting #8: cost 0 inf + 193436
6.079 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
6.079 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))
6.080 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))>
6.080 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))
6.080 * * [simplify]: iters left: 6 (11 enodes)
6.082 * * [simplify]: iters left: 5 (43 enodes)
6.091 * * [simplify]: iters left: 4 (139 enodes)
6.138 * * [simplify]: Extracting #0: cost 1 inf + 0
6.138 * * [simplify]: Extracting #1: cost 32 inf + 0
6.138 * * [simplify]: Extracting #2: cost 85 inf + 0
6.138 * * [simplify]: Extracting #3: cost 152 inf + 1364
6.139 * * [simplify]: Extracting #4: cost 163 inf + 24483
6.145 * * [simplify]: Extracting #5: cost 71 inf + 172897
6.156 * * [simplify]: Extracting #6: cost 3 inf + 277964
6.168 * * [simplify]: Extracting #7: cost 0 inf + 284573
6.181 * [simplify]: Simplified to (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2))))
6.181 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))
6.181 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.181 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.181 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.181 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.181 * * * [progress]: adding candidates to table
6.457 * * [progress]: iteration 4 / 4
6.457 * * * [progress]: picking best candidate
6.558 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.558 * * * [progress]: localizing error
6.931 * * * [progress]: generating rewritten candidates
6.931 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2)
6.933 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
6.936 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
6.938 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
6.943 * * * [progress]: generating series expansions
6.943 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2)
6.943 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
6.943 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
6.943 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
6.943 * * * [progress]: simplifying candidates
6.943 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.943 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.944 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
6.944 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.944 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
6.944 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.944 * * [simplify]: iters left: 4 (8 enodes)
6.945 * * [simplify]: iters left: 3 (23 enodes)
6.949 * * [simplify]: iters left: 2 (45 enodes)
6.957 * * [simplify]: iters left: 1 (108 enodes)
6.986 * * [simplify]: Extracting #0: cost 1 inf + 0
6.986 * * [simplify]: Extracting #1: cost 3 inf + 0
6.986 * * [simplify]: Extracting #2: cost 3 inf + 1
6.986 * * [simplify]: Extracting #3: cost 17 inf + 1
6.986 * * [simplify]: Extracting #4: cost 55 inf + 322
6.986 * * [simplify]: Extracting #5: cost 80 inf + 11197
6.988 * * [simplify]: Extracting #6: cost 84 inf + 56173
6.995 * * [simplify]: Extracting #7: cost 7 inf + 177856
7.002 * * [simplify]: Extracting #8: cost 0 inf + 193436
7.008 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
7.008 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))
7.008 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
7.009 * [simplify]: Simplifying (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))
7.009 * * [simplify]: iters left: 6 (11 enodes)
7.011 * * [simplify]: iters left: 5 (35 enodes)
7.018 * * [simplify]: iters left: 4 (111 enodes)
7.046 * * [simplify]: iters left: 3 (448 enodes)
7.405 * * [simplify]: Extracting #0: cost 1 inf + 0
7.405 * * [simplify]: Extracting #1: cost 64 inf + 0
7.407 * * [simplify]: Extracting #2: cost 370 inf + 0
7.410 * * [simplify]: Extracting #3: cost 522 inf + 6695
7.429 * * [simplify]: Extracting #4: cost 536 inf + 237314
7.517 * * [simplify]: Extracting #5: cost 132 inf + 950329
7.593 * * [simplify]: Extracting #6: cost 26 inf + 1188087
7.683 * * [simplify]: Extracting #7: cost 0 inf + 1213652
7.746 * * [simplify]: Extracting #8: cost 0 inf + 1213496
7.853 * [simplify]: Simplified to (*.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
7.853 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))
7.853 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
7.853 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.853 * * [simplify]: iters left: 4 (8 enodes)
7.855 * * [simplify]: iters left: 3 (23 enodes)
7.859 * * [simplify]: iters left: 2 (45 enodes)
7.867 * * [simplify]: iters left: 1 (108 enodes)
7.909 * * [simplify]: Extracting #0: cost 1 inf + 0
7.909 * * [simplify]: Extracting #1: cost 3 inf + 0
7.909 * * [simplify]: Extracting #2: cost 3 inf + 1
7.909 * * [simplify]: Extracting #3: cost 17 inf + 1
7.909 * * [simplify]: Extracting #4: cost 55 inf + 322
7.910 * * [simplify]: Extracting #5: cost 80 inf + 11197
7.914 * * [simplify]: Extracting #6: cost 84 inf + 56173
7.925 * * [simplify]: Extracting #7: cost 7 inf + 177856
7.938 * * [simplify]: Extracting #8: cost 0 inf + 193436
7.951 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
7.951 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
7.951 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.951 * * [simplify]: iters left: 4 (8 enodes)
7.955 * * [simplify]: iters left: 3 (28 enodes)
7.964 * * [simplify]: iters left: 2 (59 enodes)
7.975 * * [simplify]: iters left: 1 (178 enodes)
8.055 * * [simplify]: Extracting #0: cost 1 inf + 0
8.055 * * [simplify]: Extracting #1: cost 12 inf + 0
8.056 * * [simplify]: Extracting #2: cost 64 inf + 1
8.056 * * [simplify]: Extracting #3: cost 140 inf + 403
8.058 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.065 * * [simplify]: Extracting #5: cost 149 inf + 112868
8.086 * * [simplify]: Extracting #6: cost 32 inf + 315911
8.113 * * [simplify]: Extracting #7: cost 1 inf + 362422
8.144 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.170 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.170 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
8.171 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
8.171 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.171 * * [simplify]: iters left: 4 (8 enodes)
8.174 * * [simplify]: iters left: 3 (23 enodes)
8.181 * * [simplify]: iters left: 2 (45 enodes)
8.197 * * [simplify]: iters left: 1 (108 enodes)
8.251 * * [simplify]: Extracting #0: cost 1 inf + 0
8.251 * * [simplify]: Extracting #1: cost 3 inf + 0
8.251 * * [simplify]: Extracting #2: cost 3 inf + 1
8.251 * * [simplify]: Extracting #3: cost 17 inf + 1
8.251 * * [simplify]: Extracting #4: cost 55 inf + 322
8.252 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.256 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.267 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.280 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.292 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.293 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
8.293 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.293 * * [simplify]: iters left: 4 (8 enodes)
8.296 * * [simplify]: iters left: 3 (28 enodes)
8.306 * * [simplify]: iters left: 2 (59 enodes)
8.328 * * [simplify]: iters left: 1 (178 enodes)
8.432 * * [simplify]: Extracting #0: cost 1 inf + 0
8.432 * * [simplify]: Extracting #1: cost 12 inf + 0
8.432 * * [simplify]: Extracting #2: cost 64 inf + 1
8.433 * * [simplify]: Extracting #3: cost 140 inf + 403
8.435 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.442 * * [simplify]: Extracting #5: cost 149 inf + 112868
8.464 * * [simplify]: Extracting #6: cost 32 inf + 315911
8.492 * * [simplify]: Extracting #7: cost 1 inf + 362422
8.519 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.547 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.548 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
8.548 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
8.548 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.548 * * [simplify]: iters left: 4 (8 enodes)
8.551 * * [simplify]: iters left: 3 (23 enodes)
8.562 * * [simplify]: iters left: 2 (45 enodes)
8.578 * * [simplify]: iters left: 1 (108 enodes)
8.630 * * [simplify]: Extracting #0: cost 1 inf + 0
8.630 * * [simplify]: Extracting #1: cost 3 inf + 0
8.630 * * [simplify]: Extracting #2: cost 3 inf + 1
8.631 * * [simplify]: Extracting #3: cost 17 inf + 1
8.631 * * [simplify]: Extracting #4: cost 55 inf + 322
8.632 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.635 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.646 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.658 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.671 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.671 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
8.671 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.671 * * [simplify]: iters left: 4 (8 enodes)
8.675 * * [simplify]: iters left: 3 (28 enodes)
8.685 * * [simplify]: iters left: 2 (59 enodes)
8.710 * * [simplify]: iters left: 1 (178 enodes)
8.815 * * [simplify]: Extracting #0: cost 1 inf + 0
8.815 * * [simplify]: Extracting #1: cost 12 inf + 0
8.815 * * [simplify]: Extracting #2: cost 64 inf + 1
8.816 * * [simplify]: Extracting #3: cost 140 inf + 403
8.818 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.825 * * [simplify]: Extracting #5: cost 149 inf + 112868
8.849 * * [simplify]: Extracting #6: cost 32 inf + 315911
8.876 * * [simplify]: Extracting #7: cost 1 inf + 362422
8.904 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.931 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.931 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
8.932 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
8.932 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.932 * * [simplify]: iters left: 4 (8 enodes)
8.935 * * [simplify]: iters left: 3 (23 enodes)
8.943 * * [simplify]: iters left: 2 (45 enodes)
8.959 * * [simplify]: iters left: 1 (108 enodes)
9.017 * * [simplify]: Extracting #0: cost 1 inf + 0
9.017 * * [simplify]: Extracting #1: cost 3 inf + 0
9.017 * * [simplify]: Extracting #2: cost 3 inf + 1
9.017 * * [simplify]: Extracting #3: cost 17 inf + 1
9.017 * * [simplify]: Extracting #4: cost 55 inf + 322
9.018 * * [simplify]: Extracting #5: cost 80 inf + 11197
9.022 * * [simplify]: Extracting #6: cost 84 inf + 56173
9.032 * * [simplify]: Extracting #7: cost 7 inf + 177856
9.045 * * [simplify]: Extracting #8: cost 0 inf + 193436
9.057 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
9.057 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
9.058 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
9.058 * * [simplify]: iters left: 4 (8 enodes)
9.061 * * [simplify]: iters left: 3 (28 enodes)
9.070 * * [simplify]: iters left: 2 (59 enodes)
9.092 * * [simplify]: iters left: 1 (178 enodes)
9.197 * * [simplify]: Extracting #0: cost 1 inf + 0
9.197 * * [simplify]: Extracting #1: cost 12 inf + 0
9.197 * * [simplify]: Extracting #2: cost 64 inf + 1
9.198 * * [simplify]: Extracting #3: cost 140 inf + 403
9.200 * * [simplify]: Extracting #4: cost 189 inf + 12881
9.207 * * [simplify]: Extracting #5: cost 149 inf + 112868
9.229 * * [simplify]: Extracting #6: cost 32 inf + 315911
9.257 * * [simplify]: Extracting #7: cost 1 inf + 362422
9.288 * * [simplify]: Extracting #8: cost 0 inf + 365106
9.315 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
9.316 * [simplify]: Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
9.316 * * * [progress]: adding candidates to table
9.721 * [progress]: [Phase 3 of 3] Extracting.
9.722 * * [regime]: Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
9.728 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
9.729 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
10.241 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
10.744 * * * * [regimes]: Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>)
11.262 * * * [regime]: Found split indices: #<option (#s(si 4 256))>
11.262 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
11.262 * * [simplify]: iters left: 5 (9 enodes)
11.263 * * [simplify]: Extracting #0: cost 1 inf + 0
11.263 * * [simplify]: Extracting #1: cost 3 inf + 0
11.263 * * [simplify]: Extracting #2: cost 4 inf + 1
11.263 * * [simplify]: Extracting #3: cost 4 inf + 2
11.263 * * [simplify]: Extracting #4: cost 6 inf + 2
11.263 * * [simplify]: Extracting #5: cost 6 inf + 323
11.263 * * [simplify]: Extracting #6: cost 0 inf + 4258
11.263 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
11.264 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
11.334 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
11.336 * * * * [points]: Setting MPFR precision to 64
11.338 * * * * [points]: Setting MPFR precision to 320
11.340 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
11.342 * * * * [points]: Setting MPFR precision to 64
11.347 * * * * [points]: Setting MPFR precision to 320
11.351 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
11.352 * * * * [points]: Setting MPFR precision to 64
11.360 * * * * [points]: Setting MPFR precision to 320
11.369 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
11.371 * * * * [points]: Setting MPFR precision to 64
11.385 * * * * [points]: Setting MPFR precision to 320
11.403 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
11.405 * * * * [points]: Setting MPFR precision to 64
11.435 * * * * [points]: Setting MPFR precision to 320
11.472 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
11.473 * * * * [points]: Setting MPFR precision to 64
11.530 * * * * [points]: Setting MPFR precision to 320
11.650 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
11.652 * * * * [points]: Setting MPFR precision to 64
11.777 * * * * [points]: Setting MPFR precision to 320
12.359 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
12.361 * * * * [points]: Setting MPFR precision to 64
12.615 * * * * [points]: Setting MPFR precision to 320
12.926 * * * * [points]: Computing exacts for 8000 points
12.960 * * * * [points]: Setting MPFR precision to 64
14.090 * * * * [points]: Setting MPFR precision to 320
15.464 * * * * [points]: Filtering points with unrepresentable outputs
16.311 * * * * [points]: Sampling 2030 additional inputs, on iter 1 have 5970 / 8000
16.326 * * * * [points]: Computing exacts on every 126 of 2030 points to ramp up precision
16.329 * * * * [points]: Setting MPFR precision to 64
16.331 * * * * [points]: Setting MPFR precision to 320
16.333 * * * * [points]: Computing exacts on every 63 of 2030 points to ramp up precision
16.335 * * * * [points]: Setting MPFR precision to 64
16.338 * * * * [points]: Setting MPFR precision to 320
16.359 * * * * [points]: Computing exacts on every 31 of 2030 points to ramp up precision
16.361 * * * * [points]: Setting MPFR precision to 64
16.369 * * * * [points]: Setting MPFR precision to 320
16.379 * * * * [points]: Computing exacts on every 15 of 2030 points to ramp up precision
16.381 * * * * [points]: Setting MPFR precision to 64
16.396 * * * * [points]: Setting MPFR precision to 320
16.416 * * * * [points]: Computing exacts on every 7 of 2030 points to ramp up precision
16.418 * * * * [points]: Setting MPFR precision to 64
16.450 * * * * [points]: Setting MPFR precision to 320
16.489 * * * * [points]: Computing exacts on every 3 of 2030 points to ramp up precision
16.491 * * * * [points]: Setting MPFR precision to 64
16.553 * * * * [points]: Setting MPFR precision to 320
16.684 * * * * [points]: Computing exacts for 2030 points
16.686 * * * * [points]: Setting MPFR precision to 64
17.382 * * * * [points]: Setting MPFR precision to 320
17.660 * * * * [points]: Filtering points with unrepresentable outputs
17.830 * * * * [points]: Sampling 507 additional inputs, on iter 2 have 7493 / 8000
17.832 * * * * [points]: Computing exacts on every 31 of 507 points to ramp up precision
17.833 * * * * [points]: Setting MPFR precision to 64
17.835 * * * * [points]: Setting MPFR precision to 320
17.836 * * * * [points]: Computing exacts on every 15 of 507 points to ramp up precision
17.837 * * * * [points]: Setting MPFR precision to 64
17.839 * * * * [points]: Setting MPFR precision to 320
17.842 * * * * [points]: Computing exacts on every 7 of 507 points to ramp up precision
17.843 * * * * [points]: Setting MPFR precision to 64
17.847 * * * * [points]: Setting MPFR precision to 320
17.853 * * * * [points]: Computing exacts on every 3 of 507 points to ramp up precision
17.854 * * * * [points]: Setting MPFR precision to 64
17.867 * * * * [points]: Setting MPFR precision to 320
17.885 * * * * [points]: Computing exacts for 507 points
17.887 * * * * [points]: Setting MPFR precision to 64
17.975 * * * * [points]: Setting MPFR precision to 320
18.053 * * * * [points]: Filtering points with unrepresentable outputs
18.102 * * * * [points]: Sampling 122 additional inputs, on iter 3 have 7878 / 8000
18.103 * * * * [points]: Computing exacts on every 7 of 122 points to ramp up precision
18.105 * * * * [points]: Setting MPFR precision to 64
18.107 * * * * [points]: Setting MPFR precision to 320
18.109 * * * * [points]: Computing exacts on every 3 of 122 points to ramp up precision
18.111 * * * * [points]: Setting MPFR precision to 64
18.115 * * * * [points]: Setting MPFR precision to 320
18.120 * * * * [points]: Computing exacts for 122 points
18.121 * * * * [points]: Setting MPFR precision to 64
18.136 * * * * [points]: Setting MPFR precision to 320
18.154 * * * * [points]: Filtering points with unrepresentable outputs
18.206 * * * * [points]: Sampling 32 additional inputs, on iter 4 have 7968 / 8000
18.207 * * * * [points]: Computing exacts on every 2 of 32 points to ramp up precision
18.209 * * * * [points]: Setting MPFR precision to 64
18.210 * * * * [points]: Setting MPFR precision to 320
18.212 * * * * [points]: Computing exacts for 32 points
18.214 * * * * [points]: Setting MPFR precision to 64
18.218 * * * * [points]: Setting MPFR precision to 320
18.222 * * * * [points]: Filtering points with unrepresentable outputs
18.225 * * * * [points]: Sampling 11 additional inputs, on iter 5 have 7989 / 8000
18.226 * * * * [points]: Computing exacts for 11 points
18.227 * * * * [points]: Setting MPFR precision to 64
18.229 * * * * [points]: Setting MPFR precision to 320
18.231 * * * * [points]: Filtering points with unrepresentable outputs
18.232 * * * * [points]: Sampling 5 additional inputs, on iter 6 have 7995 / 8000
18.232 * * * * [points]: Computing exacts for 5 points
18.233 * * * * [points]: Setting MPFR precision to 64
18.234 * * * * [points]: Setting MPFR precision to 320
18.235 * * * * [points]: Filtering points with unrepresentable outputs
18.236 * * * * [points]: Sampled 8000 points with exact outputs
20.776 * [regime-testing]: Baseline error score: 64.0
20.778 * [regime-testing]: Oracle error score: 64.0
20.782 * [regime-testing]: End program error score: 2.262470388915334