1554304901.523 * [misc]progress:  [Phase 1 of 3] Setting up.
1554304901.524 * * * [misc]progress:  [1/2] Preparing points
1554304901.526 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1554304901.529 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1554304901.783 * * * * [misc]points:  Setting MPFR precision to 64
1554304901.786 * * * * [misc]points:  Setting MPFR precision to 320
1554304901.788 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1554304901.792 * * * * [misc]points:  Setting MPFR precision to 64
1554304901.794 * * * * [misc]points:  Setting MPFR precision to 320
1554304901.799 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1554304901.803 * * * * [misc]points:  Setting MPFR precision to 64
1554304901.809 * * * * [misc]points:  Setting MPFR precision to 320
1554304901.815 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1554304901.820 * * * * [misc]points:  Setting MPFR precision to 64
1554304901.831 * * * * [misc]points:  Setting MPFR precision to 320
1554304901.842 * * * * [misc]points:  Computing exacts for 256 points
1554304901.848 * * * * [misc]points:  Setting MPFR precision to 64
1554304901.934 * * * * [misc]points:  Setting MPFR precision to 320
1554304901.969 * * * * [misc]points:  Filtering points with unrepresentable outputs
1554304901.971 * * * * [exit]points:  Sampled 256 points with exact outputs
1554304901.971 * * * [misc]progress:  [2/2] Setting up program.
1554304902.007 * [misc]progress:  [Phase 2 of 3] Improving.
1554304902.007 * * * * [misc]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)))>
1554304902.009 * [enter]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))
1554304902.011 * * [misc]simplify:  iters left: 6 (16 enodes)
1554304902.024 * * [misc]simplify:  iters left: 5 (45 enodes)
1554304902.041 * * [misc]simplify:  iters left: 4 (91 enodes)
1554304902.081 * * [misc]simplify:  iters left: 3 (310 enodes)
1554304903.099 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304903.100 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554304903.101 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554304903.102 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554304903.104 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554304903.110 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554304903.136 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554304903.186 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554304903.229 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554304903.271 * [exit]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))
1554304903.271 * [misc]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)))
1554304903.306 * * [misc]progress:  iteration 1 / 4
1554304903.306 * * * [misc]progress:  picking best candidate
1554304903.336 * * * * [misc]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)))>
1554304903.336 * * * [misc]progress:  localizing error
1554304903.558 * * * [misc]progress:  generating rewritten candidates
1554304903.558 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1554304903.561 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1554304903.562 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1554304903.565 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1 2)
1554304903.568 * * * [misc]progress:  generating series expansions
1554304903.568 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1554304903.568 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1554304903.568 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1554304903.568 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1 2)
1554304903.568 * * * [misc]progress:  simplifying candidates
1554304903.568 * * * * [misc]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)))>
1554304903.569 * * * * [misc]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)))>
1554304903.569 * * * * [misc]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))>
1554304903.569 * * * * [misc]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))))))))>
1554304903.569 * [enter]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))))))
1554304903.569 * * [misc]simplify:  iters left: 6 (14 enodes)
1554304903.573 * * [misc]simplify:  iters left: 5 (42 enodes)
1554304903.581 * * [misc]simplify:  iters left: 4 (117 enodes)
1554304903.633 * * [misc]simplify:  iters left: 3 (426 enodes)
1554304903.882 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304903.882 * * [misc]simplify:  Extracting #1: cost 51 inf + 0
1554304903.883 * * [misc]simplify:  Extracting #2: cost 242 inf + 0
1554304903.884 * * [misc]simplify:  Extracting #3: cost 408 inf + 4895
1554304903.896 * * [misc]simplify:  Extracting #4: cost 386 inf + 288425
1554304903.945 * * [misc]simplify:  Extracting #5: cost 133 inf + 992840
1554304904.038 * * [misc]simplify:  Extracting #6: cost 2 inf + 1243260
1554304904.135 * * [misc]simplify:  Extracting #7: cost 0 inf + 1250148
1554304904.256 * [exit]simplify:  Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
1554304904.256 * [misc]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))))))))
1554304904.257 * * * * [misc]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)))>
1554304904.257 * * * * [misc]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)))>
1554304904.257 * * * * [misc]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)))>
1554304904.257 * [enter]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))
1554304904.257 * * [misc]simplify:  iters left: 6 (16 enodes)
1554304904.265 * * [misc]simplify:  iters left: 5 (45 enodes)
1554304904.275 * * [misc]simplify:  iters left: 4 (91 enodes)
1554304904.297 * * [misc]simplify:  iters left: 3 (310 enodes)
1554304904.462 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304904.462 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554304904.463 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554304904.464 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554304904.466 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554304904.472 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554304904.491 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554304904.540 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554304904.604 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554304904.646 * [exit]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))
1554304904.646 * [misc]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)))
1554304904.646 * * * * [misc]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)))>
1554304904.647 * [enter]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))
1554304904.647 * * [misc]simplify:  iters left: 6 (16 enodes)
1554304904.651 * * [misc]simplify:  iters left: 5 (45 enodes)
1554304904.668 * * [misc]simplify:  iters left: 4 (91 enodes)
1554304904.706 * * [misc]simplify:  iters left: 3 (310 enodes)
1554304904.870 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304904.870 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554304904.870 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554304904.872 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554304904.874 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554304904.880 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554304904.914 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554304904.948 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554304904.985 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554304905.049 * [exit]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))
1554304905.049 * [misc]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)))
1554304905.050 * * * * [misc]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)))>
1554304905.050 * [enter]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))
1554304905.050 * * [misc]simplify:  iters left: 6 (16 enodes)
1554304905.058 * * [misc]simplify:  iters left: 5 (45 enodes)
1554304905.070 * * [misc]simplify:  iters left: 4 (91 enodes)
1554304905.091 * * [misc]simplify:  iters left: 3 (310 enodes)
1554304905.255 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304905.255 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554304905.255 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554304905.256 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554304905.257 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554304905.260 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554304905.284 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554304905.320 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554304905.367 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554304905.412 * [exit]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))
1554304905.412 * [misc]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)))
1554304905.412 * * * * [misc]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)))>
1554304905.412 * [enter]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))
1554304905.412 * * [misc]simplify:  iters left: 6 (16 enodes)
1554304905.416 * * [misc]simplify:  iters left: 5 (45 enodes)
1554304905.425 * * [misc]simplify:  iters left: 4 (91 enodes)
1554304905.453 * * [misc]simplify:  iters left: 3 (310 enodes)
1554304905.594 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304905.594 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554304905.594 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554304905.595 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554304905.596 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554304905.599 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554304905.618 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554304905.658 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554304905.700 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554304905.759 * [exit]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))
1554304905.759 * [misc]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)))
1554304905.760 * * * [misc]progress:  adding candidates to table
1554304906.196 * * [misc]progress:  iteration 2 / 4
1554304906.196 * * * [misc]progress:  picking best candidate
1554304906.265 * * * * [misc]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))>
1554304906.265 * * * [misc]progress:  localizing error
1554304906.319 * * * [misc]progress:  generating rewritten candidates
1554304906.319 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1)
1554304906.321 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1 2)
1554304906.321 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 1 2 1 2)
1554304906.323 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1554304906.326 * * * [misc]progress:  generating series expansions
1554304906.326 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1)
1554304906.326 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1 2)
1554304906.326 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 1 2 1 2)
1554304906.326 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1554304906.326 * * * [misc]progress:  simplifying candidates
1554304906.326 * * * * [misc]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))>
1554304906.326 * * * * [misc]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))>
1554304906.326 * * * * [misc]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))>
1554304906.326 * * * * [misc]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))>
1554304906.326 * * * * [misc]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))))>
1554304906.326 * [enter]simplify:  Simplifying (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1554304906.326 * * [misc]simplify:  iters left: 5 (12 enodes)
1554304906.329 * * [misc]simplify:  iters left: 4 (37 enodes)
1554304906.336 * * [misc]simplify:  iters left: 3 (79 enodes)
1554304906.368 * * [misc]simplify:  iters left: 2 (262 enodes)
1554304906.488 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304906.488 * * [misc]simplify:  Extracting #1: cost 17 inf + 0
1554304906.488 * * [misc]simplify:  Extracting #2: cost 88 inf + 1
1554304906.489 * * [misc]simplify:  Extracting #3: cost 166 inf + 804
1554304906.491 * * [misc]simplify:  Extracting #4: cost 230 inf + 3734
1554304906.496 * * [misc]simplify:  Extracting #5: cost 225 inf + 64494
1554304906.527 * * [misc]simplify:  Extracting #6: cost 137 inf + 332479
1554304906.571 * * [misc]simplify:  Extracting #7: cost 1 inf + 596662
1554304906.599 * * [misc]simplify:  Extracting #8: cost 0 inf + 599226
1554304906.630 * [exit]simplify:  Simplified to (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))
1554304906.630 * [misc]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))))
1554304906.631 * * * * [misc]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))>
1554304906.631 * * * * [misc]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))>
1554304906.631 * * * * [misc]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))>
1554304906.631 * * * * [misc]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))>
1554304906.631 * * * [misc]progress:  adding candidates to table
1554304907.028 * * [misc]progress:  iteration 3 / 4
1554304907.028 * * * [misc]progress:  picking best candidate
1554304907.121 * * * * [misc]pick:  Picked  #<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)))>
1554304907.121 * * * [misc]progress:  localizing error
1554304907.255 * * * [misc]progress:  generating rewritten candidates
1554304907.255 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1554304907.257 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1554304907.257 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1554304907.260 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1)
1554304907.262 * * * [misc]progress:  generating series expansions
1554304907.262 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1554304907.263 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1554304907.263 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1554304907.263 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1)
1554304907.263 * * * [misc]progress:  simplifying candidates
1554304907.263 * * * * [misc]progress:  [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))>
1554304907.263 * * * * [misc]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 (*.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))))) (*.p16 (real->posit16 2) a)))>
1554304907.263 * * * * [misc]progress:  [ 3 / 10 ] 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))>
1554304907.263 * * * * [misc]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 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) 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)))))))>
1554304907.263 * [enter]simplify:  Simplifying (-.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)))))
1554304907.263 * * [misc]simplify:  iters left: 6 (14 enodes)
1554304907.267 * * [misc]simplify:  iters left: 5 (42 enodes)
1554304907.275 * * [misc]simplify:  iters left: 4 (117 enodes)
1554304907.316 * * [misc]simplify:  iters left: 3 (432 enodes)
1554304907.599 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304907.599 * * [misc]simplify:  Extracting #1: cost 51 inf + 0
1554304907.600 * * [misc]simplify:  Extracting #2: cost 242 inf + 0
1554304907.603 * * [misc]simplify:  Extracting #3: cost 412 inf + 3092
1554304907.622 * * [misc]simplify:  Extracting #4: cost 427 inf + 239293
1554304907.703 * * [misc]simplify:  Extracting #5: cost 159 inf + 940878
1554304907.829 * * [misc]simplify:  Extracting #6: cost 1 inf + 1259592
1554304907.908 * * [misc]simplify:  Extracting #7: cost 0 inf + 1262236
1554304908.033 * [exit]simplify:  Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4))))
1554304908.033 * [misc]simplify:  Simplified (2 1) to (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4)))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))
1554304908.034 * * * * [misc]progress:  [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))>
1554304908.034 * * * * [misc]progress:  [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))>
1554304908.034 * * * * [misc]progress:  [ 7 / 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)))>
1554304908.034 * * * * [misc]progress:  [ 8 / 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)))>
1554304908.034 * * * * [misc]progress:  [ 9 / 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)))>
1554304908.034 * * * * [misc]progress:  [ 10 / 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)))>
1554304908.034 * * * [misc]progress:  adding candidates to table
1554304908.686 * * [misc]progress:  iteration 4 / 4
1554304908.687 * * * [misc]progress:  picking best candidate
1554304908.837 * * * * [misc]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))))))))>
1554304908.837 * * * [misc]progress:  localizing error
1554304909.031 * * * [misc]progress:  generating rewritten candidates
1554304909.031 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2)
1554304909.038 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2)
1554304909.044 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 2)
1554304909.044 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2 2 2 1 2)
1554304909.048 * * * [misc]progress:  generating series expansions
1554304909.048 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2)
1554304909.048 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2)
1554304909.048 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 2)
1554304909.048 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2 2 2 1 2)
1554304909.048 * * * [misc]progress:  simplifying candidates
1554304909.048 * * * * [misc]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)))))>
1554304909.048 * * * * [misc]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)))))))>
1554304909.049 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1554304909.049 * * [misc]simplify:  iters left: 5 (12 enodes)
1554304909.054 * * [misc]simplify:  iters left: 4 (31 enodes)
1554304909.066 * * [misc]simplify:  iters left: 3 (64 enodes)
1554304909.093 * * [misc]simplify:  iters left: 2 (183 enodes)
1554304909.212 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304909.212 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1554304909.212 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1554304909.212 * * [misc]simplify:  Extracting #3: cost 22 inf + 804
1554304909.212 * * [misc]simplify:  Extracting #4: cost 64 inf + 1445
1554304909.212 * * [misc]simplify:  Extracting #5: cost 132 inf + 3371
1554304909.214 * * [misc]simplify:  Extracting #6: cost 212 inf + 14038
1554304909.218 * * [misc]simplify:  Extracting #7: cost 133 inf + 122101
1554304909.230 * * [misc]simplify:  Extracting #8: cost 13 inf + 330931
1554304909.254 * * [misc]simplify:  Extracting #9: cost 0 inf + 360062
1554304909.269 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1554304909.269 * [misc]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)))
1554304909.269 * * * * [misc]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)))))))>
1554304909.269 * * * * [misc]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))))))))>
1554304909.270 * * * * [misc]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))))))))>
1554304909.270 * [enter]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)))))))
1554304909.270 * * [misc]simplify:  iters left: 6 (21 enodes)
1554304909.275 * * [misc]simplify:  iters left: 5 (61 enodes)
1554304909.294 * * [misc]simplify:  iters left: 4 (154 enodes)
1554304909.359 * * [misc]simplify:  iters left: 3 (373 enodes)
1554304909.580 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304909.580 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554304909.580 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1554304909.581 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1554304909.583 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1554304909.586 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1554304909.595 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1554304909.621 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1554304909.653 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1554304909.679 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1554304909.722 * [exit]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)))
1554304909.722 * [misc]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))))
1554304909.722 * * * * [misc]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))))))))>
1554304909.723 * [enter]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)))))))
1554304909.723 * * [misc]simplify:  iters left: 6 (21 enodes)
1554304909.733 * * [misc]simplify:  iters left: 5 (61 enodes)
1554304909.757 * * [misc]simplify:  iters left: 4 (154 enodes)
1554304909.796 * * [misc]simplify:  iters left: 3 (373 enodes)
1554304909.976 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304909.976 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554304909.977 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1554304909.978 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1554304909.979 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1554304909.983 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1554304909.992 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1554304910.007 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1554304910.028 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1554304910.067 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1554304910.108 * [exit]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)))
1554304910.108 * [misc]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))))
1554304910.108 * * * * [misc]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))))))))>
1554304910.108 * [enter]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)))))))
1554304910.109 * * [misc]simplify:  iters left: 6 (21 enodes)
1554304910.119 * * [misc]simplify:  iters left: 5 (61 enodes)
1554304910.146 * * [misc]simplify:  iters left: 4 (154 enodes)
1554304910.214 * * [misc]simplify:  iters left: 3 (373 enodes)
1554304910.381 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304910.381 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554304910.381 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1554304910.382 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1554304910.383 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1554304910.385 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1554304910.389 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1554304910.403 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1554304910.436 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1554304910.479 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1554304910.519 * [exit]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)))
1554304910.519 * [misc]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))))
1554304910.520 * * * * [misc]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))))))))>
1554304910.520 * [enter]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)))))))
1554304910.520 * * [misc]simplify:  iters left: 6 (21 enodes)
1554304910.530 * * [misc]simplify:  iters left: 5 (61 enodes)
1554304910.555 * * [misc]simplify:  iters left: 4 (154 enodes)
1554304910.618 * * [misc]simplify:  iters left: 3 (373 enodes)
1554304910.887 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304910.887 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554304910.887 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1554304910.888 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1554304910.890 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1554304910.894 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1554304910.904 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1554304910.932 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1554304910.970 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1554304911.002 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1554304911.022 * [exit]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)))
1554304911.022 * [misc]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))))
1554304911.023 * * * [misc]progress:  adding candidates to table
1554304911.335 * [misc]progress:  [Phase 3 of 3] Extracting.
1554304911.335 * * [misc]regime:  Finding splitpoints for: (#<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))> #<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))> #<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) (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 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))> #<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 (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))> #<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))>)
1554304911.338 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b)
1554304911.339 * * * * [misc]regimes:  Trying to branch on c from (#<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))> #<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))> #<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) (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 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))> #<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 (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))> #<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))>)
1554304911.546 * * * * [misc]regimes:  Trying to branch on a from (#<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))> #<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))> #<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) (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 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))> #<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 (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))> #<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))>)
1554304911.749 * * * * [misc]regimes:  Trying to branch on b from (#<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))> #<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))> #<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) (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 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))> #<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 (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))> #<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))>)
1554304911.967 * * * [misc]regime:  Found split indices: #<option (#s(si 2 83) #s(si 1 256))>
1554304911.969 * [misc]binary-search:  Improving bounds with binary search for b and (#<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))> #<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))> #<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) (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 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))> #<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 (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))> #<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))>)
1554304911.969 * [misc]regimes:  Found splitpoints: (#s(sp 2 b #<cpointer:posit16>) #s(sp 1 b +nan.0)) , with alts (#<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))> #<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))> #<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) (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 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))> #<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 (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))> #<alt (λ (a b c) (/.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))))) (*.p16 (real->posit16 2) a)))>)
1554304911.970 * [enter]simplify:  Simplifying (if (<=.p16 b (real->posit16 -0.2218017578125)) (/.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 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))
1554304911.970 * * [misc]simplify:  iters left: 6 (28 enodes)
1554304911.972 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554304911.972 * * [misc]simplify:  Extracting #1: cost 4 inf + 0
1554304911.972 * * [misc]simplify:  Extracting #2: cost 10 inf + 0
1554304911.972 * * [misc]simplify:  Extracting #3: cost 15 inf + 2
1554304911.972 * * [misc]simplify:  Extracting #4: cost 17 inf + 84
1554304911.972 * * [misc]simplify:  Extracting #5: cost 19 inf + 153
1554304911.972 * * [misc]simplify:  Extracting #6: cost 17 inf + 717
1554304911.973 * * [misc]simplify:  Extracting #7: cost 10 inf + 2488
1554304911.973 * * [misc]simplify:  Extracting #8: cost 7 inf + 6621
1554304911.973 * * [misc]simplify:  Extracting #9: cost 5 inf + 8949
1554304911.974 * * [misc]simplify:  Extracting #10: cost 3 inf + 11838
1554304911.974 * * [misc]simplify:  Extracting #11: cost 1 inf + 16808
1554304911.975 * * [misc]simplify:  Extracting #12: cost 0 inf + 20744
1554304911.975 * [exit]simplify:  Simplified to (if (<=.p16 b (real->posit16 -0.2218017578125)) (/.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 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))
1554304911.975 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1554304912.010 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1554304912.012 * * * * [misc]points:  Setting MPFR precision to 64
1554304912.014 * * * * [misc]points:  Setting MPFR precision to 320
1554304912.015 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1554304912.017 * * * * [misc]points:  Setting MPFR precision to 64
1554304912.021 * * * * [misc]points:  Setting MPFR precision to 320
1554304912.025 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1554304912.031 * * * * [misc]points:  Setting MPFR precision to 64
1554304912.038 * * * * [misc]points:  Setting MPFR precision to 320
1554304912.046 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1554304912.051 * * * * [misc]points:  Setting MPFR precision to 64
1554304912.066 * * * * [misc]points:  Setting MPFR precision to 320
1554304912.081 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1554304912.086 * * * * [misc]points:  Setting MPFR precision to 64
1554304912.148 * * * * [misc]points:  Setting MPFR precision to 320
1554304912.178 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1554304912.184 * * * * [misc]points:  Setting MPFR precision to 64
1554304912.247 * * * * [misc]points:  Setting MPFR precision to 320
1554304912.310 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1554304912.315 * * * * [misc]points:  Setting MPFR precision to 64
1554304912.496 * * * * [misc]points:  Setting MPFR precision to 320
1554304912.680 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1554304912.685 * * * * [misc]points:  Setting MPFR precision to 64
1554304912.986 * * * * [misc]points:  Setting MPFR precision to 320
1554304913.296 * * * * [misc]points:  Computing exacts for 8000 points
1554304913.302 * * * * [misc]points:  Setting MPFR precision to 64
1554304914.586 * * * * [misc]points:  Setting MPFR precision to 320
1554304915.496 * * * * [misc]points:  Filtering points with unrepresentable outputs
1554304915.516 * * * * [exit]points:  Sampled 8000 points with exact outputs
1554304924.377 * [misc]regime-testing:  Baseline error score: 64.0
1554304924.381 * [misc]regime-testing:  Oracle error score: 64.0
1554304924.390 * [misc]regime-testing:  End program error score: 0.5616442814262933