1554300745.758 * [misc]progress:  [Phase 1 of 3] Setting up.
1554300745.759 * * * [misc]progress:  [1/2] Preparing points
1554300745.760 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1554300745.762 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1554300745.797 * * * * [misc]points:  Setting MPFR precision to 64
1554300745.799 * * * * [misc]points:  Setting MPFR precision to 320
1554300745.800 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1554300745.803 * * * * [misc]points:  Setting MPFR precision to 64
1554300745.805 * * * * [misc]points:  Setting MPFR precision to 320
1554300745.807 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1554300745.810 * * * * [misc]points:  Setting MPFR precision to 64
1554300745.813 * * * * [misc]points:  Setting MPFR precision to 320
1554300745.817 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1554300745.819 * * * * [misc]points:  Setting MPFR precision to 64
1554300745.826 * * * * [misc]points:  Setting MPFR precision to 320
1554300745.832 * * * * [misc]points:  Computing exacts for 256 points
1554300745.835 * * * * [misc]points:  Setting MPFR precision to 64
1554300745.897 * * * * [misc]points:  Setting MPFR precision to 320
1554300745.931 * * * * [misc]points:  Filtering points with unrepresentable outputs
1554300745.933 * * * * [exit]points:  Sampled 256 points with exact outputs
1554300745.933 * * * [misc]progress:  [2/2] Setting up program.
1554300745.967 * [misc]progress:  [Phase 2 of 3] Improving.
1554300745.967 * * * * [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)))>
1554300745.968 * [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))
1554300745.970 * * [misc]simplify:  iters left: 6 (16 enodes)
1554300745.982 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300745.999 * * [misc]simplify:  iters left: 4 (91 enodes)
1554300746.037 * * [misc]simplify:  iters left: 3 (310 enodes)
1554300746.583 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300746.583 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554300746.583 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554300746.584 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554300746.585 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554300746.588 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554300746.615 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554300746.647 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554300746.681 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554300746.719 * [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))
1554300746.719 * [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)))
1554300746.746 * * [misc]progress:  iteration 1 / 4
1554300746.746 * * * [misc]progress:  picking best candidate
1554300746.769 * * * * [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)))>
1554300746.769 * * * [misc]progress:  localizing error
1554300747.041 * * * [misc]progress:  generating rewritten candidates
1554300747.042 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1554300747.047 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1554300747.048 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1554300747.053 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1 2)
1554300747.058 * * * [misc]progress:  generating series expansions
1554300747.059 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1554300747.059 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1554300747.059 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1554300747.059 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1 2)
1554300747.059 * * * [misc]progress:  simplifying candidates
1554300747.059 * * * * [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)))>
1554300747.059 * * * * [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)))>
1554300747.059 * * * * [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))>
1554300747.060 * * * * [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))))))))>
1554300747.060 * [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))))))
1554300747.060 * * [misc]simplify:  iters left: 6 (14 enodes)
1554300747.067 * * [misc]simplify:  iters left: 5 (42 enodes)
1554300747.083 * * [misc]simplify:  iters left: 4 (117 enodes)
1554300747.146 * * [misc]simplify:  iters left: 3 (426 enodes)
1554300747.434 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300747.434 * * [misc]simplify:  Extracting #1: cost 51 inf + 0
1554300747.435 * * [misc]simplify:  Extracting #2: cost 242 inf + 0
1554300747.438 * * [misc]simplify:  Extracting #3: cost 408 inf + 4895
1554300747.459 * * [misc]simplify:  Extracting #4: cost 386 inf + 288425
1554300747.516 * * [misc]simplify:  Extracting #5: cost 133 inf + 992840
1554300747.591 * * [misc]simplify:  Extracting #6: cost 2 inf + 1243260
1554300747.664 * * [misc]simplify:  Extracting #7: cost 0 inf + 1250148
1554300747.770 * [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)))
1554300747.770 * [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))))))))
1554300747.770 * * * * [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)))>
1554300747.770 * * * * [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)))>
1554300747.770 * * * * [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)))>
1554300747.771 * [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))
1554300747.771 * * [misc]simplify:  iters left: 6 (16 enodes)
1554300747.774 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300747.783 * * [misc]simplify:  iters left: 4 (91 enodes)
1554300747.803 * * [misc]simplify:  iters left: 3 (310 enodes)
1554300747.974 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300747.974 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554300747.975 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554300747.976 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554300747.978 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554300747.983 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554300748.012 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554300748.070 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554300748.102 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554300748.133 * [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))
1554300748.133 * [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)))
1554300748.133 * * * * [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)))>
1554300748.133 * [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))
1554300748.133 * * [misc]simplify:  iters left: 6 (16 enodes)
1554300748.137 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300748.153 * * [misc]simplify:  iters left: 4 (91 enodes)
1554300748.189 * * [misc]simplify:  iters left: 3 (310 enodes)
1554300748.342 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300748.342 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554300748.342 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554300748.343 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554300748.344 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554300748.347 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554300748.362 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554300748.413 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554300748.443 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554300748.498 * [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))
1554300748.498 * [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)))
1554300748.499 * * * * [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)))>
1554300748.499 * [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))
1554300748.499 * * [misc]simplify:  iters left: 6 (16 enodes)
1554300748.507 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300748.524 * * [misc]simplify:  iters left: 4 (91 enodes)
1554300748.543 * * [misc]simplify:  iters left: 3 (310 enodes)
1554300748.721 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300748.721 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554300748.722 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554300748.723 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554300748.725 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554300748.737 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554300748.764 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554300748.811 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554300748.850 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554300748.910 * [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))
1554300748.910 * [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)))
1554300748.910 * * * * [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)))>
1554300748.910 * [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))
1554300748.911 * * [misc]simplify:  iters left: 6 (16 enodes)
1554300748.918 * * [misc]simplify:  iters left: 5 (45 enodes)
1554300748.933 * * [misc]simplify:  iters left: 4 (91 enodes)
1554300748.970 * * [misc]simplify:  iters left: 3 (310 enodes)
1554300749.092 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300749.092 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1554300749.093 * * [misc]simplify:  Extracting #2: cost 123 inf + 1
1554300749.093 * * [misc]simplify:  Extracting #3: cost 201 inf + 1129
1554300749.094 * * [misc]simplify:  Extracting #4: cost 263 inf + 9871
1554300749.097 * * [misc]simplify:  Extracting #5: cost 270 inf + 82040
1554300749.111 * * [misc]simplify:  Extracting #6: cost 192 inf + 363234
1554300749.155 * * [misc]simplify:  Extracting #7: cost 15 inf + 679901
1554300749.191 * * [misc]simplify:  Extracting #8: cost 0 inf + 712557
1554300749.225 * [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))
1554300749.225 * [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)))
1554300749.225 * * * [misc]progress:  adding candidates to table
1554300749.847 * * [misc]progress:  iteration 2 / 4
1554300749.847 * * * [misc]progress:  picking best candidate
1554300749.958 * * * * [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))>
1554300749.958 * * * [misc]progress:  localizing error
1554300749.996 * * * [misc]progress:  generating rewritten candidates
1554300749.996 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1)
1554300749.999 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1 2)
1554300749.999 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 1 2 1 2)
1554300750.002 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1554300750.008 * * * [misc]progress:  generating series expansions
1554300750.008 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1)
1554300750.008 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1 2)
1554300750.008 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 1 2 1 2)
1554300750.008 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1554300750.008 * * * [misc]progress:  simplifying candidates
1554300750.008 * * * * [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))>
1554300750.008 * * * * [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))>
1554300750.008 * * * * [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))>
1554300750.008 * * * * [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))>
1554300750.008 * * * * [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))))>
1554300750.009 * [enter]simplify:  Simplifying (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1554300750.009 * * [misc]simplify:  iters left: 5 (12 enodes)
1554300750.022 * * [misc]simplify:  iters left: 4 (37 enodes)
1554300750.035 * * [misc]simplify:  iters left: 3 (79 enodes)
1554300750.068 * * [misc]simplify:  iters left: 2 (262 enodes)
1554300750.199 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300750.199 * * [misc]simplify:  Extracting #1: cost 17 inf + 0
1554300750.199 * * [misc]simplify:  Extracting #2: cost 88 inf + 1
1554300750.200 * * [misc]simplify:  Extracting #3: cost 166 inf + 804
1554300750.200 * * [misc]simplify:  Extracting #4: cost 230 inf + 3734
1554300750.203 * * [misc]simplify:  Extracting #5: cost 225 inf + 64494
1554300750.218 * * [misc]simplify:  Extracting #6: cost 137 inf + 332479
1554300750.266 * * [misc]simplify:  Extracting #7: cost 1 inf + 596662
1554300750.314 * * [misc]simplify:  Extracting #8: cost 0 inf + 599226
1554300750.364 * [exit]simplify:  Simplified to (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))))
1554300750.364 * [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))))
1554300750.364 * * * * [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))>
1554300750.364 * * * * [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))>
1554300750.364 * * * * [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))>
1554300750.364 * * * * [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))>
1554300750.364 * * * [misc]progress:  adding candidates to table
1554300750.788 * * [misc]progress:  iteration 3 / 4
1554300750.789 * * * [misc]progress:  picking best candidate
1554300750.884 * * * * [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)))>
1554300750.884 * * * [misc]progress:  localizing error
1554300751.084 * * * [misc]progress:  generating rewritten candidates
1554300751.084 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1554300751.087 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1554300751.088 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1554300751.093 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1)
1554300751.097 * * * [misc]progress:  generating series expansions
1554300751.098 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1554300751.098 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1554300751.098 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1554300751.098 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1)
1554300751.098 * * * [misc]progress:  simplifying candidates
1554300751.098 * * * * [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)))>
1554300751.098 * * * * [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)))>
1554300751.098 * * * * [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))>
1554300751.098 * * * * [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)))))))>
1554300751.098 * [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)))))
1554300751.099 * * [misc]simplify:  iters left: 6 (14 enodes)
1554300751.105 * * [misc]simplify:  iters left: 5 (42 enodes)
1554300751.121 * * [misc]simplify:  iters left: 4 (117 enodes)
1554300751.175 * * [misc]simplify:  iters left: 3 (432 enodes)
1554300751.480 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300751.481 * * [misc]simplify:  Extracting #1: cost 51 inf + 0
1554300751.481 * * [misc]simplify:  Extracting #2: cost 242 inf + 0
1554300751.483 * * [misc]simplify:  Extracting #3: cost 412 inf + 3092
1554300751.491 * * [misc]simplify:  Extracting #4: cost 427 inf + 239293
1554300751.539 * * [misc]simplify:  Extracting #5: cost 159 inf + 940878
1554300751.627 * * [misc]simplify:  Extracting #6: cost 1 inf + 1259592
1554300751.708 * * [misc]simplify:  Extracting #7: cost 0 inf + 1262236
1554300751.833 * [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))))
1554300751.833 * [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)))))))
1554300751.833 * * * * [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)))>
1554300751.833 * * * * [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)))>
1554300751.833 * * * * [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)))>
1554300751.833 * * * * [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)))>
1554300751.833 * * * * [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)))>
1554300751.833 * * * * [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)))>
1554300751.833 * * * [misc]progress:  adding candidates to table
1554300752.362 * * [misc]progress:  iteration 4 / 4
1554300752.362 * * * [misc]progress:  picking best candidate
1554300752.453 * * * * [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))))))))>
1554300752.453 * * * [misc]progress:  localizing error
1554300752.593 * * * [misc]progress:  generating rewritten candidates
1554300752.593 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2)
1554300752.595 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2)
1554300752.598 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 2)
1554300752.598 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2 2 2 1 2)
1554300752.600 * * * [misc]progress:  generating series expansions
1554300752.600 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2)
1554300752.600 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2)
1554300752.600 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 2)
1554300752.600 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2 2 2 1 2)
1554300752.600 * * * [misc]progress:  simplifying candidates
1554300752.600 * * * * [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)))))>
1554300752.600 * * * * [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)))))))>
1554300752.600 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))
1554300752.600 * * [misc]simplify:  iters left: 5 (12 enodes)
1554300752.603 * * [misc]simplify:  iters left: 4 (31 enodes)
1554300752.609 * * [misc]simplify:  iters left: 3 (64 enodes)
1554300752.622 * * [misc]simplify:  iters left: 2 (183 enodes)
1554300752.689 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300752.689 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1554300752.689 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1554300752.689 * * [misc]simplify:  Extracting #3: cost 22 inf + 804
1554300752.689 * * [misc]simplify:  Extracting #4: cost 64 inf + 1445
1554300752.690 * * [misc]simplify:  Extracting #5: cost 132 inf + 3371
1554300752.691 * * [misc]simplify:  Extracting #6: cost 212 inf + 14038
1554300752.694 * * [misc]simplify:  Extracting #7: cost 133 inf + 122101
1554300752.705 * * [misc]simplify:  Extracting #8: cost 13 inf + 330931
1554300752.718 * * [misc]simplify:  Extracting #9: cost 0 inf + 360062
1554300752.731 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1554300752.732 * [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)))
1554300752.732 * * * * [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)))))))>
1554300752.732 * * * * [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))))))))>
1554300752.732 * * * * [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))))))))>
1554300752.732 * [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)))))))
1554300752.732 * * [misc]simplify:  iters left: 6 (21 enodes)
1554300752.740 * * [misc]simplify:  iters left: 5 (61 enodes)
1554300752.752 * * [misc]simplify:  iters left: 4 (154 enodes)
1554300752.786 * * [misc]simplify:  iters left: 3 (373 enodes)
1554300752.961 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300752.961 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554300752.961 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1554300752.962 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1554300752.963 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1554300752.967 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1554300752.975 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1554300752.999 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1554300753.035 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1554300753.073 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1554300753.111 * [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)))
1554300753.112 * [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))))
1554300753.112 * * * * [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))))))))>
1554300753.112 * [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)))))))
1554300753.112 * * [misc]simplify:  iters left: 6 (21 enodes)
1554300753.124 * * [misc]simplify:  iters left: 5 (61 enodes)
1554300753.137 * * [misc]simplify:  iters left: 4 (154 enodes)
1554300753.179 * * [misc]simplify:  iters left: 3 (373 enodes)
1554300753.326 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300753.326 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554300753.326 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1554300753.327 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1554300753.328 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1554300753.330 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1554300753.337 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1554300753.350 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1554300753.379 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1554300753.416 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1554300753.455 * [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)))
1554300753.456 * [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))))
1554300753.456 * * * * [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))))))))>
1554300753.456 * [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)))))))
1554300753.456 * * [misc]simplify:  iters left: 6 (21 enodes)
1554300753.462 * * [misc]simplify:  iters left: 5 (61 enodes)
1554300753.474 * * [misc]simplify:  iters left: 4 (154 enodes)
1554300753.524 * * [misc]simplify:  iters left: 3 (373 enodes)
1554300753.760 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300753.760 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554300753.760 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1554300753.761 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1554300753.763 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1554300753.767 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1554300753.774 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1554300753.797 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1554300753.837 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1554300753.874 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1554300753.904 * [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)))
1554300753.904 * [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))))
1554300753.904 * * * * [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))))))))>
1554300753.904 * [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)))))))
1554300753.904 * * [misc]simplify:  iters left: 6 (21 enodes)
1554300753.910 * * [misc]simplify:  iters left: 5 (61 enodes)
1554300753.922 * * [misc]simplify:  iters left: 4 (154 enodes)
1554300753.982 * * [misc]simplify:  iters left: 3 (373 enodes)
1554300754.166 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300754.166 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554300754.167 * * [misc]simplify:  Extracting #2: cost 59 inf + 0
1554300754.168 * * [misc]simplify:  Extracting #3: cost 119 inf + 83
1554300754.169 * * [misc]simplify:  Extracting #4: cost 137 inf + 11032
1554300754.171 * * [misc]simplify:  Extracting #5: cost 183 inf + 27270
1554300754.175 * * [misc]simplify:  Extracting #6: cost 223 inf + 84764
1554300754.187 * * [misc]simplify:  Extracting #7: cost 60 inf + 347389
1554300754.206 * * [misc]simplify:  Extracting #8: cost 1 inf + 460459
1554300754.225 * * [misc]simplify:  Extracting #9: cost 0 inf + 461583
1554300754.248 * [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)))
1554300754.248 * [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))))
1554300754.249 * * * [misc]progress:  adding candidates to table
1554300754.635 * [misc]progress:  [Phase 3 of 3] Extracting.
1554300754.635 * * [misc]regime:  Finding splitpoints for: (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (-.p16 (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 (*.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)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (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)))))))>)
1554300754.646 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b)
1554300754.646 * * * * [misc]regimes:  Trying to branch on c from (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (-.p16 (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 (*.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)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (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)))))))>)
1554300754.880 * * * * [misc]regimes:  Trying to branch on a from (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (-.p16 (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 (*.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)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (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)))))))>)
1554300755.128 * * * * [misc]regimes:  Trying to branch on b from (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (-.p16 (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 (*.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)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (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)))))))>)
1554300755.330 * * * [misc]regime:  Found split indices: #<option (#s(si 1 83) #s(si 5 256))>
1554300755.331 * [misc]binary-search:  Improving bounds with binary search for b and (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (-.p16 (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 (*.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)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (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)))))))>)
1554300755.332 * [misc]regimes:  Found splitpoints: (#s(sp 1 b #<cpointer:posit16>) #s(sp 5 b +nan.0)) , with alts (#<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (real->posit16 2) a)) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))))> #<alt (λ (a b c) (/.p16 (-.p16 (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 (*.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)))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 (real->posit16 4) (*.p16 a c))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (+.p16 (*.p16 (real->posit16 4) (*.p16 c a)) (real->posit16 0.0)) (*.p16 (real->posit16 2) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) a))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (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)))))))>)
1554300755.332 * [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))
1554300755.333 * * [misc]simplify:  iters left: 6 (28 enodes)
1554300755.338 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300755.338 * * [misc]simplify:  Extracting #1: cost 4 inf + 0
1554300755.338 * * [misc]simplify:  Extracting #2: cost 10 inf + 0
1554300755.338 * * [misc]simplify:  Extracting #3: cost 15 inf + 2
1554300755.338 * * [misc]simplify:  Extracting #4: cost 17 inf + 84
1554300755.338 * * [misc]simplify:  Extracting #5: cost 19 inf + 153
1554300755.338 * * [misc]simplify:  Extracting #6: cost 17 inf + 717
1554300755.338 * * [misc]simplify:  Extracting #7: cost 10 inf + 2488
1554300755.339 * * [misc]simplify:  Extracting #8: cost 7 inf + 6621
1554300755.339 * * [misc]simplify:  Extracting #9: cost 5 inf + 8949
1554300755.339 * * [misc]simplify:  Extracting #10: cost 3 inf + 11838
1554300755.340 * * [misc]simplify:  Extracting #11: cost 1 inf + 16808
1554300755.340 * * [misc]simplify:  Extracting #12: cost 0 inf + 20744
1554300755.341 * [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))
1554300755.341 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1554300755.375 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1554300755.377 * * * * [misc]points:  Setting MPFR precision to 64
1554300755.378 * * * * [misc]points:  Setting MPFR precision to 320
1554300755.379 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1554300755.382 * * * * [misc]points:  Setting MPFR precision to 64
1554300755.384 * * * * [misc]points:  Setting MPFR precision to 320
1554300755.386 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1554300755.389 * * * * [misc]points:  Setting MPFR precision to 64
1554300755.393 * * * * [misc]points:  Setting MPFR precision to 320
1554300755.398 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1554300755.400 * * * * [misc]points:  Setting MPFR precision to 64
1554300755.409 * * * * [misc]points:  Setting MPFR precision to 320
1554300755.418 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1554300755.421 * * * * [misc]points:  Setting MPFR precision to 64
1554300755.444 * * * * [misc]points:  Setting MPFR precision to 320
1554300755.477 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1554300755.482 * * * * [misc]points:  Setting MPFR precision to 64
1554300755.555 * * * * [misc]points:  Setting MPFR precision to 320
1554300755.600 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1554300755.603 * * * * [misc]points:  Setting MPFR precision to 64
1554300755.742 * * * * [misc]points:  Setting MPFR precision to 320
1554300755.830 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1554300755.833 * * * * [misc]points:  Setting MPFR precision to 64
1554300756.087 * * * * [misc]points:  Setting MPFR precision to 320
1554300756.371 * * * * [misc]points:  Computing exacts for 8000 points
1554300756.374 * * * * [misc]points:  Setting MPFR precision to 64
1554300757.977 * * * * [misc]points:  Setting MPFR precision to 320
1554300759.183 * * * * [misc]points:  Filtering points with unrepresentable outputs
1554300759.224 * * * * [exit]points:  Sampled 8000 points with exact outputs
1554300766.325 * [misc]regime-testing:  Baseline error score: 64.0
1554300766.327 * [misc]regime-testing:  Oracle error score: 64.0
1554300766.331 * [misc]regime-testing:  End program error score: 0.5616442814262933