0.005 * [progress]: [Phase 1 of 3] Setting up.
0.006 * * * [progress]: [1/2] Preparing points
0.009 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.011 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.112 * * * * [points]: Setting MPFR precision to 64
0.117 * * * * [points]: Setting MPFR precision to 320
0.120 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.123 * * * * [points]: Setting MPFR precision to 64
0.126 * * * * [points]: Setting MPFR precision to 320
0.130 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.132 * * * * [points]: Setting MPFR precision to 64
0.138 * * * * [points]: Setting MPFR precision to 320
0.177 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.179 * * * * [points]: Setting MPFR precision to 64
0.187 * * * * [points]: Setting MPFR precision to 320
0.197 * * * * [points]: Computing exacts for 256 points
0.198 * * * * [points]: Setting MPFR precision to 64
0.220 * * * * [points]: Setting MPFR precision to 320
0.377 * * * * [points]: Filtering points with unrepresentable outputs
0.379 * * * * [points]: Sampled 256 points with exact outputs
0.380 * * * [progress]: [2/2] Setting up program.
0.397 * [progress]: [Phase 2 of 3] Improving.
0.398 * * * * [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.399 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
0.400 * * [simplify]: iters left: 5 (10 enodes)
0.406 * * [simplify]: iters left: 4 (25 enodes)
0.444 * * [simplify]: iters left: 3 (48 enodes)
0.495 * * [simplify]: iters left: 2 (111 enodes)
0.551 * * [simplify]: iters left: 1 (394 enodes)
0.883 * * [simplify]: Extracting #0: cost 1 inf + 0
0.884 * * [simplify]: Extracting #1: cost 10 inf + 0
0.884 * * [simplify]: Extracting #2: cost 35 inf + 1
0.885 * * [simplify]: Extracting #3: cost 92 inf + 83
0.886 * * [simplify]: Extracting #4: cost 333 inf + 1810
0.890 * * [simplify]: Extracting #5: cost 518 inf + 5618
0.913 * * [simplify]: Extracting #6: cost 470 inf + 184191
0.977 * * [simplify]: Extracting #7: cost 61 inf + 918877
1.063 * * [simplify]: Extracting #8: cost 0 inf + 1055660
1.145 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.145 * [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.158 * * [progress]: iteration 1 / 4
1.158 * * * [progress]: picking best candidate
1.162 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1.163 * * * [progress]: localizing error
1.336 * * * [progress]: generating rewritten candidates
1.336 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1.342 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1)
1.343 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1.348 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1.355 * * * [progress]: generating series expansions
1.356 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1.356 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1)
1.356 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1.356 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1.356 * * * [progress]: simplifying candidates
1.356 * * * * [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.357 * * * * [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.357 * * * * [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.357 * [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.357 * * [simplify]: iters left: 5 (9 enodes)
1.361 * * [simplify]: iters left: 4 (32 enodes)
1.373 * * [simplify]: iters left: 3 (94 enodes)
1.408 * * [simplify]: iters left: 2 (340 enodes)
1.627 * * [simplify]: Extracting #0: cost 1 inf + 0
1.627 * * [simplify]: Extracting #1: cost 50 inf + 0
1.628 * * [simplify]: Extracting #2: cost 240 inf + 0
1.633 * * [simplify]: Extracting #3: cost 363 inf + 51025
1.660 * * [simplify]: Extracting #4: cost 279 inf + 363866
1.730 * * [simplify]: Extracting #5: cost 63 inf + 808744
1.785 * * [simplify]: Extracting #6: cost 1 inf + 916546
1.827 * * [simplify]: Extracting #7: cost 0 inf + 919829
1.875 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1.875 * [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.875 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))) b_2) a))>
1.875 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
1.875 * * * * [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.875 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1.875 * * [simplify]: iters left: 5 (9 enodes)
1.879 * * [simplify]: iters left: 4 (29 enodes)
1.886 * * [simplify]: iters left: 3 (62 enodes)
1.899 * * [simplify]: iters left: 2 (199 enodes)
1.985 * * [simplify]: Extracting #0: cost 1 inf + 0
1.986 * * [simplify]: Extracting #1: cost 20 inf + 0
1.986 * * [simplify]: Extracting #2: cost 94 inf + 1
1.986 * * [simplify]: Extracting #3: cost 162 inf + 1046
1.988 * * [simplify]: Extracting #4: cost 205 inf + 21625
1.991 * * [simplify]: Extracting #5: cost 170 inf + 98466
2.002 * * [simplify]: Extracting #6: cost 65 inf + 303687
2.020 * * [simplify]: Extracting #7: cost 1 inf + 408042
2.036 * * [simplify]: Extracting #8: cost 0 inf + 411325
2.061 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.061 * [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.061 * * * * [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.061 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.062 * * [simplify]: iters left: 5 (9 enodes)
2.065 * * [simplify]: iters left: 4 (29 enodes)
2.076 * * [simplify]: iters left: 3 (62 enodes)
2.101 * * [simplify]: iters left: 2 (199 enodes)
2.207 * * [simplify]: Extracting #0: cost 1 inf + 0
2.207 * * [simplify]: Extracting #1: cost 20 inf + 0
2.208 * * [simplify]: Extracting #2: cost 94 inf + 1
2.208 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.209 * * [simplify]: Extracting #4: cost 205 inf + 21625
2.213 * * [simplify]: Extracting #5: cost 170 inf + 98466
2.223 * * [simplify]: Extracting #6: cost 65 inf + 303687
2.239 * * [simplify]: Extracting #7: cost 1 inf + 408042
2.265 * * [simplify]: Extracting #8: cost 0 inf + 411325
2.281 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.282 * [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.282 * * * * [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.282 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.282 * * [simplify]: iters left: 5 (9 enodes)
2.284 * * [simplify]: iters left: 4 (29 enodes)
2.290 * * [simplify]: iters left: 3 (62 enodes)
2.307 * * [simplify]: iters left: 2 (199 enodes)
2.394 * * [simplify]: Extracting #0: cost 1 inf + 0
2.394 * * [simplify]: Extracting #1: cost 20 inf + 0
2.394 * * [simplify]: Extracting #2: cost 94 inf + 1
2.394 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.396 * * [simplify]: Extracting #4: cost 205 inf + 21625
2.399 * * [simplify]: Extracting #5: cost 170 inf + 98466
2.410 * * [simplify]: Extracting #6: cost 65 inf + 303687
2.428 * * [simplify]: Extracting #7: cost 1 inf + 408042
2.450 * * [simplify]: Extracting #8: cost 0 inf + 411325
2.467 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
2.467 * [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.467 * * * * [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.467 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
2.467 * * [simplify]: iters left: 5 (9 enodes)
2.469 * * [simplify]: iters left: 4 (29 enodes)
2.474 * * [simplify]: iters left: 3 (62 enodes)
2.497 * * [simplify]: iters left: 2 (199 enodes)
2.614 * * [simplify]: Extracting #0: cost 1 inf + 0
2.614 * * [simplify]: Extracting #1: cost 20 inf + 0
2.614 * * [simplify]: Extracting #2: cost 94 inf + 1
2.615 * * [simplify]: Extracting #3: cost 162 inf + 1046
2.617 * * [simplify]: Extracting #4: cost 205 inf + 21625
2.624 * * [simplify]: Extracting #5: cost 170 inf + 98466
2.645 * * [simplify]: Extracting #6: cost 65 inf + 303687
2.677 * * [simplify]: Extracting #7: cost 1 inf + 408042
2.711 * * [simplify]: Extracting #8: cost 0 inf + 411325
2.741 * [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.742 * * * [progress]: adding candidates to table
2.848 * * [progress]: iteration 2 / 4
2.848 * * * [progress]: picking best candidate
2.863 * * * * [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.863 * * * [progress]: localizing error
3.056 * * * [progress]: generating rewritten candidates
3.056 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
3.070 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
3.072 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
3.072 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
3.076 * * * [progress]: generating series expansions
3.076 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
3.076 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
3.076 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
3.076 * * * * [progress]: [ 4 / 4 ] generating series at (2)
3.076 * * * [progress]: simplifying candidates
3.076 * * * * [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.076 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
3.076 * * [simplify]: iters left: 2 (6 enodes)
3.078 * * [simplify]: iters left: 1 (14 enodes)
3.079 * * [simplify]: Extracting #0: cost 1 inf + 0
3.080 * * [simplify]: Extracting #1: cost 3 inf + 0
3.080 * * [simplify]: Extracting #2: cost 6 inf + 0
3.080 * * [simplify]: Extracting #3: cost 2 inf + 325
3.080 * * [simplify]: Extracting #4: cost 0 inf + 1329
3.080 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
3.080 * [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.080 * * * * [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.080 * [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.080 * * [simplify]: iters left: 4 (10 enodes)
3.082 * * [simplify]: iters left: 3 (43 enodes)
3.099 * * [simplify]: iters left: 2 (121 enodes)
3.162 * * [simplify]: iters left: 1 (456 enodes)
3.607 * * [simplify]: Extracting #0: cost 1 inf + 0
3.607 * * [simplify]: Extracting #1: cost 46 inf + 0
3.609 * * [simplify]: Extracting #2: cost 270 inf + 0
3.614 * * [simplify]: Extracting #3: cost 402 inf + 62527
3.648 * * [simplify]: Extracting #4: cost 378 inf + 463702
3.730 * * [simplify]: Extracting #5: cost 11 inf + 1296655
3.819 * * [simplify]: Extracting #6: cost 0 inf + 1315117
3.896 * [simplify]: Simplified to (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))))
3.896 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))
3.896 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 b_2)) a))>
3.896 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
3.896 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
3.897 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2))
3.897 * * [simplify]: iters left: 6 (13 enodes)
3.901 * * [simplify]: iters left: 5 (47 enodes)
3.918 * * [simplify]: iters left: 4 (118 enodes)
3.974 * * [simplify]: iters left: 3 (482 enodes)
4.516 * * [simplify]: Extracting #0: cost 1 inf + 0
4.516 * * [simplify]: Extracting #1: cost 47 inf + 0
4.517 * * [simplify]: Extracting #2: cost 266 inf + 0
4.521 * * [simplify]: Extracting #3: cost 536 inf + 28392
4.553 * * [simplify]: Extracting #4: cost 646 inf + 405570
4.649 * * [simplify]: Extracting #5: cost 179 inf + 1412113
4.792 * * [simplify]: Extracting #6: cost 2 inf + 1774901
4.957 * * [simplify]: Extracting #7: cost 0 inf + 1777784
5.119 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
5.119 * [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.119 * * * * [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.119 * * * * [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.119 * * * * [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.119 * * * * [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.120 * * * [progress]: adding candidates to table
5.274 * * [progress]: iteration 3 / 4
5.274 * * * [progress]: picking best candidate
5.315 * * * * [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.315 * * * [progress]: localizing error
5.573 * * * [progress]: generating rewritten candidates
5.573 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
5.587 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
5.592 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
5.601 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
5.602 * * * [progress]: generating series expansions
5.602 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
5.602 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
5.602 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
5.602 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
5.602 * * * [progress]: simplifying candidates
5.603 * * * * [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.603 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.603 * * [simplify]: iters left: 4 (8 enodes)
5.605 * * [simplify]: iters left: 3 (23 enodes)
5.609 * * [simplify]: iters left: 2 (45 enodes)
5.617 * * [simplify]: iters left: 1 (108 enodes)
5.647 * * [simplify]: Extracting #0: cost 1 inf + 0
5.647 * * [simplify]: Extracting #1: cost 3 inf + 0
5.647 * * [simplify]: Extracting #2: cost 3 inf + 1
5.647 * * [simplify]: Extracting #3: cost 17 inf + 1
5.647 * * [simplify]: Extracting #4: cost 55 inf + 322
5.648 * * [simplify]: Extracting #5: cost 80 inf + 11197
5.652 * * [simplify]: Extracting #6: cost 84 inf + 56173
5.662 * * [simplify]: Extracting #7: cost 7 inf + 177856
5.675 * * [simplify]: Extracting #8: cost 0 inf + 193436
5.687 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.688 * [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.688 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.688 * * [simplify]: iters left: 4 (8 enodes)
5.691 * * [simplify]: iters left: 3 (28 enodes)
5.695 * * [simplify]: iters left: 2 (59 enodes)
5.707 * * [simplify]: iters left: 1 (178 enodes)
5.775 * * [simplify]: Extracting #0: cost 1 inf + 0
5.775 * * [simplify]: Extracting #1: cost 12 inf + 0
5.775 * * [simplify]: Extracting #2: cost 64 inf + 1
5.776 * * [simplify]: Extracting #3: cost 140 inf + 403
5.777 * * [simplify]: Extracting #4: cost 187 inf + 15607
5.781 * * [simplify]: Extracting #5: cost 136 inf + 133387
5.793 * * [simplify]: Extracting #6: cost 33 inf + 315910
5.807 * * [simplify]: Extracting #7: cost 1 inf + 363183
5.835 * * [simplify]: Extracting #8: cost 0 inf + 364746
5.863 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
5.864 * [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.864 * * * * [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.864 * * * * [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.864 * * * * [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.864 * * * * [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.864 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
5.864 * * [simplify]: iters left: 4 (8 enodes)
5.868 * * [simplify]: iters left: 3 (23 enodes)
5.875 * * [simplify]: iters left: 2 (45 enodes)
5.894 * * [simplify]: iters left: 1 (108 enodes)
5.923 * * [simplify]: Extracting #0: cost 1 inf + 0
5.923 * * [simplify]: Extracting #1: cost 3 inf + 0
5.923 * * [simplify]: Extracting #2: cost 3 inf + 1
5.923 * * [simplify]: Extracting #3: cost 17 inf + 1
5.924 * * [simplify]: Extracting #4: cost 55 inf + 322
5.924 * * [simplify]: Extracting #5: cost 80 inf + 11197
5.926 * * [simplify]: Extracting #6: cost 84 inf + 56173
5.931 * * [simplify]: Extracting #7: cost 7 inf + 177856
5.938 * * [simplify]: Extracting #8: cost 0 inf + 193436
5.945 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
5.945 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))
5.945 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))>
5.945 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))
5.945 * * [simplify]: iters left: 6 (11 enodes)
5.948 * * [simplify]: iters left: 5 (43 enodes)
5.957 * * [simplify]: iters left: 4 (139 enodes)
6.032 * * [simplify]: Extracting #0: cost 1 inf + 0
6.032 * * [simplify]: Extracting #1: cost 32 inf + 0
6.032 * * [simplify]: Extracting #2: cost 85 inf + 0
6.033 * * [simplify]: Extracting #3: cost 152 inf + 1364
6.033 * * [simplify]: Extracting #4: cost 166 inf + 20000
6.039 * * [simplify]: Extracting #5: cost 75 inf + 165167
6.049 * * [simplify]: Extracting #6: cost 1 inf + 282810
6.060 * * [simplify]: Extracting #7: cost 0 inf + 285213
6.081 * [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.081 * [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.081 * * * * [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.081 * * * * [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.081 * * * * [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.081 * * * * [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.082 * * * [progress]: adding candidates to table
6.274 * * [progress]: iteration 4 / 4
6.274 * * * [progress]: picking best candidate
6.345 * * * * [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.345 * * * [progress]: localizing error
6.599 * * * [progress]: generating rewritten candidates
6.599 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
6.604 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
6.609 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
6.613 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
6.622 * * * [progress]: generating series expansions
6.622 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
6.622 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
6.623 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
6.623 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
6.623 * * * [progress]: simplifying candidates
6.623 * * * * [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.623 * * * * [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.623 * * * * [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.623 * * * * [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.623 * * * * [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.623 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
6.623 * * [simplify]: iters left: 4 (8 enodes)
6.627 * * [simplify]: iters left: 3 (23 enodes)
6.634 * * [simplify]: iters left: 2 (45 enodes)
6.651 * * [simplify]: iters left: 1 (108 enodes)
6.710 * * [simplify]: Extracting #0: cost 1 inf + 0
6.710 * * [simplify]: Extracting #1: cost 3 inf + 0
6.710 * * [simplify]: Extracting #2: cost 3 inf + 1
6.710 * * [simplify]: Extracting #3: cost 17 inf + 1
6.710 * * [simplify]: Extracting #4: cost 55 inf + 322
6.711 * * [simplify]: Extracting #5: cost 80 inf + 11197
6.715 * * [simplify]: Extracting #6: cost 84 inf + 56173
6.725 * * [simplify]: Extracting #7: cost 7 inf + 177856
6.738 * * [simplify]: Extracting #8: cost 0 inf + 193436
6.746 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
6.746 * [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.746 * * * * [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.746 * [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.746 * * [simplify]: iters left: 6 (11 enodes)
6.748 * * [simplify]: iters left: 5 (35 enodes)
6.755 * * [simplify]: iters left: 4 (111 enodes)
6.790 * * [simplify]: iters left: 3 (448 enodes)
7.188 * * [simplify]: Extracting #0: cost 1 inf + 0
7.189 * * [simplify]: Extracting #1: cost 64 inf + 0
7.190 * * [simplify]: Extracting #2: cost 370 inf + 0
7.191 * * [simplify]: Extracting #3: cost 525 inf + 6695
7.205 * * [simplify]: Extracting #4: cost 541 inf + 226661
7.274 * * [simplify]: Extracting #5: cost 130 inf + 956060
7.352 * * [simplify]: Extracting #6: cost 30 inf + 1175202
7.430 * * [simplify]: Extracting #7: cost 0 inf + 1216547
7.533 * * [simplify]: Extracting #8: cost 0 inf + 1216352
7.612 * [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.612 * [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.613 * * * * [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.613 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.613 * * [simplify]: iters left: 4 (8 enodes)
7.616 * * [simplify]: iters left: 3 (23 enodes)
7.622 * * [simplify]: iters left: 2 (45 enodes)
7.638 * * [simplify]: iters left: 1 (108 enodes)
7.686 * * [simplify]: Extracting #0: cost 1 inf + 0
7.686 * * [simplify]: Extracting #1: cost 3 inf + 0
7.686 * * [simplify]: Extracting #2: cost 3 inf + 1
7.686 * * [simplify]: Extracting #3: cost 17 inf + 1
7.686 * * [simplify]: Extracting #4: cost 55 inf + 322
7.687 * * [simplify]: Extracting #5: cost 80 inf + 11197
7.691 * * [simplify]: Extracting #6: cost 84 inf + 56173
7.701 * * [simplify]: Extracting #7: cost 7 inf + 177856
7.713 * * [simplify]: Extracting #8: cost 0 inf + 193436
7.727 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
7.727 * [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.727 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.727 * * [simplify]: iters left: 4 (8 enodes)
7.731 * * [simplify]: iters left: 3 (28 enodes)
7.740 * * [simplify]: iters left: 2 (59 enodes)
7.762 * * [simplify]: iters left: 1 (178 enodes)
7.868 * * [simplify]: Extracting #0: cost 1 inf + 0
7.868 * * [simplify]: Extracting #1: cost 12 inf + 0
7.869 * * [simplify]: Extracting #2: cost 64 inf + 1
7.869 * * [simplify]: Extracting #3: cost 140 inf + 403
7.871 * * [simplify]: Extracting #4: cost 187 inf + 15607
7.880 * * [simplify]: Extracting #5: cost 136 inf + 133387
7.895 * * [simplify]: Extracting #6: cost 33 inf + 315910
7.915 * * [simplify]: Extracting #7: cost 1 inf + 363183
7.939 * * [simplify]: Extracting #8: cost 0 inf + 364746
7.957 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
7.957 * [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.957 * * * * [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))>
7.958 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
7.958 * * [simplify]: iters left: 4 (8 enodes)
7.959 * * [simplify]: iters left: 3 (23 enodes)
7.963 * * [simplify]: iters left: 2 (45 enodes)
7.971 * * [simplify]: iters left: 1 (108 enodes)
8.026 * * [simplify]: Extracting #0: cost 1 inf + 0
8.027 * * [simplify]: Extracting #1: cost 3 inf + 0
8.027 * * [simplify]: Extracting #2: cost 3 inf + 1
8.027 * * [simplify]: Extracting #3: cost 17 inf + 1
8.027 * * [simplify]: Extracting #4: cost 55 inf + 322
8.028 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.031 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.037 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.043 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.050 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.050 * [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.050 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.050 * * [simplify]: iters left: 4 (8 enodes)
8.052 * * [simplify]: iters left: 3 (28 enodes)
8.057 * * [simplify]: iters left: 2 (59 enodes)
8.077 * * [simplify]: iters left: 1 (178 enodes)
8.153 * * [simplify]: Extracting #0: cost 1 inf + 0
8.154 * * [simplify]: Extracting #1: cost 12 inf + 0
8.154 * * [simplify]: Extracting #2: cost 64 inf + 1
8.155 * * [simplify]: Extracting #3: cost 140 inf + 403
8.157 * * [simplify]: Extracting #4: cost 187 inf + 15607
8.166 * * [simplify]: Extracting #5: cost 136 inf + 133387
8.189 * * [simplify]: Extracting #6: cost 33 inf + 315910
8.217 * * [simplify]: Extracting #7: cost 1 inf + 363183
8.246 * * [simplify]: Extracting #8: cost 0 inf + 364746
8.682 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
8.682 * [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.683 * * * * [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.683 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.683 * * [simplify]: iters left: 4 (8 enodes)
8.686 * * [simplify]: iters left: 3 (23 enodes)
8.694 * * [simplify]: iters left: 2 (45 enodes)
8.710 * * [simplify]: iters left: 1 (108 enodes)
8.765 * * [simplify]: Extracting #0: cost 1 inf + 0
8.765 * * [simplify]: Extracting #1: cost 3 inf + 0
8.765 * * [simplify]: Extracting #2: cost 3 inf + 1
8.765 * * [simplify]: Extracting #3: cost 17 inf + 1
8.766 * * [simplify]: Extracting #4: cost 55 inf + 322
8.767 * * [simplify]: Extracting #5: cost 80 inf + 11197
8.770 * * [simplify]: Extracting #6: cost 84 inf + 56173
8.780 * * [simplify]: Extracting #7: cost 7 inf + 177856
8.786 * * [simplify]: Extracting #8: cost 0 inf + 193436
8.801 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
8.801 * [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.801 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
8.801 * * [simplify]: iters left: 4 (8 enodes)
8.803 * * [simplify]: iters left: 3 (28 enodes)
8.808 * * [simplify]: iters left: 2 (59 enodes)
8.829 * * [simplify]: iters left: 1 (178 enodes)
8.937 * * [simplify]: Extracting #0: cost 1 inf + 0
8.937 * * [simplify]: Extracting #1: cost 12 inf + 0
8.937 * * [simplify]: Extracting #2: cost 64 inf + 1
8.938 * * [simplify]: Extracting #3: cost 140 inf + 403
8.940 * * [simplify]: Extracting #4: cost 187 inf + 15607
8.949 * * [simplify]: Extracting #5: cost 136 inf + 133387
8.971 * * [simplify]: Extracting #6: cost 33 inf + 315910
8.986 * * [simplify]: Extracting #7: cost 1 inf + 363183
9.000 * * [simplify]: Extracting #8: cost 0 inf + 364746
9.015 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
9.015 * [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.015 * * * * [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))>
9.015 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
9.015 * * [simplify]: iters left: 4 (8 enodes)
9.017 * * [simplify]: iters left: 3 (23 enodes)
9.022 * * [simplify]: iters left: 2 (45 enodes)
9.032 * * [simplify]: iters left: 1 (108 enodes)
9.059 * * [simplify]: Extracting #0: cost 1 inf + 0
9.059 * * [simplify]: Extracting #1: cost 3 inf + 0
9.059 * * [simplify]: Extracting #2: cost 3 inf + 1
9.059 * * [simplify]: Extracting #3: cost 17 inf + 1
9.060 * * [simplify]: Extracting #4: cost 55 inf + 322
9.060 * * [simplify]: Extracting #5: cost 80 inf + 11197
9.062 * * [simplify]: Extracting #6: cost 84 inf + 56173
9.068 * * [simplify]: Extracting #7: cost 7 inf + 177856
9.074 * * [simplify]: Extracting #8: cost 0 inf + 193436
9.081 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
9.081 * [simplify]: Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
9.081 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
9.081 * * [simplify]: iters left: 4 (8 enodes)
9.083 * * [simplify]: iters left: 3 (28 enodes)
9.088 * * [simplify]: iters left: 2 (59 enodes)
9.099 * * [simplify]: iters left: 1 (178 enodes)
9.154 * * [simplify]: Extracting #0: cost 1 inf + 0
9.154 * * [simplify]: Extracting #1: cost 12 inf + 0
9.155 * * [simplify]: Extracting #2: cost 64 inf + 1
9.155 * * [simplify]: Extracting #3: cost 140 inf + 403
9.156 * * [simplify]: Extracting #4: cost 187 inf + 15607
9.161 * * [simplify]: Extracting #5: cost 136 inf + 133387
9.172 * * [simplify]: Extracting #6: cost 33 inf + 315910
9.188 * * [simplify]: Extracting #7: cost 1 inf + 363183
9.203 * * [simplify]: Extracting #8: cost 0 inf + 364746
9.218 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
9.218 * [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.219 * * * [progress]: adding candidates to table
9.319 * [progress]: [Phase 3 of 3] Extracting.
9.320 * * [regime]: Finding splitpoints for: (#<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 (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 (*.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 (*.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 (+.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 (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 (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 (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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.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))>)
9.325 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
9.325 * * * * [regimes]: Trying to branch on c from (#<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 (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 (*.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 (*.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 (+.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 (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 (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 (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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.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))>)
9.437 * * * * [regimes]: Trying to branch on a from (#<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 (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 (*.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 (*.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 (+.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 (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 (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 (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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.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))>)
9.542 * * * * [regimes]: Trying to branch on b_2 from (#<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 (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 (*.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 (*.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 (+.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 (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 (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 (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 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.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))>)
9.649 * * * [regime]: Found split indices: #<option (#s(si 6 256))>
9.650 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
9.650 * * [simplify]: iters left: 5 (9 enodes)
9.650 * * [simplify]: Extracting #0: cost 1 inf + 0
9.650 * * [simplify]: Extracting #1: cost 3 inf + 0
9.650 * * [simplify]: Extracting #2: cost 4 inf + 1
9.650 * * [simplify]: Extracting #3: cost 4 inf + 2
9.650 * * [simplify]: Extracting #4: cost 6 inf + 2
9.650 * * [simplify]: Extracting #5: cost 6 inf + 323
9.651 * * [simplify]: Extracting #6: cost 0 inf + 4258
9.651 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
9.651 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
9.688 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
9.689 * * * * [points]: Setting MPFR precision to 64
9.690 * * * * [points]: Setting MPFR precision to 320
9.691 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
9.692 * * * * [points]: Setting MPFR precision to 64
9.694 * * * * [points]: Setting MPFR precision to 320
9.697 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
9.698 * * * * [points]: Setting MPFR precision to 64
9.702 * * * * [points]: Setting MPFR precision to 320
9.706 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
9.708 * * * * [points]: Setting MPFR precision to 64
9.716 * * * * [points]: Setting MPFR precision to 320
9.726 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
9.727 * * * * [points]: Setting MPFR precision to 64
9.743 * * * * [points]: Setting MPFR precision to 320
9.759 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
9.761 * * * * [points]: Setting MPFR precision to 64
9.792 * * * * [points]: Setting MPFR precision to 320
9.850 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
9.851 * * * * [points]: Setting MPFR precision to 64
9.960 * * * * [points]: Setting MPFR precision to 320
10.134 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
10.136 * * * * [points]: Setting MPFR precision to 64
10.348 * * * * [points]: Setting MPFR precision to 320
10.614 * * * * [points]: Computing exacts for 8000 points
10.615 * * * * [points]: Setting MPFR precision to 64
11.352 * * * * [points]: Setting MPFR precision to 320
12.452 * * * * [points]: Filtering points with unrepresentable outputs
12.531 * * * * [points]: Sampled 8000 points with exact outputs
14.750 * [regime-testing]: Baseline error score: 64.0
14.756 * [regime-testing]: Oracle error score: 64.0
14.770 * [regime-testing]: End program error score: 1.68233582330905