1550842780.634 * [misc]progress:  [Phase 1 of 3] Setting up.
1550842780.636 * * * [misc]progress:  [1/2] Preparing points
1550842780.637 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1550842780.645 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1550842780.739 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.743 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.746 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1550842780.751 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.754 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.758 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1550842780.763 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.769 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.775 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1550842780.780 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.789 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.800 * * * * [misc]points:  Computing exacts for 256 points
1550842780.805 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.832 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.166 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.185 * * * * [misc]points:  Sampling 80 additional inputs, on iter 1 have 176 / 256
1550842781.186 * * * * [misc]points:  Computing exacts on every 5 of 80 points to ramp up precision
1550842781.191 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.192 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.194 * * * * [misc]points:  Computing exacts on every 2 of 80 points to ramp up precision
1550842781.199 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.202 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.206 * * * * [misc]points:  Computing exacts for 80 points
1550842781.213 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.222 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.233 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.240 * * * * [misc]points:  Sampling 19 additional inputs, on iter 2 have 237 / 256
1550842781.240 * * * * [misc]points:  Computing exacts for 19 points
1550842781.245 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.247 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.250 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.252 * * * * [misc]points:  Sampling 4 additional inputs, on iter 3 have 253 / 256
1550842781.252 * * * * [misc]points:  Computing exacts for 4 points
1550842781.256 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.257 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.257 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.257 * * * * [exit]points:  Sampled 256 points with exact outputs
1550842781.258 * * * [misc]progress:  [2/2] Setting up program.
1550842781.287 * [misc]progress:  [Phase 2 of 3] Improving.
1550842781.288 * * * * [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)))>
1550842781.289 * [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))
1550842781.291 * * [misc]simplify:  iters left: 6 (16 enodes)
1550842781.323 * * [misc]simplify:  iters left: 5 (45 enodes)
1550842781.334 * * [misc]simplify:  iters left: 4 (91 enodes)
1550842781.354 * * [misc]simplify:  iters left: 3 (310 enodes)
1550842781.784 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842781.784 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842781.787 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1550842781.799 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1550842781.801 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1550842781.807 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1550842781.835 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1550842781.890 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1550842781.949 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1550842782.010 * [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))
1550842782.011 * [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)))
1550842782.064 * * [misc]progress:  iteration 1 / 4
1550842782.064 * * * [misc]progress:  picking best candidate
1550842782.114 * * * * [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)))>
1550842782.114 * * * [misc]progress:  localizing error
1550842782.657 * * * [misc]progress:  generating rewritten candidates
1550842782.658 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1550842782.663 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1550842782.664 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550842782.687 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1 2)
1550842782.692 * * * [misc]progress:  generating series expansions
1550842782.692 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1550842782.693 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1550842782.693 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550842782.693 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1 2)
1550842782.693 * * * [misc]progress:  simplifying candidates
1550842782.693 * * * * [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)))>
1550842782.693 * * * * [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)))>
1550842782.693 * * * * [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))>
1550842782.693 * * * * [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))))))))>
1550842782.694 * [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))))))
1550842782.694 * * [misc]simplify:  iters left: 6 (14 enodes)
1550842782.700 * * [misc]simplify:  iters left: 5 (42 enodes)
1550842782.716 * * [misc]simplify:  iters left: 4 (117 enodes)
1550842782.748 * * [misc]simplify:  iters left: 3 (426 enodes)
1550842783.026 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.026 * * [misc]simplify:  Extracting #1: cost 51 inf + 0
1550842783.027 * * [misc]simplify:  Extracting #2: cost 242 inf + 0
1550842783.028 * * [misc]simplify:  Extracting #3: cost 408 inf + 4895
1550842783.039 * * [misc]simplify:  Extracting #4: cost 386 inf + 288425
1550842783.111 * * [misc]simplify:  Extracting #5: cost 133 inf + 992840
1550842783.181 * * [misc]simplify:  Extracting #6: cost 2 inf + 1243260
1550842783.265 * * [misc]simplify:  Extracting #7: cost 0 inf + 1250148
1550842783.362 * [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)))
1550842783.362 * [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))))))))
1550842783.362 * * * * [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)))>
1550842783.362 * * * * [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)))>
1550842783.362 * * * * [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)))>
1550842783.363 * [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))
1550842783.363 * * [misc]simplify:  iters left: 6 (16 enodes)
1550842783.370 * * [misc]simplify:  iters left: 5 (45 enodes)
1550842783.386 * * [misc]simplify:  iters left: 4 (91 enodes)
1550842783.425 * * [misc]simplify:  iters left: 3 (310 enodes)
1550842783.583 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.583 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842783.584 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1550842783.585 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1550842783.587 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1550842783.593 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1550842783.621 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1550842783.674 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1550842783.729 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1550842783.766 * [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))
1550842783.766 * [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)))
1550842783.766 * * * * [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)))>
1550842783.766 * [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))
1550842783.767 * * [misc]simplify:  iters left: 6 (16 enodes)
1550842783.774 * * [misc]simplify:  iters left: 5 (45 enodes)
1550842783.789 * * [misc]simplify:  iters left: 4 (91 enodes)
1550842783.813 * * [misc]simplify:  iters left: 3 (310 enodes)
1550842783.991 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.991 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842783.991 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1550842783.993 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1550842783.994 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1550842784.000 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1550842784.028 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1550842784.072 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1550842784.105 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1550842784.149 * [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))
1550842784.149 * [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)))
1550842784.149 * * * * [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)))>
1550842784.150 * [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))
1550842784.150 * * [misc]simplify:  iters left: 6 (16 enodes)
1550842784.154 * * [misc]simplify:  iters left: 5 (45 enodes)
1550842784.162 * * [misc]simplify:  iters left: 4 (91 enodes)
1550842784.182 * * [misc]simplify:  iters left: 3 (310 enodes)
1550842784.324 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842784.325 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842784.325 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1550842784.325 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1550842784.326 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1550842784.329 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1550842784.343 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1550842784.390 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1550842784.436 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1550842784.466 * [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))
1550842784.466 * [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)))
1550842784.466 * * * * [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)))>
1550842784.466 * [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))
1550842784.467 * * [misc]simplify:  iters left: 6 (16 enodes)
1550842784.471 * * [misc]simplify:  iters left: 5 (45 enodes)
1550842784.486 * * [misc]simplify:  iters left: 4 (91 enodes)
1550842784.527 * * [misc]simplify:  iters left: 3 (310 enodes)
1550842784.688 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842784.688 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842784.688 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1550842784.689 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1550842784.690 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1550842784.693 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1550842784.707 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1550842784.748 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1550842784.809 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1550842784.867 * [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))
1550842784.867 * [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)))
1550842784.868 * * * [misc]progress:  adding candidates to table
1550842785.646 * * [misc]progress:  iteration 2 / 4
1550842785.646 * * * [misc]progress:  picking best candidate
1550842785.836 * * * * [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))))))))>
1550842785.837 * * * [misc]progress:  localizing error
1550842786.206 * * * [misc]progress:  generating rewritten candidates
1550842786.206 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2)
1550842786.211 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2)
1550842786.217 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 2)
1550842786.217 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2 2 2 1 2)
1550842786.221 * * * [misc]progress:  generating series expansions
1550842786.221 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2)
1550842786.221 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2)
1550842786.221 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 2)
1550842786.221 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2 2 2 1 2)
1550842786.221 * * * [misc]progress:  simplifying candidates
1550842786.221 * * * * [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)))))>
1550842786.221 * * * * [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)))))))>
1550842786.221 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1550842786.222 * * [misc]simplify:  iters left: 5 (12 enodes)
1550842786.227 * * [misc]simplify:  iters left: 4 (31 enodes)
1550842786.238 * * [misc]simplify:  iters left: 3 (64 enodes)
1550842786.263 * * [misc]simplify:  iters left: 2 (183 enodes)
1550842786.348 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842786.348 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550842786.348 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550842786.348 * * [misc]simplify:  Extracting #3: cost 22 inf + 804
1550842786.349 * * [misc]simplify:  Extracting #4: cost 64 inf + 1445
1550842786.349 * * [misc]simplify:  Extracting #5: cost 132 inf + 3371
1550842786.350 * * [misc]simplify:  Extracting #6: cost 212 inf + 14038
1550842786.355 * * [misc]simplify:  Extracting #7: cost 133 inf + 122101
1550842786.365 * * [misc]simplify:  Extracting #8: cost 13 inf + 330931
1550842786.384 * * [misc]simplify:  Extracting #9: cost 0 inf + 360062
1550842786.400 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1550842786.401 * [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)))
1550842786.401 * * * * [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)))))))>
1550842786.401 * * * * [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))))))))>
1550842786.401 * * * * [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))))))))>
1550842786.401 * [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)))))))
1550842786.401 * * [misc]simplify:  iters left: 6 (21 enodes)
1550842786.406 * * [misc]simplify:  iters left: 5 (61 enodes)
1550842786.418 * * [misc]simplify:  iters left: 4 (154 enodes)
1550842786.451 * * [misc]simplify:  iters left: 3 (373 enodes)
1550842786.592 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842786.592 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550842786.592 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1550842786.593 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1550842786.594 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1550842786.595 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1550842786.599 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1550842786.612 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1550842786.630 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1550842786.649 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1550842786.670 * [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)))
1550842786.670 * [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))))
1550842786.670 * * * * [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))))))))>
1550842786.670 * [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)))))))
1550842786.670 * * [misc]simplify:  iters left: 6 (21 enodes)
1550842786.676 * * [misc]simplify:  iters left: 5 (61 enodes)
1550842786.687 * * [misc]simplify:  iters left: 4 (154 enodes)
1550842786.719 * * [misc]simplify:  iters left: 3 (373 enodes)
1550842786.860 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842786.860 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550842786.860 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1550842786.860 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1550842786.861 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1550842786.863 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1550842786.867 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1550842786.891 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1550842786.927 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1550842786.966 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1550842787.008 * [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)))
1550842787.008 * [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))))
1550842787.008 * * * * [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))))))))>
1550842787.009 * [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)))))))
1550842787.009 * * [misc]simplify:  iters left: 6 (21 enodes)
1550842787.016 * * [misc]simplify:  iters left: 5 (61 enodes)
1550842787.028 * * [misc]simplify:  iters left: 4 (154 enodes)
1550842787.060 * * [misc]simplify:  iters left: 3 (373 enodes)
1550842787.324 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842787.324 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550842787.325 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1550842787.325 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1550842787.327 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1550842787.330 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1550842787.338 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1550842787.356 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1550842787.375 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1550842787.414 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1550842787.433 * [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)))
1550842787.433 * [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))))
1550842787.434 * * * * [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))))))))>
1550842787.434 * [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)))))))
1550842787.434 * * [misc]simplify:  iters left: 6 (21 enodes)
1550842787.439 * * [misc]simplify:  iters left: 5 (61 enodes)
1550842787.462 * * [misc]simplify:  iters left: 4 (154 enodes)
1550842787.526 * * [misc]simplify:  iters left: 3 (373 enodes)
1550842787.732 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842787.732 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550842787.732 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1550842787.732 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1550842787.733 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1550842787.735 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1550842787.739 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1550842787.763 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1550842787.786 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1550842787.814 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1550842787.843 * [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)))
1550842787.844 * [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))))
1550842787.844 * * * [misc]progress:  adding candidates to table
1550842788.478 * * [misc]progress:  iteration 3 / 4
1550842788.478 * * * [misc]progress:  picking best candidate
1550842788.645 * * * * [misc]pick:  Picked  #<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)))))))>
1550842788.645 * * * [misc]progress:  localizing error
1550842788.710 * * * [misc]progress:  generating rewritten candidates
1550842788.710 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2)
1550842788.713 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1550842788.715 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2)
1550842788.715 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1550842788.718 * * * [misc]progress:  generating series expansions
1550842788.718 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2)
1550842788.718 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1550842788.719 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2)
1550842788.719 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1550842788.719 * * * [misc]progress:  simplifying candidates
1550842788.719 * * * * [misc]progress:  [ 1 / 7 ] 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 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (neg.p16 b))))>
1550842788.719 * * * * [misc]progress:  [ 2 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>
1550842788.719 * * * * [misc]progress:  [ 3 / 7 ] 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 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))))>
1550842788.719 * [enter]simplify:  Simplifying (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
1550842788.719 * * [misc]simplify:  iters left: 4 (12 enodes)
1550842788.722 * * [misc]simplify:  iters left: 3 (31 enodes)
1550842788.727 * * [misc]simplify:  iters left: 2 (66 enodes)
1550842788.741 * * [misc]simplify:  iters left: 1 (156 enodes)
1550842788.808 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842788.808 * * [misc]simplify:  Extracting #1: cost 26 inf + 0
1550842788.808 * * [misc]simplify:  Extracting #2: cost 79 inf + 0
1550842788.809 * * [misc]simplify:  Extracting #3: cost 80 inf + 326
1550842788.809 * * [misc]simplify:  Extracting #4: cost 76 inf + 1455
1550842788.810 * * [misc]simplify:  Extracting #5: cost 39 inf + 27807
1550842788.813 * * [misc]simplify:  Extracting #6: cost 7 inf + 55521
1550842788.816 * * [misc]simplify:  Extracting #7: cost 0 inf + 65333
1550842788.819 * [exit]simplify:  Simplified to (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0))
1550842788.819 * [misc]simplify:  Simplified (2 1) to (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))))
1550842788.819 * * * * [misc]progress:  [ 4 / 7 ] 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)))))))>
1550842788.819 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1550842788.820 * * [misc]simplify:  iters left: 5 (12 enodes)
1550842788.823 * * [misc]simplify:  iters left: 4 (31 enodes)
1550842788.828 * * [misc]simplify:  iters left: 3 (64 enodes)
1550842788.844 * * [misc]simplify:  iters left: 2 (183 enodes)
1550842788.903 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842788.903 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550842788.903 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550842788.904 * * [misc]simplify:  Extracting #3: cost 22 inf + 804
1550842788.904 * * [misc]simplify:  Extracting #4: cost 64 inf + 1445
1550842788.904 * * [misc]simplify:  Extracting #5: cost 132 inf + 3371
1550842788.905 * * [misc]simplify:  Extracting #6: cost 212 inf + 14038
1550842788.909 * * [misc]simplify:  Extracting #7: cost 133 inf + 122101
1550842788.920 * * [misc]simplify:  Extracting #8: cost 13 inf + 330931
1550842788.933 * * [misc]simplify:  Extracting #9: cost 0 inf + 360062
1550842788.955 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1550842788.955 * [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)))
1550842788.955 * * * * [misc]progress:  [ 5 / 7 ] 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)))))))>
1550842788.956 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1550842788.956 * * [misc]simplify:  iters left: 5 (12 enodes)
1550842788.961 * * [misc]simplify:  iters left: 4 (31 enodes)
1550842788.972 * * [misc]simplify:  iters left: 3 (64 enodes)
1550842788.998 * * [misc]simplify:  iters left: 2 (183 enodes)
1550842789.068 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.068 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550842789.068 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550842789.068 * * [misc]simplify:  Extracting #3: cost 22 inf + 804
1550842789.068 * * [misc]simplify:  Extracting #4: cost 64 inf + 1445
1550842789.068 * * [misc]simplify:  Extracting #5: cost 132 inf + 3371
1550842789.070 * * [misc]simplify:  Extracting #6: cost 212 inf + 14038
1550842789.076 * * [misc]simplify:  Extracting #7: cost 133 inf + 122101
1550842789.087 * * [misc]simplify:  Extracting #8: cost 13 inf + 330931
1550842789.101 * * [misc]simplify:  Extracting #9: cost 0 inf + 360062
1550842789.114 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1550842789.114 * [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)))
1550842789.115 * * * * [misc]progress:  [ 6 / 7 ] 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)))))))>
1550842789.115 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1550842789.115 * * [misc]simplify:  iters left: 5 (12 enodes)
1550842789.118 * * [misc]simplify:  iters left: 4 (31 enodes)
1550842789.123 * * [misc]simplify:  iters left: 3 (64 enodes)
1550842789.136 * * [misc]simplify:  iters left: 2 (183 enodes)
1550842789.194 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.194 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550842789.194 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550842789.195 * * [misc]simplify:  Extracting #3: cost 22 inf + 804
1550842789.195 * * [misc]simplify:  Extracting #4: cost 64 inf + 1445
1550842789.195 * * [misc]simplify:  Extracting #5: cost 132 inf + 3371
1550842789.196 * * [misc]simplify:  Extracting #6: cost 212 inf + 14038
1550842789.200 * * [misc]simplify:  Extracting #7: cost 133 inf + 122101
1550842789.210 * * [misc]simplify:  Extracting #8: cost 13 inf + 330931
1550842789.226 * * [misc]simplify:  Extracting #9: cost 0 inf + 360062
1550842789.241 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1550842789.241 * [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)))
1550842789.241 * * * * [misc]progress:  [ 7 / 7 ] 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)))))))>
1550842789.241 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1550842789.241 * * [misc]simplify:  iters left: 5 (12 enodes)
1550842789.244 * * [misc]simplify:  iters left: 4 (31 enodes)
1550842789.250 * * [misc]simplify:  iters left: 3 (64 enodes)
1550842789.264 * * [misc]simplify:  iters left: 2 (183 enodes)
1550842789.335 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.335 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550842789.335 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550842789.335 * * [misc]simplify:  Extracting #3: cost 22 inf + 804
1550842789.335 * * [misc]simplify:  Extracting #4: cost 64 inf + 1445
1550842789.336 * * [misc]simplify:  Extracting #5: cost 132 inf + 3371
1550842789.338 * * [misc]simplify:  Extracting #6: cost 212 inf + 14038
1550842789.347 * * [misc]simplify:  Extracting #7: cost 133 inf + 122101
1550842789.370 * * [misc]simplify:  Extracting #8: cost 13 inf + 330931
1550842789.397 * * [misc]simplify:  Extracting #9: cost 0 inf + 360062
1550842789.428 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1550842789.428 * [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)))
1550842789.428 * * * [misc]progress:  adding candidates to table
1550842789.895 * * [misc]progress:  iteration 4 / 4
1550842789.895 * * * [misc]progress:  picking best candidate
1550842790.076 * * * * [misc]pick:  Picked  #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>
1550842790.076 * * * [misc]progress:  localizing error
1550842790.172 * * * [misc]progress:  generating rewritten candidates
1550842790.172 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2)
1550842790.175 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1550842790.176 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2)
1550842790.177 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1550842790.181 * * * [misc]progress:  generating series expansions
1550842790.181 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2)
1550842790.181 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1550842790.181 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2)
1550842790.181 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1550842790.181 * * * [misc]progress:  simplifying candidates
1550842790.181 * * * * [misc]progress:  [ 1 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (neg.p16 b))))>
1550842790.181 * * * * [misc]progress:  [ 2 / 7 ] 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 a (real->posit16 2))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>
1550842790.181 * [enter]simplify:  Simplifying (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c)))
1550842790.181 * * [misc]simplify:  iters left: 4 (12 enodes)
1550842790.184 * * [misc]simplify:  iters left: 3 (31 enodes)
1550842790.190 * * [misc]simplify:  iters left: 2 (66 enodes)
1550842790.210 * * [misc]simplify:  iters left: 1 (156 enodes)
1550842790.275 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842790.275 * * [misc]simplify:  Extracting #1: cost 26 inf + 0
1550842790.276 * * [misc]simplify:  Extracting #2: cost 79 inf + 0
1550842790.276 * * [misc]simplify:  Extracting #3: cost 80 inf + 326
1550842790.276 * * [misc]simplify:  Extracting #4: cost 76 inf + 1455
1550842790.277 * * [misc]simplify:  Extracting #5: cost 39 inf + 27807
1550842790.280 * * [misc]simplify:  Extracting #6: cost 7 inf + 55521
1550842790.283 * * [misc]simplify:  Extracting #7: cost 0 inf + 65333
1550842790.286 * [exit]simplify:  Simplified to (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0))
1550842790.286 * [misc]simplify:  Simplified (2 1 1) to (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 a (real->posit16 2))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))
1550842790.286 * * * * [misc]progress:  [ 3 / 7 ] 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))) (real->posit16 2)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) a)))>
1550842790.286 * [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))) (real->posit16 2))
1550842790.287 * * [misc]simplify:  iters left: 5 (15 enodes)
1550842790.291 * * [misc]simplify:  iters left: 4 (35 enodes)
1550842790.298 * * [misc]simplify:  iters left: 3 (70 enodes)
1550842790.315 * * [misc]simplify:  iters left: 2 (160 enodes)
1550842790.417 * * [misc]simplify:  iters left: 1 (371 enodes)
1550842791.309 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842791.310 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842791.310 * * [misc]simplify:  Extracting #2: cost 66 inf + 0
1550842791.311 * * [misc]simplify:  Extracting #3: cost 232 inf + 648
1550842791.313 * * [misc]simplify:  Extracting #4: cost 188 inf + 21482
1550842791.322 * * [misc]simplify:  Extracting #5: cost 34 inf + 116176
1550842791.333 * * [misc]simplify:  Extracting #6: cost 1 inf + 146523
1550842791.346 * * [misc]simplify:  Extracting #7: cost 0 inf + 147884
1550842791.357 * [exit]simplify:  Simplified to (/.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 2))
1550842791.357 * [misc]simplify:  Simplified (2 1) to (λ (a b c) (/.p16 (/.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 2)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) a)))
1550842791.357 * * * * [misc]progress:  [ 4 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>
1550842791.357 * * * * [misc]progress:  [ 5 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>
1550842791.357 * * * * [misc]progress:  [ 6 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>
1550842791.357 * * * * [misc]progress:  [ 7 / 7 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))>
1550842791.358 * * * [misc]progress:  adding candidates to table
1550842791.885 * [misc]progress:  [Phase 3 of 3] Extracting.
1550842791.885 * * [misc]regime:  Finding splitpoints for: (#<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)))> #<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 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (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 (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)))))))> #<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 (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 (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)))>)
1550842791.891 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b)
1550842791.892 * * * * [misc]regimes:  Trying to branch on c from (#<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)))> #<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 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (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 (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)))))))> #<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 (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 (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)))>)
1550842792.566 * * * * [misc]regimes:  Trying to branch on a from (#<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)))> #<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 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (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 (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)))))))> #<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 (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 (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)))>)
1550842793.259 * * * * [misc]regimes:  Trying to branch on b from (#<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)))> #<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 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (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 (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)))))))> #<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 (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 (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)))>)
1550842793.843 * * * [misc]regime:  Found split indices: #<option (#s(si 3 147) #s(si 6 256))>
1550842793.845 * [misc]binary-search:  Improving bounds with binary search for b and (#<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)))> #<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 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (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 (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)))))))> #<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 (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 (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)))>)
1550842793.846 * [misc]regimes:  Found splitpoints: (#s(sp 3 b #<cpointer:posit16>) #s(sp 6 b +nan.0)) , with alts (#<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)))> #<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 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (real->posit16 2)) (*.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (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 (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)))))))> #<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 (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 (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)))>)
1550842793.847 * [enter]simplify:  Simplifying (if (<=.p16 b (real->posit16 0.0584716796875)) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (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))
1550842793.847 * * [misc]simplify:  iters left: 6 (28 enodes)
1550842793.849 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842793.849 * * [misc]simplify:  Extracting #1: cost 4 inf + 0
1550842793.849 * * [misc]simplify:  Extracting #2: cost 10 inf + 0
1550842793.849 * * [misc]simplify:  Extracting #3: cost 14 inf + 2
1550842793.849 * * [misc]simplify:  Extracting #4: cost 15 inf + 84
1550842793.849 * * [misc]simplify:  Extracting #5: cost 15 inf + 153
1550842793.849 * * [misc]simplify:  Extracting #6: cost 17 inf + 475
1550842793.849 * * [misc]simplify:  Extracting #7: cost 17 inf + 717
1550842793.849 * * [misc]simplify:  Extracting #8: cost 11 inf + 2166
1550842793.849 * * [misc]simplify:  Extracting #9: cost 8 inf + 5979
1550842793.850 * * [misc]simplify:  Extracting #10: cost 5 inf + 10352
1550842793.850 * * [misc]simplify:  Extracting #11: cost 3 inf + 13241
1550842793.851 * * [misc]simplify:  Extracting #12: cost 1 inf + 18331
1550842793.851 * * [misc]simplify:  Extracting #13: cost 0 inf + 22387
1550842793.852 * [exit]simplify:  Simplified to (if (<=.p16 b (real->posit16 0.0584716796875)) (/.p16 (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (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))
1550842793.852 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1550842793.897 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1550842793.900 * * * * [misc]points:  Setting MPFR precision to 64
1550842793.902 * * * * [misc]points:  Setting MPFR precision to 320
1550842793.904 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1550842793.909 * * * * [misc]points:  Setting MPFR precision to 64
1550842793.913 * * * * [misc]points:  Setting MPFR precision to 320
1550842793.918 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1550842793.923 * * * * [misc]points:  Setting MPFR precision to 64
1550842793.932 * * * * [misc]points:  Setting MPFR precision to 320
1550842793.942 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1550842793.947 * * * * [misc]points:  Setting MPFR precision to 64
1550842793.962 * * * * [misc]points:  Setting MPFR precision to 320
1550842793.981 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1550842793.985 * * * * [misc]points:  Setting MPFR precision to 64
1550842794.013 * * * * [misc]points:  Setting MPFR precision to 320
1550842794.076 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1550842794.081 * * * * [misc]points:  Setting MPFR precision to 64
1550842794.125 * * * * [misc]points:  Setting MPFR precision to 320
1550842794.203 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1550842794.208 * * * * [misc]points:  Setting MPFR precision to 64
1550842794.389 * * * * [misc]points:  Setting MPFR precision to 320
1550842794.612 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1550842794.618 * * * * [misc]points:  Setting MPFR precision to 64
1550842794.916 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.271 * * * * [misc]points:  Computing exacts for 8000 points
1550842795.276 * * * * [misc]points:  Setting MPFR precision to 64
1550842796.440 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.635 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842798.372 * * * * [misc]points:  Sampling 2397 additional inputs, on iter 1 have 5603 / 8000
1550842798.390 * * * * [misc]points:  Computing exacts on every 149 of 2397 points to ramp up precision
1550842798.395 * * * * [misc]points:  Setting MPFR precision to 64
1550842798.397 * * * * [misc]points:  Setting MPFR precision to 320
1550842798.400 * * * * [misc]points:  Computing exacts on every 74 of 2397 points to ramp up precision
1550842798.405 * * * * [misc]points:  Setting MPFR precision to 64
1550842798.409 * * * * [misc]points:  Setting MPFR precision to 320
1550842798.414 * * * * [misc]points:  Computing exacts on every 37 of 2397 points to ramp up precision
1550842798.419 * * * * [misc]points:  Setting MPFR precision to 64
1550842798.428 * * * * [misc]points:  Setting MPFR precision to 320
1550842798.438 * * * * [misc]points:  Computing exacts on every 18 of 2397 points to ramp up precision
1550842798.443 * * * * [misc]points:  Setting MPFR precision to 64
1550842798.460 * * * * [misc]points:  Setting MPFR precision to 320
1550842798.480 * * * * [misc]points:  Computing exacts on every 9 of 2397 points to ramp up precision
1550842798.485 * * * * [misc]points:  Setting MPFR precision to 64
1550842798.515 * * * * [misc]points:  Setting MPFR precision to 320
1550842798.553 * * * * [misc]points:  Computing exacts on every 4 of 2397 points to ramp up precision
1550842798.558 * * * * [misc]points:  Setting MPFR precision to 64
1550842798.661 * * * * [misc]points:  Setting MPFR precision to 320
1550842798.738 * * * * [misc]points:  Computing exacts on every 2 of 2397 points to ramp up precision
1550842798.743 * * * * [misc]points:  Setting MPFR precision to 64
1550842798.869 * * * * [misc]points:  Setting MPFR precision to 320
1550842798.939 * * * * [misc]points:  Computing exacts for 2397 points
1550842798.941 * * * * [misc]points:  Setting MPFR precision to 64
1550842799.429 * * * * [misc]points:  Setting MPFR precision to 320
1550842799.664 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842799.803 * * * * [misc]points:  Sampling 717 additional inputs, on iter 2 have 7283 / 8000
1550842799.807 * * * * [misc]points:  Computing exacts on every 44 of 717 points to ramp up precision
1550842799.810 * * * * [misc]points:  Setting MPFR precision to 64
1550842799.811 * * * * [misc]points:  Setting MPFR precision to 320
1550842799.812 * * * * [misc]points:  Computing exacts on every 22 of 717 points to ramp up precision
1550842799.814 * * * * [misc]points:  Setting MPFR precision to 64
1550842799.831 * * * * [misc]points:  Setting MPFR precision to 320
1550842799.836 * * * * [misc]points:  Computing exacts on every 11 of 717 points to ramp up precision
1550842799.841 * * * * [misc]points:  Setting MPFR precision to 64
1550842799.848 * * * * [misc]points:  Setting MPFR precision to 320
1550842799.856 * * * * [misc]points:  Computing exacts on every 5 of 717 points to ramp up precision
1550842799.858 * * * * [misc]points:  Setting MPFR precision to 64
1550842799.866 * * * * [misc]points:  Setting MPFR precision to 320
1550842799.876 * * * * [misc]points:  Computing exacts on every 2 of 717 points to ramp up precision
1550842799.879 * * * * [misc]points:  Setting MPFR precision to 64
1550842799.894 * * * * [misc]points:  Setting MPFR precision to 320
1550842799.914 * * * * [misc]points:  Computing exacts for 717 points
1550842799.917 * * * * [misc]points:  Setting MPFR precision to 64
1550842799.990 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.050 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842800.085 * * * * [misc]points:  Sampling 204 additional inputs, on iter 3 have 7796 / 8000
1550842800.087 * * * * [misc]points:  Computing exacts on every 12 of 204 points to ramp up precision
1550842800.091 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.131 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.133 * * * * [misc]points:  Computing exacts on every 6 of 204 points to ramp up precision
1550842800.141 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.145 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.150 * * * * [misc]points:  Computing exacts on every 3 of 204 points to ramp up precision
1550842800.154 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.161 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.169 * * * * [misc]points:  Computing exacts for 204 points
1550842800.174 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.198 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.227 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842800.238 * * * * [misc]points:  Sampling 57 additional inputs, on iter 4 have 7943 / 8000
1550842800.239 * * * * [misc]points:  Computing exacts on every 3 of 57 points to ramp up precision
1550842800.241 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.242 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.243 * * * * [misc]points:  Computing exacts for 57 points
1550842800.246 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.250 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.254 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842800.257 * * * * [misc]points:  Sampling 21 additional inputs, on iter 5 have 7979 / 8000
1550842800.258 * * * * [misc]points:  Computing exacts for 21 points
1550842800.260 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.262 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.263 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842800.265 * * * * [misc]points:  Sampling 5 additional inputs, on iter 6 have 7995 / 8000
1550842800.265 * * * * [misc]points:  Computing exacts for 5 points
1550842800.267 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.268 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.268 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842800.269 * * * * [misc]points:  Sampling 4 additional inputs, on iter 7 have 7998 / 8000
1550842800.269 * * * * [misc]points:  Computing exacts for 4 points
1550842800.271 * * * * [misc]points:  Setting MPFR precision to 64
1550842800.271 * * * * [misc]points:  Setting MPFR precision to 320
1550842800.272 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842800.272 * * * * [exit]points:  Sampled 8001 points with exact outputs
1550842809.282 * [misc]regime-testing:  Baseline error score: 64.0
1550842809.285 * [misc]regime-testing:  Oracle error score: 64.0
1550842809.292 * [misc]regime-testing:  End program error score: 0.8270642745867933