1554300744.222 * [misc]progress:  [Phase 1 of 3] Setting up.
1554300744.223 * * * [misc]progress:  [1/2] Preparing points
1554300744.223 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1554300744.225 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1554300744.325 * * * * [misc]points:  Setting MPFR precision to 64
1554300744.330 * * * * [misc]points:  Setting MPFR precision to 320
1554300744.333 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1554300744.337 * * * * [misc]points:  Setting MPFR precision to 64
1554300744.342 * * * * [misc]points:  Setting MPFR precision to 320
1554300744.347 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1554300744.349 * * * * [misc]points:  Setting MPFR precision to 64
1554300744.356 * * * * [misc]points:  Setting MPFR precision to 320
1554300744.361 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1554300744.363 * * * * [misc]points:  Setting MPFR precision to 64
1554300744.403 * * * * [misc]points:  Setting MPFR precision to 320
1554300744.417 * * * * [misc]points:  Computing exacts for 256 points
1554300744.420 * * * * [misc]points:  Setting MPFR precision to 64
1554300744.487 * * * * [misc]points:  Setting MPFR precision to 320
1554300744.521 * * * * [misc]points:  Filtering points with unrepresentable outputs
1554300744.584 * * * * [exit]points:  Sampled 256 points with exact outputs
1554300744.585 * * * [misc]progress:  [2/2] Setting up program.
1554300744.609 * [misc]progress:  [Phase 2 of 3] Improving.
1554300744.609 * * * * [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))>
1554300744.611 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1554300744.612 * * [misc]simplify:  iters left: 5 (10 enodes)
1554300744.621 * * [misc]simplify:  iters left: 4 (31 enodes)
1554300744.632 * * [misc]simplify:  iters left: 3 (65 enodes)
1554300744.656 * * [misc]simplify:  iters left: 2 (207 enodes)
1554300745.562 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300745.562 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1554300745.563 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1554300745.564 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1554300745.566 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1554300745.575 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1554300745.600 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1554300745.636 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1554300745.671 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1554300745.713 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1554300745.713 * [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))
1554300745.736 * * [misc]progress:  iteration 1 / 4
1554300745.736 * * * [misc]progress:  picking best candidate
1554300745.755 * * * * [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))>
1554300745.755 * * * [misc]progress:  localizing error
1554300745.969 * * * [misc]progress:  generating rewritten candidates
1554300745.969 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1554300745.972 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1554300745.973 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1554300745.975 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1)
1554300745.977 * * * [misc]progress:  generating series expansions
1554300745.977 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1554300745.977 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1554300745.978 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1554300745.978 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1)
1554300745.978 * * * [misc]progress:  simplifying candidates
1554300745.978 * * * * [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))>
1554300745.978 * * * * [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))>
1554300745.978 * * * * [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)))))))>
1554300745.978 * [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)))))
1554300745.978 * * [misc]simplify:  iters left: 5 (11 enodes)
1554300745.980 * * [misc]simplify:  iters left: 4 (35 enodes)
1554300745.986 * * [misc]simplify:  iters left: 3 (100 enodes)
1554300746.008 * * [misc]simplify:  iters left: 2 (360 enodes)
1554300746.206 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300746.207 * * [misc]simplify:  Extracting #1: cost 48 inf + 0
1554300746.207 * * [misc]simplify:  Extracting #2: cost 223 inf + 0
1554300746.209 * * [misc]simplify:  Extracting #3: cost 348 inf + 45039
1554300746.222 * * [misc]simplify:  Extracting #4: cost 315 inf + 336131
1554300746.266 * * [misc]simplify:  Extracting #5: cost 84 inf + 852438
1554300746.309 * * [misc]simplify:  Extracting #6: cost 1 inf + 990774
1554300746.353 * * [misc]simplify:  Extracting #7: cost 0 inf + 992777
1554300746.401 * [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))))
1554300746.401 * [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)))))))
1554300746.401 * * * * [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))>
1554300746.401 * * * * [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))>
1554300746.401 * * * * [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))>
1554300746.402 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1554300746.402 * * [misc]simplify:  iters left: 5 (10 enodes)
1554300746.405 * * [misc]simplify:  iters left: 4 (31 enodes)
1554300746.414 * * [misc]simplify:  iters left: 3 (65 enodes)
1554300746.435 * * [misc]simplify:  iters left: 2 (207 enodes)
1554300746.534 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300746.534 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1554300746.534 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1554300746.534 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1554300746.536 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1554300746.539 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1554300746.551 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1554300746.584 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1554300746.617 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1554300746.633 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1554300746.633 * [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))
1554300746.633 * * * * [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))>
1554300746.633 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1554300746.634 * * [misc]simplify:  iters left: 5 (10 enodes)
1554300746.635 * * [misc]simplify:  iters left: 4 (31 enodes)
1554300746.645 * * [misc]simplify:  iters left: 3 (65 enodes)
1554300746.671 * * [misc]simplify:  iters left: 2 (207 enodes)
1554300746.758 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300746.758 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1554300746.758 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1554300746.759 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1554300746.761 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1554300746.767 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1554300746.790 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1554300746.816 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1554300746.832 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1554300746.863 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1554300746.864 * [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))
1554300746.864 * * * * [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))>
1554300746.864 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1554300746.864 * * [misc]simplify:  iters left: 5 (10 enodes)
1554300746.868 * * [misc]simplify:  iters left: 4 (31 enodes)
1554300746.878 * * [misc]simplify:  iters left: 3 (65 enodes)
1554300746.892 * * [misc]simplify:  iters left: 2 (207 enodes)
1554300746.971 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300746.971 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1554300746.971 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1554300746.972 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1554300746.973 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1554300746.979 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1554300747.002 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1554300747.033 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1554300747.070 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1554300747.087 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1554300747.088 * [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))
1554300747.088 * * * * [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))>
1554300747.088 * [enter]simplify:  Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1554300747.088 * * [misc]simplify:  iters left: 5 (10 enodes)
1554300747.090 * * [misc]simplify:  iters left: 4 (31 enodes)
1554300747.095 * * [misc]simplify:  iters left: 3 (65 enodes)
1554300747.111 * * [misc]simplify:  iters left: 2 (207 enodes)
1554300747.184 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300747.184 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1554300747.185 * * [misc]simplify:  Extracting #2: cost 89 inf + 1
1554300747.185 * * [misc]simplify:  Extracting #3: cost 168 inf + 83
1554300747.186 * * [misc]simplify:  Extracting #4: cost 227 inf + 12401
1554300747.189 * * [misc]simplify:  Extracting #5: cost 180 inf + 98398
1554300747.201 * * [misc]simplify:  Extracting #6: cost 61 inf + 349602
1554300747.229 * * [misc]simplify:  Extracting #7: cost 2 inf + 436444
1554300747.261 * * [misc]simplify:  Extracting #8: cost 0 inf + 442330
1554300747.278 * [exit]simplify:  Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)
1554300747.278 * [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))
1554300747.278 * * * [misc]progress:  adding candidates to table
1554300747.507 * * [misc]progress:  iteration 2 / 4
1554300747.507 * * * [misc]progress:  picking best candidate
1554300747.565 * * * * [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)))))))>
1554300747.565 * * * [misc]progress:  localizing error
1554300747.733 * * * [misc]progress:  generating rewritten candidates
1554300747.733 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2 2)
1554300747.739 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2)
1554300747.743 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2 2)
1554300747.743 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 2 2 2 1)
1554300747.746 * * * [misc]progress:  generating series expansions
1554300747.746 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2 2)
1554300747.746 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2)
1554300747.746 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2 2)
1554300747.746 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 2 2 2 1)
1554300747.746 * * * [misc]progress:  simplifying candidates
1554300747.746 * * * * [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)))))>
1554300747.746 * * * * [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))))))>
1554300747.746 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554300747.746 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300747.750 * * [misc]simplify:  iters left: 3 (24 enodes)
1554300747.758 * * [misc]simplify:  iters left: 2 (47 enodes)
1554300747.775 * * [misc]simplify:  iters left: 1 (110 enodes)
1554300747.826 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300747.826 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1554300747.826 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1554300747.826 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1554300747.827 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1554300747.827 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1554300747.829 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1554300747.837 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1554300747.843 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1554300747.848 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554300747.848 * [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)))
1554300747.849 * * * * [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))))))))>
1554300747.849 * * * * [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))))))))>
1554300747.849 * * * * [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)))))))>
1554300747.849 * [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))))))
1554300747.849 * * [misc]simplify:  iters left: 6 (15 enodes)
1554300747.852 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300747.863 * * [misc]simplify:  iters left: 4 (100 enodes)
1554300747.900 * * [misc]simplify:  iters left: 3 (250 enodes)
1554300748.042 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300748.042 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554300748.042 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1554300748.042 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1554300748.043 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1554300748.046 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1554300748.052 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1554300748.061 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1554300748.071 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1554300748.088 * [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)))
1554300748.088 * [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))))
1554300748.089 * * * * [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)))))))>
1554300748.089 * [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))))))
1554300748.089 * * [misc]simplify:  iters left: 6 (15 enodes)
1554300748.095 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300748.113 * * [misc]simplify:  iters left: 4 (100 enodes)
1554300748.150 * * [misc]simplify:  iters left: 3 (250 enodes)
1554300748.254 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300748.254 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554300748.255 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1554300748.255 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1554300748.256 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1554300748.259 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1554300748.265 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1554300748.274 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1554300748.282 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1554300748.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)))
1554300748.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))))
1554300748.292 * * * * [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)))))))>
1554300748.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))))))
1554300748.293 * * [misc]simplify:  iters left: 6 (15 enodes)
1554300748.299 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300748.316 * * [misc]simplify:  iters left: 4 (100 enodes)
1554300748.359 * * [misc]simplify:  iters left: 3 (250 enodes)
1554300748.512 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300748.512 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554300748.512 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1554300748.512 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1554300748.513 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1554300748.516 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1554300748.522 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1554300748.530 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1554300748.539 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1554300748.555 * [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)))
1554300748.555 * [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))))
1554300748.555 * * * * [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)))))))>
1554300748.555 * [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))))))
1554300748.555 * * [misc]simplify:  iters left: 6 (15 enodes)
1554300748.562 * * [misc]simplify:  iters left: 5 (47 enodes)
1554300748.579 * * [misc]simplify:  iters left: 4 (100 enodes)
1554300748.616 * * [misc]simplify:  iters left: 3 (250 enodes)
1554300748.782 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300748.782 * * [misc]simplify:  Extracting #1: cost 7 inf + 0
1554300748.782 * * [misc]simplify:  Extracting #2: cost 38 inf + 0
1554300748.783 * * [misc]simplify:  Extracting #3: cost 89 inf + 404
1554300748.784 * * [misc]simplify:  Extracting #4: cost 105 inf + 13282
1554300748.790 * * [misc]simplify:  Extracting #5: cost 75 inf + 74603
1554300748.802 * * [misc]simplify:  Extracting #6: cost 45 inf + 171652
1554300748.821 * * [misc]simplify:  Extracting #7: cost 3 inf + 235044
1554300748.839 * * [misc]simplify:  Extracting #8: cost 0 inf + 242171
1554300748.856 * [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)))
1554300748.856 * [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))))
1554300748.856 * * * [misc]progress:  adding candidates to table
1554300749.105 * * [misc]progress:  iteration 3 / 4
1554300749.105 * * * [misc]progress:  picking best candidate
1554300749.148 * * * * [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))))))>
1554300749.148 * * * [misc]progress:  localizing error
1554300749.193 * * * [misc]progress:  generating rewritten candidates
1554300749.193 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 2)
1554300749.196 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1554300749.197 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 2 2)
1554300749.197 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1554300749.200 * * * [misc]progress:  generating series expansions
1554300749.200 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 2)
1554300749.200 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1554300749.200 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 2 2)
1554300749.200 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1554300749.200 * * * [misc]progress:  simplifying candidates
1554300749.200 * * * * [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))))>
1554300749.200 * * * * [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)))>
1554300749.201 * [enter]simplify:  Simplifying (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2))))
1554300749.201 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300749.203 * * [misc]simplify:  iters left: 3 (24 enodes)
1554300749.212 * * [misc]simplify:  iters left: 2 (53 enodes)
1554300749.224 * * [misc]simplify:  iters left: 1 (140 enodes)
1554300749.306 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300749.306 * * [misc]simplify:  Extracting #1: cost 24 inf + 0
1554300749.306 * * [misc]simplify:  Extracting #2: cost 70 inf + 0
1554300749.306 * * [misc]simplify:  Extracting #3: cost 62 inf + 3454
1554300749.308 * * [misc]simplify:  Extracting #4: cost 19 inf + 33897
1554300749.311 * * [misc]simplify:  Extracting #5: cost 0 inf + 53655
1554300749.314 * [exit]simplify:  Simplified to (+.p16 (*.p16 c a) (real->posit16 0.0))
1554300749.314 * [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)))
1554300749.314 * * * * [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))))))>
1554300749.314 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554300749.314 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300749.316 * * [misc]simplify:  iters left: 3 (24 enodes)
1554300749.319 * * [misc]simplify:  iters left: 2 (47 enodes)
1554300749.329 * * [misc]simplify:  iters left: 1 (110 enodes)
1554300749.375 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300749.375 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1554300749.375 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1554300749.375 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1554300749.375 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1554300749.375 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1554300749.377 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1554300749.382 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1554300749.388 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1554300749.394 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554300749.394 * [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)))
1554300749.394 * * * * [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))))))>
1554300749.394 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554300749.394 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300749.396 * * [misc]simplify:  iters left: 3 (24 enodes)
1554300749.400 * * [misc]simplify:  iters left: 2 (47 enodes)
1554300749.408 * * [misc]simplify:  iters left: 1 (110 enodes)
1554300749.437 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300749.437 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1554300749.437 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1554300749.437 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1554300749.437 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1554300749.437 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1554300749.439 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1554300749.444 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1554300749.450 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1554300749.456 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554300749.456 * [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)))
1554300749.456 * * * * [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))))))>
1554300749.456 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554300749.456 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300749.460 * * [misc]simplify:  iters left: 3 (24 enodes)
1554300749.467 * * [misc]simplify:  iters left: 2 (47 enodes)
1554300749.478 * * [misc]simplify:  iters left: 1 (110 enodes)
1554300749.504 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300749.504 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1554300749.504 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1554300749.504 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1554300749.504 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1554300749.505 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1554300749.506 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1554300749.513 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1554300749.519 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1554300749.525 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554300749.525 * [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)))
1554300749.525 * * * * [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))))))>
1554300749.525 * [enter]simplify:  Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554300749.525 * * [misc]simplify:  iters left: 4 (9 enodes)
1554300749.527 * * [misc]simplify:  iters left: 3 (24 enodes)
1554300749.531 * * [misc]simplify:  iters left: 2 (47 enodes)
1554300749.539 * * [misc]simplify:  iters left: 1 (110 enodes)
1554300749.565 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300749.565 * * [misc]simplify:  Extracting #1: cost 6 inf + 0
1554300749.565 * * [misc]simplify:  Extracting #2: cost 10 inf + 1
1554300749.565 * * [misc]simplify:  Extracting #3: cost 23 inf + 403
1554300749.565 * * [misc]simplify:  Extracting #4: cost 60 inf + 1445
1554300749.566 * * [misc]simplify:  Extracting #5: cost 79 inf + 13843
1554300749.568 * * [misc]simplify:  Extracting #6: cost 73 inf + 57826
1554300749.572 * * [misc]simplify:  Extracting #7: cost 3 inf + 171780
1554300749.578 * * [misc]simplify:  Extracting #8: cost 0 inf + 178629
1554300749.589 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554300749.589 * [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)))
1554300749.590 * * * [misc]progress:  adding candidates to table
1554300749.693 * * [misc]progress:  iteration 4 / 4
1554300749.693 * * * [misc]progress:  picking best candidate
1554300749.743 * * * * [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))>
1554300749.743 * * * [misc]progress:  localizing error
1554300749.942 * * * [misc]progress:  generating rewritten candidates
1554300749.942 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 2 1)
1554300749.946 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1554300749.947 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 2)
1554300749.948 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1554300749.950 * * * [misc]progress:  generating series expansions
1554300749.950 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 2 1)
1554300749.950 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1554300749.950 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 2)
1554300749.950 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1554300749.950 * * * [misc]progress:  simplifying candidates
1554300749.950 * * * * [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))>
1554300749.950 * [enter]simplify:  Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c))
1554300749.950 * * [misc]simplify:  iters left: 2 (6 enodes)
1554300749.951 * * [misc]simplify:  iters left: 1 (14 enodes)
1554300749.953 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300749.953 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1554300749.953 * * [misc]simplify:  Extracting #2: cost 6 inf + 0
1554300749.953 * * [misc]simplify:  Extracting #3: cost 2 inf + 325
1554300749.953 * * [misc]simplify:  Extracting #4: cost 0 inf + 1329
1554300749.953 * [exit]simplify:  Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2))
1554300749.953 * [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))
1554300749.953 * * * * [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))>
1554300749.953 * [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))))
1554300749.954 * * [misc]simplify:  iters left: 4 (10 enodes)
1554300749.956 * * [misc]simplify:  iters left: 3 (43 enodes)
1554300749.964 * * [misc]simplify:  iters left: 2 (121 enodes)
1554300750.024 * * [misc]simplify:  iters left: 1 (429 enodes)
1554300750.352 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300750.352 * * [misc]simplify:  Extracting #1: cost 46 inf + 0
1554300750.353 * * [misc]simplify:  Extracting #2: cost 270 inf + 0
1554300750.355 * * [misc]simplify:  Extracting #3: cost 354 inf + 59003
1554300750.369 * * [misc]simplify:  Extracting #4: cost 345 inf + 369227
1554300750.430 * * [misc]simplify:  Extracting #5: cost 22 inf + 1102360
1554300750.535 * * [misc]simplify:  Extracting #6: cost 1 inf + 1150488
1554300750.626 * * [misc]simplify:  Extracting #7: cost 0 inf + 1155051
1554300750.681 * [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))))
1554300750.681 * [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))
1554300750.681 * * * * [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))>
1554300750.681 * * * * [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))>
1554300750.681 * * * * [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))))))))>
1554300750.681 * [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))))))
1554300750.681 * * [misc]simplify:  iters left: 6 (15 enodes)
1554300750.685 * * [misc]simplify:  iters left: 5 (50 enodes)
1554300750.693 * * [misc]simplify:  iters left: 4 (126 enodes)
1554300750.723 * * [misc]simplify:  iters left: 3 (499 enodes)
1554300751.100 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300751.100 * * [misc]simplify:  Extracting #1: cost 42 inf + 0
1554300751.100 * * [misc]simplify:  Extracting #2: cost 280 inf + 0
1554300751.102 * * [misc]simplify:  Extracting #3: cost 597 inf + 12843
1554300751.112 * * [misc]simplify:  Extracting #4: cost 810 inf + 280829
1554300751.177 * * [misc]simplify:  Extracting #5: cost 230 inf + 1598730
1554300751.295 * * [misc]simplify:  Extracting #6: cost 4 inf + 2036734
1554300751.385 * * [misc]simplify:  Extracting #7: cost 0 inf + 2038740
1554300751.550 * [exit]simplify:  Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b_2) b_2) (-.p16 (neg.p16 b_2) b_2)) (*.p16 c a))
1554300751.551 * [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))))))))
1554300751.551 * * * * [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))>
1554300751.551 * * * * [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))>
1554300751.551 * * * * [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))>
1554300751.551 * * * * [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))>
1554300751.551 * * * [misc]progress:  adding candidates to table
1554300751.749 * [misc]progress:  [Phase 3 of 3] Extracting.
1554300751.750 * * [misc]regime:  Finding splitpoints for: (#<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 (*.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 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)))))))> #<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 (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))))))))> #<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 (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))>)
1554300751.754 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b_2)
1554300751.754 * * * * [misc]regimes:  Trying to branch on c from (#<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 (*.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 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)))))))> #<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 (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))))))))> #<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 (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))>)
1554300751.901 * * * * [misc]regimes:  Trying to branch on a from (#<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 (*.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 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)))))))> #<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 (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))))))))> #<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 (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))>)
1554300752.116 * * * * [misc]regimes:  Trying to branch on b_2 from (#<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 (*.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 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)))))))> #<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 (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))))))))> #<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 (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))>)
1554300752.314 * * * [misc]regime:  Found split indices: #<option (#s(si 1 108) #s(si 2 256))>
1554300752.316 * [misc]binary-search:  Improving bounds with binary search for b_2 and (#<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 (*.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 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)))))))> #<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 (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))))))))> #<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 (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))>)
1554300752.317 * [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 (-.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 (*.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 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)))))))> #<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 (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))))))))> #<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 (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))>)
1554300752.318 * [enter]simplify:  Simplifying (if (<=.p16 b_2 (real->posit16 -0.0083465576171875)) (/.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))
1554300752.318 * * [misc]simplify:  iters left: 6 (21 enodes)
1554300752.320 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1554300752.320 * * [misc]simplify:  Extracting #1: cost 4 inf + 0
1554300752.320 * * [misc]simplify:  Extracting #2: cost 10 inf + 0
1554300752.320 * * [misc]simplify:  Extracting #3: cost 12 inf + 2
1554300752.320 * * [misc]simplify:  Extracting #4: cost 13 inf + 84
1554300752.321 * * [misc]simplify:  Extracting #5: cost 15 inf + 152
1554300752.321 * * [misc]simplify:  Extracting #6: cost 11 inf + 716
1554300752.321 * * [misc]simplify:  Extracting #7: cost 6 inf + 3848
1554300752.321 * * [misc]simplify:  Extracting #8: cost 3 inf + 6937
1554300752.322 * * [misc]simplify:  Extracting #9: cost 0 inf + 13357
1554300752.323 * [exit]simplify:  Simplified to (if (<=.p16 b_2 (real->posit16 -0.0083465576171875)) (/.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))
1554300752.323 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1554300752.393 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1554300752.395 * * * * [misc]points:  Setting MPFR precision to 64
1554300752.397 * * * * [misc]points:  Setting MPFR precision to 320
1554300752.399 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1554300752.401 * * * * [misc]points:  Setting MPFR precision to 64
1554300752.405 * * * * [misc]points:  Setting MPFR precision to 320
1554300752.409 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1554300752.411 * * * * [misc]points:  Setting MPFR precision to 64
1554300752.419 * * * * [misc]points:  Setting MPFR precision to 320
1554300752.426 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1554300752.428 * * * * [misc]points:  Setting MPFR precision to 64
1554300752.443 * * * * [misc]points:  Setting MPFR precision to 320
1554300752.459 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1554300752.461 * * * * [misc]points:  Setting MPFR precision to 64
1554300752.490 * * * * [misc]points:  Setting MPFR precision to 320
1554300752.520 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1554300752.522 * * * * [misc]points:  Setting MPFR precision to 64
1554300752.573 * * * * [misc]points:  Setting MPFR precision to 320
1554300752.661 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1554300752.662 * * * * [misc]points:  Setting MPFR precision to 64
1554300752.728 * * * * [misc]points:  Setting MPFR precision to 320
1554300752.853 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1554300752.855 * * * * [misc]points:  Setting MPFR precision to 64
1554300753.054 * * * * [misc]points:  Setting MPFR precision to 320
1554300753.238 * * * * [misc]points:  Computing exacts for 8000 points
1554300753.239 * * * * [misc]points:  Setting MPFR precision to 64
1554300754.508 * * * * [misc]points:  Setting MPFR precision to 320
1554300755.569 * * * * [misc]points:  Filtering points with unrepresentable outputs
1554300755.647 * * * * [exit]points:  Sampled 8000 points with exact outputs
1554300759.565 * [misc]regime-testing:  Baseline error score: 64.0
1554300759.568 * [misc]regime-testing:  Oracle error score: 64.0
1554300759.572 * [misc]regime-testing:  End program error score: 0.428295540680606