0.002 * [progress]: [Phase 1 of 3] Setting up.
0.037 * * * [progress]: [1/2] Preparing points
0.040 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.043 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.237 * * * * [points]: Setting MPFR precision to 64
0.242 * * * * [points]: Setting MPFR precision to 320
0.244 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.247 * * * * [points]: Setting MPFR precision to 64
0.252 * * * * [points]: Setting MPFR precision to 320
0.256 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.258 * * * * [points]: Setting MPFR precision to 64
0.264 * * * * [points]: Setting MPFR precision to 320
0.271 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.273 * * * * [points]: Setting MPFR precision to 64
0.283 * * * * [points]: Setting MPFR precision to 320
0.293 * * * * [points]: Computing exacts for 256 points
0.295 * * * * [points]: Setting MPFR precision to 64
0.327 * * * * [points]: Setting MPFR precision to 320
0.359 * * * * [points]: Filtering points with unrepresentable outputs
0.361 * * * * [points]: Sampled 256 points with exact outputs
0.361 * * * [progress]: [2/2] Setting up program.
0.384 * [progress]: [Phase 2 of 3] Improving.
0.384 * * * * [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.386 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.388 * * [simplify]: iters left: 5 (10 enodes)
0.449 * * [simplify]: iters left: 4 (25 enodes)
0.460 * * [simplify]: iters left: 3 (48 enodes)
0.480 * * [simplify]: iters left: 2 (111 enodes)
0.535 * * [simplify]: iters left: 1 (394 enodes)
0.925 * * [simplify]: Extracting #0: cost 1 inf + 0
0.926 * * [simplify]: Extracting #1: cost 10 inf + 0
0.926 * * [simplify]: Extracting #2: cost 35 inf + 1
0.927 * * [simplify]: Extracting #3: cost 92 inf + 83
0.929 * * [simplify]: Extracting #4: cost 333 inf + 1810
0.933 * * [simplify]: Extracting #5: cost 518 inf + 5618
0.947 * * [simplify]: Extracting #6: cost 470 inf + 184191
1.008 * * [simplify]: Extracting #7: cost 61 inf + 918877
1.081 * * [simplify]: Extracting #8: cost 0 inf + 1055660
1.140 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.140 * [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.160 * * [progress]: iteration 1 / 4
1.160 * * * [progress]: picking best candidate
1.169 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1.169 * * * [progress]: localizing error
1.377 * * * [progress]: generating rewritten candidates
1.377 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.384 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
1.390 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
1.390 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1.397 * * * [progress]: generating series expansions
1.397 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.398 * * * * [progress]: [ 2 / 4 ] generating series at (2)
1.398 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
1.398 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1.398 * * * [progress]: simplifying candidates
1.398 * * * * [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.398 * [simplify]: Simplifying (neg.p16 b_2)
1.399 * * [simplify]: iters left: 1 (2 enodes)
1.399 * * [simplify]: Extracting #0: cost 1 inf + 0
1.399 * * [simplify]: Extracting #1: cost 2 inf + 0
1.399 * * [simplify]: Extracting #2: cost 1 inf + 1
1.400 * * [simplify]: Extracting #3: cost 0 inf + 82
1.400 * [simplify]: Simplified to (neg.p16 b_2)
1.400 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2)) a))
1.400 * * * * [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.400 * [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.400 * * [simplify]: iters left: 5 (9 enodes)
1.404 * * [simplify]: iters left: 4 (32 enodes)
1.416 * * [simplify]: iters left: 3 (94 enodes)
1.450 * * [simplify]: iters left: 2 (340 enodes)
1.653 * * [simplify]: Extracting #0: cost 1 inf + 0
1.654 * * [simplify]: Extracting #1: cost 50 inf + 0
1.655 * * [simplify]: Extracting #2: cost 240 inf + 0
1.660 * * [simplify]: Extracting #3: cost 363 inf + 51025
1.686 * * [simplify]: Extracting #4: cost 279 inf + 363866
1.747 * * [simplify]: Extracting #5: cost 63 inf + 808744
1.801 * * [simplify]: Extracting #6: cost 1 inf + 916546
1.852 * * [simplify]: Extracting #7: cost 0 inf + 919829
1.892 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1.893 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1.893 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1.893 * * [simplify]: iters left: 4 (8 enodes)
1.895 * * [simplify]: iters left: 3 (23 enodes)
1.898 * * [simplify]: iters left: 2 (45 enodes)
1.912 * * [simplify]: iters left: 1 (108 enodes)
1.942 * * [simplify]: Extracting #0: cost 1 inf + 0
1.942 * * [simplify]: Extracting #1: cost 3 inf + 0
1.942 * * [simplify]: Extracting #2: cost 3 inf + 1
1.942 * * [simplify]: Extracting #3: cost 17 inf + 1
1.943 * * [simplify]: Extracting #4: cost 55 inf + 322
1.943 * * [simplify]: Extracting #5: cost 80 inf + 11197
1.946 * * [simplify]: Extracting #6: cost 84 inf + 56173
1.951 * * [simplify]: Extracting #7: cost 7 inf + 177856
1.957 * * [simplify]: Extracting #8: cost 0 inf + 193436
1.964 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1.964 * [simplify]: Simplified (2 1 2) to (λ (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 a c))))) a))
1.964 * * * * [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.964 * [simplify]: Simplifying (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
1.965 * * [simplify]: iters left: 5 (9 enodes)
1.967 * * [simplify]: iters left: 4 (31 enodes)
1.972 * * [simplify]: iters left: 3 (55 enodes)
1.987 * * [simplify]: iters left: 2 (114 enodes)
2.041 * * [simplify]: iters left: 1 (406 enodes)
2.386 * * [simplify]: Extracting #0: cost 1 inf + 0
2.386 * * [simplify]: Extracting #1: cost 5 inf + 0
2.386 * * [simplify]: Extracting #2: cost 6 inf + 1
2.386 * * [simplify]: Extracting #3: cost 5 inf + 324
2.386 * * [simplify]: Extracting #4: cost 51 inf + 324
2.393 * * [simplify]: Extracting #5: cost 257 inf + 645
2.397 * * [simplify]: Extracting #6: cost 464 inf + 11760
2.411 * * [simplify]: Extracting #7: cost 370 inf + 309548
2.453 * * [simplify]: Extracting #8: cost 43 inf + 972742
2.523 * * [simplify]: Extracting #9: cost 0 inf + 1034433
2.595 * * [simplify]: Extracting #10: cost 0 inf + 1033793
2.664 * [simplify]: Simplified to (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
2.664 * [simplify]: Simplified (2 2) to (λ (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 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)))
2.664 * * * * [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))>
2.664 * [simplify]: Simplifying (neg.p16 (*.p16 c a))
2.664 * * [simplify]: iters left: 2 (4 enodes)
2.665 * * [simplify]: iters left: 1 (9 enodes)
2.666 * * [simplify]: Extracting #0: cost 1 inf + 0
2.666 * * [simplify]: Extracting #1: cost 2 inf + 0
2.666 * * [simplify]: Extracting #2: cost 4 inf + 0
2.666 * * [simplify]: Extracting #3: cost 2 inf + 2
2.666 * * [simplify]: Extracting #4: cost 0 inf + 726
2.666 * [simplify]: Simplified to (neg.p16 (*.p16 a c))
2.666 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c)))) b_2) a))
2.666 * * * * [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))>
2.667 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
2.667 * * [simplify]: iters left: 3 (8 enodes)
2.669 * * [simplify]: iters left: 2 (33 enodes)
2.676 * * [simplify]: iters left: 1 (79 enodes)
2.709 * * [simplify]: Extracting #0: cost 1 inf + 0
2.709 * * [simplify]: Extracting #1: cost 21 inf + 0
2.709 * * [simplify]: Extracting #2: cost 51 inf + 0
2.710 * * [simplify]: Extracting #3: cost 77 inf + 5301
2.713 * * [simplify]: Extracting #4: cost 37 inf + 63309
2.720 * * [simplify]: Extracting #5: cost 2 inf + 116709
2.728 * * [simplify]: Extracting #6: cost 0 inf + 120953
2.736 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
2.736 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
2.736 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
2.736 * * [simplify]: iters left: 2 (6 enodes)
2.739 * * [simplify]: iters left: 1 (14 enodes)
2.742 * * [simplify]: Extracting #0: cost 1 inf + 0
2.742 * * [simplify]: Extracting #1: cost 3 inf + 0
2.742 * * [simplify]: Extracting #2: cost 6 inf + 0
2.742 * * [simplify]: Extracting #3: cost 2 inf + 325
2.742 * * [simplify]: Extracting #4: cost 0 inf + 1329
2.742 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
2.742 * [simplify]: Simplified (2 1 1 1 2) to (λ (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 a c) (*.p16 b_2 b_2)))) b_2) a))
2.742 * * * * [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))>
2.742 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.742 * * [simplify]: iters left: 5 (9 enodes)
2.744 * * [simplify]: iters left: 4 (29 enodes)
2.749 * * [simplify]: iters left: 3 (62 enodes)
2.762 * * [simplify]: iters left: 2 (199 enodes)
2.834 * * [simplify]: Extracting #0: cost 1 inf + 0
2.834 * * [simplify]: Extracting #1: cost 20 inf + 0
2.835 * * [simplify]: Extracting #2: cost 94 inf + 1
2.835 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.838 * * [simplify]: Extracting #4: cost 205 inf + 21625
2.844 * * [simplify]: Extracting #5: cost 170 inf + 98466
2.864 * * [simplify]: Extracting #6: cost 65 inf + 303687
2.888 * * [simplify]: Extracting #7: cost 1 inf + 408042
2.903 * * [simplify]: Extracting #8: cost 0 inf + 411325
2.932 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.932 * [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.932 * * * * [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.933 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.933 * * [simplify]: iters left: 5 (9 enodes)
2.937 * * [simplify]: iters left: 4 (29 enodes)
2.944 * * [simplify]: iters left: 3 (62 enodes)
2.955 * * [simplify]: iters left: 2 (199 enodes)
3.038 * * [simplify]: Extracting #0: cost 1 inf + 0
3.038 * * [simplify]: Extracting #1: cost 20 inf + 0
3.039 * * [simplify]: Extracting #2: cost 94 inf + 1
3.040 * * [simplify]: Extracting #3: cost 162 inf + 1046
3.042 * * [simplify]: Extracting #4: cost 205 inf + 21625
3.048 * * [simplify]: Extracting #5: cost 170 inf + 98466
3.069 * * [simplify]: Extracting #6: cost 65 inf + 303687
3.097 * * [simplify]: Extracting #7: cost 1 inf + 408042
3.116 * * [simplify]: Extracting #8: cost 0 inf + 411325
3.146 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
3.146 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
3.146 * * * * [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))>
3.146 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
3.147 * * [simplify]: iters left: 5 (9 enodes)
3.150 * * [simplify]: iters left: 4 (29 enodes)
3.160 * * [simplify]: iters left: 3 (62 enodes)
3.184 * * [simplify]: iters left: 2 (199 enodes)
3.269 * * [simplify]: Extracting #0: cost 1 inf + 0
3.270 * * [simplify]: Extracting #1: cost 20 inf + 0
3.270 * * [simplify]: Extracting #2: cost 94 inf + 1
3.271 * * [simplify]: Extracting #3: cost 162 inf + 1046
3.273 * * [simplify]: Extracting #4: cost 205 inf + 21625
3.280 * * [simplify]: Extracting #5: cost 170 inf + 98466
3.291 * * [simplify]: Extracting #6: cost 65 inf + 303687
3.306 * * [simplify]: Extracting #7: cost 1 inf + 408042
3.331 * * [simplify]: Extracting #8: cost 0 inf + 411325
3.347 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
3.347 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
3.347 * * * * [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))>
3.347 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
3.347 * * [simplify]: iters left: 5 (9 enodes)
3.349 * * [simplify]: iters left: 4 (29 enodes)
3.354 * * [simplify]: iters left: 3 (62 enodes)
3.378 * * [simplify]: iters left: 2 (199 enodes)
3.467 * * [simplify]: Extracting #0: cost 1 inf + 0
3.467 * * [simplify]: Extracting #1: cost 20 inf + 0
3.468 * * [simplify]: Extracting #2: cost 94 inf + 1
3.468 * * [simplify]: Extracting #3: cost 162 inf + 1046
3.470 * * [simplify]: Extracting #4: cost 205 inf + 21625
3.477 * * [simplify]: Extracting #5: cost 170 inf + 98466
3.498 * * [simplify]: Extracting #6: cost 65 inf + 303687
3.518 * * [simplify]: Extracting #7: cost 1 inf + 408042
3.537 * * [simplify]: Extracting #8: cost 0 inf + 411325
3.553 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
3.553 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
3.553 * * * [progress]: adding candidates to table
3.674 * * [progress]: iteration 2 / 4
3.674 * * * [progress]: picking best candidate
3.689 * * * * [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))>
3.689 * * * [progress]: localizing error
3.878 * * * [progress]: generating rewritten candidates
3.878 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
3.886 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
3.887 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
3.890 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
3.890 * * * [progress]: generating series expansions
3.890 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
3.890 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
3.890 * * * * [progress]: [ 3 / 4 ] generating series at (2)
3.891 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
3.891 * * * [progress]: simplifying candidates
3.891 * * * * [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.891 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))
3.891 * * [simplify]: iters left: 3 (8 enodes)
3.893 * * [simplify]: iters left: 2 (22 enodes)
3.899 * * [simplify]: iters left: 1 (45 enodes)
3.916 * * [simplify]: Extracting #0: cost 1 inf + 0
3.916 * * [simplify]: Extracting #1: cost 10 inf + 0
3.916 * * [simplify]: Extracting #2: cost 26 inf + 0
3.916 * * [simplify]: Extracting #3: cost 37 inf + 0
3.916 * * [simplify]: Extracting #4: cost 47 inf + 2734
3.918 * * [simplify]: Extracting #5: cost 18 inf + 30834
3.921 * * [simplify]: Extracting #6: cost 0 inf + 59476
3.924 * * [simplify]: Extracting #7: cost 0 inf + 58996
3.928 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
3.928 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (/.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) b_2) a))
3.928 * * * * [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.928 * [simplify]: Simplifying (*.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))))
3.928 * * [simplify]: iters left: 4 (10 enodes)
3.934 * * [simplify]: iters left: 3 (34 enodes)
3.947 * * [simplify]: iters left: 2 (91 enodes)
3.979 * * [simplify]: iters left: 1 (280 enodes)
4.169 * * [simplify]: Extracting #0: cost 1 inf + 0
4.170 * * [simplify]: Extracting #1: cost 20 inf + 0
4.171 * * [simplify]: Extracting #2: cost 96 inf + 0
4.175 * * [simplify]: Extracting #3: cost 106 inf + 12956
4.185 * * [simplify]: Extracting #4: cost 19 inf + 129586
4.197 * * [simplify]: Extracting #5: cost 0 inf + 160920
4.204 * * [simplify]: Extracting #6: cost 0 inf + 159960
4.211 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))
4.211 * [simplify]: Simplified (2 1 1 1 2) 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 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 a c) (*.p16 b_2 b_2)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c)))))) b_2) a))
4.211 * * * * [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.211 * [simplify]: Simplifying (neg.p16 b_2)
4.211 * * [simplify]: iters left: 1 (2 enodes)
4.212 * * [simplify]: Extracting #0: cost 1 inf + 0
4.212 * * [simplify]: Extracting #1: cost 2 inf + 0
4.212 * * [simplify]: Extracting #2: cost 1 inf + 1
4.212 * * [simplify]: Extracting #3: cost 0 inf + 82
4.212 * [simplify]: Simplified to (neg.p16 b_2)
4.212 * [simplify]: Simplified (2 1 2) to (λ (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.212 * * * * [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.212 * [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.212 * * [simplify]: iters left: 6 (13 enodes)
4.215 * * [simplify]: iters left: 5 (47 enodes)
4.224 * * [simplify]: iters left: 4 (118 enodes)
4.264 * * [simplify]: iters left: 3 (482 enodes)
4.774 * * [simplify]: Extracting #0: cost 1 inf + 0
4.775 * * [simplify]: Extracting #1: cost 47 inf + 0
4.776 * * [simplify]: Extracting #2: cost 266 inf + 0
4.780 * * [simplify]: Extracting #3: cost 536 inf + 28392
4.800 * * [simplify]: Extracting #4: cost 646 inf + 405570
4.878 * * [simplify]: Extracting #5: cost 179 inf + 1412113
4.986 * * [simplify]: Extracting #6: cost 2 inf + 1774901
5.140 * * [simplify]: Extracting #7: cost 0 inf + 1777784
5.274 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
5.274 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.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))
5.275 * [simplify]: Simplifying (+.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.275 * * [simplify]: iters left: 6 (12 enodes)
5.281 * * [simplify]: iters left: 5 (38 enodes)
5.295 * * [simplify]: iters left: 4 (86 enodes)
5.331 * * [simplify]: iters left: 3 (285 enodes)
5.569 * * [simplify]: Extracting #0: cost 1 inf + 0
5.569 * * [simplify]: Extracting #1: cost 3 inf + 0
5.569 * * [simplify]: Extracting #2: cost 3 inf + 1
5.569 * * [simplify]: Extracting #3: cost 60 inf + 1
5.569 * * [simplify]: Extracting #4: cost 225 inf + 322
5.571 * * [simplify]: Extracting #5: cost 353 inf + 24300
5.581 * * [simplify]: Extracting #6: cost 198 inf + 338281
5.615 * * [simplify]: Extracting #7: cost 14 inf + 719955
5.662 * * [simplify]: Extracting #8: cost 0 inf + 754556
5.700 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.701 * [simplify]: Simplified (2 1 2) to (λ (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 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
5.701 * * * * [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))))>
5.701 * [simplify]: Simplifying (*.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.701 * * [simplify]: iters left: 6 (13 enodes)
5.707 * * [simplify]: iters left: 5 (46 enodes)
5.724 * * [simplify]: iters left: 4 (94 enodes)
5.746 * * [simplify]: iters left: 3 (279 enodes)
5.972 * * [simplify]: Extracting #0: cost 1 inf + 0
5.972 * * [simplify]: Extracting #1: cost 5 inf + 0
5.972 * * [simplify]: Extracting #2: cost 6 inf + 1
5.972 * * [simplify]: Extracting #3: cost 5 inf + 324
5.972 * * [simplify]: Extracting #4: cost 62 inf + 324
5.973 * * [simplify]: Extracting #5: cost 227 inf + 645
5.976 * * [simplify]: Extracting #6: cost 373 inf + 17528
5.992 * * [simplify]: Extracting #7: cost 255 inf + 233381
6.032 * * [simplify]: Extracting #8: cost 42 inf + 659523
6.064 * * [simplify]: Extracting #9: cost 1 inf + 762007
6.113 * * [simplify]: Extracting #10: cost 0 inf + 765050
6.179 * [simplify]: Simplified to (*.p16 a (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
6.179 * [simplify]: Simplified (2 2) to (λ (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 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))
6.180 * * * * [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))>
6.180 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
6.180 * * [simplify]: iters left: 3 (8 enodes)
6.184 * * [simplify]: iters left: 2 (33 enodes)
6.196 * * [simplify]: iters left: 1 (79 enodes)
6.230 * * [simplify]: Extracting #0: cost 1 inf + 0
6.230 * * [simplify]: Extracting #1: cost 21 inf + 0
6.230 * * [simplify]: Extracting #2: cost 51 inf + 0
6.231 * * [simplify]: Extracting #3: cost 77 inf + 5301
6.234 * * [simplify]: Extracting #4: cost 37 inf + 63309
6.241 * * [simplify]: Extracting #5: cost 2 inf + 116709
6.248 * * [simplify]: Extracting #6: cost 0 inf + 120953
6.256 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
6.256 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
6.256 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
6.257 * * [simplify]: iters left: 2 (6 enodes)
6.259 * * [simplify]: iters left: 1 (14 enodes)
6.263 * * [simplify]: Extracting #0: cost 1 inf + 0
6.263 * * [simplify]: Extracting #1: cost 3 inf + 0
6.263 * * [simplify]: Extracting #2: cost 6 inf + 0
6.263 * * [simplify]: Extracting #3: cost 2 inf + 325
6.263 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.264 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
6.264 * [simplify]: Simplified (2 1 1 1 2) to (λ (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 a c) (*.p16 b_2 b_2)))) b_2) a))
6.264 * * * * [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))>
6.264 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
6.264 * * [simplify]: iters left: 3 (8 enodes)
6.268 * * [simplify]: iters left: 2 (33 enodes)
6.280 * * [simplify]: iters left: 1 (79 enodes)
6.313 * * [simplify]: Extracting #0: cost 1 inf + 0
6.314 * * [simplify]: Extracting #1: cost 21 inf + 0
6.314 * * [simplify]: Extracting #2: cost 51 inf + 0
6.314 * * [simplify]: Extracting #3: cost 77 inf + 5301
6.319 * * [simplify]: Extracting #4: cost 37 inf + 63309
6.326 * * [simplify]: Extracting #5: cost 2 inf + 116709
6.333 * * [simplify]: Extracting #6: cost 0 inf + 120953
6.340 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
6.340 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
6.341 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
6.341 * * [simplify]: iters left: 2 (6 enodes)
6.342 * * [simplify]: iters left: 1 (14 enodes)
6.344 * * [simplify]: Extracting #0: cost 1 inf + 0
6.344 * * [simplify]: Extracting #1: cost 3 inf + 0
6.344 * * [simplify]: Extracting #2: cost 6 inf + 0
6.344 * * [simplify]: Extracting #3: cost 2 inf + 325
6.344 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.344 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
6.344 * [simplify]: Simplified (2 1 1 1 2) to (λ (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 a c) (*.p16 b_2 b_2)))) b_2) a))
6.344 * * * * [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))>
6.344 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
6.344 * * [simplify]: iters left: 3 (8 enodes)
6.346 * * [simplify]: iters left: 2 (33 enodes)
6.352 * * [simplify]: iters left: 1 (79 enodes)
6.369 * * [simplify]: Extracting #0: cost 1 inf + 0
6.369 * * [simplify]: Extracting #1: cost 21 inf + 0
6.369 * * [simplify]: Extracting #2: cost 51 inf + 0
6.370 * * [simplify]: Extracting #3: cost 77 inf + 5301
6.371 * * [simplify]: Extracting #4: cost 37 inf + 63309
6.375 * * [simplify]: Extracting #5: cost 2 inf + 116709
6.378 * * [simplify]: Extracting #6: cost 0 inf + 120953
6.382 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
6.382 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
6.382 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
6.382 * * [simplify]: iters left: 2 (6 enodes)
6.383 * * [simplify]: iters left: 1 (14 enodes)
6.385 * * [simplify]: Extracting #0: cost 1 inf + 0
6.385 * * [simplify]: Extracting #1: cost 3 inf + 0
6.385 * * [simplify]: Extracting #2: cost 6 inf + 0
6.385 * * [simplify]: Extracting #3: cost 2 inf + 325
6.385 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.385 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
6.385 * [simplify]: Simplified (2 1 1 1 2) to (λ (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 a c) (*.p16 b_2 b_2)))) b_2) a))
6.386 * * * * [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))>
6.386 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))
6.386 * * [simplify]: iters left: 3 (8 enodes)
6.387 * * [simplify]: iters left: 2 (33 enodes)
6.393 * * [simplify]: iters left: 1 (79 enodes)
6.416 * * [simplify]: Extracting #0: cost 1 inf + 0
6.416 * * [simplify]: Extracting #1: cost 21 inf + 0
6.416 * * [simplify]: Extracting #2: cost 51 inf + 0
6.417 * * [simplify]: Extracting #3: cost 77 inf + 5301
6.420 * * [simplify]: Extracting #4: cost 37 inf + 63309
6.427 * * [simplify]: Extracting #5: cost 2 inf + 116709
6.433 * * [simplify]: Extracting #6: cost 0 inf + 120953
6.437 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))
6.437 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))
6.438 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
6.438 * * [simplify]: iters left: 2 (6 enodes)
6.439 * * [simplify]: iters left: 1 (14 enodes)
6.441 * * [simplify]: Extracting #0: cost 1 inf + 0
6.441 * * [simplify]: Extracting #1: cost 3 inf + 0
6.441 * * [simplify]: Extracting #2: cost 6 inf + 0
6.441 * * [simplify]: Extracting #3: cost 2 inf + 325
6.441 * * [simplify]: Extracting #4: cost 0 inf + 1329
6.441 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
6.441 * [simplify]: Simplified (2 1 1 1 2) to (λ (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 a c) (*.p16 b_2 b_2)))) b_2) a))
6.441 * * * [progress]: adding candidates to table
6.549 * * [progress]: iteration 3 / 4
6.549 * * * [progress]: picking best candidate
6.581 * * * * [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))>
6.581 * * * [progress]: localizing error
6.799 * * * [progress]: generating rewritten candidates
6.799 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
6.802 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
6.805 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
6.810 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
6.815 * * * [progress]: generating series expansions
6.816 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
6.816 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
6.816 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
6.816 * * * * [progress]: [ 4 / 4 ] generating series at (2)
6.816 * * * [progress]: simplifying candidates
6.816 * * * * [progress]: [ 1 / 11 ] 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))>
6.816 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.816 * * [simplify]: iters left: 4 (8 enodes)
6.818 * * [simplify]: iters left: 3 (23 enodes)
6.821 * * [simplify]: iters left: 2 (45 enodes)
6.829 * * [simplify]: iters left: 1 (108 enodes)
6.881 * * [simplify]: Extracting #0: cost 1 inf + 0
6.881 * * [simplify]: Extracting #1: cost 3 inf + 0
6.881 * * [simplify]: Extracting #2: cost 3 inf + 1
6.881 * * [simplify]: Extracting #3: cost 17 inf + 1
6.881 * * [simplify]: Extracting #4: cost 55 inf + 322
6.885 * * [simplify]: Extracting #5: cost 80 inf + 11197
6.889 * * [simplify]: Extracting #6: cost 84 inf + 56173
6.899 * * [simplify]: Extracting #7: cost 7 inf + 177856
6.912 * * [simplify]: Extracting #8: cost 0 inf + 193436
6.924 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
6.925 * [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))
6.925 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.925 * * [simplify]: iters left: 4 (8 enodes)
6.929 * * [simplify]: iters left: 3 (28 enodes)
6.939 * * [simplify]: iters left: 2 (59 enodes)
6.961 * * [simplify]: iters left: 1 (178 enodes)
7.070 * * [simplify]: Extracting #0: cost 1 inf + 0
7.070 * * [simplify]: Extracting #1: cost 12 inf + 0
7.070 * * [simplify]: Extracting #2: cost 64 inf + 1
7.071 * * [simplify]: Extracting #3: cost 140 inf + 403
7.073 * * [simplify]: Extracting #4: cost 187 inf + 15607
7.081 * * [simplify]: Extracting #5: cost 136 inf + 133387
7.101 * * [simplify]: Extracting #6: cost 33 inf + 315910
7.118 * * [simplify]: Extracting #7: cost 1 inf + 363183
7.132 * * [simplify]: Extracting #8: cost 0 inf + 364746
7.158 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
7.158 * [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))
7.159 * * * * [progress]: [ 2 / 11 ] 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))>
7.159 * [simplify]: Simplifying (neg.p16 (*.p16 b_2 b_2))
7.159 * * [simplify]: iters left: 2 (3 enodes)
7.160 * * [simplify]: iters left: 1 (5 enodes)
7.162 * * [simplify]: Extracting #0: cost 1 inf + 0
7.162 * * [simplify]: Extracting #1: cost 2 inf + 0
7.162 * * [simplify]: Extracting #2: cost 3 inf + 0
7.162 * * [simplify]: Extracting #3: cost 2 inf + 1
7.162 * * [simplify]: Extracting #4: cost 0 inf + 723
7.162 * [simplify]: Simplified to (neg.p16 (*.p16 b_2 b_2))
7.162 * [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))) (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))
7.163 * * * * [progress]: [ 3 / 11 ] 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))>
7.163 * [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)))
7.163 * * [simplify]: iters left: 6 (11 enodes)
7.167 * * [simplify]: iters left: 5 (43 enodes)
7.176 * * [simplify]: iters left: 4 (139 enodes)
7.250 * * [simplify]: Extracting #0: cost 1 inf + 0
7.250 * * [simplify]: Extracting #1: cost 32 inf + 0
7.250 * * [simplify]: Extracting #2: cost 85 inf + 0
7.251 * * [simplify]: Extracting #3: cost 152 inf + 1364
7.253 * * [simplify]: Extracting #4: cost 166 inf + 20000
7.258 * * [simplify]: Extracting #5: cost 75 inf + 165167
7.268 * * [simplify]: Extracting #6: cost 1 inf + 282810
7.282 * * [simplify]: Extracting #7: cost 0 inf + 285213
7.303 * [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))))
7.303 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.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))) (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))
7.304 * [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))
7.304 * * [simplify]: iters left: 5 (9 enodes)
7.308 * * [simplify]: iters left: 4 (24 enodes)
7.316 * * [simplify]: iters left: 3 (52 enodes)
7.329 * * [simplify]: iters left: 2 (126 enodes)
7.363 * * [simplify]: iters left: 1 (448 enodes)
8.123 * * [simplify]: Extracting #0: cost 1 inf + 0
8.123 * * [simplify]: Extracting #1: cost 21 inf + 0
8.124 * * [simplify]: Extracting #2: cost 138 inf + 0
8.126 * * [simplify]: Extracting #3: cost 398 inf + 4059
8.136 * * [simplify]: Extracting #4: cost 479 inf + 121592
8.194 * * [simplify]: Extracting #5: cost 171 inf + 722802
8.244 * * [simplify]: Extracting #6: cost 1 inf + 1087820
8.335 * * [simplify]: Extracting #7: cost 0 inf + 1091423
8.430 * [simplify]: Simplified to (+.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)) (*.p16 b_2 b_2))
8.430 * [simplify]: Simplified (2 1 1 2) to (λ (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 (*.p16 b_2 b_2) (*.p16 a c)) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
8.431 * * * * [progress]: [ 4 / 11 ] 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))>
8.431 * * * * [progress]: [ 5 / 11 ] 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))>
8.431 * [simplify]: Simplifying (/.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))
8.431 * * [simplify]: iters left: 5 (10 enodes)
8.435 * * [simplify]: iters left: 4 (30 enodes)
8.446 * * [simplify]: iters left: 3 (62 enodes)
8.469 * * [simplify]: iters left: 2 (195 enodes)
8.589 * * [simplify]: Extracting #0: cost 1 inf + 0
8.589 * * [simplify]: Extracting #1: cost 19 inf + 0
8.589 * * [simplify]: Extracting #2: cost 92 inf + 0
8.590 * * [simplify]: Extracting #3: cost 147 inf + 685
8.592 * * [simplify]: Extracting #4: cost 197 inf + 18145
8.605 * * [simplify]: Extracting #5: cost 136 inf + 180081
8.634 * * [simplify]: Extracting #6: cost 44 inf + 357497
8.666 * * [simplify]: Extracting #7: cost 1 inf + 421516
8.696 * * [simplify]: Extracting #8: cost 0 inf + 424799
8.713 * [simplify]: Simplified to (/.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 a c))) b_2))
8.713 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.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 a c))) b_2))) a))
8.713 * * * * [progress]: [ 6 / 11 ] 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))>
8.713 * [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)))
8.713 * * [simplify]: iters left: 6 (11 enodes)
8.716 * * [simplify]: iters left: 5 (34 enodes)
8.723 * * [simplify]: iters left: 4 (120 enodes)
8.766 * * [simplify]: iters left: 3 (324 enodes)
8.934 * * [simplify]: Extracting #0: cost 1 inf + 0
8.934 * * [simplify]: Extracting #1: cost 56 inf + 0
8.935 * * [simplify]: Extracting #2: cost 156 inf + 0
8.937 * * [simplify]: Extracting #3: cost 277 inf + 3087
8.941 * * [simplify]: Extracting #4: cost 283 inf + 34132
8.964 * * [simplify]: Extracting #5: cost 117 inf + 305537
9.007 * * [simplify]: Extracting #6: cost 0 inf + 511038
9.054 * * [simplify]: Extracting #7: cost 0 inf + 508518
9.099 * [simplify]: Simplified to (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
9.099 * [simplify]: Simplified (2 1 2) to (λ (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 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) a))
9.099 * * * * [progress]: [ 7 / 11 ] 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))))>
9.099 * [simplify]: Simplifying (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
9.099 * * [simplify]: iters left: 5 (9 enodes)
9.101 * * [simplify]: iters left: 4 (31 enodes)
9.106 * * [simplify]: iters left: 3 (55 enodes)
9.115 * * [simplify]: iters left: 2 (114 enodes)
9.142 * * [simplify]: iters left: 1 (406 enodes)
9.429 * * [simplify]: Extracting #0: cost 1 inf + 0
9.429 * * [simplify]: Extracting #1: cost 5 inf + 0
9.429 * * [simplify]: Extracting #2: cost 6 inf + 1
9.429 * * [simplify]: Extracting #3: cost 5 inf + 324
9.429 * * [simplify]: Extracting #4: cost 51 inf + 324
9.430 * * [simplify]: Extracting #5: cost 257 inf + 645
9.432 * * [simplify]: Extracting #6: cost 464 inf + 11760
9.443 * * [simplify]: Extracting #7: cost 370 inf + 309548
9.488 * * [simplify]: Extracting #8: cost 43 inf + 972742
9.530 * * [simplify]: Extracting #9: cost 0 inf + 1034433
9.592 * * [simplify]: Extracting #10: cost 0 inf + 1033793
9.639 * [simplify]: Simplified to (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
9.639 * [simplify]: Simplified (2 2) to (λ (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 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)))
9.639 * * * * [progress]: [ 8 / 11 ] 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))>
9.639 * [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))
9.639 * * [simplify]: iters left: 5 (9 enodes)
9.642 * * [simplify]: iters left: 4 (32 enodes)
9.647 * * [simplify]: iters left: 3 (94 enodes)
9.684 * * [simplify]: iters left: 2 (340 enodes)
9.940 * * [simplify]: Extracting #0: cost 1 inf + 0
9.940 * * [simplify]: Extracting #1: cost 50 inf + 0
9.941 * * [simplify]: Extracting #2: cost 240 inf + 0
9.946 * * [simplify]: Extracting #3: cost 363 inf + 51025
9.972 * * [simplify]: Extracting #4: cost 279 inf + 363866
10.039 * * [simplify]: Extracting #5: cost 63 inf + 808744
10.093 * * [simplify]: Extracting #6: cost 1 inf + 916546
10.174 * * [simplify]: Extracting #7: cost 0 inf + 919829
10.222 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
10.222 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
10.222 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
10.222 * * [simplify]: iters left: 4 (8 enodes)
10.225 * * [simplify]: iters left: 3 (23 enodes)
10.233 * * [simplify]: iters left: 2 (45 enodes)
10.249 * * [simplify]: iters left: 1 (108 enodes)
10.307 * * [simplify]: Extracting #0: cost 1 inf + 0
10.307 * * [simplify]: Extracting #1: cost 3 inf + 0
10.309 * * [simplify]: Extracting #2: cost 3 inf + 1
10.309 * * [simplify]: Extracting #3: cost 17 inf + 1
10.309 * * [simplify]: Extracting #4: cost 55 inf + 322
10.310 * * [simplify]: Extracting #5: cost 80 inf + 11197
10.314 * * [simplify]: Extracting #6: cost 84 inf + 56173
10.325 * * [simplify]: Extracting #7: cost 7 inf + 177856
10.337 * * [simplify]: Extracting #8: cost 0 inf + 193436
10.350 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
10.350 * [simplify]: Simplified (2 1 2) to (λ (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 a c))))) a))
10.350 * * * * [progress]: [ 9 / 11 ] 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))>
10.350 * [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))
10.350 * * [simplify]: iters left: 5 (9 enodes)
10.355 * * [simplify]: iters left: 4 (32 enodes)
10.364 * * [simplify]: iters left: 3 (94 enodes)
10.385 * * [simplify]: iters left: 2 (340 enodes)
10.653 * * [simplify]: Extracting #0: cost 1 inf + 0
10.654 * * [simplify]: Extracting #1: cost 50 inf + 0
10.654 * * [simplify]: Extracting #2: cost 240 inf + 0
10.657 * * [simplify]: Extracting #3: cost 363 inf + 51025
10.670 * * [simplify]: Extracting #4: cost 279 inf + 363866
10.702 * * [simplify]: Extracting #5: cost 63 inf + 808744
10.752 * * [simplify]: Extracting #6: cost 1 inf + 916546
10.829 * * [simplify]: Extracting #7: cost 0 inf + 919829
10.905 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
10.905 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
10.905 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
10.905 * * [simplify]: iters left: 4 (8 enodes)
10.907 * * [simplify]: iters left: 3 (23 enodes)
10.911 * * [simplify]: iters left: 2 (45 enodes)
10.919 * * [simplify]: iters left: 1 (108 enodes)
10.971 * * [simplify]: Extracting #0: cost 1 inf + 0
10.971 * * [simplify]: Extracting #1: cost 3 inf + 0
10.971 * * [simplify]: Extracting #2: cost 3 inf + 1
10.971 * * [simplify]: Extracting #3: cost 17 inf + 1
10.972 * * [simplify]: Extracting #4: cost 55 inf + 322
10.973 * * [simplify]: Extracting #5: cost 80 inf + 11197
10.976 * * [simplify]: Extracting #6: cost 84 inf + 56173
10.984 * * [simplify]: Extracting #7: cost 7 inf + 177856
10.990 * * [simplify]: Extracting #8: cost 0 inf + 193436
10.998 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
10.998 * [simplify]: Simplified (2 1 2) to (λ (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 a c))))) a))
10.998 * * * * [progress]: [ 10 / 11 ] 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))>
10.998 * [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))
10.999 * * [simplify]: iters left: 5 (9 enodes)
11.001 * * [simplify]: iters left: 4 (32 enodes)
11.007 * * [simplify]: iters left: 3 (94 enodes)
11.036 * * [simplify]: iters left: 2 (340 enodes)
11.243 * * [simplify]: Extracting #0: cost 1 inf + 0
11.243 * * [simplify]: Extracting #1: cost 50 inf + 0
11.243 * * [simplify]: Extracting #2: cost 240 inf + 0
11.246 * * [simplify]: Extracting #3: cost 363 inf + 51025
11.265 * * [simplify]: Extracting #4: cost 279 inf + 363866
11.326 * * [simplify]: Extracting #5: cost 63 inf + 808744
11.408 * * [simplify]: Extracting #6: cost 1 inf + 916546
11.484 * * [simplify]: Extracting #7: cost 0 inf + 919829
11.564 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
11.564 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
11.564 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
11.564 * * [simplify]: iters left: 4 (8 enodes)
11.568 * * [simplify]: iters left: 3 (23 enodes)
11.575 * * [simplify]: iters left: 2 (45 enodes)
11.592 * * [simplify]: iters left: 1 (108 enodes)
11.646 * * [simplify]: Extracting #0: cost 1 inf + 0
11.646 * * [simplify]: Extracting #1: cost 3 inf + 0
11.646 * * [simplify]: Extracting #2: cost 3 inf + 1
11.646 * * [simplify]: Extracting #3: cost 17 inf + 1
11.647 * * [simplify]: Extracting #4: cost 55 inf + 322
11.648 * * [simplify]: Extracting #5: cost 80 inf + 11197
11.651 * * [simplify]: Extracting #6: cost 84 inf + 56173
11.661 * * [simplify]: Extracting #7: cost 7 inf + 177856
11.674 * * [simplify]: Extracting #8: cost 0 inf + 193436
11.686 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
11.687 * [simplify]: Simplified (2 1 2) to (λ (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 a c))))) a))
11.687 * * * * [progress]: [ 11 / 11 ] 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))>
11.687 * [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))
11.687 * * [simplify]: iters left: 5 (9 enodes)
11.691 * * [simplify]: iters left: 4 (32 enodes)
11.704 * * [simplify]: iters left: 3 (94 enodes)
11.735 * * [simplify]: iters left: 2 (340 enodes)
11.984 * * [simplify]: Extracting #0: cost 1 inf + 0
11.984 * * [simplify]: Extracting #1: cost 50 inf + 0
11.985 * * [simplify]: Extracting #2: cost 240 inf + 0
11.996 * * [simplify]: Extracting #3: cost 363 inf + 51025
12.020 * * [simplify]: Extracting #4: cost 279 inf + 363866
12.052 * * [simplify]: Extracting #5: cost 63 inf + 808744
12.100 * * [simplify]: Extracting #6: cost 1 inf + 916546
12.147 * * [simplify]: Extracting #7: cost 0 inf + 919829
12.188 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
12.188 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
12.188 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
12.188 * * [simplify]: iters left: 4 (8 enodes)
12.190 * * [simplify]: iters left: 3 (23 enodes)
12.194 * * [simplify]: iters left: 2 (45 enodes)
12.203 * * [simplify]: iters left: 1 (108 enodes)
12.229 * * [simplify]: Extracting #0: cost 1 inf + 0
12.229 * * [simplify]: Extracting #1: cost 3 inf + 0
12.229 * * [simplify]: Extracting #2: cost 3 inf + 1
12.229 * * [simplify]: Extracting #3: cost 17 inf + 1
12.229 * * [simplify]: Extracting #4: cost 55 inf + 322
12.230 * * [simplify]: Extracting #5: cost 80 inf + 11197
12.232 * * [simplify]: Extracting #6: cost 84 inf + 56173
12.237 * * [simplify]: Extracting #7: cost 7 inf + 177856
12.243 * * [simplify]: Extracting #8: cost 0 inf + 193436
12.249 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
12.250 * [simplify]: Simplified (2 1 2) to (λ (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 a c))))) a))
12.250 * * * [progress]: adding candidates to table
12.363 * * [progress]: iteration 4 / 4
12.363 * * * [progress]: picking best candidate
12.420 * * * * [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))>
12.420 * * * [progress]: localizing error
12.624 * * * [progress]: generating rewritten candidates
12.624 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
12.627 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
12.636 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
12.638 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
12.644 * * * [progress]: generating series expansions
12.644 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
12.644 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
12.644 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
12.644 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
12.644 * * * [progress]: simplifying candidates
12.644 * * * * [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))>
12.644 * * * * [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))>
12.644 * * * * [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))>
12.644 * [simplify]: Simplifying (neg.p16 b_2)
12.644 * * [simplify]: iters left: 1 (2 enodes)
12.645 * * [simplify]: Extracting #0: cost 1 inf + 0
12.645 * * [simplify]: Extracting #1: cost 2 inf + 0
12.645 * * [simplify]: Extracting #2: cost 1 inf + 1
12.645 * * [simplify]: Extracting #3: cost 0 inf + 82
12.645 * [simplify]: Simplified to (neg.p16 b_2)
12.645 * [simplify]: Simplified (2 1 1 2 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 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
12.645 * * * * [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))>
12.645 * [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))
12.645 * * [simplify]: iters left: 5 (9 enodes)
12.647 * * [simplify]: iters left: 4 (32 enodes)
12.656 * * [simplify]: iters left: 3 (94 enodes)
12.689 * * [simplify]: iters left: 2 (340 enodes)
12.939 * * [simplify]: Extracting #0: cost 1 inf + 0
12.939 * * [simplify]: Extracting #1: cost 50 inf + 0
12.940 * * [simplify]: Extracting #2: cost 240 inf + 0
12.945 * * [simplify]: Extracting #3: cost 363 inf + 51025
12.971 * * [simplify]: Extracting #4: cost 279 inf + 363866
13.035 * * [simplify]: Extracting #5: cost 63 inf + 808744
13.119 * * [simplify]: Extracting #6: cost 1 inf + 916546
13.167 * * [simplify]: Extracting #7: cost 0 inf + 919829
13.241 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
13.241 * [simplify]: Simplified (2 1 1 2 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (-.p16 (real->posit16 0.0) (*.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))
13.242 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
13.242 * * [simplify]: iters left: 4 (8 enodes)
13.245 * * [simplify]: iters left: 3 (23 enodes)
13.253 * * [simplify]: iters left: 2 (45 enodes)
13.265 * * [simplify]: iters left: 1 (108 enodes)
13.292 * * [simplify]: Extracting #0: cost 1 inf + 0
13.292 * * [simplify]: Extracting #1: cost 3 inf + 0
13.292 * * [simplify]: Extracting #2: cost 3 inf + 1
13.292 * * [simplify]: Extracting #3: cost 17 inf + 1
13.293 * * [simplify]: Extracting #4: cost 55 inf + 322
13.293 * * [simplify]: Extracting #5: cost 80 inf + 11197
13.295 * * [simplify]: Extracting #6: cost 84 inf + 56173
13.302 * * [simplify]: Extracting #7: cost 7 inf + 177856
13.313 * * [simplify]: Extracting #8: cost 0 inf + 193436
13.324 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
13.325 * [simplify]: Simplified (2 1 1 2 2) to (λ (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 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)) a))
13.325 * * * * [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))>
13.325 * [simplify]: Simplifying (/.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))
13.325 * * [simplify]: iters left: 5 (10 enodes)
13.329 * * [simplify]: iters left: 4 (30 enodes)
13.340 * * [simplify]: iters left: 3 (62 enodes)
13.354 * * [simplify]: iters left: 2 (195 enodes)
13.422 * * [simplify]: Extracting #0: cost 1 inf + 0
13.422 * * [simplify]: Extracting #1: cost 19 inf + 0
13.422 * * [simplify]: Extracting #2: cost 92 inf + 0
13.423 * * [simplify]: Extracting #3: cost 147 inf + 685
13.425 * * [simplify]: Extracting #4: cost 197 inf + 18145
13.437 * * [simplify]: Extracting #5: cost 136 inf + 180081
13.453 * * [simplify]: Extracting #6: cost 44 inf + 357497
13.469 * * [simplify]: Extracting #7: cost 1 inf + 421516
13.497 * * [simplify]: Extracting #8: cost 0 inf + 424799
13.531 * [simplify]: Simplified to (/.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 a c))) b_2))
13.532 * [simplify]: Simplified (2 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.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 a c))) b_2))) a))
13.532 * * * * [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))>
13.532 * [simplify]: Simplifying (*.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))
13.532 * * [simplify]: iters left: 5 (9 enodes)
13.536 * * [simplify]: iters left: 4 (30 enodes)
13.547 * * [simplify]: iters left: 3 (65 enodes)
13.573 * * [simplify]: iters left: 2 (154 enodes)
13.639 * * [simplify]: iters left: 1 (482 enodes)
14.010 * * [simplify]: Extracting #0: cost 1 inf + 0
14.011 * * [simplify]: Extracting #1: cost 24 inf + 0
14.011 * * [simplify]: Extracting #2: cost 122 inf + 0
14.014 * * [simplify]: Extracting #3: cost 346 inf + 19576
14.031 * * [simplify]: Extracting #4: cost 490 inf + 110433
14.075 * * [simplify]: Extracting #5: cost 235 inf + 604158
14.162 * * [simplify]: Extracting #6: cost 13 inf + 1060306
14.261 * * [simplify]: Extracting #7: cost 0 inf + 1079456
14.356 * [simplify]: Simplified to (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
14.356 * [simplify]: Simplified (2 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 (*.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 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) a))
14.356 * * * * [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))>
14.356 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.356 * * [simplify]: iters left: 4 (8 enodes)
14.360 * * [simplify]: iters left: 3 (23 enodes)
14.367 * * [simplify]: iters left: 2 (45 enodes)
14.384 * * [simplify]: iters left: 1 (108 enodes)
14.443 * * [simplify]: Extracting #0: cost 1 inf + 0
14.443 * * [simplify]: Extracting #1: cost 3 inf + 0
14.443 * * [simplify]: Extracting #2: cost 3 inf + 1
14.443 * * [simplify]: Extracting #3: cost 17 inf + 1
14.443 * * [simplify]: Extracting #4: cost 55 inf + 322
14.444 * * [simplify]: Extracting #5: cost 80 inf + 11197
14.448 * * [simplify]: Extracting #6: cost 84 inf + 56173
14.458 * * [simplify]: Extracting #7: cost 7 inf + 177856
14.470 * * [simplify]: Extracting #8: cost 0 inf + 193436
14.484 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
14.484 * [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))
14.484 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.484 * * [simplify]: iters left: 4 (8 enodes)
14.488 * * [simplify]: iters left: 3 (28 enodes)
14.498 * * [simplify]: iters left: 2 (59 enodes)
14.520 * * [simplify]: iters left: 1 (178 enodes)
14.630 * * [simplify]: Extracting #0: cost 1 inf + 0
14.630 * * [simplify]: Extracting #1: cost 12 inf + 0
14.630 * * [simplify]: Extracting #2: cost 64 inf + 1
14.631 * * [simplify]: Extracting #3: cost 140 inf + 403
14.633 * * [simplify]: Extracting #4: cost 187 inf + 15607
14.641 * * [simplify]: Extracting #5: cost 136 inf + 133387
14.663 * * [simplify]: Extracting #6: cost 33 inf + 315910
14.692 * * [simplify]: Extracting #7: cost 1 inf + 363183
14.721 * * [simplify]: Extracting #8: cost 0 inf + 364746
14.748 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
14.748 * [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))
14.748 * * * * [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))>
14.749 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.749 * * [simplify]: iters left: 4 (8 enodes)
14.752 * * [simplify]: iters left: 3 (23 enodes)
14.760 * * [simplify]: iters left: 2 (45 enodes)
14.776 * * [simplify]: iters left: 1 (108 enodes)
14.831 * * [simplify]: Extracting #0: cost 1 inf + 0
14.831 * * [simplify]: Extracting #1: cost 3 inf + 0
14.831 * * [simplify]: Extracting #2: cost 3 inf + 1
14.831 * * [simplify]: Extracting #3: cost 17 inf + 1
14.831 * * [simplify]: Extracting #4: cost 55 inf + 322
14.832 * * [simplify]: Extracting #5: cost 80 inf + 11197
14.836 * * [simplify]: Extracting #6: cost 84 inf + 56173
14.846 * * [simplify]: Extracting #7: cost 7 inf + 177856
14.859 * * [simplify]: Extracting #8: cost 0 inf + 193436
14.873 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
14.873 * [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))
14.873 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
14.873 * * [simplify]: iters left: 4 (8 enodes)
14.876 * * [simplify]: iters left: 3 (28 enodes)
14.886 * * [simplify]: iters left: 2 (59 enodes)
14.908 * * [simplify]: iters left: 1 (178 enodes)
14.967 * * [simplify]: Extracting #0: cost 1 inf + 0
14.967 * * [simplify]: Extracting #1: cost 12 inf + 0
14.967 * * [simplify]: Extracting #2: cost 64 inf + 1
14.968 * * [simplify]: Extracting #3: cost 140 inf + 403
14.969 * * [simplify]: Extracting #4: cost 187 inf + 15607
14.973 * * [simplify]: Extracting #5: cost 136 inf + 133387
14.995 * * [simplify]: Extracting #6: cost 33 inf + 315910
15.023 * * [simplify]: Extracting #7: cost 1 inf + 363183
15.051 * * [simplify]: Extracting #8: cost 0 inf + 364746
15.072 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
15.073 * [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))
15.073 * * * * [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))>
15.073 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
15.073 * * [simplify]: iters left: 4 (8 enodes)
15.075 * * [simplify]: iters left: 3 (23 enodes)
15.078 * * [simplify]: iters left: 2 (45 enodes)
15.086 * * [simplify]: iters left: 1 (108 enodes)
15.113 * * [simplify]: Extracting #0: cost 1 inf + 0
15.113 * * [simplify]: Extracting #1: cost 3 inf + 0
15.113 * * [simplify]: Extracting #2: cost 3 inf + 1
15.114 * * [simplify]: Extracting #3: cost 17 inf + 1
15.114 * * [simplify]: Extracting #4: cost 55 inf + 322
15.115 * * [simplify]: Extracting #5: cost 80 inf + 11197
15.119 * * [simplify]: Extracting #6: cost 84 inf + 56173
15.129 * * [simplify]: Extracting #7: cost 7 inf + 177856
15.141 * * [simplify]: Extracting #8: cost 0 inf + 193436
15.157 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
15.157 * [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))
15.158 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
15.158 * * [simplify]: iters left: 4 (8 enodes)
15.161 * * [simplify]: iters left: 3 (28 enodes)
15.172 * * [simplify]: iters left: 2 (59 enodes)
15.197 * * [simplify]: iters left: 1 (178 enodes)
15.290 * * [simplify]: Extracting #0: cost 1 inf + 0
15.290 * * [simplify]: Extracting #1: cost 12 inf + 0
15.290 * * [simplify]: Extracting #2: cost 64 inf + 1
15.291 * * [simplify]: Extracting #3: cost 140 inf + 403
15.292 * * [simplify]: Extracting #4: cost 187 inf + 15607
15.296 * * [simplify]: Extracting #5: cost 136 inf + 133387
15.308 * * [simplify]: Extracting #6: cost 33 inf + 315910
15.336 * * [simplify]: Extracting #7: cost 1 inf + 363183
15.363 * * [simplify]: Extracting #8: cost 0 inf + 364746
15.391 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
15.391 * [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))
15.391 * * * * [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))>
15.392 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
15.392 * * [simplify]: iters left: 4 (8 enodes)
15.395 * * [simplify]: iters left: 3 (23 enodes)
15.403 * * [simplify]: iters left: 2 (45 enodes)
15.422 * * [simplify]: iters left: 1 (108 enodes)
15.480 * * [simplify]: Extracting #0: cost 1 inf + 0
15.480 * * [simplify]: Extracting #1: cost 3 inf + 0
15.480 * * [simplify]: Extracting #2: cost 3 inf + 1
15.480 * * [simplify]: Extracting #3: cost 17 inf + 1
15.480 * * [simplify]: Extracting #4: cost 55 inf + 322
15.481 * * [simplify]: Extracting #5: cost 80 inf + 11197
15.485 * * [simplify]: Extracting #6: cost 84 inf + 56173
15.493 * * [simplify]: Extracting #7: cost 7 inf + 177856
15.500 * * [simplify]: Extracting #8: cost 0 inf + 193436
15.506 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
15.506 * [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))
15.506 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
15.506 * * [simplify]: iters left: 4 (8 enodes)
15.508 * * [simplify]: iters left: 3 (28 enodes)
15.513 * * [simplify]: iters left: 2 (59 enodes)
15.531 * * [simplify]: iters left: 1 (178 enodes)
15.639 * * [simplify]: Extracting #0: cost 1 inf + 0
15.639 * * [simplify]: Extracting #1: cost 12 inf + 0
15.639 * * [simplify]: Extracting #2: cost 64 inf + 1
15.640 * * [simplify]: Extracting #3: cost 140 inf + 403
15.641 * * [simplify]: Extracting #4: cost 187 inf + 15607
15.646 * * [simplify]: Extracting #5: cost 136 inf + 133387
15.659 * * [simplify]: Extracting #6: cost 33 inf + 315910
15.673 * * [simplify]: Extracting #7: cost 1 inf + 363183
15.699 * * [simplify]: Extracting #8: cost 0 inf + 364746
15.726 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
15.726 * [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))
15.726 * * * [progress]: adding candidates to table
15.923 * [progress]: [Phase 3 of 3] Extracting.
15.923 * * [regime]: Finding splitpoints for: (#<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 (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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.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 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<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 (*.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))))>)
15.931 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
15.932 * * * * [regimes]: Trying to branch on c from (#<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 (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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.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 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<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 (*.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))))>)
16.118 * * * * [regimes]: Trying to branch on a from (#<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 (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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.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 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<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 (*.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))))>)
16.232 * * * * [regimes]: Trying to branch on b_2 from (#<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 (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 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.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 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<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 (*.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))))>)
16.355 * * * [regime]: Found split indices: #<option (#s(si 2 256))>
16.355 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
16.355 * * [simplify]: iters left: 5 (9 enodes)
16.356 * * [simplify]: Extracting #0: cost 1 inf + 0
16.356 * * [simplify]: Extracting #1: cost 3 inf + 0
16.356 * * [simplify]: Extracting #2: cost 4 inf + 1
16.356 * * [simplify]: Extracting #3: cost 4 inf + 2
16.356 * * [simplify]: Extracting #4: cost 6 inf + 2
16.356 * * [simplify]: Extracting #5: cost 6 inf + 323
16.357 * * [simplify]: Extracting #6: cost 0 inf + 4258
16.357 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
16.357 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
16.419 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
16.421 * * * * [points]: Setting MPFR precision to 64
16.423 * * * * [points]: Setting MPFR precision to 320
16.425 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
16.427 * * * * [points]: Setting MPFR precision to 64
16.431 * * * * [points]: Setting MPFR precision to 320
16.435 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
16.436 * * * * [points]: Setting MPFR precision to 64
16.443 * * * * [points]: Setting MPFR precision to 320
16.451 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
16.453 * * * * [points]: Setting MPFR precision to 64
16.480 * * * * [points]: Setting MPFR precision to 320
16.495 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
16.497 * * * * [points]: Setting MPFR precision to 64
16.525 * * * * [points]: Setting MPFR precision to 320
16.553 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
16.555 * * * * [points]: Setting MPFR precision to 64
16.611 * * * * [points]: Setting MPFR precision to 320
16.642 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
16.643 * * * * [points]: Setting MPFR precision to 64
16.740 * * * * [points]: Setting MPFR precision to 320
16.911 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
16.913 * * * * [points]: Setting MPFR precision to 64
17.201 * * * * [points]: Setting MPFR precision to 320
17.439 * * * * [points]: Computing exacts for 8000 points
17.442 * * * * [points]: Setting MPFR precision to 64
18.492 * * * * [points]: Setting MPFR precision to 320
19.950 * * * * [points]: Filtering points with unrepresentable outputs
19.998 * * * * [points]: Sampled 8000 points with exact outputs
22.227 * [regime-testing]: Baseline error score: 64.0
22.233 * [regime-testing]: Oracle error score: 64.0
22.247 * [regime-testing]: End program error score: 1.6949216928040012