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.218 * * * * [points]: Setting MPFR precision to 64
0.222 * * * * [points]: Setting MPFR precision to 320
0.224 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.225 * * * * [points]: Setting MPFR precision to 64
0.227 * * * * [points]: Setting MPFR precision to 320
0.229 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.231 * * * * [points]: Setting MPFR precision to 64
0.268 * * * * [points]: Setting MPFR precision to 320
0.273 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.276 * * * * [points]: Setting MPFR precision to 64
0.284 * * * * [points]: Setting MPFR precision to 320
0.292 * * * * [points]: Computing exacts for 256 points
0.294 * * * * [points]: Setting MPFR precision to 64
0.313 * * * * [points]: Setting MPFR precision to 320
0.344 * * * * [points]: Filtering points with unrepresentable outputs
0.346 * * * * [points]: Sampled 256 points with exact outputs
0.347 * * * [progress]: [2/2] Setting up program.
0.364 * [progress]: [Phase 2 of 3] Improving.
0.364 * * * * [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.365 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.366 * * [simplify]: iters left: 5 (10 enodes)
0.372 * * [simplify]: iters left: 4 (25 enodes)
0.377 * * [simplify]: iters left: 3 (48 enodes)
0.388 * * [simplify]: iters left: 2 (111 enodes)
0.617 * * [simplify]: iters left: 1 (392 enodes)
0.976 * * [simplify]: Extracting #0: cost 1 inf + 0
0.977 * * [simplify]: Extracting #1: cost 10 inf + 0
0.977 * * [simplify]: Extracting #2: cost 35 inf + 1
0.978 * * [simplify]: Extracting #3: cost 91 inf + 405
0.980 * * [simplify]: Extracting #4: cost 331 inf + 2291
0.986 * * [simplify]: Extracting #5: cost 455 inf + 80323
1.027 * * [simplify]: Extracting #6: cost 250 inf + 579968
1.090 * * [simplify]: Extracting #7: cost 28 inf + 1003440
1.146 * * [simplify]: Extracting #8: cost 0 inf + 1069311
1.193 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.193 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
1.206 * * [progress]: iteration 1 / 4
1.207 * * * [progress]: picking best candidate
1.211 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1.211 * * * [progress]: localizing error
1.370 * * * [progress]: generating rewritten candidates
1.370 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.375 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1)
1.375 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
1.381 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
1.387 * * * [progress]: generating series expansions
1.388 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.388 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1)
1.388 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
1.388 * * * * [progress]: [ 4 / 4 ] generating series at (2)
1.388 * * * [progress]: simplifying candidates
1.388 * * * * [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.388 * * * * [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.389 * * * * [progress]: [ 3 / 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.389 * * * * [progress]: [ 4 / 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.389 * * * * [progress]: [ 5 / 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.389 * [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.389 * * [simplify]: iters left: 5 (9 enodes)
1.393 * * [simplify]: iters left: 4 (32 enodes)
1.405 * * [simplify]: iters left: 3 (94 enodes)
1.446 * * [simplify]: iters left: 2 (340 enodes)
1.697 * * [simplify]: Extracting #0: cost 1 inf + 0
1.698 * * [simplify]: Extracting #1: cost 50 inf + 0
1.699 * * [simplify]: Extracting #2: cost 240 inf + 0
1.704 * * [simplify]: Extracting #3: cost 355 inf + 61800
1.734 * * [simplify]: Extracting #4: cost 246 inf + 415499
1.774 * * [simplify]: Extracting #5: cost 58 inf + 816216
1.856 * * [simplify]: Extracting #6: cost 1 inf + 911482
1.916 * * [simplify]: Extracting #7: cost 0 inf + 914765
1.965 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1.965 * [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.965 * * * * [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.965 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.965 * * [simplify]: iters left: 5 (9 enodes)
1.967 * * [simplify]: iters left: 4 (29 enodes)
1.976 * * [simplify]: iters left: 3 (62 enodes)
1.993 * * [simplify]: iters left: 2 (199 enodes)
2.087 * * [simplify]: Extracting #0: cost 1 inf + 0
2.087 * * [simplify]: Extracting #1: cost 20 inf + 0
2.087 * * [simplify]: Extracting #2: cost 94 inf + 1
2.088 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.091 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.097 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.115 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.131 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.149 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.149 * [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.149 * * * * [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))>
2.149 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.149 * * [simplify]: iters left: 5 (9 enodes)
2.151 * * [simplify]: iters left: 4 (29 enodes)
2.158 * * [simplify]: iters left: 3 (62 enodes)
2.170 * * [simplify]: iters left: 2 (199 enodes)
2.251 * * [simplify]: Extracting #0: cost 1 inf + 0
2.252 * * [simplify]: Extracting #1: cost 20 inf + 0
2.252 * * [simplify]: Extracting #2: cost 94 inf + 1
2.253 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.255 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.261 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.273 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.288 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.304 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.304 * [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.304 * * * * [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.304 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.304 * * [simplify]: iters left: 5 (9 enodes)
2.306 * * [simplify]: iters left: 4 (29 enodes)
2.311 * * [simplify]: iters left: 3 (62 enodes)
2.324 * * [simplify]: iters left: 2 (199 enodes)
2.442 * * [simplify]: Extracting #0: cost 1 inf + 0
2.442 * * [simplify]: Extracting #1: cost 20 inf + 0
2.442 * * [simplify]: Extracting #2: cost 94 inf + 1
2.443 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.446 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.452 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.469 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.484 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.516 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.516 * [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.516 * * * * [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.516 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.517 * * [simplify]: iters left: 5 (9 enodes)
2.520 * * [simplify]: iters left: 4 (29 enodes)
2.531 * * [simplify]: iters left: 3 (62 enodes)
2.552 * * [simplify]: iters left: 2 (199 enodes)
2.668 * * [simplify]: Extracting #0: cost 1 inf + 0
2.668 * * [simplify]: Extracting #1: cost 20 inf + 0
2.668 * * [simplify]: Extracting #2: cost 94 inf + 1
2.669 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.671 * * [simplify]: Extracting #4: cost 208 inf + 17818
2.678 * * [simplify]: Extracting #5: cost 164 inf + 103714
2.693 * * [simplify]: Extracting #6: cost 47 inf + 336456
2.712 * * [simplify]: Extracting #7: cost 0 inf + 409081
2.742 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.742 * [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.743 * * * [progress]: adding candidates to table
2.917 * * [progress]: iteration 2 / 4
2.917 * * * [progress]: picking best candidate
2.948 * * * * [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.948 * * * [progress]: localizing error
3.198 * * * [progress]: generating rewritten candidates
3.198 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
3.216 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
3.219 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
3.220 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
3.225 * * * [progress]: generating series expansions
3.225 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
3.225 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
3.225 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
3.225 * * * * [progress]: [ 4 / 4 ] generating series at (2)
3.225 * * * [progress]: simplifying candidates
3.225 * * * * [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.226 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
3.226 * * [simplify]: iters left: 2 (6 enodes)
3.228 * * [simplify]: iters left: 1 (14 enodes)
3.232 * * [simplify]: Extracting #0: cost 1 inf + 0
3.232 * * [simplify]: Extracting #1: cost 3 inf + 0
3.232 * * [simplify]: Extracting #2: cost 6 inf + 0
3.233 * * [simplify]: Extracting #3: cost 2 inf + 325
3.233 * * [simplify]: Extracting #4: cost 0 inf + 1329
3.233 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
3.233 * [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.233 * * * * [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.233 * [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.233 * * [simplify]: iters left: 4 (10 enodes)
3.238 * * [simplify]: iters left: 3 (43 enodes)
3.248 * * [simplify]: iters left: 2 (121 enodes)
3.279 * * [simplify]: iters left: 1 (429 enodes)
3.607 * * [simplify]: Extracting #0: cost 1 inf + 0
3.607 * * [simplify]: Extracting #1: cost 46 inf + 0
3.608 * * [simplify]: Extracting #2: cost 270 inf + 0
3.612 * * [simplify]: Extracting #3: cost 354 inf + 59003
3.638 * * [simplify]: Extracting #4: cost 345 inf + 369227
3.725 * * [simplify]: Extracting #5: cost 22 inf + 1102360
3.827 * * [simplify]: Extracting #6: cost 1 inf + 1150488
3.918 * * [simplify]: Extracting #7: cost 0 inf + 1155051
4.020 * [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))))
4.020 * [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))
4.021 * * * * [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))>
4.021 * * * * [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))>
4.021 * * * * [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))))>
4.021 * [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))
4.021 * * [simplify]: iters left: 6 (13 enodes)
4.028 * * [simplify]: iters left: 5 (47 enodes)
4.046 * * [simplify]: iters left: 4 (118 enodes)
4.092 * * [simplify]: iters left: 3 (482 enodes)
4.596 * * [simplify]: Extracting #0: cost 1 inf + 0
4.597 * * [simplify]: Extracting #1: cost 39 inf + 0
4.598 * * [simplify]: Extracting #2: cost 255 inf + 0
4.602 * * [simplify]: Extracting #3: cost 532 inf + 10719
4.626 * * [simplify]: Extracting #4: cost 679 inf + 310118
4.723 * * [simplify]: Extracting #5: cost 214 inf + 1310578
4.882 * * [simplify]: Extracting #6: cost 5 inf + 1763746
5.046 * * [simplify]: Extracting #7: cost 0 inf + 1773035
5.161 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
5.161 * [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.161 * * * * [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.161 * * * * [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.161 * * * * [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.161 * * * * [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.161 * * * [progress]: adding candidates to table
5.280 * * [progress]: iteration 3 / 4
5.280 * * * [progress]: picking best candidate
5.324 * * * * [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.324 * * * [progress]: localizing error
5.635 * * * [progress]: generating rewritten candidates
5.635 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
5.641 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
5.646 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
5.655 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
5.657 * * * [progress]: generating series expansions
5.657 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
5.657 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
5.657 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
5.657 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
5.657 * * * [progress]: simplifying candidates
5.657 * * * * [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.657 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.657 * * [simplify]: iters left: 4 (8 enodes)
5.660 * * [simplify]: iters left: 3 (23 enodes)
5.664 * * [simplify]: iters left: 2 (45 enodes)
5.672 * * [simplify]: iters left: 1 (108 enodes)
5.700 * * [simplify]: Extracting #0: cost 1 inf + 0
5.700 * * [simplify]: Extracting #1: cost 3 inf + 0
5.700 * * [simplify]: Extracting #2: cost 3 inf + 1
5.700 * * [simplify]: Extracting #3: cost 17 inf + 1
5.700 * * [simplify]: Extracting #4: cost 55 inf + 322
5.700 * * [simplify]: Extracting #5: cost 80 inf + 11197
5.702 * * [simplify]: Extracting #6: cost 84 inf + 56173
5.707 * * [simplify]: Extracting #7: cost 7 inf + 177856
5.717 * * [simplify]: Extracting #8: cost 0 inf + 193436
5.723 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.723 * [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.724 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.724 * * [simplify]: iters left: 4 (8 enodes)
5.725 * * [simplify]: iters left: 3 (28 enodes)
5.730 * * [simplify]: iters left: 2 (59 enodes)
5.741 * * [simplify]: iters left: 1 (178 enodes)
5.798 * * [simplify]: Extracting #0: cost 1 inf + 0
5.798 * * [simplify]: Extracting #1: cost 12 inf + 0
5.798 * * [simplify]: Extracting #2: cost 64 inf + 1
5.798 * * [simplify]: Extracting #3: cost 140 inf + 403
5.799 * * [simplify]: Extracting #4: cost 189 inf + 12881
5.803 * * [simplify]: Extracting #5: cost 149 inf + 112868
5.816 * * [simplify]: Extracting #6: cost 32 inf + 315911
5.844 * * [simplify]: Extracting #7: cost 1 inf + 362422
5.872 * * [simplify]: Extracting #8: cost 0 inf + 365106
5.893 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
5.893 * [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.893 * * * * [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.893 * * * * [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.893 * * * * [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.893 * * * * [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.893 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.893 * * [simplify]: iters left: 4 (8 enodes)
5.895 * * [simplify]: iters left: 3 (23 enodes)
5.899 * * [simplify]: iters left: 2 (45 enodes)
5.909 * * [simplify]: iters left: 1 (108 enodes)
5.959 * * [simplify]: Extracting #0: cost 1 inf + 0
5.959 * * [simplify]: Extracting #1: cost 3 inf + 0
5.959 * * [simplify]: Extracting #2: cost 3 inf + 1
5.959 * * [simplify]: Extracting #3: cost 17 inf + 1
5.959 * * [simplify]: Extracting #4: cost 55 inf + 322
5.960 * * [simplify]: Extracting #5: cost 80 inf + 11197
5.964 * * [simplify]: Extracting #6: cost 84 inf + 56173
5.973 * * [simplify]: Extracting #7: cost 7 inf + 177856
5.986 * * [simplify]: Extracting #8: cost 0 inf + 193436
6.000 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
6.000 * [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.000 * * * * [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.000 * [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.001 * * [simplify]: iters left: 6 (11 enodes)
6.005 * * [simplify]: iters left: 5 (43 enodes)
6.023 * * [simplify]: iters left: 4 (139 enodes)
6.080 * * [simplify]: Extracting #0: cost 1 inf + 0
6.080 * * [simplify]: Extracting #1: cost 32 inf + 0
6.081 * * [simplify]: Extracting #2: cost 85 inf + 0
6.081 * * [simplify]: Extracting #3: cost 152 inf + 1364
6.082 * * [simplify]: Extracting #4: cost 163 inf + 24483
6.088 * * [simplify]: Extracting #5: cost 71 inf + 172897
6.098 * * [simplify]: Extracting #6: cost 3 inf + 277964
6.118 * * [simplify]: Extracting #7: cost 0 inf + 284573
6.140 * [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.140 * [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.141 * * * * [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.141 * * * * [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.141 * * * * [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.141 * * * * [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.141 * * * [progress]: adding candidates to table
6.327 * * [progress]: iteration 4 / 4
6.327 * * * [progress]: picking best candidate
6.392 * * * * [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.392 * * * [progress]: localizing error
6.632 * * * [progress]: generating rewritten candidates
6.632 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
6.637 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
6.642 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
6.645 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
6.654 * * * [progress]: generating series expansions
6.654 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
6.654 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
6.654 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
6.654 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
6.654 * * * [progress]: simplifying candidates
6.654 * * * * [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.654 * * * * [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.654 * * * * [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.655 * * * * [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.655 * * * * [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.655 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.655 * * [simplify]: iters left: 4 (8 enodes)
6.658 * * [simplify]: iters left: 3 (23 enodes)
6.665 * * [simplify]: iters left: 2 (45 enodes)
6.681 * * [simplify]: iters left: 1 (108 enodes)
6.733 * * [simplify]: Extracting #0: cost 1 inf + 0
6.733 * * [simplify]: Extracting #1: cost 3 inf + 0
6.733 * * [simplify]: Extracting #2: cost 3 inf + 1
6.733 * * [simplify]: Extracting #3: cost 17 inf + 1
6.733 * * [simplify]: Extracting #4: cost 55 inf + 322
6.734 * * [simplify]: Extracting #5: cost 80 inf + 11197
6.741 * * [simplify]: Extracting #6: cost 84 inf + 56173
6.751 * * [simplify]: Extracting #7: cost 7 inf + 177856
6.764 * * [simplify]: Extracting #8: cost 0 inf + 193436
6.776 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
6.777 * [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.777 * * * * [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.777 * [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.777 * * [simplify]: iters left: 6 (11 enodes)
6.782 * * [simplify]: iters left: 5 (35 enodes)
6.794 * * [simplify]: iters left: 4 (111 enodes)
6.832 * * [simplify]: iters left: 3 (448 enodes)
7.233 * * [simplify]: Extracting #0: cost 1 inf + 0
7.233 * * [simplify]: Extracting #1: cost 64 inf + 0
7.234 * * [simplify]: Extracting #2: cost 370 inf + 0
7.236 * * [simplify]: Extracting #3: cost 522 inf + 6695
7.246 * * [simplify]: Extracting #4: cost 536 inf + 237314
7.309 * * [simplify]: Extracting #5: cost 132 inf + 950329
7.414 * * [simplify]: Extracting #6: cost 26 inf + 1188087
7.496 * * [simplify]: Extracting #7: cost 0 inf + 1213652
7.607 * * [simplify]: Extracting #8: cost 0 inf + 1213496
7.690 * [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.690 * [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.690 * * * * [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.691 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.691 * * [simplify]: iters left: 4 (8 enodes)
7.692 * * [simplify]: iters left: 3 (23 enodes)
7.696 * * [simplify]: iters left: 2 (45 enodes)
7.704 * * [simplify]: iters left: 1 (108 enodes)
7.744 * * [simplify]: Extracting #0: cost 1 inf + 0
7.744 * * [simplify]: Extracting #1: cost 3 inf + 0
7.744 * * [simplify]: Extracting #2: cost 3 inf + 1
7.745 * * [simplify]: Extracting #3: cost 17 inf + 1
7.745 * * [simplify]: Extracting #4: cost 55 inf + 322
7.746 * * [simplify]: Extracting #5: cost 80 inf + 11197
7.749 * * [simplify]: Extracting #6: cost 84 inf + 56173
7.759 * * [simplify]: Extracting #7: cost 7 inf + 177856
7.772 * * [simplify]: Extracting #8: cost 0 inf + 193436
7.783 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
7.783 * [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.783 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.783 * * [simplify]: iters left: 4 (8 enodes)
7.785 * * [simplify]: iters left: 3 (28 enodes)
7.790 * * [simplify]: iters left: 2 (59 enodes)
7.801 * * [simplify]: iters left: 1 (178 enodes)
7.906 * * [simplify]: Extracting #0: cost 1 inf + 0
7.906 * * [simplify]: Extracting #1: cost 12 inf + 0
7.907 * * [simplify]: Extracting #2: cost 64 inf + 1
7.907 * * [simplify]: Extracting #3: cost 140 inf + 403
7.909 * * [simplify]: Extracting #4: cost 189 inf + 12881
7.912 * * [simplify]: Extracting #5: cost 149 inf + 112868
7.924 * * [simplify]: Extracting #6: cost 32 inf + 315911
7.943 * * [simplify]: Extracting #7: cost 1 inf + 362422
7.971 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.000 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.000 * [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.000 * * * * [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.001 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.001 * * [simplify]: iters left: 4 (8 enodes)
8.005 * * [simplify]: iters left: 3 (23 enodes)
8.013 * * [simplify]: iters left: 2 (45 enodes)
8.030 * * [simplify]: iters left: 1 (108 enodes)
8.086 * * [simplify]: Extracting #0: cost 1 inf + 0
8.086 * * [simplify]: Extracting #1: cost 3 inf + 0
8.086 * * [simplify]: Extracting #2: cost 3 inf + 1
8.086 * * [simplify]: Extracting #3: cost 17 inf + 1
8.086 * * [simplify]: Extracting #4: cost 55 inf + 322
8.087 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.090 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.096 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.102 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.108 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.108 * [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.109 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.109 * * [simplify]: iters left: 4 (8 enodes)
8.110 * * [simplify]: iters left: 3 (28 enodes)
8.115 * * [simplify]: iters left: 2 (59 enodes)
8.136 * * [simplify]: iters left: 1 (178 enodes)
8.217 * * [simplify]: Extracting #0: cost 1 inf + 0
8.217 * * [simplify]: Extracting #1: cost 12 inf + 0
8.217 * * [simplify]: Extracting #2: cost 64 inf + 1
8.217 * * [simplify]: Extracting #3: cost 140 inf + 403
8.218 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.222 * * [simplify]: Extracting #5: cost 149 inf + 112868
8.233 * * [simplify]: Extracting #6: cost 32 inf + 315911
8.247 * * [simplify]: Extracting #7: cost 1 inf + 362422
8.262 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.278 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.278 * [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.279 * * * * [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.279 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.279 * * [simplify]: iters left: 4 (8 enodes)
8.280 * * [simplify]: iters left: 3 (23 enodes)
8.284 * * [simplify]: iters left: 2 (45 enodes)
8.292 * * [simplify]: iters left: 1 (108 enodes)
8.319 * * [simplify]: Extracting #0: cost 1 inf + 0
8.319 * * [simplify]: Extracting #1: cost 3 inf + 0
8.319 * * [simplify]: Extracting #2: cost 3 inf + 1
8.319 * * [simplify]: Extracting #3: cost 17 inf + 1
8.319 * * [simplify]: Extracting #4: cost 55 inf + 322
8.319 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.321 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.326 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.333 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.339 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.339 * [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.340 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.340 * * [simplify]: iters left: 4 (8 enodes)
8.341 * * [simplify]: iters left: 3 (28 enodes)
8.346 * * [simplify]: iters left: 2 (59 enodes)
8.357 * * [simplify]: iters left: 1 (178 enodes)
8.414 * * [simplify]: Extracting #0: cost 1 inf + 0
8.414 * * [simplify]: Extracting #1: cost 12 inf + 0
8.414 * * [simplify]: Extracting #2: cost 64 inf + 1
8.414 * * [simplify]: Extracting #3: cost 140 inf + 403
8.415 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.423 * * [simplify]: Extracting #5: cost 149 inf + 112868
8.434 * * [simplify]: Extracting #6: cost 32 inf + 315911
8.448 * * [simplify]: Extracting #7: cost 1 inf + 362422
8.462 * * [simplify]: Extracting #8: cost 0 inf + 365106
8.477 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.477 * [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.477 * * * * [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.477 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.477 * * [simplify]: iters left: 4 (8 enodes)
8.479 * * [simplify]: iters left: 3 (23 enodes)
8.482 * * [simplify]: iters left: 2 (45 enodes)
8.491 * * [simplify]: iters left: 1 (108 enodes)
8.834 * * [simplify]: Extracting #0: cost 1 inf + 0
8.834 * * [simplify]: Extracting #1: cost 3 inf + 0
8.834 * * [simplify]: Extracting #2: cost 3 inf + 1
8.834 * * [simplify]: Extracting #3: cost 17 inf + 1
8.834 * * [simplify]: Extracting #4: cost 55 inf + 322
8.835 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.838 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.848 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.861 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.874 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.874 * [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.875 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.875 * * [simplify]: iters left: 4 (8 enodes)
8.879 * * [simplify]: iters left: 3 (28 enodes)
8.890 * * [simplify]: iters left: 2 (59 enodes)
8.902 * * [simplify]: iters left: 1 (178 enodes)
8.975 * * [simplify]: Extracting #0: cost 1 inf + 0
8.975 * * [simplify]: Extracting #1: cost 12 inf + 0
8.975 * * [simplify]: Extracting #2: cost 64 inf + 1
8.976 * * [simplify]: Extracting #3: cost 140 inf + 403
8.978 * * [simplify]: Extracting #4: cost 189 inf + 12881
8.985 * * [simplify]: Extracting #5: cost 149 inf + 112868
9.007 * * [simplify]: Extracting #6: cost 32 inf + 315911
9.039 * * [simplify]: Extracting #7: cost 1 inf + 362422
9.069 * * [simplify]: Extracting #8: cost 0 inf + 365106
9.083 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
9.083 * [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.083 * * * [progress]: adding candidates to table
9.213 * [progress]: [Phase 3 of 3] Extracting.
9.213 * * [regime]: Finding splitpoints for: (#<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 (*.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))) (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 (*.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))) 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 (*.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 (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))))> #<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))>)
9.217 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
9.218 * * * * [regimes]: Trying to branch on c from (#<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 (*.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))) (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 (*.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))) 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 (*.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 (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))))> #<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))>)
9.316 * * * * [regimes]: Trying to branch on a from (#<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 (*.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))) (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 (*.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))) 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 (*.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 (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))))> #<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))>)
9.427 * * * * [regimes]: Trying to branch on b_2 from (#<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 (*.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))) (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 (*.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))) 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 (*.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 (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))))> #<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))>)
9.522 * * * [regime]: Found split indices: #<option (#s(si 0 256))>
9.522 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
9.522 * * [simplify]: iters left: 5 (9 enodes)
9.522 * * [simplify]: Extracting #0: cost 1 inf + 0
9.522 * * [simplify]: Extracting #1: cost 3 inf + 0
9.523 * * [simplify]: Extracting #2: cost 4 inf + 1
9.523 * * [simplify]: Extracting #3: cost 4 inf + 2
9.523 * * [simplify]: Extracting #4: cost 6 inf + 2
9.523 * * [simplify]: Extracting #5: cost 6 inf + 323
9.523 * * [simplify]: Extracting #6: cost 0 inf + 4258
9.523 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
9.523 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
9.559 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
9.560 * * * * [points]: Setting MPFR precision to 64
9.561 * * * * [points]: Setting MPFR precision to 320
9.562 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
9.564 * * * * [points]: Setting MPFR precision to 64
9.566 * * * * [points]: Setting MPFR precision to 320
9.568 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
9.569 * * * * [points]: Setting MPFR precision to 64
9.573 * * * * [points]: Setting MPFR precision to 320
9.579 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
9.580 * * * * [points]: Setting MPFR precision to 64
9.588 * * * * [points]: Setting MPFR precision to 320
9.597 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
9.598 * * * * [points]: Setting MPFR precision to 64
9.614 * * * * [points]: Setting MPFR precision to 320
9.630 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
9.631 * * * * [points]: Setting MPFR precision to 64
9.711 * * * * [points]: Setting MPFR precision to 320
9.771 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
9.773 * * * * [points]: Setting MPFR precision to 64
9.933 * * * * [points]: Setting MPFR precision to 320
10.064 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
10.067 * * * * [points]: Setting MPFR precision to 64
10.340 * * * * [points]: Setting MPFR precision to 320
10.634 * * * * [points]: Computing exacts for 8000 points
10.637 * * * * [points]: Setting MPFR precision to 64
11.828 * * * * [points]: Setting MPFR precision to 320
13.025 * * * * [points]: Filtering points with unrepresentable outputs
13.044 * * * * [points]: Sampled 8000 points with exact outputs
15.934 * [regime-testing]: Baseline error score: 64.0
15.940 * [regime-testing]: Oracle error score: 64.0
15.955 * [regime-testing]: End program error score: 1.6520420666006903