1552123016.371 * [progress]: [Phase 1 of 3] Setting up.
1552123016.372 * * * [progress]: [1/2] Preparing points
1552123016.406 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
1552123016.421 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
1552123016.522 * * * * [points]: Setting MPFR precision to 64
1552123016.559 * * * * [points]: Setting MPFR precision to 320
1552123016.563 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
1552123016.571 * * * * [points]: Setting MPFR precision to 64
1552123016.575 * * * * [points]: Setting MPFR precision to 320
1552123016.581 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
1552123016.584 * * * * [points]: Setting MPFR precision to 64
1552123016.587 * * * * [points]: Setting MPFR precision to 320
1552123016.592 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
1552123016.597 * * * * [points]: Setting MPFR precision to 64
1552123016.608 * * * * [points]: Setting MPFR precision to 320
1552123016.672 * * * * [points]: Computing exacts for 256 points
1552123016.679 * * * * [points]: Setting MPFR precision to 64
1552123016.710 * * * * [points]: Setting MPFR precision to 320
1552123016.741 * * * * [points]: Filtering points with unrepresentable outputs
1552123016.754 * * * * [points]: Sampling 64 additional inputs, on iter 1 have 192 / 256
1552123016.754 * * * * [points]: Computing exacts on every 4 of 64 points to ramp up precision
1552123016.757 * * * * [points]: Setting MPFR precision to 64
1552123016.758 * * * * [points]: Setting MPFR precision to 320
1552123016.759 * * * * [points]: Computing exacts on every 2 of 64 points to ramp up precision
1552123016.761 * * * * [points]: Setting MPFR precision to 64
1552123016.764 * * * * [points]: Setting MPFR precision to 320
1552123016.768 * * * * [points]: Computing exacts for 64 points
1552123016.772 * * * * [points]: Setting MPFR precision to 64
1552123016.780 * * * * [points]: Setting MPFR precision to 320
1552123016.790 * * * * [points]: Filtering points with unrepresentable outputs
1552123016.795 * * * * [points]: Sampling 19 additional inputs, on iter 2 have 237 / 256
1552123016.795 * * * * [points]: Computing exacts for 19 points
1552123016.800 * * * * [points]: Setting MPFR precision to 64
1552123016.803 * * * * [points]: Setting MPFR precision to 320
1552123016.806 * * * * [points]: Filtering points with unrepresentable outputs
1552123016.808 * * * * [points]: Sampling 4 additional inputs, on iter 3 have 252 / 256
1552123016.808 * * * * [points]: Computing exacts for 4 points
1552123016.815 * * * * [points]: Setting MPFR precision to 64
1552123016.816 * * * * [points]: Setting MPFR precision to 320
1552123016.817 * * * * [points]: Filtering points with unrepresentable outputs
1552123016.817 * * * * [points]: Sampling 4 additional inputs, on iter 4 have 255 / 256
1552123016.817 * * * * [points]: Computing exacts for 4 points
1552123016.822 * * * * [points]: Setting MPFR precision to 64
1552123016.823 * * * * [points]: Setting MPFR precision to 320
1552123016.824 * * * * [points]: Filtering points with unrepresentable outputs
1552123016.824 * * * * [points]: Sampled 258 points with exact outputs
1552123016.825 * * * [progress]: [2/2] Setting up program.
1552123016.908 * [progress]: [Phase 2 of 3] Improving.
1552123016.908 * * * * [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)))>
1552123016.910 * [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))
1552123016.912 * * [simplify]: iters left: 6 (16 enodes)
1552123016.924 * * [simplify]: iters left: 5 (45 enodes)
1552123016.941 * * [simplify]: iters left: 4 (91 enodes)
1552123016.982 * * [simplify]: iters left: 3 (310 enodes)
1552123017.121 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123017.121 * * [simplify]: Extracting #1: cost 31 inf + 0
1552123017.122 * * [simplify]: Extracting #2: cost 123 inf + 1
1552123017.122 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552123017.123 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552123017.127 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552123017.141 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552123017.171 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552123017.217 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552123017.247 * [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))
1552123017.247 * [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)))
1552123017.275 * * [progress]: iteration 1 / 4
1552123017.275 * * * [progress]: picking best candidate
1552123017.300 * * * * [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)))>
1552123017.300 * * * [progress]: localizing error
1552123017.621 * * * [progress]: generating rewritten candidates
1552123017.621 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1552123017.624 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1552123017.624 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1552123017.627 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1 2)
1552123017.630 * * * [progress]: generating series expansions
1552123017.631 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1552123017.631 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1552123017.631 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1552123017.631 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1 2)
1552123017.631 * * * [progress]: simplifying candidates
1552123017.631 * * * * [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)))>
1552123017.631 * * * * [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)))>
1552123017.631 * * * * [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))>
1552123017.631 * * * * [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))))))))>
1552123017.632 * [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))))))
1552123017.632 * * [simplify]: iters left: 6 (14 enodes)
1552123017.635 * * [simplify]: iters left: 5 (42 enodes)
1552123017.642 * * [simplify]: iters left: 4 (117 enodes)
1552123017.669 * * [simplify]: iters left: 3 (426 enodes)
1552123017.875 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123017.875 * * [simplify]: Extracting #1: cost 51 inf + 0
1552123017.876 * * [simplify]: Extracting #2: cost 242 inf + 0
1552123017.877 * * [simplify]: Extracting #3: cost 408 inf + 4895
1552123017.892 * * [simplify]: Extracting #4: cost 386 inf + 288425
1552123017.935 * * [simplify]: Extracting #5: cost 133 inf + 992840
1552123018.048 * * [simplify]: Extracting #6: cost 2 inf + 1243260
1552123018.164 * * [simplify]: Extracting #7: cost 0 inf + 1250148
1552123018.251 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
1552123018.251 * [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))))))))
1552123018.251 * * * * [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)))>
1552123018.251 * * * * [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)))>
1552123018.251 * * * * [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)))>
1552123018.252 * [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))
1552123018.252 * * [simplify]: iters left: 6 (16 enodes)
1552123018.260 * * [simplify]: iters left: 5 (45 enodes)
1552123018.276 * * [simplify]: iters left: 4 (91 enodes)
1552123018.314 * * [simplify]: iters left: 3 (310 enodes)
1552123018.478 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123018.478 * * [simplify]: Extracting #1: cost 31 inf + 0
1552123018.479 * * [simplify]: Extracting #2: cost 123 inf + 1
1552123018.480 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552123018.482 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552123018.488 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552123018.516 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552123018.560 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552123018.603 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552123018.644 * [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))
1552123018.644 * [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)))
1552123018.644 * * * * [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)))>
1552123018.645 * [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))
1552123018.645 * * [simplify]: iters left: 6 (16 enodes)
1552123018.653 * * [simplify]: iters left: 5 (45 enodes)
1552123018.669 * * [simplify]: iters left: 4 (91 enodes)
1552123018.690 * * [simplify]: iters left: 3 (310 enodes)
1552123018.823 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123018.823 * * [simplify]: Extracting #1: cost 31 inf + 0
1552123018.823 * * [simplify]: Extracting #2: cost 123 inf + 1
1552123018.825 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552123018.826 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552123018.832 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552123018.859 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552123018.887 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552123018.927 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552123018.966 * [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))
1552123018.966 * [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)))
1552123018.967 * * * * [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)))>
1552123018.967 * [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))
1552123018.967 * * [simplify]: iters left: 6 (16 enodes)
1552123018.974 * * [simplify]: iters left: 5 (45 enodes)
1552123018.990 * * [simplify]: iters left: 4 (91 enodes)
1552123019.010 * * [simplify]: iters left: 3 (310 enodes)
1552123019.159 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123019.159 * * [simplify]: Extracting #1: cost 31 inf + 0
1552123019.160 * * [simplify]: Extracting #2: cost 123 inf + 1
1552123019.161 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552123019.163 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552123019.168 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552123019.197 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552123019.250 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552123019.283 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552123019.343 * [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))
1552123019.344 * [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)))
1552123019.344 * * * * [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)))>
1552123019.344 * [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))
1552123019.344 * * [simplify]: iters left: 6 (16 enodes)
1552123019.352 * * [simplify]: iters left: 5 (45 enodes)
1552123019.362 * * [simplify]: iters left: 4 (91 enodes)
1552123019.382 * * [simplify]: iters left: 3 (310 enodes)
1552123019.547 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123019.547 * * [simplify]: Extracting #1: cost 31 inf + 0
1552123019.547 * * [simplify]: Extracting #2: cost 123 inf + 1
1552123019.549 * * [simplify]: Extracting #3: cost 201 inf + 1129
1552123019.551 * * [simplify]: Extracting #4: cost 263 inf + 9871
1552123019.557 * * [simplify]: Extracting #5: cost 270 inf + 82040
1552123019.589 * * [simplify]: Extracting #6: cost 192 inf + 363234
1552123019.645 * * [simplify]: Extracting #7: cost 15 inf + 679901
1552123019.697 * * [simplify]: Extracting #8: cost 0 inf + 712557
1552123019.729 * [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))
1552123019.729 * [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)))
1552123019.729 * * * [progress]: adding candidates to table
1552123020.298 * * [progress]: iteration 2 / 4
1552123020.298 * * * [progress]: picking best candidate
1552123020.501 * * * * [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))>
1552123020.501 * * * [progress]: localizing error
1552123020.608 * * * [progress]: generating rewritten candidates
1552123020.608 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
1552123020.612 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2)
1552123020.612 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2 1 2)
1552123020.615 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
1552123020.621 * * * [progress]: generating series expansions
1552123020.621 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
1552123020.621 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2)
1552123020.621 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2 1 2)
1552123020.621 * * * * [progress]: [ 4 / 4 ] generating series at (2)
1552123020.621 * * * [progress]: simplifying candidates
1552123020.621 * * * * [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))>
1552123020.621 * * * * [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))>
1552123020.622 * * * * [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))>
1552123020.622 * * * * [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))>
1552123020.622 * * * * [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))))>
1552123020.622 * [simplify]: Simplifying (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1552123020.622 * * [simplify]: iters left: 5 (12 enodes)
1552123020.628 * * [simplify]: iters left: 4 (37 enodes)
1552123020.641 * * [simplify]: iters left: 3 (79 enodes)
1552123020.675 * * [simplify]: iters left: 2 (262 enodes)
1552123020.841 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123020.841 * * [simplify]: Extracting #1: cost 17 inf + 0
1552123020.841 * * [simplify]: Extracting #2: cost 88 inf + 1
1552123020.842 * * [simplify]: Extracting #3: cost 166 inf + 804
1552123020.844 * * [simplify]: Extracting #4: cost 230 inf + 3734
1552123020.848 * * [simplify]: Extracting #5: cost 225 inf + 64494
1552123020.873 * * [simplify]: Extracting #6: cost 137 inf + 332479
1552123020.918 * * [simplify]: Extracting #7: cost 1 inf + 596662
1552123020.969 * * [simplify]: Extracting #8: cost 0 inf + 599226
1552123020.999 * [simplify]: Simplified to (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))
1552123020.999 * [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))))
1552123021.000 * * * * [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))>
1552123021.000 * * * * [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))>
1552123021.000 * * * * [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))>
1552123021.000 * * * * [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))>
1552123021.000 * * * [progress]: adding candidates to table
1552123021.697 * * [progress]: iteration 3 / 4
1552123021.697 * * * [progress]: picking best candidate
1552123021.827 * * * * [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))>
1552123021.827 * * * [progress]: localizing error
1552123022.066 * * * [progress]: generating rewritten candidates
1552123022.066 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
1552123022.068 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2)
1552123022.068 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1552123022.073 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 1)
1552123022.078 * * * [progress]: generating series expansions
1552123022.078 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
1552123022.079 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2)
1552123022.079 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1552123022.079 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 1)
1552123022.079 * * * [progress]: simplifying candidates
1552123022.079 * * * * [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))>
1552123022.079 * * * * [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))>
1552123022.079 * * * * [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))))>
1552123022.079 * [simplify]: Simplifying (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
1552123022.079 * * [simplify]: iters left: 6 (12 enodes)
1552123022.085 * * [simplify]: iters left: 5 (37 enodes)
1552123022.098 * * [simplify]: iters left: 4 (79 enodes)
1552123022.141 * * [simplify]: iters left: 3 (269 enodes)
1552123022.240 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123022.240 * * [simplify]: Extracting #1: cost 17 inf + 0
1552123022.241 * * [simplify]: Extracting #2: cost 88 inf + 1
1552123022.241 * * [simplify]: Extracting #3: cost 168 inf + 804
1552123022.242 * * [simplify]: Extracting #4: cost 235 inf + 2891
1552123022.246 * * [simplify]: Extracting #5: cost 214 inf + 98858
1552123022.276 * * [simplify]: Extracting #6: cost 124 inf + 370436
1552123022.316 * * [simplify]: Extracting #7: cost 4 inf + 597686
1552123022.342 * * [simplify]: Extracting #8: cost 0 inf + 607340
1552123022.375 * [simplify]: Simplified to (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))
1552123022.375 * [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))))
1552123022.376 * * * * [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))>
1552123022.376 * * * * [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))>
1552123022.376 * * * * [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))>
1552123022.376 * * * * [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))>
1552123022.376 * * * * [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))>
1552123022.376 * * * * [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))>
1552123022.376 * * * [progress]: adding candidates to table
1552123023.334 * * [progress]: iteration 4 / 4
1552123023.334 * * * [progress]: picking best candidate
1552123023.586 * * * * [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))))))))>
1552123023.586 * * * [progress]: localizing error
1552123023.942 * * * [progress]: generating rewritten candidates
1552123023.942 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2)
1552123023.947 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
1552123023.953 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2)
1552123023.954 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2 1 2)
1552123023.957 * * * [progress]: generating series expansions
1552123023.957 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2)
1552123023.957 * * * * [progress]: [ 2 / 4 ] generating series at (2)
1552123023.958 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2)
1552123023.958 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2 1 2)
1552123023.958 * * * [progress]: simplifying candidates
1552123023.958 * * * * [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)))))>
1552123023.958 * * * * [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)))))))>
1552123023.958 * [simplify]: Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1552123023.958 * * [simplify]: iters left: 5 (12 enodes)
1552123023.969 * * [simplify]: iters left: 4 (31 enodes)
1552123023.975 * * [simplify]: iters left: 3 (64 enodes)
1552123023.987 * * [simplify]: iters left: 2 (183 enodes)
1552123024.044 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123024.044 * * [simplify]: Extracting #1: cost 6 inf + 0
1552123024.044 * * [simplify]: Extracting #2: cost 10 inf + 1
1552123024.045 * * [simplify]: Extracting #3: cost 22 inf + 804
1552123024.045 * * [simplify]: Extracting #4: cost 64 inf + 1445
1552123024.045 * * [simplify]: Extracting #5: cost 132 inf + 3371
1552123024.046 * * [simplify]: Extracting #6: cost 212 inf + 14038
1552123024.050 * * [simplify]: Extracting #7: cost 133 inf + 122101
1552123024.061 * * [simplify]: Extracting #8: cost 13 inf + 330931
1552123024.075 * * [simplify]: Extracting #9: cost 0 inf + 360062
1552123024.088 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1552123024.088 * [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)))
1552123024.089 * * * * [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)))))))>
1552123024.089 * * * * [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))))))))>
1552123024.089 * * * * [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))))))))>
1552123024.089 * [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)))))))
1552123024.089 * * [simplify]: iters left: 6 (21 enodes)
1552123024.094 * * [simplify]: iters left: 5 (61 enodes)
1552123024.107 * * [simplify]: iters left: 4 (154 enodes)
1552123024.138 * * [simplify]: iters left: 3 (373 enodes)
1552123024.320 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123024.320 * * [simplify]: Extracting #1: cost 7 inf + 0
1552123024.320 * * [simplify]: Extracting #2: cost 59 inf + 0
1552123024.321 * * [simplify]: Extracting #3: cost 119 inf + 83
1552123024.322 * * [simplify]: Extracting #4: cost 137 inf + 11032
1552123024.326 * * [simplify]: Extracting #5: cost 183 inf + 27270
1552123024.334 * * [simplify]: Extracting #6: cost 223 inf + 84764
1552123024.362 * * [simplify]: Extracting #7: cost 60 inf + 347389
1552123024.398 * * [simplify]: Extracting #8: cost 1 inf + 460459
1552123024.435 * * [simplify]: Extracting #9: cost 0 inf + 461583
1552123024.455 * [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)))
1552123024.455 * [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))))
1552123024.455 * * * * [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))))))))>
1552123024.456 * [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)))))))
1552123024.456 * * [simplify]: iters left: 6 (21 enodes)
1552123024.461 * * [simplify]: iters left: 5 (61 enodes)
1552123024.473 * * [simplify]: iters left: 4 (154 enodes)
1552123024.505 * * [simplify]: iters left: 3 (373 enodes)
1552123024.642 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123024.642 * * [simplify]: Extracting #1: cost 7 inf + 0
1552123024.643 * * [simplify]: Extracting #2: cost 59 inf + 0
1552123024.644 * * [simplify]: Extracting #3: cost 119 inf + 83
1552123024.646 * * [simplify]: Extracting #4: cost 137 inf + 11032
1552123024.650 * * [simplify]: Extracting #5: cost 183 inf + 27270
1552123024.658 * * [simplify]: Extracting #6: cost 223 inf + 84764
1552123024.687 * * [simplify]: Extracting #7: cost 60 inf + 347389
1552123024.718 * * [simplify]: Extracting #8: cost 1 inf + 460459
1552123024.737 * * [simplify]: Extracting #9: cost 0 inf + 461583
1552123024.756 * [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)))
1552123024.757 * [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))))
1552123024.757 * * * * [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))))))))>
1552123024.757 * [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)))))))
1552123024.757 * * [simplify]: iters left: 6 (21 enodes)
1552123024.762 * * [simplify]: iters left: 5 (61 enodes)
1552123024.775 * * [simplify]: iters left: 4 (154 enodes)
1552123024.809 * * [simplify]: iters left: 3 (373 enodes)
1552123024.994 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123024.995 * * [simplify]: Extracting #1: cost 7 inf + 0
1552123024.995 * * [simplify]: Extracting #2: cost 59 inf + 0
1552123024.996 * * [simplify]: Extracting #3: cost 119 inf + 83
1552123024.997 * * [simplify]: Extracting #4: cost 137 inf + 11032
1552123025.000 * * [simplify]: Extracting #5: cost 183 inf + 27270
1552123025.011 * * [simplify]: Extracting #6: cost 223 inf + 84764
1552123025.034 * * [simplify]: Extracting #7: cost 60 inf + 347389
1552123025.071 * * [simplify]: Extracting #8: cost 1 inf + 460459
1552123025.110 * * [simplify]: Extracting #9: cost 0 inf + 461583
1552123025.133 * [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)))
1552123025.133 * [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))))
1552123025.134 * * * * [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))))))))>
1552123025.134 * [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)))))))
1552123025.134 * * [simplify]: iters left: 6 (21 enodes)
1552123025.139 * * [simplify]: iters left: 5 (61 enodes)
1552123025.155 * * [simplify]: iters left: 4 (154 enodes)
1552123025.192 * * [simplify]: iters left: 3 (373 enodes)
1552123025.340 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123025.340 * * [simplify]: Extracting #1: cost 7 inf + 0
1552123025.341 * * [simplify]: Extracting #2: cost 59 inf + 0
1552123025.341 * * [simplify]: Extracting #3: cost 119 inf + 83
1552123025.342 * * [simplify]: Extracting #4: cost 137 inf + 11032
1552123025.344 * * [simplify]: Extracting #5: cost 183 inf + 27270
1552123025.351 * * [simplify]: Extracting #6: cost 223 inf + 84764
1552123025.363 * * [simplify]: Extracting #7: cost 60 inf + 347389
1552123025.382 * * [simplify]: Extracting #8: cost 1 inf + 460459
1552123025.408 * * [simplify]: Extracting #9: cost 0 inf + 461583
1552123025.446 * [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)))
1552123025.446 * [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))))
1552123025.447 * * * [progress]: adding candidates to table
1552123026.189 * [progress]: [Phase 3 of 3] Extracting.
1552123026.189 * * [regime]: Finding splitpoints for: (#<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 (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 (*.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 (+.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 (-.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 (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 (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 (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 (/.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))>)
1552123026.196 * * * [regime-changes]: Trying 3 branch expressions: (c a b)
1552123026.197 * * * * [regimes]: Trying to branch on c from (#<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 (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 (*.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 (+.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 (-.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 (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 (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 (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 (/.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))>)
1552123026.804 * * * * [regimes]: Trying to branch on a from (#<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 (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 (*.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 (+.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 (-.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 (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 (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 (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 (/.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))>)
1552123027.288 * * * * [regimes]: Trying to branch on b from (#<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 (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 (*.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 (+.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 (-.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 (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 (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 (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 (/.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))>)
1552123027.848 * * * [regime]: Found split indices: #<option (#s(si 0 113) #s(si 6 256))>
1552123027.851 * [binary-search]: Improving bounds with binary search for b and (#<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 (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 (*.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 (+.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 (-.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 (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 (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 (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 (/.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))>)
1552123027.852 * [regimes]: Found splitpoints: (#s(sp 0 b #<cpointer:posit16>) #s(sp 6 b +nan.0)) , with alts (#<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 (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 (*.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 (+.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 (-.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 (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 (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 (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 (/.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))>)
1552123027.853 * [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))
1552123027.854 * * [simplify]: iters left: 6 (32 enodes)
1552123027.857 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123027.857 * * [simplify]: Extracting #1: cost 4 inf + 0
1552123027.857 * * [simplify]: Extracting #2: cost 10 inf + 0
1552123027.857 * * [simplify]: Extracting #3: cost 15 inf + 2
1552123027.857 * * [simplify]: Extracting #4: cost 18 inf + 84
1552123027.857 * * [simplify]: Extracting #5: cost 21 inf + 153
1552123027.858 * * [simplify]: Extracting #6: cost 20 inf + 717
1552123027.858 * * [simplify]: Extracting #7: cost 14 inf + 2488
1552123027.858 * * [simplify]: Extracting #8: cost 10 inf + 6943
1552123027.859 * * [simplify]: Extracting #9: cost 8 inf + 8670
1552123027.860 * * [simplify]: Extracting #10: cost 6 inf + 10918
1552123027.861 * * [simplify]: Extracting #11: cost 3 inf + 16091
1552123027.862 * * [simplify]: Extracting #12: cost 2 inf + 17776
1552123027.863 * * [simplify]: Extracting #13: cost 1 inf + 19901
1552123027.864 * * [simplify]: Extracting #14: cost 0 inf + 24597
1552123027.865 * [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))
1552123027.865 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1552123027.928 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
1552123027.933 * * * * [points]: Setting MPFR precision to 64
1552123027.935 * * * * [points]: Setting MPFR precision to 320
1552123027.938 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
1552123027.942 * * * * [points]: Setting MPFR precision to 64
1552123027.946 * * * * [points]: Setting MPFR precision to 320
1552123027.950 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
1552123027.956 * * * * [points]: Setting MPFR precision to 64
1552123027.964 * * * * [points]: Setting MPFR precision to 320
1552123027.974 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
1552123027.979 * * * * [points]: Setting MPFR precision to 64
1552123027.996 * * * * [points]: Setting MPFR precision to 320
1552123028.017 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
1552123028.022 * * * * [points]: Setting MPFR precision to 64
1552123028.061 * * * * [points]: Setting MPFR precision to 320
1552123028.082 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
1552123028.084 * * * * [points]: Setting MPFR precision to 64
1552123028.119 * * * * [points]: Setting MPFR precision to 320
1552123028.159 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
1552123028.162 * * * * [points]: Setting MPFR precision to 64
1552123028.302 * * * * [points]: Setting MPFR precision to 320
1552123028.510 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
1552123028.515 * * * * [points]: Setting MPFR precision to 64
1552123028.743 * * * * [points]: Setting MPFR precision to 320
1552123028.979 * * * * [points]: Computing exacts for 8000 points
1552123028.984 * * * * [points]: Setting MPFR precision to 64
1552123030.590 * * * * [points]: Setting MPFR precision to 320
1552123031.498 * * * * [points]: Filtering points with unrepresentable outputs
1552123031.943 * * * * [points]: Sampling 2304 additional inputs, on iter 1 have 5696 / 8000
1552123031.953 * * * * [points]: Computing exacts on every 144 of 2304 points to ramp up precision
1552123031.955 * * * * [points]: Setting MPFR precision to 64
1552123031.956 * * * * [points]: Setting MPFR precision to 320
1552123031.957 * * * * [points]: Computing exacts on every 72 of 2304 points to ramp up precision
1552123031.960 * * * * [points]: Setting MPFR precision to 64
1552123031.962 * * * * [points]: Setting MPFR precision to 320
1552123031.965 * * * * [points]: Computing exacts on every 36 of 2304 points to ramp up precision
1552123031.967 * * * * [points]: Setting MPFR precision to 64
1552123031.972 * * * * [points]: Setting MPFR precision to 320
1552123031.977 * * * * [points]: Computing exacts on every 18 of 2304 points to ramp up precision
1552123031.979 * * * * [points]: Setting MPFR precision to 64
1552123031.987 * * * * [points]: Setting MPFR precision to 320
1552123031.997 * * * * [points]: Computing exacts on every 9 of 2304 points to ramp up precision
1552123031.999 * * * * [points]: Setting MPFR precision to 64
1552123032.035 * * * * [points]: Setting MPFR precision to 320
1552123032.061 * * * * [points]: Computing exacts on every 4 of 2304 points to ramp up precision
1552123032.065 * * * * [points]: Setting MPFR precision to 64
1552123032.122 * * * * [points]: Setting MPFR precision to 320
1552123032.188 * * * * [points]: Computing exacts on every 2 of 2304 points to ramp up precision
1552123032.192 * * * * [points]: Setting MPFR precision to 64
1552123032.310 * * * * [points]: Setting MPFR precision to 320
1552123032.401 * * * * [points]: Computing exacts for 2304 points
1552123032.403 * * * * [points]: Setting MPFR precision to 64
1552123032.715 * * * * [points]: Setting MPFR precision to 320
1552123033.110 * * * * [points]: Filtering points with unrepresentable outputs
1552123033.242 * * * * [points]: Sampling 691 additional inputs, on iter 2 have 7309 / 8000
1552123033.247 * * * * [points]: Computing exacts on every 43 of 691 points to ramp up precision
1552123033.269 * * * * [points]: Setting MPFR precision to 64
1552123033.273 * * * * [points]: Setting MPFR precision to 320
1552123033.275 * * * * [points]: Computing exacts on every 21 of 691 points to ramp up precision
1552123033.280 * * * * [points]: Setting MPFR precision to 64
1552123033.284 * * * * [points]: Setting MPFR precision to 320
1552123033.289 * * * * [points]: Computing exacts on every 10 of 691 points to ramp up precision
1552123033.293 * * * * [points]: Setting MPFR precision to 64
1552123033.301 * * * * [points]: Setting MPFR precision to 320
1552123033.311 * * * * [points]: Computing exacts on every 5 of 691 points to ramp up precision
1552123033.316 * * * * [points]: Setting MPFR precision to 64
1552123033.331 * * * * [points]: Setting MPFR precision to 320
1552123033.348 * * * * [points]: Computing exacts on every 2 of 691 points to ramp up precision
1552123033.353 * * * * [points]: Setting MPFR precision to 64
1552123033.382 * * * * [points]: Setting MPFR precision to 320
1552123033.417 * * * * [points]: Computing exacts for 691 points
1552123033.421 * * * * [points]: Setting MPFR precision to 64
1552123033.522 * * * * [points]: Setting MPFR precision to 320
1552123033.634 * * * * [points]: Filtering points with unrepresentable outputs
1552123033.674 * * * * [points]: Sampling 220 additional inputs, on iter 3 have 7780 / 8000
1552123033.675 * * * * [points]: Computing exacts on every 13 of 220 points to ramp up precision
1552123033.677 * * * * [points]: Setting MPFR precision to 64
1552123034.134 * * * * [points]: Setting MPFR precision to 320
1552123034.137 * * * * [points]: Computing exacts on every 6 of 220 points to ramp up precision
1552123034.144 * * * * [points]: Setting MPFR precision to 64
1552123034.147 * * * * [points]: Setting MPFR precision to 320
1552123034.152 * * * * [points]: Computing exacts on every 3 of 220 points to ramp up precision
1552123034.156 * * * * [points]: Setting MPFR precision to 64
1552123034.163 * * * * [points]: Setting MPFR precision to 320
1552123034.171 * * * * [points]: Computing exacts for 220 points
1552123034.175 * * * * [points]: Setting MPFR precision to 64
1552123034.200 * * * * [points]: Setting MPFR precision to 320
1552123034.231 * * * * [points]: Filtering points with unrepresentable outputs
1552123034.247 * * * * [points]: Sampling 60 additional inputs, on iter 4 have 7940 / 8000
1552123034.248 * * * * [points]: Computing exacts on every 3 of 60 points to ramp up precision
1552123034.252 * * * * [points]: Setting MPFR precision to 64
1552123034.254 * * * * [points]: Setting MPFR precision to 320
1552123034.256 * * * * [points]: Computing exacts for 60 points
1552123034.261 * * * * [points]: Setting MPFR precision to 64
1552123034.268 * * * * [points]: Setting MPFR precision to 320
1552123034.276 * * * * [points]: Filtering points with unrepresentable outputs
1552123034.281 * * * * [points]: Sampling 18 additional inputs, on iter 5 have 7982 / 8000
1552123034.281 * * * * [points]: Computing exacts for 18 points
1552123034.286 * * * * [points]: Setting MPFR precision to 64
1552123034.288 * * * * [points]: Setting MPFR precision to 320
1552123034.291 * * * * [points]: Filtering points with unrepresentable outputs
1552123034.292 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 7997 / 8000
1552123034.293 * * * * [points]: Computing exacts for 4 points
1552123034.297 * * * * [points]: Setting MPFR precision to 64
1552123034.298 * * * * [points]: Setting MPFR precision to 320
1552123034.299 * * * * [points]: Filtering points with unrepresentable outputs
1552123034.299 * * * * [points]: Sampled 8000 points with exact outputs
1552123045.059 * [regime-testing]: Baseline error score: 64.0
1552123045.064 * [regime-testing]: Oracle error score: 64.0
1552123045.080 * [regime-testing]: End program error score: 0.777480987125932