1550699424.667 * [misc]progress:  [Phase 1 of 3] Setting up.
1550699424.669 * * * [misc]progress:  [1/2] Preparing points
1550699424.670 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1550699424.678 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1550699424.789 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.794 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.798 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1550699424.800 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.803 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.807 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1550699424.810 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.815 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.825 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1550699424.826 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.837 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.848 * * * * [misc]points:  Computing exacts for 256 points
1550699424.850 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.877 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.916 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699424.999 * * * * [misc]points:  Sampling 70 additional inputs, on iter 1 have 186 / 256
1550699425.000 * * * * [misc]points:  Computing exacts on every 4 of 70 points to ramp up precision
1550699425.002 * * * * [misc]points:  Setting MPFR precision to 64
1550699425.006 * * * * [misc]points:  Setting MPFR precision to 320
1550699425.009 * * * * [misc]points:  Computing exacts on every 2 of 70 points to ramp up precision
1550699425.011 * * * * [misc]points:  Setting MPFR precision to 64
1550699425.014 * * * * [misc]points:  Setting MPFR precision to 320
1550699425.018 * * * * [misc]points:  Computing exacts for 70 points
1550699425.020 * * * * [misc]points:  Setting MPFR precision to 64
1550699425.029 * * * * [misc]points:  Setting MPFR precision to 320
1550699425.041 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699425.047 * * * * [misc]points:  Sampling 17 additional inputs, on iter 2 have 239 / 256
1550699425.047 * * * * [misc]points:  Computing exacts for 17 points
1550699425.049 * * * * [misc]points:  Setting MPFR precision to 64
1550699425.052 * * * * [misc]points:  Setting MPFR precision to 320
1550699425.054 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699425.055 * * * * [misc]points:  Sampling 6 additional inputs, on iter 3 have 250 / 256
1550699425.055 * * * * [misc]points:  Computing exacts for 6 points
1550699425.058 * * * * [misc]points:  Setting MPFR precision to 64
1550699425.059 * * * * [misc]points:  Setting MPFR precision to 320
1550699425.060 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699425.061 * * * * [misc]points:  Sampling 4 additional inputs, on iter 4 have 254 / 256
1550699425.061 * * * * [misc]points:  Computing exacts for 4 points
1550699425.064 * * * * [misc]points:  Setting MPFR precision to 64
1550699425.064 * * * * [misc]points:  Setting MPFR precision to 320
1550699425.066 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699425.066 * * * * [exit]points:  Sampled 257 points with exact outputs
1550699425.068 * * * [misc]progress:  [2/2] Setting up program.
1550699425.100 * [misc]progress:  [Phase 2 of 3] Improving.
1550699425.100 * * * * [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))>
1550699425.102 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550699425.104 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699425.113 * * [misc]simplify:  iters left: 4 (31 enodes)
1550699425.124 * * [misc]simplify:  iters left: 3 (65 enodes)
1550699425.147 * * [misc]simplify:  iters left: 2 (207 enodes)
1550699425.272 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699425.272 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699425.273 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550699425.274 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550699425.276 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550699425.282 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550699425.303 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550699425.339 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550699425.368 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550699425.396 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550699425.397 * [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))
1550699425.426 * * [misc]progress:  iteration 1 / 4
1550699425.426 * * * [misc]progress:  picking best candidate
1550699425.453 * * * * [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))>
1550699425.453 * * * [misc]progress:  localizing error
1550699425.803 * * * [misc]progress:  generating rewritten candidates
1550699425.803 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1550699425.809 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1550699425.809 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550699425.814 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1)
1550699425.819 * * * [misc]progress:  generating series expansions
1550699425.819 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1550699425.819 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1550699425.819 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550699425.819 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1)
1550699425.819 * * * [misc]progress:  simplifying candidates
1550699425.819 * * * * [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))>
1550699425.820 * * * * [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))>
1550699425.820 * * * * [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)))))))>
1550699425.820 * [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)))))
1550699425.820 * * [misc]simplify:  iters left: 5 (11 enodes)
1550699425.825 * * [misc]simplify:  iters left: 4 (35 enodes)
1550699425.838 * * [misc]simplify:  iters left: 3 (100 enodes)
1550699425.885 * * [misc]simplify:  iters left: 2 (360 enodes)
1550699426.235 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699426.236 * * [misc]simplify:  Extracting #1: cost 48 inf + 0
1550699426.237 * * [misc]simplify:  Extracting #2: cost 223 inf + 0
1550699426.242 * * [misc]simplify:  Extracting #3: cost 348 inf + 45039
1550699426.268 * * [misc]simplify:  Extracting #4: cost 315 inf + 336131
1550699426.344 * * [misc]simplify:  Extracting #5: cost 84 inf + 852438
1550699426.432 * * [misc]simplify:  Extracting #6: cost 1 inf + 990774
1550699426.518 * * [misc]simplify:  Extracting #7: cost 0 inf + 992777
1550699426.606 * [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))))
1550699426.606 * [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)))))))
1550699426.606 * * * * [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))>
1550699426.606 * * * * [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))>
1550699426.606 * * * * [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))>
1550699426.606 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550699426.606 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699426.611 * * [misc]simplify:  iters left: 4 (31 enodes)
1550699426.621 * * [misc]simplify:  iters left: 3 (65 enodes)
1550699426.647 * * [misc]simplify:  iters left: 2 (207 enodes)
1550699426.765 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699426.765 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699426.766 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550699426.767 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550699426.769 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550699426.776 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550699426.802 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550699426.840 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550699426.875 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550699426.909 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550699426.909 * [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))
1550699426.910 * * * * [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))>
1550699426.910 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550699426.910 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699426.914 * * [misc]simplify:  iters left: 4 (31 enodes)
1550699426.925 * * [misc]simplify:  iters left: 3 (65 enodes)
1550699426.950 * * [misc]simplify:  iters left: 2 (207 enodes)
1550699427.070 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699427.071 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699427.071 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550699427.072 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550699427.073 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550699427.080 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550699427.106 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550699427.140 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550699427.178 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550699427.211 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550699427.211 * [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))
1550699427.211 * * * * [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))>
1550699427.212 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550699427.212 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699427.216 * * [misc]simplify:  iters left: 4 (31 enodes)
1550699427.226 * * [misc]simplify:  iters left: 3 (65 enodes)
1550699427.251 * * [misc]simplify:  iters left: 2 (207 enodes)
1550699427.368 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699427.368 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699427.368 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550699427.369 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550699427.371 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550699427.378 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550699427.403 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550699427.437 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550699427.476 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550699427.512 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550699427.512 * [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))
1550699427.512 * * * * [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))>
1550699427.513 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550699427.513 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699427.517 * * [misc]simplify:  iters left: 4 (31 enodes)
1550699427.527 * * [misc]simplify:  iters left: 3 (65 enodes)
1550699427.549 * * [misc]simplify:  iters left: 2 (207 enodes)
1550699427.669 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699427.669 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699427.669 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1550699427.670 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1550699427.673 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1550699427.680 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1550699427.706 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1550699427.741 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1550699427.780 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1550699427.812 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1550699427.812 * [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))
1550699427.812 * * * [misc]progress:  adding candidates to table
1550699428.343 * * [misc]progress:  iteration 2 / 4
1550699428.343 * * * [misc]progress:  picking best candidate
1550699428.454 * * * * [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)))))))>
1550699428.455 * * * [misc]progress:  localizing error
1550699428.823 * * * [misc]progress:  generating rewritten candidates
1550699428.823 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2)
1550699428.829 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2)
1550699428.833 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 2)
1550699428.834 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2 2 2 1)
1550699428.837 * * * [misc]progress:  generating series expansions
1550699428.837 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2)
1550699428.837 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2)
1550699428.837 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 2)
1550699428.837 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2 2 2 1)
1550699428.838 * * * [misc]progress:  simplifying candidates
1550699428.838 * * * * [misc]progress:  [ 1 / 8 ] 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)))))>
1550699428.838 * * * * [misc]progress:  [ 2 / 8 ] 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))))))>
1550699428.838 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699428.838 * * [misc]simplify:  iters left: 4 (9 enodes)
1550699428.842 * * [misc]simplify:  iters left: 3 (24 enodes)
1550699428.850 * * [misc]simplify:  iters left: 2 (47 enodes)
1550699428.880 * * [misc]simplify:  iters left: 1 (110 enodes)
1550699428.936 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699428.936 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550699428.936 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550699428.936 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550699428.937 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550699428.938 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550699428.942 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550699428.952 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550699428.965 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550699428.978 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699428.978 * [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)))
1550699428.978 * * * * [misc]progress:  [ 3 / 8 ] 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) (neg.p16 (*.p16 a c))))))))>
1550699428.978 * * * * [misc]progress:  [ 4 / 8 ] 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 (*.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))))))))>
1550699428.979 * * * * [misc]progress:  [ 5 / 8 ] 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)))))))>
1550699428.979 * [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))))))
1550699428.979 * * [misc]simplify:  iters left: 6 (15 enodes)
1550699428.986 * * [misc]simplify:  iters left: 5 (47 enodes)
1550699429.003 * * [misc]simplify:  iters left: 4 (100 enodes)
1550699429.047 * * [misc]simplify:  iters left: 3 (250 enodes)
1550699429.272 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699429.272 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550699429.272 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1550699429.273 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1550699429.275 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1550699429.286 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1550699429.299 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1550699429.318 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1550699429.335 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1550699429.353 * [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)))
1550699429.353 * [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))))
1550699429.353 * * * * [misc]progress:  [ 6 / 8 ] 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)))))))>
1550699429.354 * [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))))))
1550699429.355 * * [misc]simplify:  iters left: 6 (15 enodes)
1550699429.361 * * [misc]simplify:  iters left: 5 (47 enodes)
1550699429.379 * * [misc]simplify:  iters left: 4 (100 enodes)
1550699429.419 * * [misc]simplify:  iters left: 3 (250 enodes)
1550699429.636 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699429.636 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550699429.637 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1550699429.637 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1550699429.639 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1550699429.646 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1550699429.659 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1550699429.681 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1550699429.701 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1550699429.721 * [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)))
1550699429.721 * [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))))
1550699429.721 * * * * [misc]progress:  [ 7 / 8 ] 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)))))))>
1550699429.722 * [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))))))
1550699429.722 * * [misc]simplify:  iters left: 6 (15 enodes)
1550699429.728 * * [misc]simplify:  iters left: 5 (47 enodes)
1550699429.746 * * [misc]simplify:  iters left: 4 (100 enodes)
1550699429.786 * * [misc]simplify:  iters left: 3 (250 enodes)
1550699430.001 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699430.001 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550699430.001 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1550699430.002 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1550699430.004 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1550699430.011 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1550699430.024 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1550699430.042 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1550699430.060 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1550699430.081 * [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)))
1550699430.081 * [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))))
1550699430.081 * * * * [misc]progress:  [ 8 / 8 ] 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)))))))>
1550699430.082 * [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))))))
1550699430.082 * * [misc]simplify:  iters left: 6 (15 enodes)
1550699430.088 * * [misc]simplify:  iters left: 5 (47 enodes)
1550699430.106 * * [misc]simplify:  iters left: 4 (100 enodes)
1550699430.144 * * [misc]simplify:  iters left: 3 (250 enodes)
1550699430.361 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699430.361 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1550699430.362 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1550699430.362 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1550699430.364 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1550699430.371 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1550699430.384 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1550699430.401 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1550699430.420 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1550699430.439 * [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)))
1550699430.439 * [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))))
1550699430.439 * * * [misc]progress:  adding candidates to table
1550699431.024 * * [misc]progress:  iteration 3 / 4
1550699431.025 * * * [misc]progress:  picking best candidate
1550699431.180 * * * * [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))))))>
1550699431.180 * * * [misc]progress:  localizing error
1550699431.284 * * * [misc]progress:  generating rewritten candidates
1550699431.284 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2)
1550699431.289 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1550699431.292 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2)
1550699431.292 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1550699431.299 * * * [misc]progress:  generating series expansions
1550699431.299 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2)
1550699431.299 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1550699431.299 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2)
1550699431.299 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1550699431.299 * * * [misc]progress:  simplifying candidates
1550699431.299 * * * * [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))))>
1550699431.299 * * * * [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)))>
1550699431.299 * [enter]simplify:  Simplifying (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2))))
1550699431.300 * * [misc]simplify:  iters left: 4 (9 enodes)
1550699431.304 * * [misc]simplify:  iters left: 3 (24 enodes)
1550699431.312 * * [misc]simplify:  iters left: 2 (53 enodes)
1550699431.343 * * [misc]simplify:  iters left: 1 (140 enodes)
1550699431.480 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699431.481 * * [misc]simplify:  Extracting #1: cost 24 inf + 0
1550699431.481 * * [misc]simplify:  Extracting #2: cost 70 inf + 0
1550699431.482 * * [misc]simplify:  Extracting #3: cost 62 inf + 3454
1550699431.485 * * [misc]simplify:  Extracting #4: cost 19 inf + 33897
1550699431.491 * * [misc]simplify:  Extracting #5: cost 0 inf + 53655
1550699431.497 * [exit]simplify:  Simplified to (+.p16 (*.p16 c a) (real->posit16 0.0))
1550699431.497 * [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)))
1550699431.498 * * * * [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))))))>
1550699431.498 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699431.498 * * [misc]simplify:  iters left: 4 (9 enodes)
1550699431.502 * * [misc]simplify:  iters left: 3 (24 enodes)
1550699431.510 * * [misc]simplify:  iters left: 2 (47 enodes)
1550699431.526 * * [misc]simplify:  iters left: 1 (110 enodes)
1550699431.583 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699431.583 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550699431.583 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550699431.583 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550699431.584 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550699431.585 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550699431.589 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550699431.600 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550699431.611 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550699431.623 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699431.624 * [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)))
1550699431.624 * * * * [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))))))>
1550699431.624 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699431.624 * * [misc]simplify:  iters left: 4 (9 enodes)
1550699431.628 * * [misc]simplify:  iters left: 3 (24 enodes)
1550699431.636 * * [misc]simplify:  iters left: 2 (47 enodes)
1550699431.653 * * [misc]simplify:  iters left: 1 (110 enodes)
1550699431.707 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699431.707 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550699431.707 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550699431.708 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550699431.708 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550699431.709 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550699431.717 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550699431.727 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550699431.739 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550699431.751 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699431.751 * [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)))
1550699431.752 * * * * [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))))))>
1550699431.752 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699431.752 * * [misc]simplify:  iters left: 4 (9 enodes)
1550699431.756 * * [misc]simplify:  iters left: 3 (24 enodes)
1550699431.763 * * [misc]simplify:  iters left: 2 (47 enodes)
1550699431.780 * * [misc]simplify:  iters left: 1 (110 enodes)
1550699431.836 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699431.836 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550699431.836 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550699431.836 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550699431.837 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550699431.838 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550699431.842 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550699431.852 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550699431.864 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550699431.878 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699431.878 * [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)))
1550699431.878 * * * * [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))))))>
1550699431.879 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699431.879 * * [misc]simplify:  iters left: 4 (9 enodes)
1550699431.882 * * [misc]simplify:  iters left: 3 (24 enodes)
1550699431.890 * * [misc]simplify:  iters left: 2 (47 enodes)
1550699431.907 * * [misc]simplify:  iters left: 1 (110 enodes)
1550699431.959 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699431.959 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1550699431.959 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1550699431.959 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1550699431.960 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1550699431.961 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1550699431.964 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1550699431.974 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1550699431.986 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1550699431.998 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699431.998 * [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)))
1550699431.999 * * * [misc]progress:  adding candidates to table
1550699432.291 * * [misc]progress:  iteration 4 / 4
1550699432.291 * * * [misc]progress:  picking best candidate
1550699432.402 * * * * [misc]pick:  Picked  #<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))>
1550699432.402 * * * [misc]progress:  localizing error
1550699432.825 * * * [misc]progress:  generating rewritten candidates
1550699432.825 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 2 1)
1550699432.832 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1550699432.835 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 2)
1550699432.836 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1550699432.840 * * * [misc]progress:  generating series expansions
1550699432.840 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 2 1)
1550699432.840 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1550699432.840 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 2)
1550699432.840 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1550699432.840 * * * [misc]progress:  simplifying candidates
1550699432.841 * * * * [misc]progress:  [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) a))>
1550699432.841 * [enter]simplify:  Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
1550699432.841 * * [misc]simplify:  iters left: 2 (6 enodes)
1550699432.843 * * [misc]simplify:  iters left: 1 (14 enodes)
1550699432.847 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699432.847 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699432.847 * * [misc]simplify:  Extracting #2: cost 6 inf + 0
1550699432.847 * * [misc]simplify:  Extracting #3: cost 2 inf + 325
1550699432.847 * * [misc]simplify:  Extracting #4: cost 0 inf + 1329
1550699432.848 * [exit]simplify:  Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
1550699432.848 * [misc]simplify:  Simplified (2 1 2 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) a))
1550699432.848 * * * * [misc]progress:  [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 a c) (*.p16 a c)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))) a))>
1550699432.848 * [enter]simplify:  Simplifying (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 a c) (*.p16 a c))))
1550699432.848 * * [misc]simplify:  iters left: 4 (10 enodes)
1550699432.852 * * [misc]simplify:  iters left: 3 (43 enodes)
1550699432.869 * * [misc]simplify:  iters left: 2 (121 enodes)
1550699432.941 * * [misc]simplify:  iters left: 1 (429 enodes)
1550699433.340 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699433.340 * * [misc]simplify:  Extracting #1: cost 46 inf + 0
1550699433.341 * * [misc]simplify:  Extracting #2: cost 270 inf + 0
1550699433.346 * * [misc]simplify:  Extracting #3: cost 354 inf + 59003
1550699433.373 * * [misc]simplify:  Extracting #4: cost 345 inf + 369227
1550699433.470 * * [misc]simplify:  Extracting #5: cost 22 inf + 1102360
1550699433.578 * * [misc]simplify:  Extracting #6: cost 1 inf + 1150488
1550699433.688 * * [misc]simplify:  Extracting #7: cost 0 inf + 1155051
1550699433.800 * [exit]simplify:  Simplified to (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))))
1550699433.800 * [misc]simplify:  Simplified (2 1 2 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))) a))
1550699433.800 * * * * [misc]progress:  [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (neg.p16 b_2) (neg.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))>
1550699433.800 * * * * [misc]progress:  [ 4 / 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 (*.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)))) (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)))))) (+.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))>
1550699433.800 * * * * [misc]progress:  [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.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)))) (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)))))) (*.p16 a (+.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))))))))>
1550699433.801 * [enter]simplify:  Simplifying (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.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)))) (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))))))
1550699433.801 * * [misc]simplify:  iters left: 6 (15 enodes)
1550699433.808 * * [misc]simplify:  iters left: 5 (50 enodes)
1550699433.827 * * [misc]simplify:  iters left: 4 (126 enodes)
1550699433.889 * * [misc]simplify:  iters left: 3 (499 enodes)
1550699434.566 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699434.566 * * [misc]simplify:  Extracting #1: cost 42 inf + 0
1550699434.567 * * [misc]simplify:  Extracting #2: cost 280 inf + 0
1550699434.571 * * [misc]simplify:  Extracting #3: cost 597 inf + 12843
1550699434.593 * * [misc]simplify:  Extracting #4: cost 810 inf + 280829
1550699435.181 * * [misc]simplify:  Extracting #5: cost 230 inf + 1598730
1550699435.343 * * [misc]simplify:  Extracting #6: cost 4 inf + 2036734
1550699435.509 * * [misc]simplify:  Extracting #7: cost 0 inf + 2038740
1550699435.675 * [exit]simplify:  Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b_2) b_2) (-.p16 (neg.p16 b_2) b_2)) (*.p16 c a))
1550699435.675 * [misc]simplify:  Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b_2) b_2) (-.p16 (neg.p16 b_2) b_2)) (*.p16 c a)) (*.p16 a (+.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))))))))
1550699435.675 * * * * [misc]progress:  [ 6 / 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))>
1550699435.675 * * * * [misc]progress:  [ 7 / 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))>
1550699435.675 * * * * [misc]progress:  [ 8 / 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))>
1550699435.675 * * * * [misc]progress:  [ 9 / 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))>
1550699435.675 * * * [misc]progress:  adding candidates to table
1550699436.191 * [misc]progress:  [Phase 3 of 3] Extracting.
1550699436.191 * * [misc]regime:  Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.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 (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 (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))> #<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 (*.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))))))))> #<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))> #<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)))))))>)
1550699436.197 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b_2)
1550699436.197 * * * * [misc]regimes:  Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.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 (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 (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))> #<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 (*.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))))))))> #<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))> #<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)))))))>)
1550699436.747 * * * * [misc]regimes:  Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.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 (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 (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))> #<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 (*.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))))))))> #<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))> #<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)))))))>)
1550699437.283 * * * * [misc]regimes:  Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.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 (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 (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))> #<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 (*.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))))))))> #<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))> #<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)))))))>)
1550699437.851 * * * [misc]regime:  Found split indices: #<option (#s(si 1 108) #s(si 2 256))>
1550699437.853 * [misc]binary-search:  Improving bounds with binary search for b_2 and (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.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 (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 (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))> #<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 (*.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))))))))> #<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))> #<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)))))))>)
1550699437.854 * [misc]regimes:  Found splitpoints: (#s(sp 1 b_2 #<cpointer:posit16>) #s(sp 2 b_2 +nan.0)) , with alts (#<alt (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.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 (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 (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))> #<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 (*.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))))))))> #<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))> #<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)))))))>)
1550699437.855 * [enter]simplify:  Simplifying (if (<=.p16 b_2 (real->posit16 -0.050323486328125)) (/.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))
1550699437.855 * * [misc]simplify:  iters left: 6 (21 enodes)
1550699437.858 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699437.858 * * [misc]simplify:  Extracting #1: cost 4 inf + 0
1550699437.858 * * [misc]simplify:  Extracting #2: cost 10 inf + 0
1550699437.858 * * [misc]simplify:  Extracting #3: cost 12 inf + 2
1550699437.858 * * [misc]simplify:  Extracting #4: cost 13 inf + 84
1550699437.858 * * [misc]simplify:  Extracting #5: cost 15 inf + 152
1550699437.858 * * [misc]simplify:  Extracting #6: cost 11 inf + 716
1550699437.859 * * [misc]simplify:  Extracting #7: cost 6 inf + 3848
1550699437.859 * * [misc]simplify:  Extracting #8: cost 3 inf + 6937
1550699437.860 * * [misc]simplify:  Extracting #9: cost 0 inf + 13357
1550699437.861 * [exit]simplify:  Simplified to (if (<=.p16 b_2 (real->posit16 -0.050323486328125)) (/.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))
1550699437.861 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1550699437.934 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1550699437.938 * * * * [misc]points:  Setting MPFR precision to 64
1550699437.940 * * * * [misc]points:  Setting MPFR precision to 320
1550699437.942 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1550699437.944 * * * * [misc]points:  Setting MPFR precision to 64
1550699437.949 * * * * [misc]points:  Setting MPFR precision to 320
1550699437.954 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1550699437.956 * * * * [misc]points:  Setting MPFR precision to 64
1550699437.964 * * * * [misc]points:  Setting MPFR precision to 320
1550699437.973 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1550699437.975 * * * * [misc]points:  Setting MPFR precision to 64
1550699437.989 * * * * [misc]points:  Setting MPFR precision to 320
1550699438.007 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1550699438.009 * * * * [misc]points:  Setting MPFR precision to 64
1550699438.037 * * * * [misc]points:  Setting MPFR precision to 320
1550699438.071 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1550699438.073 * * * * [misc]points:  Setting MPFR precision to 64
1550699438.128 * * * * [misc]points:  Setting MPFR precision to 320
1550699438.242 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1550699438.244 * * * * [misc]points:  Setting MPFR precision to 64
1550699438.354 * * * * [misc]points:  Setting MPFR precision to 320
1550699438.543 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1550699438.545 * * * * [misc]points:  Setting MPFR precision to 64
1550699438.815 * * * * [misc]points:  Setting MPFR precision to 320
1550699439.156 * * * * [misc]points:  Computing exacts for 8000 points
1550699439.158 * * * * [misc]points:  Setting MPFR precision to 64
1550699440.312 * * * * [misc]points:  Setting MPFR precision to 320
1550699442.318 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699443.070 * * * * [misc]points:  Sampling 1949 additional inputs, on iter 1 have 6051 / 8000
1550699443.085 * * * * [misc]points:  Computing exacts on every 121 of 1949 points to ramp up precision
1550699443.088 * * * * [misc]points:  Setting MPFR precision to 64
1550699443.115 * * * * [misc]points:  Setting MPFR precision to 320
1550699443.117 * * * * [misc]points:  Computing exacts on every 60 of 1949 points to ramp up precision
1550699443.119 * * * * [misc]points:  Setting MPFR precision to 64
1550699443.122 * * * * [misc]points:  Setting MPFR precision to 320
1550699443.127 * * * * [misc]points:  Computing exacts on every 30 of 1949 points to ramp up precision
1550699443.129 * * * * [misc]points:  Setting MPFR precision to 64
1550699443.136 * * * * [misc]points:  Setting MPFR precision to 320
1550699443.145 * * * * [misc]points:  Computing exacts on every 15 of 1949 points to ramp up precision
1550699443.147 * * * * [misc]points:  Setting MPFR precision to 64
1550699443.160 * * * * [misc]points:  Setting MPFR precision to 320
1550699443.177 * * * * [misc]points:  Computing exacts on every 7 of 1949 points to ramp up precision
1550699443.179 * * * * [misc]points:  Setting MPFR precision to 64
1550699443.205 * * * * [misc]points:  Setting MPFR precision to 320
1550699443.239 * * * * [misc]points:  Computing exacts on every 3 of 1949 points to ramp up precision
1550699443.241 * * * * [misc]points:  Setting MPFR precision to 64
1550699443.296 * * * * [misc]points:  Setting MPFR precision to 320
1550699443.424 * * * * [misc]points:  Computing exacts for 1949 points
1550699443.426 * * * * [misc]points:  Setting MPFR precision to 64
1550699443.714 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.043 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699444.265 * * * * [misc]points:  Sampling 473 additional inputs, on iter 2 have 7527 / 8000
1550699444.269 * * * * [misc]points:  Computing exacts on every 29 of 473 points to ramp up precision
1550699444.271 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.273 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.275 * * * * [misc]points:  Computing exacts on every 14 of 473 points to ramp up precision
1550699444.277 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.280 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.285 * * * * [misc]points:  Computing exacts on every 7 of 473 points to ramp up precision
1550699444.286 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.292 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.300 * * * * [misc]points:  Computing exacts on every 3 of 473 points to ramp up precision
1550699444.302 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.315 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.331 * * * * [misc]points:  Computing exacts for 473 points
1550699444.332 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.415 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.496 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699444.552 * * * * [misc]points:  Sampling 109 additional inputs, on iter 3 have 7891 / 8000
1550699444.553 * * * * [misc]points:  Computing exacts on every 6 of 109 points to ramp up precision
1550699444.556 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.558 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.561 * * * * [misc]points:  Computing exacts on every 3 of 109 points to ramp up precision
1550699444.563 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.567 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.572 * * * * [misc]points:  Computing exacts for 109 points
1550699444.574 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.587 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.604 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699444.616 * * * * [misc]points:  Sampling 31 additional inputs, on iter 4 have 7969 / 8000
1550699444.616 * * * * [misc]points:  Computing exacts for 31 points
1550699444.618 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.622 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.626 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699444.629 * * * * [misc]points:  Sampling 11 additional inputs, on iter 5 have 7989 / 8000
1550699444.630 * * * * [misc]points:  Computing exacts for 11 points
1550699444.631 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.633 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.635 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699444.636 * * * * [misc]points:  Sampling 4 additional inputs, on iter 6 have 7997 / 8000
1550699444.636 * * * * [misc]points:  Computing exacts for 4 points
1550699444.638 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.639 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.639 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699444.639 * * * * [misc]points:  Sampling 4 additional inputs, on iter 7 have 7998 / 8000
1550699444.639 * * * * [misc]points:  Computing exacts for 4 points
1550699444.641 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.642 * * * * [misc]points:  Setting MPFR precision to 320
1550699444.643 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699444.643 * * * * [exit]points:  Sampled 8001 points with exact outputs
1550699450.927 * [misc]regime-testing:  Baseline error score: 64.0
1550699450.931 * [misc]regime-testing:  Oracle error score: 64.0
1550699450.941 * [misc]regime-testing:  End program error score: 0.6080163782800997