0.003 * [progress]: [Phase 1 of 3] Setting up.
0.004 * * * [progress]: [1/2] Preparing points
0.006 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
0.009 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
0.109 * * * * [points]: Setting MPFR precision to 64
0.113 * * * * [points]: Setting MPFR precision to 320
0.115 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
0.120 * * * * [points]: Setting MPFR precision to 64
0.123 * * * * [points]: Setting MPFR precision to 320
0.126 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
0.131 * * * * [points]: Setting MPFR precision to 64
0.136 * * * * [points]: Setting MPFR precision to 320
0.142 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
0.146 * * * * [points]: Setting MPFR precision to 64
0.154 * * * * [points]: Setting MPFR precision to 320
0.163 * * * * [points]: Computing exacts for 256 points
0.167 * * * * [points]: Setting MPFR precision to 64
0.194 * * * * [points]: Setting MPFR precision to 320
0.221 * * * * [points]: Filtering points with unrepresentable outputs
0.222 * * * * [points]: Sampled 256 points with exact outputs
0.223 * * * [progress]: [2/2] Setting up program.
0.257 * [progress]: [Phase 2 of 3] Improving.
0.257 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
0.259 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
0.260 * * [simplify]: iters left: 6 (16 enodes)
0.299 * * [simplify]: iters left: 5 (39 enodes)
0.307 * * [simplify]: iters left: 4 (72 enodes)
0.322 * * [simplify]: iters left: 3 (196 enodes)
0.421 * * [simplify]: Extracting #0: cost 1 inf + 0
0.421 * * [simplify]: Extracting #1: cost 5 inf + 0
0.422 * * [simplify]: Extracting #2: cost 11 inf + 1
0.422 * * [simplify]: Extracting #3: cost 16 inf + 2
0.422 * * [simplify]: Extracting #4: cost 26 inf + 807
0.423 * * [simplify]: Extracting #5: cost 66 inf + 1770
0.424 * * [simplify]: Extracting #6: cost 135 inf + 3695
0.426 * * [simplify]: Extracting #7: cost 209 inf + 14082
0.434 * * [simplify]: Extracting #8: cost 138 inf + 107732
0.453 * * [simplify]: Extracting #9: cost 36 inf + 289941
0.480 * * [simplify]: Extracting #10: cost 2 inf + 355093
0.508 * * [simplify]: Extracting #11: cost 1 inf + 357016
0.540 * * [simplify]: Extracting #12: cost 0 inf + 360620
0.569 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
0.571 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))
0.622 * * [progress]: iteration 1 / 4
0.622 * * * [progress]: picking best candidate
0.647 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
0.647 * * * [progress]: localizing error
0.897 * * * [progress]: generating rewritten candidates
0.897 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
0.903 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
0.909 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
0.910 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
0.920 * * * [progress]: generating series expansions
0.921 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
0.921 * * * * [progress]: [ 2 / 4 ] generating series at (2)
0.921 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
0.921 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
0.921 * * * [progress]: simplifying candidates
0.921 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))>
0.921 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))>
0.922 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
0.922 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))>
0.922 * [simplify]: Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))
0.922 * * [simplify]: iters left: 6 (12 enodes)
0.928 * * [simplify]: iters left: 5 (39 enodes)
0.943 * * [simplify]: iters left: 4 (111 enodes)
0.970 * * [simplify]: iters left: 3 (427 enodes)
1.285 * * [simplify]: Extracting #0: cost 1 inf + 0
1.286 * * [simplify]: Extracting #1: cost 47 inf + 0
1.286 * * [simplify]: Extracting #2: cost 231 inf + 0
1.287 * * [simplify]: Extracting #3: cost 400 inf + 3216
1.299 * * [simplify]: Extracting #4: cost 473 inf + 191470
1.369 * * [simplify]: Extracting #5: cost 180 inf + 866467
1.445 * * [simplify]: Extracting #6: cost 4 inf + 1232579
1.510 * * [simplify]: Extracting #7: cost 0 inf + 1241757
1.581 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4)))
1.582 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))
1.582 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
1.582 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
1.582 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
1.582 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
1.582 * * [simplify]: iters left: 6 (15 enodes)
1.588 * * [simplify]: iters left: 5 (43 enodes)
1.596 * * [simplify]: iters left: 4 (88 enodes)
1.617 * * [simplify]: iters left: 3 (307 enodes)
1.760 * * [simplify]: Extracting #0: cost 1 inf + 0
1.761 * * [simplify]: Extracting #1: cost 31 inf + 0
1.761 * * [simplify]: Extracting #2: cost 125 inf + 1
1.762 * * [simplify]: Extracting #3: cost 193 inf + 2734
1.764 * * [simplify]: Extracting #4: cost 253 inf + 8433
1.769 * * [simplify]: Extracting #5: cost 273 inf + 63950
1.796 * * [simplify]: Extracting #6: cost 175 inf + 356651
1.833 * * [simplify]: Extracting #7: cost 6 inf + 666712
1.883 * * [simplify]: Extracting #8: cost 0 inf + 674735
1.939 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
1.940 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
1.940 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
1.940 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
1.940 * * [simplify]: iters left: 6 (15 enodes)
1.947 * * [simplify]: iters left: 5 (43 enodes)
1.965 * * [simplify]: iters left: 4 (88 enodes)
2.002 * * [simplify]: iters left: 3 (307 enodes)
2.185 * * [simplify]: Extracting #0: cost 1 inf + 0
2.186 * * [simplify]: Extracting #1: cost 31 inf + 0
2.186 * * [simplify]: Extracting #2: cost 125 inf + 1
2.187 * * [simplify]: Extracting #3: cost 193 inf + 2734
2.189 * * [simplify]: Extracting #4: cost 253 inf + 8433
2.194 * * [simplify]: Extracting #5: cost 273 inf + 63950
2.221 * * [simplify]: Extracting #6: cost 175 inf + 356651
2.265 * * [simplify]: Extracting #7: cost 6 inf + 666712
2.309 * * [simplify]: Extracting #8: cost 0 inf + 674735
2.370 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
2.370 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
2.370 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
2.371 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
2.371 * * [simplify]: iters left: 6 (15 enodes)
2.378 * * [simplify]: iters left: 5 (43 enodes)
2.393 * * [simplify]: iters left: 4 (88 enodes)
2.424 * * [simplify]: iters left: 3 (307 enodes)
2.528 * * [simplify]: Extracting #0: cost 1 inf + 0
2.528 * * [simplify]: Extracting #1: cost 31 inf + 0
2.529 * * [simplify]: Extracting #2: cost 125 inf + 1
2.529 * * [simplify]: Extracting #3: cost 193 inf + 2734
2.530 * * [simplify]: Extracting #4: cost 253 inf + 8433
2.533 * * [simplify]: Extracting #5: cost 273 inf + 63950
2.547 * * [simplify]: Extracting #6: cost 175 inf + 356651
2.573 * * [simplify]: Extracting #7: cost 6 inf + 666712
2.615 * * [simplify]: Extracting #8: cost 0 inf + 674735
2.642 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
2.643 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
2.643 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
2.643 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
2.643 * * [simplify]: iters left: 6 (15 enodes)
2.647 * * [simplify]: iters left: 5 (43 enodes)
2.655 * * [simplify]: iters left: 4 (88 enodes)
2.676 * * [simplify]: iters left: 3 (307 enodes)
2.802 * * [simplify]: Extracting #0: cost 1 inf + 0
2.802 * * [simplify]: Extracting #1: cost 31 inf + 0
2.803 * * [simplify]: Extracting #2: cost 125 inf + 1
2.804 * * [simplify]: Extracting #3: cost 193 inf + 2734
2.806 * * [simplify]: Extracting #4: cost 253 inf + 8433
2.811 * * [simplify]: Extracting #5: cost 273 inf + 63950
2.839 * * [simplify]: Extracting #6: cost 175 inf + 356651
2.895 * * [simplify]: Extracting #7: cost 6 inf + 666712
2.927 * * [simplify]: Extracting #8: cost 0 inf + 674735
2.957 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
2.957 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
2.957 * * * [progress]: adding candidates to table
3.214 * * [progress]: iteration 2 / 4
3.214 * * * [progress]: picking best candidate
3.271 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
3.272 * * * [progress]: localizing error
3.514 * * * [progress]: generating rewritten candidates
3.514 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
3.517 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
3.518 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
3.526 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 1)
3.535 * * * [progress]: generating series expansions
3.535 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
3.535 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
3.535 * * * * [progress]: [ 3 / 4 ] generating series at (2)
3.535 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 1)
3.535 * * * [progress]: simplifying candidates
3.535 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (real->posit16 2)) a))>
3.535 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
3.535 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))>
3.535 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
3.536 * * [simplify]: iters left: 5 (11 enodes)
3.541 * * [simplify]: iters left: 4 (35 enodes)
3.554 * * [simplify]: iters left: 3 (76 enodes)
3.585 * * [simplify]: iters left: 2 (261 enodes)
3.679 * * [simplify]: Extracting #0: cost 1 inf + 0
3.679 * * [simplify]: Extracting #1: cost 12 inf + 0
3.679 * * [simplify]: Extracting #2: cost 66 inf + 1
3.680 * * [simplify]: Extracting #3: cost 146 inf + 403
3.681 * * [simplify]: Extracting #4: cost 205 inf + 4899
3.682 * * [simplify]: Extracting #5: cost 241 inf + 36908
3.692 * * [simplify]: Extracting #6: cost 176 inf + 271128
3.712 * * [simplify]: Extracting #7: cost 10 inf + 555810
3.741 * * [simplify]: Extracting #8: cost 0 inf + 573768
3.767 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b)
3.767 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
3.767 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))>
3.767 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (real->posit16 2)) a))>
3.767 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
3.767 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
3.767 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
3.767 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
3.767 * * * [progress]: adding candidates to table
4.031 * * [progress]: iteration 3 / 4
4.031 * * * [progress]: picking best candidate
4.086 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
4.086 * * * [progress]: localizing error
4.438 * * * [progress]: generating rewritten candidates
4.438 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
4.445 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2)
4.450 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
4.459 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 1)
4.460 * * * [progress]: generating series expansions
4.460 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
4.461 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2)
4.461 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
4.461 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 1)
4.461 * * * [progress]: simplifying candidates
4.461 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
4.461 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
4.461 * * [simplify]: iters left: 5 (11 enodes)
4.466 * * [simplify]: iters left: 4 (30 enodes)
4.477 * * [simplify]: iters left: 3 (62 enodes)
4.502 * * [simplify]: iters left: 2 (181 enodes)
4.580 * * [simplify]: Extracting #0: cost 1 inf + 0
4.580 * * [simplify]: Extracting #1: cost 3 inf + 0
4.580 * * [simplify]: Extracting #2: cost 3 inf + 1
4.580 * * [simplify]: Extracting #3: cost 17 inf + 1
4.581 * * [simplify]: Extracting #4: cost 59 inf + 322
4.581 * * [simplify]: Extracting #5: cost 133 inf + 1287
4.582 * * [simplify]: Extracting #6: cost 191 inf + 13674
4.585 * * [simplify]: Extracting #7: cost 131 inf + 89074
4.594 * * [simplify]: Extracting #8: cost 15 inf + 300176
4.608 * * [simplify]: Extracting #9: cost 0 inf + 335752
4.633 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
4.633 * [simplify]: Simplified (2 1 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))
4.634 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
4.634 * * [simplify]: iters left: 5 (11 enodes)
4.637 * * [simplify]: iters left: 4 (35 enodes)
4.643 * * [simplify]: iters left: 3 (76 enodes)
4.659 * * [simplify]: iters left: 2 (261 enodes)
4.747 * * [simplify]: Extracting #0: cost 1 inf + 0
4.747 * * [simplify]: Extracting #1: cost 12 inf + 0
4.748 * * [simplify]: Extracting #2: cost 66 inf + 1
4.748 * * [simplify]: Extracting #3: cost 146 inf + 403
4.749 * * [simplify]: Extracting #4: cost 205 inf + 4899
4.750 * * [simplify]: Extracting #5: cost 241 inf + 36908
4.760 * * [simplify]: Extracting #6: cost 176 inf + 271128
4.781 * * [simplify]: Extracting #7: cost 10 inf + 555810
4.805 * * [simplify]: Extracting #8: cost 0 inf + 573768
4.831 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b)
4.831 * [simplify]: Simplified (2 1 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))
4.831 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (neg.p16 (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
4.831 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
4.831 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (real->posit16 2)) a))>
4.831 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>
4.831 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
4.831 * * [simplify]: iters left: 5 (11 enodes)
4.834 * * [simplify]: iters left: 4 (30 enodes)
4.839 * * [simplify]: iters left: 3 (62 enodes)
4.852 * * [simplify]: iters left: 2 (181 enodes)
4.913 * * [simplify]: Extracting #0: cost 1 inf + 0
4.913 * * [simplify]: Extracting #1: cost 3 inf + 0
4.913 * * [simplify]: Extracting #2: cost 3 inf + 1
4.913 * * [simplify]: Extracting #3: cost 17 inf + 1
4.913 * * [simplify]: Extracting #4: cost 59 inf + 322
4.914 * * [simplify]: Extracting #5: cost 133 inf + 1287
4.915 * * [simplify]: Extracting #6: cost 191 inf + 13674
4.918 * * [simplify]: Extracting #7: cost 131 inf + 89074
4.927 * * [simplify]: Extracting #8: cost 15 inf + 300176
4.940 * * [simplify]: Extracting #9: cost 0 inf + 335752
4.956 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
4.956 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))
4.956 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))>
4.956 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b)))
4.956 * * [simplify]: iters left: 6 (14 enodes)
4.960 * * [simplify]: iters left: 5 (50 enodes)
4.971 * * [simplify]: iters left: 4 (159 enodes)
5.033 * * [simplify]: Extracting #0: cost 1 inf + 0
5.034 * * [simplify]: Extracting #1: cost 28 inf + 0
5.034 * * [simplify]: Extracting #2: cost 80 inf + 0
5.035 * * [simplify]: Extracting #3: cost 153 inf + 322
5.039 * * [simplify]: Extracting #4: cost 182 inf + 8818
5.044 * * [simplify]: Extracting #5: cost 166 inf + 64938
5.061 * * [simplify]: Extracting #6: cost 44 inf + 258136
5.088 * * [simplify]: Extracting #7: cost 1 inf + 350866
5.118 * * [simplify]: Extracting #8: cost 0 inf + 351990
5.147 * [simplify]: Simplified to (*.p16 (-.p16 (*.p16 b b) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))) (+.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))) (*.p16 b b)))
5.147 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (*.p16 (-.p16 (*.p16 b b) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 b b))) (+.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))
5.147 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
5.148 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
5.148 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
5.148 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
5.148 * * * [progress]: adding candidates to table
5.483 * * [progress]: iteration 4 / 4
5.483 * * * [progress]: picking best candidate
5.567 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>
5.567 * * * [progress]: localizing error
5.812 * * * [progress]: generating rewritten candidates
5.812 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2 2)
5.814 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2 1)
5.816 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
5.819 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
5.823 * * * [progress]: generating series expansions
5.824 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2 2)
5.824 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2 1)
5.824 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
5.824 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
5.824 * * * [progress]: simplifying candidates
5.824 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)))) (real->posit16 2)) a))>
5.824 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)))) (real->posit16 2)) a))>
5.824 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>
5.824 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>
5.824 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
5.824 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
5.824 * * [simplify]: iters left: 5 (11 enodes)
5.832 * * [simplify]: iters left: 4 (30 enodes)
5.837 * * [simplify]: iters left: 3 (62 enodes)
5.850 * * [simplify]: iters left: 2 (181 enodes)
5.911 * * [simplify]: Extracting #0: cost 1 inf + 0
5.911 * * [simplify]: Extracting #1: cost 3 inf + 0
5.911 * * [simplify]: Extracting #2: cost 3 inf + 1
5.911 * * [simplify]: Extracting #3: cost 17 inf + 1
5.911 * * [simplify]: Extracting #4: cost 59 inf + 322
5.911 * * [simplify]: Extracting #5: cost 133 inf + 1287
5.912 * * [simplify]: Extracting #6: cost 191 inf + 13674
5.915 * * [simplify]: Extracting #7: cost 131 inf + 89074
5.932 * * [simplify]: Extracting #8: cost 15 inf + 300176
5.955 * * [simplify]: Extracting #9: cost 0 inf + 335752
5.968 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
5.968 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))) (real->posit16 2)) a))
5.968 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (*.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
5.969 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
5.969 * * [simplify]: iters left: 5 (11 enodes)
5.971 * * [simplify]: iters left: 4 (35 enodes)
5.978 * * [simplify]: iters left: 3 (76 enodes)
5.998 * * [simplify]: iters left: 2 (261 enodes)
6.112 * * [simplify]: Extracting #0: cost 1 inf + 0
6.112 * * [simplify]: Extracting #1: cost 12 inf + 0
6.112 * * [simplify]: Extracting #2: cost 66 inf + 1
6.113 * * [simplify]: Extracting #3: cost 146 inf + 403
6.113 * * [simplify]: Extracting #4: cost 205 inf + 4899
6.115 * * [simplify]: Extracting #5: cost 241 inf + 36908
6.131 * * [simplify]: Extracting #6: cost 176 inf + 271128
6.160 * * [simplify]: Extracting #7: cost 10 inf + 555810
6.197 * * [simplify]: Extracting #8: cost 0 inf + 573768
6.229 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b)
6.229 * [simplify]: Simplified (2 1 1 2) to (λ (a b c) (/.p16 (/.p16 (*.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b)) (real->posit16 2)) a))
6.230 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>
6.230 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
6.230 * * [simplify]: iters left: 5 (11 enodes)
6.233 * * [simplify]: iters left: 4 (30 enodes)
6.238 * * [simplify]: iters left: 3 (62 enodes)
6.251 * * [simplify]: iters left: 2 (181 enodes)
6.373 * * [simplify]: Extracting #0: cost 1 inf + 0
6.373 * * [simplify]: Extracting #1: cost 3 inf + 0
6.373 * * [simplify]: Extracting #2: cost 3 inf + 1
6.373 * * [simplify]: Extracting #3: cost 17 inf + 1
6.373 * * [simplify]: Extracting #4: cost 59 inf + 322
6.374 * * [simplify]: Extracting #5: cost 133 inf + 1287
6.376 * * [simplify]: Extracting #6: cost 191 inf + 13674
6.381 * * [simplify]: Extracting #7: cost 131 inf + 89074
6.403 * * [simplify]: Extracting #8: cost 15 inf + 300176
6.429 * * [simplify]: Extracting #9: cost 0 inf + 335752
6.455 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
6.455 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))
6.455 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>
6.455 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
6.455 * * [simplify]: iters left: 5 (11 enodes)
6.461 * * [simplify]: iters left: 4 (30 enodes)
6.471 * * [simplify]: iters left: 3 (62 enodes)
6.498 * * [simplify]: iters left: 2 (181 enodes)
6.615 * * [simplify]: Extracting #0: cost 1 inf + 0
6.616 * * [simplify]: Extracting #1: cost 3 inf + 0
6.616 * * [simplify]: Extracting #2: cost 3 inf + 1
6.616 * * [simplify]: Extracting #3: cost 17 inf + 1
6.616 * * [simplify]: Extracting #4: cost 59 inf + 322
6.617 * * [simplify]: Extracting #5: cost 133 inf + 1287
6.619 * * [simplify]: Extracting #6: cost 191 inf + 13674
6.626 * * [simplify]: Extracting #7: cost 131 inf + 89074
6.645 * * [simplify]: Extracting #8: cost 15 inf + 300176
6.669 * * [simplify]: Extracting #9: cost 0 inf + 335752
6.698 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
6.698 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))
6.699 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>
6.699 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
6.699 * * [simplify]: iters left: 5 (11 enodes)
6.704 * * [simplify]: iters left: 4 (30 enodes)
6.715 * * [simplify]: iters left: 3 (62 enodes)
6.741 * * [simplify]: iters left: 2 (181 enodes)
6.827 * * [simplify]: Extracting #0: cost 1 inf + 0
6.827 * * [simplify]: Extracting #1: cost 3 inf + 0
6.827 * * [simplify]: Extracting #2: cost 3 inf + 1
6.827 * * [simplify]: Extracting #3: cost 17 inf + 1
6.828 * * [simplify]: Extracting #4: cost 59 inf + 322
6.828 * * [simplify]: Extracting #5: cost 133 inf + 1287
6.829 * * [simplify]: Extracting #6: cost 191 inf + 13674
6.832 * * [simplify]: Extracting #7: cost 131 inf + 89074
6.842 * * [simplify]: Extracting #8: cost 15 inf + 300176
6.854 * * [simplify]: Extracting #9: cost 0 inf + 335752
6.868 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
6.868 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))
6.868 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>
6.869 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
6.869 * * [simplify]: iters left: 5 (11 enodes)
6.873 * * [simplify]: iters left: 4 (30 enodes)
6.886 * * [simplify]: iters left: 3 (62 enodes)
6.905 * * [simplify]: iters left: 2 (181 enodes)
6.992 * * [simplify]: Extracting #0: cost 1 inf + 0
6.992 * * [simplify]: Extracting #1: cost 3 inf + 0
6.992 * * [simplify]: Extracting #2: cost 3 inf + 1
6.992 * * [simplify]: Extracting #3: cost 17 inf + 1
6.992 * * [simplify]: Extracting #4: cost 59 inf + 322
6.993 * * [simplify]: Extracting #5: cost 133 inf + 1287
6.994 * * [simplify]: Extracting #6: cost 191 inf + 13674
6.999 * * [simplify]: Extracting #7: cost 131 inf + 89074
7.016 * * [simplify]: Extracting #8: cost 15 inf + 300176
7.037 * * [simplify]: Extracting #9: cost 0 inf + 335752
7.059 * [simplify]: Simplified to (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))))
7.060 * [simplify]: Simplified (2 1 1 1) to (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 b (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))
7.060 * * * [progress]: adding candidates to table
7.462 * [progress]: [Phase 3 of 3] Extracting.
7.463 * * [regime]: Finding splitpoints for: (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>)
7.472 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
7.473 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>)
7.818 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>)
8.148 * * * * [regimes]: Trying to branch on b from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))) (*.p16 (*.p16 b b) (*.p16 b b))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 c a) (real->posit16 4)) (*.p16 (*.p16 c a) (real->posit16 4)))) (+.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))) (real->posit16 2)) a))>)
8.477 * * * [regime]: Found split indices: #<option (#s(si 6 256))>
8.477 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
8.478 * * [simplify]: iters left: 6 (15 enodes)
8.481 * * [simplify]: Extracting #0: cost 1 inf + 0
8.481 * * [simplify]: Extracting #1: cost 3 inf + 0
8.481 * * [simplify]: Extracting #2: cost 7 inf + 0
8.481 * * [simplify]: Extracting #3: cost 7 inf + 2
8.481 * * [simplify]: Extracting #4: cost 6 inf + 326
8.481 * * [simplify]: Extracting #5: cost 7 inf + 647
8.481 * * [simplify]: Extracting #6: cost 9 inf + 647
8.481 * * [simplify]: Extracting #7: cost 6 inf + 971
8.481 * * [simplify]: Extracting #8: cost 4 inf + 1615
8.482 * * [simplify]: Extracting #9: cost 2 inf + 3743
8.482 * * [simplify]: Extracting #10: cost 0 inf + 6832
8.483 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
8.483 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
8.546 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
8.551 * * * * [points]: Setting MPFR precision to 64
8.553 * * * * [points]: Setting MPFR precision to 320
8.555 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
8.560 * * * * [points]: Setting MPFR precision to 64
8.564 * * * * [points]: Setting MPFR precision to 320
8.568 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
8.572 * * * * [points]: Setting MPFR precision to 64
8.580 * * * * [points]: Setting MPFR precision to 320
8.589 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
8.594 * * * * [points]: Setting MPFR precision to 64
8.610 * * * * [points]: Setting MPFR precision to 320
8.624 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
8.630 * * * * [points]: Setting MPFR precision to 64
8.691 * * * * [points]: Setting MPFR precision to 320
8.721 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
8.726 * * * * [points]: Setting MPFR precision to 64
8.778 * * * * [points]: Setting MPFR precision to 320
8.833 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
8.838 * * * * [points]: Setting MPFR precision to 64
8.999 * * * * [points]: Setting MPFR precision to 320
9.129 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
9.138 * * * * [points]: Setting MPFR precision to 64
9.439 * * * * [points]: Setting MPFR precision to 320
10.144 * * * * [points]: Computing exacts for 8000 points
10.147 * * * * [points]: Setting MPFR precision to 64
11.252 * * * * [points]: Setting MPFR precision to 320
12.350 * * * * [points]: Filtering points with unrepresentable outputs
12.423 * * * * [points]: Sampled 8000 points with exact outputs
18.479 * [regime-testing]: Baseline error score: 64.0
18.485 * [regime-testing]: Oracle error score: 64.0
18.497 * [regime-testing]: End program error score: 1.5769512122681504