0.004 * [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.010 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.123 * * * * [points]: Setting MPFR precision to 64
0.128 * * * * [points]: Setting MPFR precision to 320
0.130 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.133 * * * * [points]: Setting MPFR precision to 64
0.137 * * * * [points]: Setting MPFR precision to 320
0.141 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.143 * * * * [points]: Setting MPFR precision to 64
0.149 * * * * [points]: Setting MPFR precision to 320
0.155 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.157 * * * * [points]: Setting MPFR precision to 64
0.166 * * * * [points]: Setting MPFR precision to 320
0.176 * * * * [points]: Computing exacts for 256 points
0.178 * * * * [points]: Setting MPFR precision to 64
0.206 * * * * [points]: Setting MPFR precision to 320
0.226 * * * * [points]: Filtering points with unrepresentable outputs
0.227 * * * * [points]: Sampled 256 points with exact outputs
0.228 * * * [progress]: [2/2] Setting up program.
0.239 * [progress]: [Phase 2 of 3] Improving.
0.239 * * * * [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.240 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.241 * * [simplify]: iters left: 5 (10 enodes)
0.291 * * [simplify]: iters left: 4 (25 enodes)
0.301 * * [simplify]: iters left: 3 (48 enodes)
0.319 * * [simplify]: iters left: 2 (111 enodes)
0.372 * * [simplify]: iters left: 1 (392 enodes)
0.696 * * [simplify]: Extracting #0: cost 1 inf + 0
0.697 * * [simplify]: Extracting #1: cost 10 inf + 0
0.697 * * [simplify]: Extracting #2: cost 35 inf + 1
0.697 * * [simplify]: Extracting #3: cost 91 inf + 405
0.698 * * [simplify]: Extracting #4: cost 331 inf + 2291
0.701 * * [simplify]: Extracting #5: cost 455 inf + 80323
0.740 * * [simplify]: Extracting #6: cost 250 inf + 579968
0.789 * * [simplify]: Extracting #7: cost 28 inf + 1003440
0.848 * * [simplify]: Extracting #8: cost 0 inf + 1069311
0.929 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
0.929 * [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.942 * * [progress]: iteration 1 / 4
0.942 * * * [progress]: picking best candidate
0.946 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
0.946 * * * [progress]: localizing error
1.104 * * * [progress]: generating rewritten candidates
1.104 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.107 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1)
1.107 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1.110 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1.114 * * * [progress]: generating series expansions
1.114 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.115 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1)
1.115 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1.115 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1.115 * * * [progress]: simplifying candidates
1.115 * * * * [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.115 * * * * [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.115 * * * * [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.115 * [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.115 * * [simplify]: iters left: 5 (9 enodes)
1.117 * * [simplify]: iters left: 4 (32 enodes)
1.124 * * [simplify]: iters left: 3 (94 enodes)
1.179 * * [simplify]: iters left: 2 (340 enodes)
1.397 * * [simplify]: Extracting #0: cost 1 inf + 0
1.397 * * [simplify]: Extracting #1: cost 50 inf + 0
1.398 * * [simplify]: Extracting #2: cost 240 inf + 0
1.404 * * [simplify]: Extracting #3: cost 355 inf + 61800
1.434 * * [simplify]: Extracting #4: cost 246 inf + 415499
1.502 * * [simplify]: Extracting #5: cost 58 inf + 816216
1.545 * * [simplify]: Extracting #6: cost 1 inf + 911482
1.625 * * [simplify]: Extracting #7: cost 0 inf + 914765
1.700 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1.700 * [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.701 * * * * [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.701 * * * * [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.701 * * * * [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.701 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.701 * * [simplify]: iters left: 5 (9 enodes)
1.703 * * [simplify]: iters left: 4 (29 enodes)
1.708 * * [simplify]: iters left: 3 (62 enodes)
1.720 * * [simplify]: iters left: 2 (199 enodes)
1.829 * * [simplify]: Extracting #0: cost 1 inf + 0
1.829 * * [simplify]: Extracting #1: cost 20 inf + 0
1.829 * * [simplify]: Extracting #2: cost 94 inf + 1
1.830 * * [simplify]: Extracting #3: cost 162 inf + 1046
1.832 * * [simplify]: Extracting #4: cost 208 inf + 17818
1.839 * * [simplify]: Extracting #5: cost 164 inf + 103714
1.858 * * [simplify]: Extracting #6: cost 47 inf + 336456
1.876 * * [simplify]: Extracting #7: cost 0 inf + 409081
1.901 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1.901 * [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.901 * * * * [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.902 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.902 * * [simplify]: iters left: 5 (9 enodes)
1.906 * * [simplify]: iters left: 4 (29 enodes)
1.916 * * [simplify]: iters left: 3 (62 enodes)
1.929 * * [simplify]: iters left: 2 (199 enodes)
2.021 * * [simplify]: Extracting #0: cost 1 inf + 0
2.022 * * [simplify]: Extracting #1: cost 20 inf + 0
2.022 * * [simplify]: Extracting #2: cost 94 inf + 1
2.023 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.025 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.031 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.054 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.085 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.120 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.120 * [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.120 * * * * [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.120 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.121 * * [simplify]: iters left: 5 (9 enodes)
2.124 * * [simplify]: iters left: 4 (29 enodes)
2.134 * * [simplify]: iters left: 3 (62 enodes)
2.152 * * [simplify]: iters left: 2 (199 enodes)
2.227 * * [simplify]: Extracting #0: cost 1 inf + 0
2.227 * * [simplify]: Extracting #1: cost 20 inf + 0
2.228 * * [simplify]: Extracting #2: cost 94 inf + 1
2.228 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.231 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.237 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.255 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.270 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.294 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.295 * [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.295 * * * * [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.295 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.295 * * [simplify]: iters left: 5 (9 enodes)
2.299 * * [simplify]: iters left: 4 (29 enodes)
2.309 * * [simplify]: iters left: 3 (62 enodes)
2.337 * * [simplify]: iters left: 2 (199 enodes)
2.426 * * [simplify]: Extracting #0: cost 1 inf + 0
2.426 * * [simplify]: Extracting #1: cost 20 inf + 0
2.426 * * [simplify]: Extracting #2: cost 94 inf + 1
2.427 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.430 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.437 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.449 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.464 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.490 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.490 * [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.490 * * * [progress]: adding candidates to table
2.610 * * [progress]: iteration 2 / 4
2.610 * * * [progress]: picking best candidate
2.633 * * * * [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.633 * * * [progress]: localizing error
2.899 * * * [progress]: generating rewritten candidates
2.899 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
2.912 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
2.914 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
2.914 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
2.916 * * * [progress]: generating series expansions
2.916 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
2.916 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
2.916 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
2.916 * * * * [progress]: [ 4 / 4 ] generating series at (2)
2.917 * * * [progress]: simplifying candidates
2.917 * * * * [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))>
2.917 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
2.917 * * [simplify]: iters left: 2 (6 enodes)
2.918 * * [simplify]: iters left: 1 (14 enodes)
2.920 * * [simplify]: Extracting #0: cost 1 inf + 0
2.920 * * [simplify]: Extracting #1: cost 3 inf + 0
2.920 * * [simplify]: Extracting #2: cost 6 inf + 0
2.920 * * [simplify]: Extracting #3: cost 2 inf + 325
2.920 * * [simplify]: Extracting #4: cost 0 inf + 1329
2.920 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
2.920 * [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))
2.920 * * * * [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))>
2.920 * [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))))
2.920 * * [simplify]: iters left: 4 (10 enodes)
2.923 * * [simplify]: iters left: 3 (43 enodes)
2.931 * * [simplify]: iters left: 2 (121 enodes)
2.985 * * [simplify]: iters left: 1 (429 enodes)
3.324 * * [simplify]: Extracting #0: cost 1 inf + 0
3.324 * * [simplify]: Extracting #1: cost 46 inf + 0
3.325 * * [simplify]: Extracting #2: cost 270 inf + 0
3.330 * * [simplify]: Extracting #3: cost 354 inf + 59003
3.345 * * [simplify]: Extracting #4: cost 345 inf + 369227
3.402 * * [simplify]: Extracting #5: cost 22 inf + 1102360
3.498 * * [simplify]: Extracting #6: cost 1 inf + 1150488
3.574 * * [simplify]: Extracting #7: cost 0 inf + 1155051
3.675 * [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.676 * [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.676 * * * * [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.676 * * * * [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.676 * * * * [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.676 * [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.677 * * [simplify]: iters left: 6 (13 enodes)
3.683 * * [simplify]: iters left: 5 (47 enodes)
3.701 * * [simplify]: iters left: 4 (118 enodes)
3.761 * * [simplify]: iters left: 3 (482 enodes)
4.356 * * [simplify]: Extracting #0: cost 1 inf + 0
4.356 * * [simplify]: Extracting #1: cost 39 inf + 0
4.357 * * [simplify]: Extracting #2: cost 255 inf + 0
4.360 * * [simplify]: Extracting #3: cost 532 inf + 10719
4.384 * * [simplify]: Extracting #4: cost 679 inf + 310118
4.484 * * [simplify]: Extracting #5: cost 214 inf + 1310578
4.610 * * [simplify]: Extracting #6: cost 5 inf + 1763746
4.766 * * [simplify]: Extracting #7: cost 0 inf + 1773035
4.905 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
4.905 * [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))))
4.906 * * * * [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))>
4.906 * * * * [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))>
4.906 * * * * [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))>
4.906 * * * * [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))>
4.906 * * * [progress]: adding candidates to table
5.077 * * [progress]: iteration 3 / 4
5.077 * * * [progress]: picking best candidate
5.106 * * * * [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.107 * * * [progress]: localizing error
5.410 * * * [progress]: generating rewritten candidates
5.410 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
5.416 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
5.421 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
5.431 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
5.432 * * * [progress]: generating series expansions
5.432 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
5.432 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
5.432 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
5.432 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
5.432 * * * [progress]: simplifying candidates
5.432 * * * * [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.433 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.433 * * [simplify]: iters left: 4 (8 enodes)
5.436 * * [simplify]: iters left: 3 (23 enodes)
5.444 * * [simplify]: iters left: 2 (45 enodes)
5.461 * * [simplify]: iters left: 1 (108 enodes)
5.521 * * [simplify]: Extracting #0: cost 1 inf + 0
5.522 * * [simplify]: Extracting #1: cost 3 inf + 0
5.522 * * [simplify]: Extracting #2: cost 3 inf + 1
5.522 * * [simplify]: Extracting #3: cost 17 inf + 1
5.522 * * [simplify]: Extracting #4: cost 55 inf + 322
5.523 * * [simplify]: Extracting #5: cost 80 inf + 11197
5.527 * * [simplify]: Extracting #6: cost 84 inf + 56173
5.537 * * [simplify]: Extracting #7: cost 7 inf + 177856
5.550 * * [simplify]: Extracting #8: cost 0 inf + 193436
5.563 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.563 * [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.563 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.563 * * [simplify]: iters left: 4 (8 enodes)
5.567 * * [simplify]: iters left: 3 (28 enodes)
5.576 * * [simplify]: iters left: 2 (59 enodes)
5.588 * * [simplify]: iters left: 1 (178 enodes)
5.663 * * [simplify]: Extracting #0: cost 1 inf + 0
5.663 * * [simplify]: Extracting #1: cost 12 inf + 0
5.663 * * [simplify]: Extracting #2: cost 64 inf + 1
5.664 * * [simplify]: Extracting #3: cost 140 inf + 403
5.666 * * [simplify]: Extracting #4: cost 189 inf + 12881
5.674 * * [simplify]: Extracting #5: cost 149 inf + 112868
5.695 * * [simplify]: Extracting #6: cost 32 inf + 315911
5.721 * * [simplify]: Extracting #7: cost 1 inf + 362422
5.741 * * [simplify]: Extracting #8: cost 0 inf + 365106
5.755 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
5.756 * [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))
5.756 * * * * [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))>
5.756 * * * * [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))>
5.756 * * * * [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))>
5.756 * * * * [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))>
5.756 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.756 * * [simplify]: iters left: 4 (8 enodes)
5.758 * * [simplify]: iters left: 3 (23 enodes)
5.761 * * [simplify]: iters left: 2 (45 enodes)
5.769 * * [simplify]: iters left: 1 (108 enodes)
5.808 * * [simplify]: Extracting #0: cost 1 inf + 0
5.808 * * [simplify]: Extracting #1: cost 3 inf + 0
5.808 * * [simplify]: Extracting #2: cost 3 inf + 1
5.808 * * [simplify]: Extracting #3: cost 17 inf + 1
5.809 * * [simplify]: Extracting #4: cost 55 inf + 322
5.810 * * [simplify]: Extracting #5: cost 80 inf + 11197
5.813 * * [simplify]: Extracting #6: cost 84 inf + 56173
5.818 * * [simplify]: Extracting #7: cost 7 inf + 177856
5.824 * * [simplify]: Extracting #8: cost 0 inf + 193436
5.832 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.832 * [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))
5.832 * * * * [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))>
5.833 * [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)))
5.833 * * [simplify]: iters left: 6 (11 enodes)
5.835 * * [simplify]: iters left: 5 (43 enodes)
5.843 * * [simplify]: iters left: 4 (139 enodes)
5.887 * * [simplify]: Extracting #0: cost 1 inf + 0
5.887 * * [simplify]: Extracting #1: cost 32 inf + 0
5.887 * * [simplify]: Extracting #2: cost 85 inf + 0
5.887 * * [simplify]: Extracting #3: cost 152 inf + 1364
5.888 * * [simplify]: Extracting #4: cost 163 inf + 24483
5.895 * * [simplify]: Extracting #5: cost 71 inf + 172897
5.905 * * [simplify]: Extracting #6: cost 3 inf + 277964
5.926 * * [simplify]: Extracting #7: cost 0 inf + 284573
5.938 * [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))))
5.939 * [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))
5.939 * * * * [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))>
5.939 * * * * [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))>
5.939 * * * * [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))>
5.939 * * * * [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))>
5.939 * * * [progress]: adding candidates to table
6.038 * * [progress]: iteration 4 / 4
6.038 * * * [progress]: picking best candidate
6.094 * * * * [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.094 * * * [progress]: localizing error
6.368 * * * [progress]: generating rewritten candidates
6.368 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
6.373 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
6.378 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
6.381 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
6.391 * * * [progress]: generating series expansions
6.391 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
6.391 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
6.391 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
6.391 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
6.391 * * * [progress]: simplifying candidates
6.391 * * * * [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 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
6.391 * * * * [progress]: [ 2 / 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.391 * * * * [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))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
6.391 * * * * [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))) 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.391 * * * * [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.392 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.392 * * [simplify]: iters left: 4 (8 enodes)
6.395 * * [simplify]: iters left: 3 (23 enodes)
6.403 * * [simplify]: iters left: 2 (45 enodes)
6.418 * * [simplify]: iters left: 1 (108 enodes)
6.471 * * [simplify]: Extracting #0: cost 1 inf + 0
6.471 * * [simplify]: Extracting #1: cost 3 inf + 0
6.471 * * [simplify]: Extracting #2: cost 3 inf + 1
6.471 * * [simplify]: Extracting #3: cost 17 inf + 1
6.471 * * [simplify]: Extracting #4: cost 55 inf + 322
6.471 * * [simplify]: Extracting #5: cost 80 inf + 11197
6.473 * * [simplify]: Extracting #6: cost 84 inf + 56173
6.479 * * [simplify]: Extracting #7: cost 7 inf + 177856
6.485 * * [simplify]: Extracting #8: cost 0 inf + 193436
6.491 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
6.491 * [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.492 * * * * [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))>
6.492 * [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)))
6.492 * * [simplify]: iters left: 6 (11 enodes)
6.494 * * [simplify]: iters left: 5 (35 enodes)
6.503 * * [simplify]: iters left: 4 (111 enodes)
6.555 * * [simplify]: iters left: 3 (448 enodes)
7.278 * * [simplify]: Extracting #0: cost 1 inf + 0
7.278 * * [simplify]: Extracting #1: cost 64 inf + 0
7.280 * * [simplify]: Extracting #2: cost 370 inf + 0
7.283 * * [simplify]: Extracting #3: cost 522 inf + 6695
7.303 * * [simplify]: Extracting #4: cost 536 inf + 237314
7.380 * * [simplify]: Extracting #5: cost 132 inf + 950329
7.466 * * [simplify]: Extracting #6: cost 26 inf + 1188087
7.550 * * [simplify]: Extracting #7: cost 0 inf + 1213652
7.660 * * [simplify]: Extracting #8: cost 0 inf + 1213496
7.771 * [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.772 * [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.772 * * * * [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.772 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.772 * * [simplify]: iters left: 4 (8 enodes)
7.775 * * [simplify]: iters left: 3 (23 enodes)
7.783 * * [simplify]: iters left: 2 (45 enodes)
7.792 * * [simplify]: iters left: 1 (108 enodes)
7.820 * * [simplify]: Extracting #0: cost 1 inf + 0
7.820 * * [simplify]: Extracting #1: cost 3 inf + 0
7.820 * * [simplify]: Extracting #2: cost 3 inf + 1
7.820 * * [simplify]: Extracting #3: cost 17 inf + 1
7.820 * * [simplify]: Extracting #4: cost 55 inf + 322
7.821 * * [simplify]: Extracting #5: cost 80 inf + 11197
7.825 * * [simplify]: Extracting #6: cost 84 inf + 56173
7.835 * * [simplify]: Extracting #7: cost 7 inf + 177856
7.848 * * [simplify]: Extracting #8: cost 0 inf + 193436
7.861 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
7.862 * [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.862 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.862 * * [simplify]: iters left: 4 (8 enodes)
7.865 * * [simplify]: iters left: 3 (28 enodes)
7.875 * * [simplify]: iters left: 2 (59 enodes)
7.895 * * [simplify]: iters left: 1 (178 enodes)
7.954 * * [simplify]: Extracting #0: cost 1 inf + 0
7.954 * * [simplify]: Extracting #1: cost 12 inf + 0
7.954 * * [simplify]: Extracting #2: cost 64 inf + 1
7.955 * * [simplify]: Extracting #3: cost 140 inf + 403
7.956 * * [simplify]: Extracting #4: cost 189 inf + 12881
7.961 * * [simplify]: Extracting #5: cost 149 inf + 112868
7.972 * * [simplify]: Extracting #6: cost 32 inf + 315911
7.994 * * [simplify]: Extracting #7: cost 1 inf + 362422
8.023 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.050 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.051 * [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.051 * * * * [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.051 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.051 * * [simplify]: iters left: 4 (8 enodes)
8.054 * * [simplify]: iters left: 3 (23 enodes)
8.062 * * [simplify]: iters left: 2 (45 enodes)
8.073 * * [simplify]: iters left: 1 (108 enodes)
8.105 * * [simplify]: Extracting #0: cost 1 inf + 0
8.105 * * [simplify]: Extracting #1: cost 3 inf + 0
8.105 * * [simplify]: Extracting #2: cost 3 inf + 1
8.105 * * [simplify]: Extracting #3: cost 17 inf + 1
8.105 * * [simplify]: Extracting #4: cost 55 inf + 322
8.106 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.109 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.119 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.132 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.145 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.145 * [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.145 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.145 * * [simplify]: iters left: 4 (8 enodes)
8.149 * * [simplify]: iters left: 3 (28 enodes)
8.160 * * [simplify]: iters left: 2 (59 enodes)
8.183 * * [simplify]: iters left: 1 (178 enodes)
8.252 * * [simplify]: Extracting #0: cost 1 inf + 0
8.252 * * [simplify]: Extracting #1: cost 12 inf + 0
8.252 * * [simplify]: Extracting #2: cost 64 inf + 1
8.253 * * [simplify]: Extracting #3: cost 140 inf + 403
8.253 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.257 * * [simplify]: Extracting #5: cost 149 inf + 112868
8.271 * * [simplify]: Extracting #6: cost 32 inf + 315911
8.301 * * [simplify]: Extracting #7: cost 1 inf + 362422
8.329 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.357 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.357 * [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.357 * * * * [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.358 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.358 * * [simplify]: iters left: 4 (8 enodes)
8.361 * * [simplify]: iters left: 3 (23 enodes)
8.369 * * [simplify]: iters left: 2 (45 enodes)
8.386 * * [simplify]: iters left: 1 (108 enodes)
8.443 * * [simplify]: Extracting #0: cost 1 inf + 0
8.443 * * [simplify]: Extracting #1: cost 3 inf + 0
8.443 * * [simplify]: Extracting #2: cost 3 inf + 1
8.443 * * [simplify]: Extracting #3: cost 17 inf + 1
8.443 * * [simplify]: Extracting #4: cost 55 inf + 322
8.444 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.450 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.460 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.472 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.485 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.485 * [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.486 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.486 * * [simplify]: iters left: 4 (8 enodes)
8.489 * * [simplify]: iters left: 3 (28 enodes)
8.499 * * [simplify]: iters left: 2 (59 enodes)
8.522 * * [simplify]: iters left: 1 (178 enodes)
8.625 * * [simplify]: Extracting #0: cost 1 inf + 0
8.625 * * [simplify]: Extracting #1: cost 12 inf + 0
8.626 * * [simplify]: Extracting #2: cost 64 inf + 1
8.626 * * [simplify]: Extracting #3: cost 140 inf + 403
8.628 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.635 * * [simplify]: Extracting #5: cost 149 inf + 112868
8.658 * * [simplify]: Extracting #6: cost 32 inf + 315911
8.679 * * [simplify]: Extracting #7: cost 1 inf + 362422
8.693 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.707 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.707 * [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.707 * * * * [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.707 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.707 * * [simplify]: iters left: 4 (8 enodes)
8.711 * * [simplify]: iters left: 3 (23 enodes)
8.715 * * [simplify]: iters left: 2 (45 enodes)
8.722 * * [simplify]: iters left: 1 (108 enodes)
8.762 * * [simplify]: Extracting #0: cost 1 inf + 0
8.762 * * [simplify]: Extracting #1: cost 3 inf + 0
8.762 * * [simplify]: Extracting #2: cost 3 inf + 1
8.762 * * [simplify]: Extracting #3: cost 17 inf + 1
8.762 * * [simplify]: Extracting #4: cost 55 inf + 322
8.763 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.767 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.778 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.791 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.804 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.804 * [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.804 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.805 * * [simplify]: iters left: 4 (8 enodes)
8.808 * * [simplify]: iters left: 3 (28 enodes)
8.818 * * [simplify]: iters left: 2 (59 enodes)
8.843 * * [simplify]: iters left: 1 (178 enodes)
8.944 * * [simplify]: Extracting #0: cost 1 inf + 0
8.944 * * [simplify]: Extracting #1: cost 12 inf + 0
8.945 * * [simplify]: Extracting #2: cost 64 inf + 1
8.945 * * [simplify]: Extracting #3: cost 140 inf + 403
8.947 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.958 * * [simplify]: Extracting #5: cost 149 inf + 112868
8.979 * * [simplify]: Extracting #6: cost 32 inf + 315911
9.001 * * [simplify]: Extracting #7: cost 1 inf + 362422
9.015 * * [simplify]: Extracting #8: cost 0 inf + 365106
9.030 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
9.030 * [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.030 * * * [progress]: adding candidates to table
9.142 * [progress]: [Phase 3 of 3] Extracting.
9.142 * * [regime]: Finding splitpoints for: (#<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 (/.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))> #<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 (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 (-.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 (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 (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))))> #<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))>)
9.153 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
9.154 * * * * [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))) (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 (/.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))> #<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 (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 (-.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 (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 (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))))> #<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))>)
9.311 * * * * [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))) (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 (/.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))> #<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 (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 (-.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 (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 (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))))> #<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))>)
9.420 * * * * [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))) (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 (/.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))> #<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 (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 (-.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 (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 (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))))> #<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))>)
9.544 * * * [regime]: Found split indices: #<option (#s(si 3 256))>
9.544 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
9.544 * * [simplify]: iters left: 5 (9 enodes)
9.544 * * [simplify]: Extracting #0: cost 1 inf + 0
9.544 * * [simplify]: Extracting #1: cost 3 inf + 0
9.544 * * [simplify]: Extracting #2: cost 4 inf + 1
9.544 * * [simplify]: Extracting #3: cost 4 inf + 2
9.545 * * [simplify]: Extracting #4: cost 6 inf + 2
9.545 * * [simplify]: Extracting #5: cost 6 inf + 323
9.545 * * [simplify]: Extracting #6: cost 0 inf + 4258
9.545 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
9.545 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
9.590 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
9.592 * * * * [points]: Setting MPFR precision to 64
9.593 * * * * [points]: Setting MPFR precision to 320
9.594 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
9.595 * * * * [points]: Setting MPFR precision to 64
9.597 * * * * [points]: Setting MPFR precision to 320
9.599 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
9.607 * * * * [points]: Setting MPFR precision to 64
9.614 * * * * [points]: Setting MPFR precision to 320
9.618 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
9.619 * * * * [points]: Setting MPFR precision to 64
9.629 * * * * [points]: Setting MPFR precision to 320
9.644 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
9.646 * * * * [points]: Setting MPFR precision to 64
9.675 * * * * [points]: Setting MPFR precision to 320
9.705 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
9.707 * * * * [points]: Setting MPFR precision to 64
9.765 * * * * [points]: Setting MPFR precision to 320
9.875 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
9.877 * * * * [points]: Setting MPFR precision to 64
9.998 * * * * [points]: Setting MPFR precision to 320
10.160 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
10.162 * * * * [points]: Setting MPFR precision to 64
10.457 * * * * [points]: Setting MPFR precision to 320
10.725 * * * * [points]: Computing exacts for 8000 points
10.727 * * * * [points]: Setting MPFR precision to 64
11.767 * * * * [points]: Setting MPFR precision to 320
13.248 * * * * [points]: Filtering points with unrepresentable outputs
13.328 * * * * [points]: Sampled 8000 points with exact outputs
16.302 * [regime-testing]: Baseline error score: 64.0
16.306 * [regime-testing]: Oracle error score: 64.0
16.312 * [regime-testing]: End program error score: 1.6680361805022776