1550698889.748 * [misc]progress:  [Phase 1 of 3] Setting up.
1550698889.750 * * * [misc]progress:  [1/2] Preparing points
1550698889.751 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1550698889.760 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1550698889.810 * * * * [misc]points:  Setting MPFR precision to 64
1550698889.813 * * * * [misc]points:  Setting MPFR precision to 320
1550698889.815 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1550698889.816 * * * * [misc]points:  Setting MPFR precision to 64
1550698889.818 * * * * [misc]points:  Setting MPFR precision to 320
1550698889.820 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1550698889.821 * * * * [misc]points:  Setting MPFR precision to 64
1550698889.825 * * * * [misc]points:  Setting MPFR precision to 320
1550698889.829 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1550698889.830 * * * * [misc]points:  Setting MPFR precision to 64
1550698889.883 * * * * [misc]points:  Setting MPFR precision to 320
1550698889.895 * * * * [misc]points:  Computing exacts for 256 points
1550698889.897 * * * * [misc]points:  Setting MPFR precision to 64
1550698889.928 * * * * [misc]points:  Setting MPFR precision to 320
1550698889.966 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698889.994 * * * * [misc]points:  Sampling 66 additional inputs, on iter 1 have 190 / 256
1550698889.994 * * * * [misc]points:  Computing exacts on every 4 of 66 points to ramp up precision
1550698889.996 * * * * [misc]points:  Setting MPFR precision to 64
1550698889.998 * * * * [misc]points:  Setting MPFR precision to 320
1550698890.000 * * * * [misc]points:  Computing exacts on every 2 of 66 points to ramp up precision
1550698890.002 * * * * [misc]points:  Setting MPFR precision to 64
1550698890.004 * * * * [misc]points:  Setting MPFR precision to 320
1550698890.008 * * * * [misc]points:  Computing exacts for 66 points
1550698890.010 * * * * [misc]points:  Setting MPFR precision to 64
1550698890.019 * * * * [misc]points:  Setting MPFR precision to 320
1550698890.029 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698890.035 * * * * [misc]points:  Sampling 19 additional inputs, on iter 2 have 237 / 256
1550698890.035 * * * * [misc]points:  Computing exacts for 19 points
1550698890.036 * * * * [misc]points:  Setting MPFR precision to 64
1550698890.037 * * * * [misc]points:  Setting MPFR precision to 320
1550698890.039 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698890.040 * * * * [misc]points:  Sampling 4 additional inputs, on iter 3 have 253 / 256
1550698890.040 * * * * [misc]points:  Computing exacts for 4 points
1550698890.041 * * * * [misc]points:  Setting MPFR precision to 64
1550698890.041 * * * * [misc]points:  Setting MPFR precision to 320
1550698890.042 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698890.042 * * * * [exit]points:  Sampled 256 points with exact outputs
1550698890.043 * * * [misc]progress:  [2/2] Setting up program.
1550698890.064 * [misc]progress:  [Phase 2 of 3] Improving.
1550698890.064 * * * * [misc]progress:  [ 1 / 1 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1550698890.066 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550698890.067 * * [misc]simplify:  iters left: 5 (10 enodes)
1550698890.117 * * [misc]simplify:  iters left: 4 (31 enodes)
1550698890.129 * * [misc]simplify:  iters left: 3 (65 enodes)
1550698890.155 * * [misc]simplify:  iters left: 2 (207 enodes)
1550698890.278 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698890.279 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698890.280 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550698890.281 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550698890.283 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550698890.290 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550698890.314 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550698890.345 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550698890.378 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550698890.410 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550698890.411 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
1550698890.452 * * [misc]progress:  iteration 1 / 4
1550698890.452 * * * [misc]progress:  picking best candidate
1550698890.485 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1550698890.486 * * * [misc]progress:  localizing error
1550698890.834 * * * [misc]progress:  generating rewritten candidates
1550698890.835 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1550698890.840 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1550698890.841 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550698890.845 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1)
1550698890.849 * * * [misc]progress:  generating series expansions
1550698890.850 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1550698890.850 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1550698890.850 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550698890.850 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1)
1550698890.850 * * * [misc]progress:  simplifying candidates
1550698890.850 * * * * [misc]progress:  [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (neg.p16 b_2) (neg.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
1550698890.850 * * * * [misc]progress:  [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
1550698890.850 * * * * [misc]progress:  [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
1550698890.851 * [enter]simplify:  Simplifying (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1550698890.851 * * [misc]simplify:  iters left: 5 (11 enodes)
1550698890.855 * * [misc]simplify:  iters left: 4 (35 enodes)
1550698890.881 * * [misc]simplify:  iters left: 3 (100 enodes)
1550698890.927 * * [misc]simplify:  iters left: 2 (360 enodes)
1550698891.250 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698891.250 * * [misc]simplify:  Extracting #1: cost 48 inf + 0
1550698891.251 * * [misc]simplify:  Extracting #2: cost 223 inf + 0
1550698891.256 * * [misc]simplify:  Extracting #3: cost 348 inf + 45039
1550698891.282 * * [misc]simplify:  Extracting #4: cost 315 inf + 336131
1550698891.347 * * [misc]simplify:  Extracting #5: cost 84 inf + 852438
1550698891.425 * * [misc]simplify:  Extracting #6: cost 1 inf + 990774
1550698891.475 * * [misc]simplify:  Extracting #7: cost 0 inf + 992777
1550698891.525 * [exit]simplify:  Simplified to (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2))))
1550698891.525 * [misc]simplify:  Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))
1550698891.525 * * * * [misc]progress:  [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c))))) a))>
1550698891.525 * * * * [misc]progress:  [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>
1550698891.525 * * * * [misc]progress:  [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1550698891.525 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550698891.525 * * [misc]simplify:  iters left: 5 (10 enodes)
1550698891.527 * * [misc]simplify:  iters left: 4 (31 enodes)
1550698891.532 * * [misc]simplify:  iters left: 3 (65 enodes)
1550698891.558 * * [misc]simplify:  iters left: 2 (207 enodes)
1550698891.674 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698891.674 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698891.674 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550698891.675 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550698891.677 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550698891.684 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550698891.708 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550698891.741 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550698891.773 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550698891.805 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550698891.806 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
1550698891.806 * * * * [misc]progress:  [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1550698891.806 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550698891.806 * * [misc]simplify:  iters left: 5 (10 enodes)
1550698891.812 * * [misc]simplify:  iters left: 4 (31 enodes)
1550698891.823 * * [misc]simplify:  iters left: 3 (65 enodes)
1550698891.849 * * [misc]simplify:  iters left: 2 (207 enodes)
1550698891.963 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698891.964 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698891.964 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550698891.965 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550698891.967 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550698891.973 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550698891.996 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550698892.028 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550698892.050 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550698892.067 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550698892.067 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
1550698892.067 * * * * [misc]progress:  [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1550698892.067 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550698892.067 * * [misc]simplify:  iters left: 5 (10 enodes)
1550698892.069 * * [misc]simplify:  iters left: 4 (31 enodes)
1550698892.079 * * [misc]simplify:  iters left: 3 (65 enodes)
1550698892.091 * * [misc]simplify:  iters left: 2 (207 enodes)
1550698892.163 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698892.163 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698892.163 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550698892.163 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550698892.164 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550698892.171 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550698892.194 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550698892.227 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550698892.260 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550698892.292 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550698892.292 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
1550698892.292 * * * * [misc]progress:  [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))>
1550698892.292 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550698892.292 * * [misc]simplify:  iters left: 5 (10 enodes)
1550698892.296 * * [misc]simplify:  iters left: 4 (31 enodes)
1550698892.310 * * [misc]simplify:  iters left: 3 (65 enodes)
1550698892.336 * * [misc]simplify:  iters left: 2 (207 enodes)
1550698892.450 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698892.450 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698892.450 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550698892.451 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550698892.452 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550698892.455 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550698892.468 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550698892.487 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550698892.519 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550698892.550 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550698892.550 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a))
1550698892.550 * * * [misc]progress:  adding candidates to table
1550698892.925 * * [misc]progress:  iteration 2 / 4
1550698892.925 * * * [misc]progress:  picking best candidate
1550698892.983 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
1550698892.983 * * * [misc]progress:  localizing error
1550698893.214 * * * [misc]progress:  generating rewritten candidates
1550698893.214 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2)
1550698893.219 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2)
1550698893.223 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 2)
1550698893.224 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2)
1550698893.228 * * * [misc]progress:  generating series expansions
1550698893.229 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2)
1550698893.229 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2)
1550698893.229 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 2)
1550698893.229 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2)
1550698893.229 * * * [misc]progress:  simplifying candidates
1550698893.229 * * * * [misc]progress:  [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (neg.p16 b_2)))))>
1550698893.229 * * * * [misc]progress:  [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
1550698893.229 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698893.229 * * [misc]simplify:  iters left: 4 (9 enodes)
1550698893.233 * * [misc]simplify:  iters left: 3 (24 enodes)
1550698893.241 * * [misc]simplify:  iters left: 2 (47 enodes)
1550698893.257 * * [misc]simplify:  iters left: 1 (110 enodes)
1550698893.313 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698893.313 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550698893.313 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550698893.313 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550698893.314 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550698893.315 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550698893.318 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550698893.327 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550698893.339 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550698893.350 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698893.350 * [misc]simplify:  Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698893.350 * * * * [misc]progress:  [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 a (neg.p16 b_2)) (*.p16 a (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
1550698893.351 * [enter]simplify:  Simplifying (*.p16 a (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698893.351 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698893.354 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698893.361 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698893.377 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698893.429 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698893.429 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698893.429 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698893.429 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698893.429 * * [misc]simplify:  Extracting #4: cost 56 inf + 1
1550698893.430 * * [misc]simplify:  Extracting #5: cost 91 inf + 727
1550698893.431 * * [misc]simplify:  Extracting #6: cost 116 inf + 19295
1550698893.441 * * [misc]simplify:  Extracting #7: cost 31 inf + 140495
1550698893.453 * * [misc]simplify:  Extracting #8: cost 4 inf + 182028
1550698893.465 * * [misc]simplify:  Extracting #9: cost 0 inf + 191878
1550698893.477 * [exit]simplify:  Simplified to (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a)
1550698893.477 * [misc]simplify:  Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 a (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a))))
1550698893.477 * * * * [misc]progress:  [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))>
1550698893.477 * [enter]simplify:  Simplifying (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a)
1550698893.477 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698893.481 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698893.488 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698893.505 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698893.561 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698893.561 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698893.561 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698893.561 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698893.561 * * [misc]simplify:  Extracting #4: cost 56 inf + 1
1550698893.562 * * [misc]simplify:  Extracting #5: cost 91 inf + 1048
1550698893.565 * * [misc]simplify:  Extracting #6: cost 93 inf + 43948
1550698893.574 * * [misc]simplify:  Extracting #7: cost 7 inf + 178456
1550698893.588 * * [misc]simplify:  Extracting #8: cost 0 inf + 193716
1550698893.599 * [exit]simplify:  Simplified to (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a)
1550698893.599 * [misc]simplify:  Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a))))
1550698893.599 * * * * [misc]progress:  [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)))>
1550698893.599 * * * * [misc]progress:  [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
1550698893.600 * [enter]simplify:  Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
1550698893.600 * * [misc]simplify:  iters left: 6 (15 enodes)
1550698893.607 * * [misc]simplify:  iters left: 5 (47 enodes)
1550698893.624 * * [misc]simplify:  iters left: 4 (100 enodes)
1550698893.662 * * [misc]simplify:  iters left: 3 (250 enodes)
1550698893.872 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698893.872 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550698893.872 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1550698893.873 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1550698893.874 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1550698893.880 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1550698893.892 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1550698893.909 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1550698893.928 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1550698893.946 * [exit]simplify:  Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698893.946 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
1550698893.946 * * * * [misc]progress:  [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
1550698893.946 * [enter]simplify:  Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
1550698893.947 * * [misc]simplify:  iters left: 6 (15 enodes)
1550698893.953 * * [misc]simplify:  iters left: 5 (47 enodes)
1550698893.974 * * [misc]simplify:  iters left: 4 (100 enodes)
1550698894.012 * * [misc]simplify:  iters left: 3 (250 enodes)
1550698894.219 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698894.219 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550698894.219 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1550698894.220 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1550698894.221 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1550698894.227 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1550698894.240 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1550698894.257 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1550698894.274 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1550698894.292 * [exit]simplify:  Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698894.292 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
1550698894.292 * * * * [misc]progress:  [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
1550698894.292 * [enter]simplify:  Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
1550698894.293 * * [misc]simplify:  iters left: 6 (15 enodes)
1550698894.299 * * [misc]simplify:  iters left: 5 (47 enodes)
1550698894.316 * * [misc]simplify:  iters left: 4 (100 enodes)
1550698894.359 * * [misc]simplify:  iters left: 3 (250 enodes)
1550698894.537 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698894.537 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550698894.537 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1550698894.537 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1550698894.539 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1550698894.545 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1550698894.557 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1550698894.574 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1550698894.592 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1550698894.611 * [exit]simplify:  Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698894.611 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
1550698894.611 * * * * [misc]progress:  [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
1550698894.611 * [enter]simplify:  Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))
1550698894.612 * * [misc]simplify:  iters left: 6 (15 enodes)
1550698894.618 * * [misc]simplify:  iters left: 5 (47 enodes)
1550698894.636 * * [misc]simplify:  iters left: 4 (100 enodes)
1550698894.669 * * [misc]simplify:  iters left: 3 (250 enodes)
1550698894.836 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698894.836 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550698894.836 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1550698894.836 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1550698894.838 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1550698894.844 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1550698894.857 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1550698894.877 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1550698894.895 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1550698894.913 * [exit]simplify:  Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698894.913 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
1550698894.913 * * * [misc]progress:  adding candidates to table
1550698895.477 * * [misc]progress:  iteration 3 / 4
1550698895.477 * * * [misc]progress:  picking best candidate
1550698895.551 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
1550698895.551 * * * [misc]progress:  localizing error
1550698895.666 * * * [misc]progress:  generating rewritten candidates
1550698895.666 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2)
1550698895.671 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 2 2)
1550698895.672 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1)
1550698895.674 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1550698895.681 * * * [misc]progress:  generating series expansions
1550698895.681 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2)
1550698895.681 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 2 2)
1550698895.681 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1)
1550698895.681 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1550698895.681 * * * [misc]progress:  simplifying candidates
1550698895.681 * * * * [misc]progress:  [ 1 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (neg.p16 b_2))))>
1550698895.681 * * * * [misc]progress:  [ 2 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)))>
1550698895.681 * [enter]simplify:  Simplifying (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2))))
1550698895.681 * * [misc]simplify:  iters left: 4 (9 enodes)
1550698895.685 * * [misc]simplify:  iters left: 3 (24 enodes)
1550698895.694 * * [misc]simplify:  iters left: 2 (53 enodes)
1550698895.716 * * [misc]simplify:  iters left: 1 (140 enodes)
1550698895.856 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698895.856 * * [misc]simplify:  Extracting #1: cost 24 inf + 0
1550698895.856 * * [misc]simplify:  Extracting #2: cost 70 inf + 0
1550698895.857 * * [misc]simplify:  Extracting #3: cost 62 inf + 3454
1550698895.860 * * [misc]simplify:  Extracting #4: cost 19 inf + 33897
1550698895.866 * * [misc]simplify:  Extracting #5: cost 0 inf + 53655
1550698895.871 * [exit]simplify:  Simplified to (+.p16 (*.p16 c a) (real->posit16 0.0))
1550698895.872 * [misc]simplify:  Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)))
1550698895.872 * * * * [misc]progress:  [ 3 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
1550698895.872 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698895.872 * * [misc]simplify:  iters left: 4 (9 enodes)
1550698895.876 * * [misc]simplify:  iters left: 3 (24 enodes)
1550698895.883 * * [misc]simplify:  iters left: 2 (47 enodes)
1550698895.899 * * [misc]simplify:  iters left: 1 (110 enodes)
1550698895.952 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698895.953 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550698895.953 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550698895.953 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550698895.953 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550698895.954 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550698895.958 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550698895.967 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550698895.979 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550698895.991 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698895.991 * [misc]simplify:  Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698895.991 * * * * [misc]progress:  [ 4 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
1550698895.992 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698895.992 * * [misc]simplify:  iters left: 4 (9 enodes)
1550698895.996 * * [misc]simplify:  iters left: 3 (24 enodes)
1550698896.004 * * [misc]simplify:  iters left: 2 (47 enodes)
1550698896.020 * * [misc]simplify:  iters left: 1 (110 enodes)
1550698896.074 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698896.074 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550698896.074 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550698896.074 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550698896.074 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550698896.075 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550698896.079 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550698896.089 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550698896.100 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550698896.110 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698896.110 * [misc]simplify:  Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698896.111 * * * * [misc]progress:  [ 5 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
1550698896.111 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698896.111 * * [misc]simplify:  iters left: 4 (9 enodes)
1550698896.114 * * [misc]simplify:  iters left: 3 (24 enodes)
1550698896.122 * * [misc]simplify:  iters left: 2 (47 enodes)
1550698896.139 * * [misc]simplify:  iters left: 1 (110 enodes)
1550698896.194 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698896.194 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550698896.194 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550698896.194 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550698896.194 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550698896.195 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550698896.198 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550698896.208 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550698896.219 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550698896.231 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698896.231 * [misc]simplify:  Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698896.231 * * * * [misc]progress:  [ 6 / 6 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
1550698896.231 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698896.231 * * [misc]simplify:  iters left: 4 (9 enodes)
1550698896.235 * * [misc]simplify:  iters left: 3 (24 enodes)
1550698896.243 * * [misc]simplify:  iters left: 2 (47 enodes)
1550698896.260 * * [misc]simplify:  iters left: 1 (110 enodes)
1550698896.313 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698896.313 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550698896.313 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550698896.314 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550698896.314 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550698896.315 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550698896.318 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550698896.328 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550698896.339 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550698896.351 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698896.351 * [misc]simplify:  Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698896.351 * * * [misc]progress:  adding candidates to table
1550698896.674 * * [misc]progress:  iteration 4 / 4
1550698896.674 * * * [misc]progress:  picking best candidate
1550698896.753 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))>
1550698896.753 * * * [misc]progress:  localizing error
1550698896.988 * * * [misc]progress:  generating rewritten candidates
1550698896.988 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2)
1550698896.993 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2)
1550698896.997 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 1)
1550698896.997 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2 2 1 1)
1550698897.000 * * * [misc]progress:  generating series expansions
1550698897.000 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2)
1550698897.000 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2)
1550698897.000 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 1)
1550698897.000 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2 2 1 1)
1550698897.000 * * * [misc]progress:  simplifying candidates
1550698897.000 * * * * [misc]progress:  [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))>
1550698897.001 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698897.001 * * [misc]simplify:  iters left: 4 (9 enodes)
1550698897.004 * * [misc]simplify:  iters left: 3 (24 enodes)
1550698897.011 * * [misc]simplify:  iters left: 2 (47 enodes)
1550698897.026 * * [misc]simplify:  iters left: 1 (110 enodes)
1550698897.073 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698897.074 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550698897.074 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550698897.074 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550698897.074 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550698897.075 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550698897.078 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550698897.091 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550698897.101 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550698897.111 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698897.111 * [misc]simplify:  Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
1550698897.111 * * * * [misc]progress:  [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a) (*.p16 (neg.p16 b_2) a))))>
1550698897.111 * * * * [misc]progress:  [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))>
1550698897.112 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698897.112 * * [misc]simplify:  iters left: 4 (9 enodes)
1550698897.115 * * [misc]simplify:  iters left: 3 (24 enodes)
1550698897.122 * * [misc]simplify:  iters left: 2 (47 enodes)
1550698897.136 * * [misc]simplify:  iters left: 1 (110 enodes)
1550698897.182 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698897.182 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550698897.182 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550698897.183 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550698897.183 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550698897.184 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550698897.187 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550698897.195 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550698897.205 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550698897.216 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698897.217 * [misc]simplify:  Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))
1550698897.217 * * * * [misc]progress:  [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 a c)))) a))))>
1550698897.217 * * * * [misc]progress:  [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))))>
1550698897.217 * * * * [misc]progress:  [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))>
1550698897.217 * [enter]simplify:  Simplifying (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a)
1550698897.217 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698897.220 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698897.226 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698897.240 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698897.290 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698897.290 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698897.290 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698897.290 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698897.291 * * [misc]simplify:  Extracting #4: cost 56 inf + 1
1550698897.291 * * [misc]simplify:  Extracting #5: cost 91 inf + 1048
1550698897.294 * * [misc]simplify:  Extracting #6: cost 93 inf + 43948
1550698897.303 * * [misc]simplify:  Extracting #7: cost 7 inf + 178456
1550698897.313 * * [misc]simplify:  Extracting #8: cost 0 inf + 193716
1550698897.323 * [exit]simplify:  Simplified to (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a)
1550698897.323 * [misc]simplify:  Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a))))
1550698897.324 * * * * [misc]progress:  [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))>
1550698897.324 * [enter]simplify:  Simplifying (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a)
1550698897.324 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698897.327 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698897.333 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698897.347 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698897.391 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698897.391 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698897.391 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698897.391 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698897.391 * * [misc]simplify:  Extracting #4: cost 56 inf + 1
1550698897.392 * * [misc]simplify:  Extracting #5: cost 91 inf + 1048
1550698897.393 * * [misc]simplify:  Extracting #6: cost 93 inf + 43948
1550698897.398 * * [misc]simplify:  Extracting #7: cost 7 inf + 178456
1550698897.404 * * [misc]simplify:  Extracting #8: cost 0 inf + 193716
1550698897.410 * [exit]simplify:  Simplified to (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a)
1550698897.410 * [misc]simplify:  Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a))))
1550698897.410 * * * * [misc]progress:  [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))>
1550698897.410 * [enter]simplify:  Simplifying (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a)
1550698897.411 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698897.412 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698897.416 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698897.423 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698897.479 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698897.479 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698897.479 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698897.479 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698897.479 * * [misc]simplify:  Extracting #4: cost 56 inf + 1
1550698897.480 * * [misc]simplify:  Extracting #5: cost 91 inf + 1048
1550698897.483 * * [misc]simplify:  Extracting #6: cost 93 inf + 43948
1550698897.492 * * [misc]simplify:  Extracting #7: cost 7 inf + 178456
1550698897.503 * * [misc]simplify:  Extracting #8: cost 0 inf + 193716
1550698897.516 * [exit]simplify:  Simplified to (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a)
1550698897.516 * [misc]simplify:  Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a))))
1550698897.516 * * * * [misc]progress:  [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))>
1550698897.517 * [enter]simplify:  Simplifying (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a)
1550698897.517 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698897.520 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698897.528 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698897.544 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698897.602 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698897.602 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698897.602 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698897.603 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698897.603 * * [misc]simplify:  Extracting #4: cost 56 inf + 1
1550698897.603 * * [misc]simplify:  Extracting #5: cost 91 inf + 1048
1550698897.606 * * [misc]simplify:  Extracting #6: cost 93 inf + 43948
1550698897.616 * * [misc]simplify:  Extracting #7: cost 7 inf + 178456
1550698897.628 * * [misc]simplify:  Extracting #8: cost 0 inf + 193716
1550698897.640 * [exit]simplify:  Simplified to (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a)
1550698897.640 * [misc]simplify:  Simplified (2 2 2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) a))))
1550698897.641 * * * [misc]progress:  adding candidates to table
1550698898.212 * [misc]progress:  [Phase 3 of 3] Extracting.
1550698898.212 * * [misc]regime:  Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
1550698898.216 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b_2)
1550698898.217 * * * * [misc]regimes:  Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
1550698898.628 * * * * [misc]regimes:  Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
1550698898.979 * * * * [misc]regimes:  Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
1550698899.347 * * * [misc]regime:  Found split indices: #<option (#s(si 2 136) #s(si 1 256))>
1550698899.348 * [misc]binary-search:  Improving bounds with binary search for b_2 and (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
1550698899.350 * [misc]regimes:  Found splitpoints: (#s(sp 2 b_2 #<cpointer:posit16>) #s(sp 1 b_2 +nan.0)) , with alts (#<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))> #<alt (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (+.p16 (*.p16 (neg.p16 b_2) a) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) a))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))>)
1550698899.351 * [enter]simplify:  Simplifying (if (<=.p16 b_2 (real->posit16 0.00255584716796875)) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))
1550698899.351 * * [misc]simplify:  iters left: 6 (21 enodes)
1550698899.353 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698899.353 * * [misc]simplify:  Extracting #1: cost 4 inf + 0
1550698899.353 * * [misc]simplify:  Extracting #2: cost 10 inf + 0
1550698899.353 * * [misc]simplify:  Extracting #3: cost 12 inf + 2
1550698899.353 * * [misc]simplify:  Extracting #4: cost 13 inf + 84
1550698899.353 * * [misc]simplify:  Extracting #5: cost 15 inf + 152
1550698899.354 * * [misc]simplify:  Extracting #6: cost 11 inf + 716
1550698899.354 * * [misc]simplify:  Extracting #7: cost 6 inf + 3848
1550698899.354 * * [misc]simplify:  Extracting #8: cost 3 inf + 6937
1550698899.355 * * [misc]simplify:  Extracting #9: cost 0 inf + 13357
1550698899.355 * [exit]simplify:  Simplified to (if (<=.p16 b_2 (real->posit16 0.00255584716796875)) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))
1550698899.356 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1550698899.418 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1550698899.420 * * * * [misc]points:  Setting MPFR precision to 64
1550698899.422 * * * * [misc]points:  Setting MPFR precision to 320
1550698899.424 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1550698899.425 * * * * [misc]points:  Setting MPFR precision to 64
1550698899.429 * * * * [misc]points:  Setting MPFR precision to 320
1550698899.434 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1550698899.435 * * * * [misc]points:  Setting MPFR precision to 64
1550698899.443 * * * * [misc]points:  Setting MPFR precision to 320
1550698899.451 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1550698899.453 * * * * [misc]points:  Setting MPFR precision to 64
1550698899.467 * * * * [misc]points:  Setting MPFR precision to 320
1550698899.486 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1550698899.488 * * * * [misc]points:  Setting MPFR precision to 64
1550698899.517 * * * * [misc]points:  Setting MPFR precision to 320
1550698899.552 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1550698899.593 * * * * [misc]points:  Setting MPFR precision to 64
1550698899.650 * * * * [misc]points:  Setting MPFR precision to 320
1550698899.715 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1550698899.717 * * * * [misc]points:  Setting MPFR precision to 64
1550698899.876 * * * * [misc]points:  Setting MPFR precision to 320
1550698900.024 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1550698900.026 * * * * [misc]points:  Setting MPFR precision to 64
1550698900.317 * * * * [misc]points:  Setting MPFR precision to 320
1550698900.999 * * * * [misc]points:  Computing exacts for 8000 points
1550698901.000 * * * * [misc]points:  Setting MPFR precision to 64
1550698902.161 * * * * [misc]points:  Setting MPFR precision to 320
1550698903.576 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698904.395 * * * * [misc]points:  Sampling 1963 additional inputs, on iter 1 have 6037 / 8000
1550698904.410 * * * * [misc]points:  Computing exacts on every 122 of 1963 points to ramp up precision
1550698904.412 * * * * [misc]points:  Setting MPFR precision to 64
1550698904.414 * * * * [misc]points:  Setting MPFR precision to 320
1550698904.416 * * * * [misc]points:  Computing exacts on every 61 of 1963 points to ramp up precision
1550698904.418 * * * * [misc]points:  Setting MPFR precision to 64
1550698904.422 * * * * [misc]points:  Setting MPFR precision to 320
1550698904.427 * * * * [misc]points:  Computing exacts on every 30 of 1963 points to ramp up precision
1550698904.428 * * * * [misc]points:  Setting MPFR precision to 64
1550698904.436 * * * * [misc]points:  Setting MPFR precision to 320
1550698904.446 * * * * [misc]points:  Computing exacts on every 15 of 1963 points to ramp up precision
1550698904.448 * * * * [misc]points:  Setting MPFR precision to 64
1550698904.462 * * * * [misc]points:  Setting MPFR precision to 320
1550698904.482 * * * * [misc]points:  Computing exacts on every 7 of 1963 points to ramp up precision
1550698904.484 * * * * [misc]points:  Setting MPFR precision to 64
1550698904.513 * * * * [misc]points:  Setting MPFR precision to 320
1550698904.543 * * * * [misc]points:  Computing exacts on every 3 of 1963 points to ramp up precision
1550698904.544 * * * * [misc]points:  Setting MPFR precision to 64
1550698904.602 * * * * [misc]points:  Setting MPFR precision to 320
1550698904.667 * * * * [misc]points:  Computing exacts for 1963 points
1550698904.669 * * * * [misc]points:  Setting MPFR precision to 64
1550698904.873 * * * * [misc]points:  Setting MPFR precision to 320
1550698905.214 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698905.436 * * * * [misc]points:  Sampling 509 additional inputs, on iter 2 have 7491 / 8000
1550698905.440 * * * * [misc]points:  Computing exacts on every 31 of 509 points to ramp up precision
1550698905.442 * * * * [misc]points:  Setting MPFR precision to 64
1550698905.444 * * * * [misc]points:  Setting MPFR precision to 320
1550698905.446 * * * * [misc]points:  Computing exacts on every 15 of 509 points to ramp up precision
1550698905.448 * * * * [misc]points:  Setting MPFR precision to 64
1550698905.452 * * * * [misc]points:  Setting MPFR precision to 320
1550698905.456 * * * * [misc]points:  Computing exacts on every 7 of 509 points to ramp up precision
1550698905.458 * * * * [misc]points:  Setting MPFR precision to 64
1550698905.466 * * * * [misc]points:  Setting MPFR precision to 320
1550698905.938 * * * * [misc]points:  Computing exacts on every 3 of 509 points to ramp up precision
1550698905.939 * * * * [misc]points:  Setting MPFR precision to 64
1550698905.952 * * * * [misc]points:  Setting MPFR precision to 320
1550698905.968 * * * * [misc]points:  Computing exacts for 509 points
1550698905.970 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.033 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.103 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698906.185 * * * * [misc]points:  Sampling 133 additional inputs, on iter 3 have 7867 / 8000
1550698906.186 * * * * [misc]points:  Computing exacts on every 8 of 133 points to ramp up precision
1550698906.188 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.190 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.192 * * * * [misc]points:  Computing exacts on every 4 of 133 points to ramp up precision
1550698906.193 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.199 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.202 * * * * [misc]points:  Computing exacts on every 2 of 133 points to ramp up precision
1550698906.204 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.209 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.215 * * * * [misc]points:  Computing exacts for 133 points
1550698906.217 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.232 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.254 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698906.268 * * * * [misc]points:  Sampling 30 additional inputs, on iter 4 have 7970 / 8000
1550698906.268 * * * * [misc]points:  Computing exacts for 30 points
1550698906.270 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.274 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.278 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698906.281 * * * * [misc]points:  Sampling 6 additional inputs, on iter 5 have 7994 / 8000
1550698906.281 * * * * [misc]points:  Computing exacts for 6 points
1550698906.283 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.284 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.285 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698906.286 * * * * [misc]points:  Sampling 4 additional inputs, on iter 6 have 7999 / 8000
1550698906.286 * * * * [misc]points:  Computing exacts for 4 points
1550698906.288 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.288 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.289 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698906.289 * * * * [exit]points:  Sampled 8001 points with exact outputs
1550698911.394 * [misc]regime-testing:  Baseline error score: 64.0
1550698911.397 * [misc]regime-testing:  Oracle error score: 64.0
1550698911.413 * [misc]regime-testing:  End program error score: 0.6101850534276506