1552126484.766 * [progress]: [Phase 1 of 3] Setting up.
1552126484.768 * * * [progress]: [1/2] Preparing points
1552126484.769 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
1552126484.779 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
1552126484.868 * * * * [points]: Setting MPFR precision to 64
1552126484.872 * * * * [points]: Setting MPFR precision to 320
1552126484.876 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
1552126484.881 * * * * [points]: Setting MPFR precision to 64
1552126484.885 * * * * [points]: Setting MPFR precision to 320
1552126484.889 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
1552126484.894 * * * * [points]: Setting MPFR precision to 64
1552126484.902 * * * * [points]: Setting MPFR precision to 320
1552126484.910 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
1552126484.915 * * * * [points]: Setting MPFR precision to 64
1552126484.926 * * * * [points]: Setting MPFR precision to 320
1552126485.038 * * * * [points]: Computing exacts for 256 points
1552126485.045 * * * * [points]: Setting MPFR precision to 64
1552126485.117 * * * * [points]: Setting MPFR precision to 320
1552126485.193 * * * * [points]: Filtering points with unrepresentable outputs
1552126485.215 * * * * [points]: Sampling 64 additional inputs, on iter 1 have 192 / 256
1552126485.215 * * * * [points]: Computing exacts on every 4 of 64 points to ramp up precision
1552126485.218 * * * * [points]: Setting MPFR precision to 64
1552126485.220 * * * * [points]: Setting MPFR precision to 320
1552126485.221 * * * * [points]: Computing exacts on every 2 of 64 points to ramp up precision
1552126485.224 * * * * [points]: Setting MPFR precision to 64
1552126485.226 * * * * [points]: Setting MPFR precision to 320
1552126485.228 * * * * [points]: Computing exacts for 64 points
1552126485.232 * * * * [points]: Setting MPFR precision to 64
1552126485.237 * * * * [points]: Setting MPFR precision to 320
1552126485.243 * * * * [points]: Filtering points with unrepresentable outputs
1552126485.247 * * * * [points]: Sampling 19 additional inputs, on iter 2 have 237 / 256
1552126485.248 * * * * [points]: Computing exacts for 19 points
1552126485.255 * * * * [points]: Setting MPFR precision to 64
1552126485.258 * * * * [points]: Setting MPFR precision to 320
1552126485.261 * * * * [points]: Filtering points with unrepresentable outputs
1552126485.263 * * * * [points]: Sampling 4 additional inputs, on iter 3 have 252 / 256
1552126485.263 * * * * [points]: Computing exacts for 4 points
1552126485.269 * * * * [points]: Setting MPFR precision to 64
1552126485.270 * * * * [points]: Setting MPFR precision to 320
1552126485.271 * * * * [points]: Filtering points with unrepresentable outputs
1552126485.271 * * * * [points]: Sampling 4 additional inputs, on iter 4 have 255 / 256
1552126485.271 * * * * [points]: Computing exacts for 4 points
1552126485.308 * * * * [points]: Setting MPFR precision to 64
1552126485.310 * * * * [points]: Setting MPFR precision to 320
1552126485.311 * * * * [points]: Filtering points with unrepresentable outputs
1552126485.312 * * * * [points]: Sampled 258 points with exact outputs
1552126485.315 * * * [progress]: [2/2] Setting up program.
1552126485.502 * [progress]: [Phase 2 of 3] Improving.
1552126485.502 * * * * [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)))>
1552126485.504 * [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))
1552126485.506 * * [simplify]: iters left: 6 (16 enodes)
1552126485.520 * * [simplify]: iters left: 5 (45 enodes)
1552126485.538 * * [simplify]: iters left: 4 (91 enodes)
1552126485.583 * * [simplify]: iters left: 3 (310 enodes)
1552126485.917 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126485.918 * * [simplify]: Extracting #1: cost 31 inf + 0
1552126485.919 * * [simplify]: Extracting #2: cost 123 inf + 1
1552126485.920 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552126485.923 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552126485.929 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552126485.950 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552126485.980 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552126486.109 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552126486.186 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
1552126486.187 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
1552126486.227 * * [progress]: iteration 1 / 4
1552126486.227 * * * [progress]: picking best candidate
1552126486.272 * * * * [pick]: Picked  #<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)))>
1552126486.272 * * * [progress]: localizing error
1552126486.723 * * * [progress]: generating rewritten candidates
1552126486.723 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1552126486.727 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1552126486.728 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1552126486.731 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1 2)
1552126486.733 * * * [progress]: generating series expansions
1552126486.734 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1552126486.734 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1552126486.734 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1552126486.734 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1 2)
1552126486.734 * * * [progress]: simplifying candidates
1552126486.734 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
1552126486.734 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))>
1552126486.734 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
1552126486.734 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
1552126486.734 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))
1552126486.735 * * [simplify]: iters left: 6 (14 enodes)
1552126486.738 * * [simplify]: iters left: 5 (42 enodes)
1552126486.746 * * [simplify]: iters left: 4 (117 enodes)
1552126486.774 * * [simplify]: iters left: 3 (426 enodes)
1552126487.036 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126487.036 * * [simplify]: Extracting #1: cost 51 inf + 0
1552126487.037 * * [simplify]: Extracting #2: cost 242 inf + 0
1552126487.039 * * [simplify]: Extracting #3: cost 408 inf + 4895
1552126487.055 * * [simplify]: Extracting #4: cost 386 inf + 288425
1552126487.119 * * [simplify]: Extracting #5: cost 133 inf + 992840
1552126487.187 * * [simplify]: Extracting #6: cost 2 inf + 1243260
1552126487.299 * * [simplify]: Extracting #7: cost 0 inf + 1250148
1552126487.405 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
1552126487.405 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))
1552126487.405 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))>
1552126487.405 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))>
1552126487.405 * * * * [progress]: [ 7 / 10 ] 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)))>
1552126487.406 * [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))
1552126487.406 * * [simplify]: iters left: 6 (16 enodes)
1552126487.413 * * [simplify]: iters left: 5 (45 enodes)
1552126487.427 * * [simplify]: iters left: 4 (91 enodes)
1552126487.462 * * [simplify]: iters left: 3 (310 enodes)
1552126487.629 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126487.629 * * [simplify]: Extracting #1: cost 31 inf + 0
1552126487.630 * * [simplify]: Extracting #2: cost 123 inf + 1
1552126487.632 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552126487.634 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552126487.639 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552126487.653 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552126487.697 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552126487.762 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552126487.801 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
1552126487.801 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
1552126487.801 * * * * [progress]: [ 8 / 10 ] 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)))>
1552126487.802 * [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))
1552126487.802 * * [simplify]: iters left: 6 (16 enodes)
1552126487.806 * * [simplify]: iters left: 5 (45 enodes)
1552126487.818 * * [simplify]: iters left: 4 (91 enodes)
1552126487.851 * * [simplify]: iters left: 3 (310 enodes)
1552126488.035 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126488.036 * * [simplify]: Extracting #1: cost 31 inf + 0
1552126488.036 * * [simplify]: Extracting #2: cost 123 inf + 1
1552126488.037 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552126488.039 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552126488.046 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552126488.075 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552126488.108 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552126488.141 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552126488.187 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
1552126488.188 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
1552126488.188 * * * * [progress]: [ 9 / 10 ] 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)))>
1552126488.188 * [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))
1552126488.188 * * [simplify]: iters left: 6 (16 enodes)
1552126488.192 * * [simplify]: iters left: 5 (45 enodes)
1552126488.200 * * [simplify]: iters left: 4 (91 enodes)
1552126488.223 * * [simplify]: iters left: 3 (310 enodes)
1552126488.372 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126488.372 * * [simplify]: Extracting #1: cost 31 inf + 0
1552126488.372 * * [simplify]: Extracting #2: cost 123 inf + 1
1552126488.373 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552126488.374 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552126488.377 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552126488.393 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552126488.442 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552126488.493 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552126488.542 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
1552126488.542 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
1552126488.542 * * * * [progress]: [ 10 / 10 ] 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)))>
1552126488.542 * [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))
1552126488.542 * * [simplify]: iters left: 6 (16 enodes)
1552126488.547 * * [simplify]: iters left: 5 (45 enodes)
1552126488.556 * * [simplify]: iters left: 4 (91 enodes)
1552126488.595 * * [simplify]: iters left: 3 (310 enodes)
1552126488.792 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126488.792 * * [simplify]: Extracting #1: cost 31 inf + 0
1552126488.793 * * [simplify]: Extracting #2: cost 123 inf + 1
1552126488.794 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552126488.801 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552126488.807 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552126488.835 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552126488.890 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552126488.950 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552126489.001 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a))
1552126489.001 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 (real->posit16 2) a)))
1552126489.001 * * * [progress]: adding candidates to table
1552126489.550 * * [progress]: iteration 2 / 4
1552126489.550 * * * [progress]: picking best candidate
1552126489.711 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
1552126489.711 * * * [progress]: localizing error
1552126489.816 * * * [progress]: generating rewritten candidates
1552126489.817 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
1552126489.820 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2)
1552126489.820 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2 1 2)
1552126489.823 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
1552126489.829 * * * [progress]: generating series expansions
1552126489.829 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
1552126489.829 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2)
1552126489.829 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2 1 2)
1552126489.829 * * * * [progress]: [ 4 / 4 ] generating series at (2)
1552126489.829 * * * [progress]: simplifying candidates
1552126489.829 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))>
1552126489.829 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))>
1552126489.829 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
1552126489.830 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (real->posit16 2)) a))>
1552126489.830 * * * * [progress]: [ 5 / 9 ] 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 a (real->posit16 2))))>
1552126489.830 * [simplify]: Simplifying (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1552126489.830 * * [simplify]: iters left: 5 (12 enodes)
1552126489.836 * * [simplify]: iters left: 4 (37 enodes)
1552126489.849 * * [simplify]: iters left: 3 (79 enodes)
1552126489.884 * * [simplify]: iters left: 2 (262 enodes)
1552126490.007 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126490.007 * * [simplify]: Extracting #1: cost 17 inf + 0
1552126490.008 * * [simplify]: Extracting #2: cost 88 inf + 1
1552126490.008 * * [simplify]: Extracting #3: cost 166 inf + 804
1552126490.009 * * [simplify]: Extracting #4: cost 230 inf + 3734
1552126490.011 * * [simplify]: Extracting #5: cost 225 inf + 64494
1552126490.024 * * [simplify]: Extracting #6: cost 137 inf + 332479
1552126490.046 * * [simplify]: Extracting #7: cost 1 inf + 596662
1552126490.072 * * [simplify]: Extracting #8: cost 0 inf + 599226
1552126490.099 * [simplify]: Simplified to (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))
1552126490.100 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 a (real->posit16 2))))
1552126490.100 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
1552126490.100 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
1552126490.100 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
1552126490.100 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))>
1552126490.100 * * * [progress]: adding candidates to table
1552126490.750 * * [progress]: iteration 3 / 4
1552126490.750 * * * [progress]: picking best candidate
1552126490.877 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
1552126490.877 * * * [progress]: localizing error
1552126491.153 * * * [progress]: generating rewritten candidates
1552126491.153 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
1552126491.156 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2)
1552126491.157 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1552126491.162 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 1)
1552126491.177 * * * [progress]: generating series expansions
1552126491.177 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
1552126491.177 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2)
1552126491.177 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1552126491.177 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 1)
1552126491.177 * * * [progress]: simplifying candidates
1552126491.177 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))>
1552126491.178 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))>
1552126491.178 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 a (real->posit16 2))))>
1552126491.178 * [simplify]: Simplifying (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
1552126491.178 * * [simplify]: iters left: 6 (12 enodes)
1552126491.184 * * [simplify]: iters left: 5 (37 enodes)
1552126491.198 * * [simplify]: iters left: 4 (79 enodes)
1552126491.221 * * [simplify]: iters left: 3 (269 enodes)
1552126491.327 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126491.327 * * [simplify]: Extracting #1: cost 17 inf + 0
1552126491.328 * * [simplify]: Extracting #2: cost 88 inf + 1
1552126491.328 * * [simplify]: Extracting #3: cost 168 inf + 804
1552126491.329 * * [simplify]: Extracting #4: cost 235 inf + 2891
1552126491.332 * * [simplify]: Extracting #5: cost 214 inf + 98858
1552126491.351 * * [simplify]: Extracting #6: cost 124 inf + 370436
1552126491.380 * * [simplify]: Extracting #7: cost 4 inf + 597686
1552126491.432 * * [simplify]: Extracting #8: cost 0 inf + 607340
1552126491.482 * [simplify]: Simplified to (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
1552126491.482 * [simplify]: Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 a (real->posit16 2))))
1552126491.482 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))>
1552126491.482 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))>
1552126491.482 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
1552126491.482 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
1552126491.483 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
1552126491.483 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))>
1552126491.483 * * * [progress]: adding candidates to table
1552126491.949 * * [progress]: iteration 4 / 4
1552126491.949 * * * [progress]: picking best candidate
1552126492.181 * * * * [pick]: Picked  #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
1552126492.181 * * * [progress]: localizing error
1552126492.520 * * * [progress]: generating rewritten candidates
1552126492.520 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
1552126492.523 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
1552126492.526 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2)
1552126492.526 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2 1 2)
1552126492.528 * * * [progress]: generating series expansions
1552126492.528 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
1552126492.528 * * * * [progress]: [ 2 / 4 ] generating series at (2)
1552126492.528 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2)
1552126492.528 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2 1 2)
1552126492.528 * * * [progress]: simplifying candidates
1552126492.528 * * * * [progress]: [ 1 / 8 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (neg.p16 b)))))>
1552126492.528 * * * * [progress]: [ 2 / 8 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>
1552126492.529 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1552126492.529 * * [simplify]: iters left: 5 (12 enodes)
1552126492.532 * * [simplify]: iters left: 4 (31 enodes)
1552126492.538 * * [simplify]: iters left: 3 (64 enodes)
1552126492.551 * * [simplify]: iters left: 2 (183 enodes)
1552126492.636 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126492.636 * * [simplify]: Extracting #1: cost 6 inf + 0
1552126492.636 * * [simplify]: Extracting #2: cost 10 inf + 1
1552126492.637 * * [simplify]: Extracting #3: cost 22 inf + 804
1552126492.637 * * [simplify]: Extracting #4: cost 64 inf + 1445
1552126492.637 * * [simplify]: Extracting #5: cost 132 inf + 3371
1552126492.638 * * [simplify]: Extracting #6: cost 212 inf + 14038
1552126492.643 * * [simplify]: Extracting #7: cost 133 inf + 122101
1552126492.653 * * [simplify]: Extracting #8: cost 13 inf + 330931
1552126492.668 * * [simplify]: Extracting #9: cost 0 inf + 360062
1552126492.695 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1552126492.695 * [simplify]: Simplified (2 2) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)))
1552126492.695 * * * * [progress]: [ 3 / 8 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))>
1552126492.695 * * * * [progress]: [ 4 / 8 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))))))>
1552126492.695 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
1552126492.696 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))
1552126492.696 * * [simplify]: iters left: 6 (21 enodes)
1552126492.709 * * [simplify]: iters left: 5 (61 enodes)
1552126492.733 * * [simplify]: iters left: 4 (154 enodes)
1552126492.772 * * [simplify]: iters left: 3 (373 enodes)
1552126493.021 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126493.022 * * [simplify]: Extracting #1: cost 7 inf + 0
1552126493.022 * * [simplify]: Extracting #2: cost 59 inf + 0
1552126493.022 * * [simplify]: Extracting #3: cost 119 inf + 83
1552126493.023 * * [simplify]: Extracting #4: cost 137 inf + 11032
1552126493.025 * * [simplify]: Extracting #5: cost 183 inf + 27270
1552126493.029 * * [simplify]: Extracting #6: cost 223 inf + 84764
1552126493.041 * * [simplify]: Extracting #7: cost 60 inf + 347389
1552126493.061 * * [simplify]: Extracting #8: cost 1 inf + 460459
1552126493.081 * * [simplify]: Extracting #9: cost 0 inf + 461583
1552126493.101 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a)))
1552126493.101 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))
1552126493.101 * * * * [progress]: [ 6 / 8 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
1552126493.102 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))
1552126493.102 * * [simplify]: iters left: 6 (21 enodes)
1552126493.107 * * [simplify]: iters left: 5 (61 enodes)
1552126493.129 * * [simplify]: iters left: 4 (154 enodes)
1552126493.175 * * [simplify]: iters left: 3 (373 enodes)
1552126493.341 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126493.341 * * [simplify]: Extracting #1: cost 7 inf + 0
1552126493.342 * * [simplify]: Extracting #2: cost 59 inf + 0
1552126493.342 * * [simplify]: Extracting #3: cost 119 inf + 83
1552126493.343 * * [simplify]: Extracting #4: cost 137 inf + 11032
1552126493.345 * * [simplify]: Extracting #5: cost 183 inf + 27270
1552126493.349 * * [simplify]: Extracting #6: cost 223 inf + 84764
1552126493.361 * * [simplify]: Extracting #7: cost 60 inf + 347389
1552126493.379 * * [simplify]: Extracting #8: cost 1 inf + 460459
1552126493.399 * * [simplify]: Extracting #9: cost 0 inf + 461583
1552126493.422 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a)))
1552126493.422 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))
1552126493.422 * * * * [progress]: [ 7 / 8 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
1552126493.422 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))
1552126493.422 * * [simplify]: iters left: 6 (21 enodes)
1552126493.427 * * [simplify]: iters left: 5 (61 enodes)
1552126493.439 * * [simplify]: iters left: 4 (154 enodes)
1552126493.502 * * [simplify]: iters left: 3 (373 enodes)
1552126493.772 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126493.773 * * [simplify]: Extracting #1: cost 7 inf + 0
1552126493.773 * * [simplify]: Extracting #2: cost 59 inf + 0
1552126493.773 * * [simplify]: Extracting #3: cost 119 inf + 83
1552126493.775 * * [simplify]: Extracting #4: cost 137 inf + 11032
1552126493.779 * * [simplify]: Extracting #5: cost 183 inf + 27270
1552126493.787 * * [simplify]: Extracting #6: cost 223 inf + 84764
1552126493.811 * * [simplify]: Extracting #7: cost 60 inf + 347389
1552126493.848 * * [simplify]: Extracting #8: cost 1 inf + 460459
1552126493.869 * * [simplify]: Extracting #9: cost 0 inf + 461583
1552126493.893 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a)))
1552126493.893 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))
1552126493.893 * * * * [progress]: [ 8 / 8 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>
1552126493.893 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))
1552126493.893 * * [simplify]: iters left: 6 (21 enodes)
1552126493.898 * * [simplify]: iters left: 5 (61 enodes)
1552126493.911 * * [simplify]: iters left: 4 (154 enodes)
1552126493.943 * * [simplify]: iters left: 3 (373 enodes)
1552126494.166 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126494.166 * * [simplify]: Extracting #1: cost 7 inf + 0
1552126494.166 * * [simplify]: Extracting #2: cost 59 inf + 0
1552126494.167 * * [simplify]: Extracting #3: cost 119 inf + 83
1552126494.168 * * [simplify]: Extracting #4: cost 137 inf + 11032
1552126494.172 * * [simplify]: Extracting #5: cost 183 inf + 27270
1552126494.180 * * [simplify]: Extracting #6: cost 223 inf + 84764
1552126494.205 * * [simplify]: Extracting #7: cost 60 inf + 347389
1552126494.241 * * [simplify]: Extracting #8: cost 1 inf + 460459
1552126494.280 * * [simplify]: Extracting #9: cost 0 inf + 461583
1552126494.322 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a)))
1552126494.323 * [simplify]: Simplified (2) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))
1552126494.323 * * * [progress]: adding candidates to table
1552126495.029 * [progress]: [Phase 3 of 3] Extracting.
1552126495.030 * * [regime]: Finding splitpoints for: (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<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)))>)
1552126495.037 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
1552126495.038 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<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)))>)
1552126495.656 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<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)))>)
1552126496.277 * * * * [regimes]: Trying to branch on b from (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<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)))>)
1552126496.715 * * * [regime]: Found split indices: #<option (#s(si 1 113) #s(si 2 256))>
1552126496.717 * [binary-search]: Improving bounds with binary search for b and (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<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)))>)
1552126496.718 * [regimes]: Found splitpoints: (#s(sp 1 b #<cpointer:posit16>) #s(sp 2 b +nan.0)) , with alts (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<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)))>)
1552126496.719 * [simplify]: Simplifying (if (<=.p16 b (real->posit16 -0.09344482421875)) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))
1552126496.719 * * [simplify]: iters left: 6 (32 enodes)
1552126496.721 * * [simplify]: Extracting #0: cost 1 inf + 0
1552126496.721 * * [simplify]: Extracting #1: cost 4 inf + 0
1552126496.721 * * [simplify]: Extracting #2: cost 10 inf + 0
1552126496.721 * * [simplify]: Extracting #3: cost 15 inf + 2
1552126496.721 * * [simplify]: Extracting #4: cost 18 inf + 84
1552126496.722 * * [simplify]: Extracting #5: cost 21 inf + 153
1552126496.722 * * [simplify]: Extracting #6: cost 20 inf + 717
1552126496.722 * * [simplify]: Extracting #7: cost 14 inf + 2488
1552126496.722 * * [simplify]: Extracting #8: cost 10 inf + 6943
1552126496.722 * * [simplify]: Extracting #9: cost 8 inf + 8670
1552126496.723 * * [simplify]: Extracting #10: cost 6 inf + 10918
1552126496.723 * * [simplify]: Extracting #11: cost 3 inf + 16091
1552126496.724 * * [simplify]: Extracting #12: cost 2 inf + 17776
1552126496.724 * * [simplify]: Extracting #13: cost 1 inf + 19901
1552126496.725 * * [simplify]: Extracting #14: cost 0 inf + 24597
1552126496.726 * [simplify]: Simplified to (if (<=.p16 b (real->posit16 -0.09344482421875)) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) a))
1552126496.726 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1552126496.763 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
1552126496.766 * * * * [points]: Setting MPFR precision to 64
1552126496.767 * * * * [points]: Setting MPFR precision to 320
1552126496.768 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
1552126496.771 * * * * [points]: Setting MPFR precision to 64
1552126496.773 * * * * [points]: Setting MPFR precision to 320
1552126496.775 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
1552126496.778 * * * * [points]: Setting MPFR precision to 64
1552126496.782 * * * * [points]: Setting MPFR precision to 320
1552126496.788 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
1552126496.790 * * * * [points]: Setting MPFR precision to 64
1552126496.810 * * * * [points]: Setting MPFR precision to 320
1552126496.822 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
1552126496.824 * * * * [points]: Setting MPFR precision to 64
1552126496.843 * * * * [points]: Setting MPFR precision to 320
1552126496.866 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
1552126496.869 * * * * [points]: Setting MPFR precision to 64
1552126496.903 * * * * [points]: Setting MPFR precision to 320
1552126496.978 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
1552126496.981 * * * * [points]: Setting MPFR precision to 64
1552126497.055 * * * * [points]: Setting MPFR precision to 320
1552126497.510 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
1552126497.513 * * * * [points]: Setting MPFR precision to 64
1552126497.686 * * * * [points]: Setting MPFR precision to 320
1552126497.930 * * * * [points]: Computing exacts for 8000 points
1552126497.933 * * * * [points]: Setting MPFR precision to 64
1552126498.901 * * * * [points]: Setting MPFR precision to 320
1552126500.821 * * * * [points]: Filtering points with unrepresentable outputs
1552126501.601 * * * * [points]: Sampling 2304 additional inputs, on iter 1 have 5696 / 8000
1552126501.612 * * * * [points]: Computing exacts on every 144 of 2304 points to ramp up precision
1552126501.615 * * * * [points]: Setting MPFR precision to 64
1552126501.616 * * * * [points]: Setting MPFR precision to 320
1552126501.618 * * * * [points]: Computing exacts on every 72 of 2304 points to ramp up precision
1552126501.623 * * * * [points]: Setting MPFR precision to 64
1552126501.627 * * * * [points]: Setting MPFR precision to 320
1552126501.632 * * * * [points]: Computing exacts on every 36 of 2304 points to ramp up precision
1552126501.637 * * * * [points]: Setting MPFR precision to 64
1552126501.645 * * * * [points]: Setting MPFR precision to 320
1552126501.654 * * * * [points]: Computing exacts on every 18 of 2304 points to ramp up precision
1552126501.679 * * * * [points]: Setting MPFR precision to 64
1552126501.689 * * * * [points]: Setting MPFR precision to 320
1552126501.699 * * * * [points]: Computing exacts on every 9 of 2304 points to ramp up precision
1552126501.702 * * * * [points]: Setting MPFR precision to 64
1552126501.725 * * * * [points]: Setting MPFR precision to 320
1552126501.745 * * * * [points]: Computing exacts on every 4 of 2304 points to ramp up precision
1552126501.748 * * * * [points]: Setting MPFR precision to 64
1552126501.780 * * * * [points]: Setting MPFR precision to 320
1552126501.876 * * * * [points]: Computing exacts on every 2 of 2304 points to ramp up precision
1552126501.879 * * * * [points]: Setting MPFR precision to 64
1552126501.977 * * * * [points]: Setting MPFR precision to 320
1552126502.133 * * * * [points]: Computing exacts for 2304 points
1552126502.139 * * * * [points]: Setting MPFR precision to 64
1552126502.409 * * * * [points]: Setting MPFR precision to 320
1552126502.785 * * * * [points]: Filtering points with unrepresentable outputs
1552126503.002 * * * * [points]: Sampling 691 additional inputs, on iter 2 have 7309 / 8000
1552126503.007 * * * * [points]: Computing exacts on every 43 of 691 points to ramp up precision
1552126503.013 * * * * [points]: Setting MPFR precision to 64
1552126503.016 * * * * [points]: Setting MPFR precision to 320
1552126503.018 * * * * [points]: Computing exacts on every 21 of 691 points to ramp up precision
1552126503.023 * * * * [points]: Setting MPFR precision to 64
1552126503.027 * * * * [points]: Setting MPFR precision to 320
1552126503.032 * * * * [points]: Computing exacts on every 10 of 691 points to ramp up precision
1552126503.037 * * * * [points]: Setting MPFR precision to 64
1552126503.045 * * * * [points]: Setting MPFR precision to 320
1552126503.054 * * * * [points]: Computing exacts on every 5 of 691 points to ramp up precision
1552126503.059 * * * * [points]: Setting MPFR precision to 64
1552126503.073 * * * * [points]: Setting MPFR precision to 320
1552126503.092 * * * * [points]: Computing exacts on every 2 of 691 points to ramp up precision
1552126503.096 * * * * [points]: Setting MPFR precision to 64
1552126503.126 * * * * [points]: Setting MPFR precision to 320
1552126503.165 * * * * [points]: Computing exacts for 691 points
1552126503.193 * * * * [points]: Setting MPFR precision to 64
1552126503.249 * * * * [points]: Setting MPFR precision to 320
1552126503.309 * * * * [points]: Filtering points with unrepresentable outputs
1552126503.374 * * * * [points]: Sampling 220 additional inputs, on iter 3 have 7780 / 8000
1552126503.376 * * * * [points]: Computing exacts on every 13 of 220 points to ramp up precision
1552126503.381 * * * * [points]: Setting MPFR precision to 64
1552126503.383 * * * * [points]: Setting MPFR precision to 320
1552126503.385 * * * * [points]: Computing exacts on every 6 of 220 points to ramp up precision
1552126503.391 * * * * [points]: Setting MPFR precision to 64
1552126503.396 * * * * [points]: Setting MPFR precision to 320
1552126503.401 * * * * [points]: Computing exacts on every 3 of 220 points to ramp up precision
1552126503.406 * * * * [points]: Setting MPFR precision to 64
1552126503.412 * * * * [points]: Setting MPFR precision to 320
1552126503.421 * * * * [points]: Computing exacts for 220 points
1552126503.426 * * * * [points]: Setting MPFR precision to 64
1552126503.453 * * * * [points]: Setting MPFR precision to 320
1552126503.487 * * * * [points]: Filtering points with unrepresentable outputs
1552126503.507 * * * * [points]: Sampling 60 additional inputs, on iter 4 have 7940 / 8000
1552126503.507 * * * * [points]: Computing exacts on every 3 of 60 points to ramp up precision
1552126503.512 * * * * [points]: Setting MPFR precision to 64
1552126503.514 * * * * [points]: Setting MPFR precision to 320
1552126503.517 * * * * [points]: Computing exacts for 60 points
1552126503.522 * * * * [points]: Setting MPFR precision to 64
1552126503.565 * * * * [points]: Setting MPFR precision to 320
1552126503.577 * * * * [points]: Filtering points with unrepresentable outputs
1552126503.583 * * * * [points]: Sampling 18 additional inputs, on iter 5 have 7982 / 8000
1552126503.583 * * * * [points]: Computing exacts for 18 points
1552126503.588 * * * * [points]: Setting MPFR precision to 64
1552126503.591 * * * * [points]: Setting MPFR precision to 320
1552126503.593 * * * * [points]: Filtering points with unrepresentable outputs
1552126503.595 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 7997 / 8000
1552126503.595 * * * * [points]: Computing exacts for 4 points
1552126503.600 * * * * [points]: Setting MPFR precision to 64
1552126503.601 * * * * [points]: Setting MPFR precision to 320
1552126503.602 * * * * [points]: Filtering points with unrepresentable outputs
1552126503.602 * * * * [points]: Sampled 8000 points with exact outputs
1552126514.770 * [regime-testing]: Baseline error score: 64.0
1552126514.774 * [regime-testing]: Oracle error score: 64.0
1552126514.783 * [regime-testing]: End program error score: 0.777480987125932