1550699424.404 * [misc]progress:  [Phase 1 of 3] Setting up.
1550699424.406 * * * [misc]progress:  [1/2] Preparing points
1550699424.407 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1550699424.415 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1550699424.519 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.525 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.529 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1550699424.531 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.535 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.539 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1550699424.542 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.548 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.556 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1550699424.558 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.568 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.581 * * * * [misc]points:  Computing exacts for 256 points
1550699424.583 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.613 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.647 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699424.729 * * * * [misc]points:  Sampling 70 additional inputs, on iter 1 have 186 / 256
1550699424.729 * * * * [misc]points:  Computing exacts on every 4 of 70 points to ramp up precision
1550699424.735 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.737 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.739 * * * * [misc]points:  Computing exacts on every 2 of 70 points to ramp up precision
1550699424.741 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.744 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.748 * * * * [misc]points:  Computing exacts for 70 points
1550699424.750 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.758 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.768 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699424.775 * * * * [misc]points:  Sampling 17 additional inputs, on iter 2 have 239 / 256
1550699424.775 * * * * [misc]points:  Computing exacts for 17 points
1550699424.777 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.779 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.782 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699424.783 * * * * [misc]points:  Sampling 6 additional inputs, on iter 3 have 250 / 256
1550699424.783 * * * * [misc]points:  Computing exacts for 6 points
1550699424.785 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.786 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.787 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699424.788 * * * * [misc]points:  Sampling 4 additional inputs, on iter 4 have 254 / 256
1550699424.788 * * * * [misc]points:  Computing exacts for 4 points
1550699424.790 * * * * [misc]points:  Setting MPFR precision to 64
1550699424.790 * * * * [misc]points:  Setting MPFR precision to 320
1550699424.791 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699424.791 * * * * [exit]points:  Sampled 257 points with exact outputs
1550699424.792 * * * [misc]progress:  [2/2] Setting up program.
1550699424.827 * [misc]progress:  [Phase 2 of 3] Improving.
1550699424.828 * * * * [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))>
1550699424.829 * [enter]simplify:  Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550699424.831 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699424.842 * * [misc]simplify:  iters left: 4 (25 enodes)
1550699424.850 * * [misc]simplify:  iters left: 3 (48 enodes)
1550699424.869 * * [misc]simplify:  iters left: 2 (111 enodes)
1550699424.943 * * [misc]simplify:  iters left: 1 (392 enodes)
1550699425.858 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699425.859 * * [misc]simplify:  Extracting #1: cost 10 inf + 0
1550699425.859 * * [misc]simplify:  Extracting #2: cost 35 inf + 1
1550699425.860 * * [misc]simplify:  Extracting #3: cost 91 inf + 405
1550699425.862 * * [misc]simplify:  Extracting #4: cost 331 inf + 2291
1550699425.869 * * [misc]simplify:  Extracting #5: cost 455 inf + 80323
1550699425.907 * * [misc]simplify:  Extracting #6: cost 250 inf + 579968
1550699425.985 * * [misc]simplify:  Extracting #7: cost 28 inf + 1003440
1550699426.079 * * [misc]simplify:  Extracting #8: cost 0 inf + 1069311
1550699426.167 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550699426.167 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
1550699426.232 * * [misc]progress:  iteration 1 / 4
1550699426.232 * * * [misc]progress:  picking best candidate
1550699426.259 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1550699426.259 * * * [misc]progress:  localizing error
1550699426.574 * * * [misc]progress:  generating rewritten candidates
1550699426.575 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1550699426.579 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1)
1550699426.580 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550699426.584 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1 1)
1550699426.588 * * * [misc]progress:  generating series expansions
1550699426.589 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1550699426.589 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1)
1550699426.589 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550699426.589 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1 1)
1550699426.589 * * * [misc]progress:  simplifying candidates
1550699426.589 * * * * [misc]progress:  [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2)) a))>
1550699426.589 * * * * [misc]progress:  [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699426.589 * * * * [misc]progress:  [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))>
1550699426.590 * [enter]simplify:  Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))
1550699426.590 * * [misc]simplify:  iters left: 5 (9 enodes)
1550699426.594 * * [misc]simplify:  iters left: 4 (32 enodes)
1550699426.606 * * [misc]simplify:  iters left: 3 (94 enodes)
1550699426.663 * * [misc]simplify:  iters left: 2 (340 enodes)
1550699426.987 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699426.987 * * [misc]simplify:  Extracting #1: cost 50 inf + 0
1550699426.988 * * [misc]simplify:  Extracting #2: cost 240 inf + 0
1550699426.994 * * [misc]simplify:  Extracting #3: cost 355 inf + 61800
1550699427.023 * * [misc]simplify:  Extracting #4: cost 246 inf + 415499
1550699427.093 * * [misc]simplify:  Extracting #5: cost 58 inf + 816216
1550699427.169 * * [misc]simplify:  Extracting #6: cost 1 inf + 911482
1550699427.248 * * [misc]simplify:  Extracting #7: cost 0 inf + 914765
1550699427.328 * [exit]simplify:  Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1550699427.328 * [misc]simplify:  Simplified (2 1) to (λ (a b_2 c) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))
1550699427.328 * * * * [misc]progress:  [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b_2 b_2) (neg.p16 (*.p16 c a)))) b_2) a))>
1550699427.328 * * * * [misc]progress:  [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
1550699427.328 * * * * [misc]progress:  [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1550699427.328 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550699427.329 * * [misc]simplify:  iters left: 5 (9 enodes)
1550699427.332 * * [misc]simplify:  iters left: 4 (29 enodes)
1550699427.343 * * [misc]simplify:  iters left: 3 (62 enodes)
1550699427.367 * * [misc]simplify:  iters left: 2 (199 enodes)
1550699427.487 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699427.487 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699427.488 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550699427.489 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550699427.491 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550699427.498 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550699427.521 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550699427.557 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550699427.589 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550699427.589 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1550699427.589 * * * * [misc]progress:  [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1550699427.589 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550699427.589 * * [misc]simplify:  iters left: 5 (9 enodes)
1550699427.593 * * [misc]simplify:  iters left: 4 (29 enodes)
1550699427.603 * * [misc]simplify:  iters left: 3 (62 enodes)
1550699427.627 * * [misc]simplify:  iters left: 2 (199 enodes)
1550699427.743 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699427.743 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699427.744 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550699427.745 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550699427.747 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550699427.753 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550699427.777 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550699427.808 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550699427.846 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550699427.846 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1550699427.846 * * * * [misc]progress:  [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1550699427.846 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550699427.846 * * [misc]simplify:  iters left: 5 (9 enodes)
1550699427.850 * * [misc]simplify:  iters left: 4 (29 enodes)
1550699427.861 * * [misc]simplify:  iters left: 3 (62 enodes)
1550699427.887 * * [misc]simplify:  iters left: 2 (199 enodes)
1550699428.008 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699428.008 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699428.009 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550699428.009 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550699428.012 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550699428.018 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550699428.042 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550699428.073 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550699428.106 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550699428.106 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1550699428.106 * * * * [misc]progress:  [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1550699428.106 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550699428.107 * * [misc]simplify:  iters left: 5 (9 enodes)
1550699428.110 * * [misc]simplify:  iters left: 4 (29 enodes)
1550699428.120 * * [misc]simplify:  iters left: 3 (62 enodes)
1550699428.147 * * [misc]simplify:  iters left: 2 (199 enodes)
1550699428.262 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699428.263 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550699428.263 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550699428.264 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550699428.266 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550699428.277 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550699428.302 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550699428.333 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550699428.366 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550699428.366 * [misc]simplify:  Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1550699428.366 * * * [misc]progress:  adding candidates to table
1550699428.799 * * [misc]progress:  iteration 2 / 4
1550699428.799 * * * [misc]progress:  picking best candidate
1550699428.872 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699428.872 * * * [misc]progress:  localizing error
1550699429.140 * * * [misc]progress:  generating rewritten candidates
1550699429.140 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1)
1550699429.143 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1550699429.146 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1)
1550699429.153 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1)
1550699429.154 * * * [misc]progress:  generating series expansions
1550699429.154 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1)
1550699429.154 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1550699429.154 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1)
1550699429.154 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1)
1550699429.154 * * * [misc]progress:  simplifying candidates
1550699429.154 * * * * [misc]progress:  [ 1 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699429.154 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699429.155 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699429.158 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699429.166 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699429.181 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699429.231 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699429.231 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699429.231 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699429.231 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699429.232 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699429.232 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699429.236 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699429.245 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699429.256 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699429.271 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699429.272 * [misc]simplify:  Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699429.272 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699429.272 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699429.275 * * [misc]simplify:  iters left: 3 (28 enodes)
1550699429.284 * * [misc]simplify:  iters left: 2 (59 enodes)
1550699429.305 * * [misc]simplify:  iters left: 1 (178 enodes)
1550699429.409 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699429.409 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550699429.409 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550699429.410 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550699429.412 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550699429.418 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550699429.440 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550699429.464 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550699429.489 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550699429.515 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550699429.515 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699429.515 * * * * [misc]progress:  [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699429.515 * * * * [misc]progress:  [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699429.515 * * * * [misc]progress:  [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
1550699429.515 * * * * [misc]progress:  [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
1550699429.515 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699429.515 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699429.518 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699429.525 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699429.541 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699429.594 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699429.594 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699429.594 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699429.595 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699429.595 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699429.596 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699429.599 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699429.609 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699429.621 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699429.632 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699429.632 * [misc]simplify:  Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))
1550699429.633 * * * * [misc]progress:  [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))>
1550699429.633 * [enter]simplify:  Simplifying (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))
1550699429.633 * * [misc]simplify:  iters left: 6 (11 enodes)
1550699429.638 * * [misc]simplify:  iters left: 5 (43 enodes)
1550699429.654 * * [misc]simplify:  iters left: 4 (139 enodes)
1550699429.741 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699429.741 * * [misc]simplify:  Extracting #1: cost 32 inf + 0
1550699429.742 * * [misc]simplify:  Extracting #2: cost 85 inf + 0
1550699429.742 * * [misc]simplify:  Extracting #3: cost 152 inf + 1364
1550699429.744 * * [misc]simplify:  Extracting #4: cost 163 inf + 24483
1550699429.755 * * [misc]simplify:  Extracting #5: cost 71 inf + 172897
1550699429.773 * * [misc]simplify:  Extracting #6: cost 3 inf + 277964
1550699429.793 * * [misc]simplify:  Extracting #7: cost 0 inf + 284573
1550699429.812 * [exit]simplify:  Simplified to (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2))))
1550699429.813 * [misc]simplify:  Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (-.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))
1550699429.813 * * * * [misc]progress:  [ 7 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699429.813 * * * * [misc]progress:  [ 8 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699429.813 * * * * [misc]progress:  [ 9 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699429.813 * * * * [misc]progress:  [ 10 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699429.813 * * * [misc]progress:  adding candidates to table
1550699430.314 * * [misc]progress:  iteration 3 / 4
1550699430.314 * * * [misc]progress:  picking best candidate
1550699430.488 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699430.488 * * * [misc]progress:  localizing error
1550699430.647 * * * [misc]progress:  generating rewritten candidates
1550699430.647 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1 2)
1550699430.650 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1550699430.654 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 1 1)
1550699430.658 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1)
1550699430.666 * * * [misc]progress:  generating series expansions
1550699430.666 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1 2)
1550699430.666 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1550699430.666 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 1 1)
1550699430.666 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1)
1550699430.666 * * * [misc]progress:  simplifying candidates
1550699430.666 * * * * [misc]progress:  [ 1 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699430.666 * * * * [misc]progress:  [ 2 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699430.667 * * * * [misc]progress:  [ 3 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
1550699430.667 * * * * [misc]progress:  [ 4 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699430.667 * * * * [misc]progress:  [ 5 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699430.667 * [enter]simplify:  Simplifying (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))
1550699430.667 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699430.671 * * [misc]simplify:  iters left: 4 (26 enodes)
1550699430.679 * * [misc]simplify:  iters left: 3 (56 enodes)
1550699430.713 * * [misc]simplify:  iters left: 2 (117 enodes)
1550699430.772 * * [misc]simplify:  iters left: 1 (404 enodes)
1550699431.168 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699431.168 * * [misc]simplify:  Extracting #1: cost 5 inf + 0
1550699431.168 * * [misc]simplify:  Extracting #2: cost 7 inf + 0
1550699431.168 * * [misc]simplify:  Extracting #3: cost 7 inf + 1
1550699431.168 * * [misc]simplify:  Extracting #4: cost 51 inf + 483
1550699431.170 * * [misc]simplify:  Extracting #5: cost 256 inf + 804
1550699431.174 * * [misc]simplify:  Extracting #6: cost 403 inf + 36487
1550699431.216 * * [misc]simplify:  Extracting #7: cost 236 inf + 480253
1550699431.291 * * [misc]simplify:  Extracting #8: cost 3 inf + 938234
1550699431.373 * * [misc]simplify:  Extracting #9: cost 0 inf + 943361
1550699431.455 * [exit]simplify:  Simplified to (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1550699431.455 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699431.455 * * * * [misc]progress:  [ 6 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (*.p16 (neg.p16 b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699431.455 * [enter]simplify:  Simplifying (*.p16 (neg.p16 b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))
1550699431.455 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699431.459 * * [misc]simplify:  iters left: 4 (32 enodes)
1550699431.470 * * [misc]simplify:  iters left: 3 (56 enodes)
1550699431.489 * * [misc]simplify:  iters left: 2 (119 enodes)
1550699431.550 * * [misc]simplify:  iters left: 1 (419 enodes)
1550699431.956 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699431.956 * * [misc]simplify:  Extracting #1: cost 5 inf + 0
1550699431.956 * * [misc]simplify:  Extracting #2: cost 7 inf + 0
1550699431.956 * * [misc]simplify:  Extracting #3: cost 7 inf + 1
1550699431.956 * * [misc]simplify:  Extracting #4: cost 52 inf + 483
1550699431.958 * * [misc]simplify:  Extracting #5: cost 268 inf + 804
1550699431.963 * * [misc]simplify:  Extracting #6: cost 433 inf + 22386
1550699431.997 * * [misc]simplify:  Extracting #7: cost 293 inf + 485657
1550699432.084 * * [misc]simplify:  Extracting #8: cost 10 inf + 1039724
1550699432.171 * * [misc]simplify:  Extracting #9: cost 0 inf + 1050430
1550699432.260 * * [misc]simplify:  Extracting #10: cost 0 inf + 1045670
1550699432.351 * [exit]simplify:  Simplified to (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (neg.p16 b_2))
1550699432.351 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699432.351 * * * * [misc]progress:  [ 7 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699432.352 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699432.352 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699432.355 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699432.363 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699432.380 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699432.439 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699432.439 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699432.440 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699432.440 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699432.440 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699432.441 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699432.445 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699432.456 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699432.469 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699432.482 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699432.482 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699432.483 * * * * [misc]progress:  [ 8 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699432.483 * * * * [misc]progress:  [ 9 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699432.483 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699432.483 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699432.487 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699432.495 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699432.511 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699432.569 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699432.569 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699432.569 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699432.569 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699432.570 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699432.571 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699432.575 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699432.585 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699432.601 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699432.614 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699432.615 * [misc]simplify:  Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699432.615 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699432.615 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699432.619 * * [misc]simplify:  iters left: 3 (28 enodes)
1550699432.628 * * [misc]simplify:  iters left: 2 (59 enodes)
1550699432.651 * * [misc]simplify:  iters left: 1 (178 enodes)
1550699432.766 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699432.766 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550699432.766 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550699432.767 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550699432.769 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550699432.776 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550699432.798 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550699432.826 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550699432.854 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550699432.883 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550699432.884 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699432.884 * * * * [misc]progress:  [ 10 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699432.884 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699432.884 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699432.888 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699432.895 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699432.914 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699432.970 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699432.970 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699432.970 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699432.970 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699432.971 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699432.972 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699432.975 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699432.986 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699432.998 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699433.011 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699433.011 * [misc]simplify:  Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699433.012 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699433.012 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699433.015 * * [misc]simplify:  iters left: 3 (28 enodes)
1550699433.025 * * [misc]simplify:  iters left: 2 (59 enodes)
1550699433.048 * * [misc]simplify:  iters left: 1 (178 enodes)
1550699433.159 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699433.159 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550699433.159 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550699433.160 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550699433.162 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550699433.170 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550699433.195 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550699433.223 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550699433.251 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550699433.279 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550699433.279 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699433.279 * * * * [misc]progress:  [ 11 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699433.280 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699433.280 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699433.283 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699433.291 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699433.307 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699433.368 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699433.368 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699433.368 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699433.368 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699433.368 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699433.369 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699433.373 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699433.383 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699433.397 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699433.410 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699433.410 * [misc]simplify:  Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699433.410 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699433.410 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699433.414 * * [misc]simplify:  iters left: 3 (28 enodes)
1550699433.423 * * [misc]simplify:  iters left: 2 (59 enodes)
1550699433.446 * * [misc]simplify:  iters left: 1 (178 enodes)
1550699433.560 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699433.560 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550699433.560 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550699433.561 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550699433.563 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550699433.570 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550699433.591 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550699433.619 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550699433.647 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550699433.679 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550699433.679 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699433.679 * * * * [misc]progress:  [ 12 / 12 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699433.679 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699433.679 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699433.683 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699433.690 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699433.707 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699433.761 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699433.761 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699433.761 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699433.761 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699433.761 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699433.762 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699433.766 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699433.777 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699433.789 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699433.803 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699433.803 * [misc]simplify:  Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699433.804 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699433.804 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699433.808 * * [misc]simplify:  iters left: 3 (28 enodes)
1550699433.818 * * [misc]simplify:  iters left: 2 (59 enodes)
1550699433.841 * * [misc]simplify:  iters left: 1 (178 enodes)
1550699433.953 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699433.953 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550699433.953 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550699433.954 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550699433.956 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550699433.964 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550699433.987 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550699434.014 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550699434.042 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550699434.070 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550699434.070 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699434.070 * * * [misc]progress:  adding candidates to table
1550699434.700 * * [misc]progress:  iteration 4 / 4
1550699434.700 * * * [misc]progress:  picking best candidate
1550699434.906 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699434.906 * * * [misc]progress:  localizing error
1550699435.205 * * * [misc]progress:  generating rewritten candidates
1550699435.205 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1)
1550699435.212 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1550699435.216 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 1 2 1)
1550699435.219 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1 1 1)
1550699435.224 * * * [misc]progress:  generating series expansions
1550699435.224 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1)
1550699435.224 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1550699435.224 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 1 2 1)
1550699435.224 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1 1 1)
1550699435.224 * * * [misc]progress:  simplifying candidates
1550699435.224 * * * * [misc]progress:  [ 1 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699435.225 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699435.225 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699435.228 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699435.236 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699435.252 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699435.301 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699435.302 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699435.302 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699435.302 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699435.302 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699435.303 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699435.306 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699435.317 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699435.331 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699435.344 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699435.344 * [misc]simplify:  Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699435.345 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))
1550699435.345 * * [misc]simplify:  iters left: 4 (9 enodes)
1550699435.349 * * [misc]simplify:  iters left: 3 (25 enodes)
1550699435.357 * * [misc]simplify:  iters left: 2 (51 enodes)
1550699435.375 * * [misc]simplify:  iters left: 1 (118 enodes)
1550699435.435 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699435.435 * * [misc]simplify:  Extracting #1: cost 9 inf + 0
1550699435.435 * * [misc]simplify:  Extracting #2: cost 31 inf + 1
1550699435.435 * * [misc]simplify:  Extracting #3: cost 65 inf + 403
1550699435.436 * * [misc]simplify:  Extracting #4: cost 109 inf + 4971
1550699435.437 * * [misc]simplify:  Extracting #5: cost 145 inf + 16482
1550699435.444 * * [misc]simplify:  Extracting #6: cost 57 inf + 134951
1550699435.458 * * [misc]simplify:  Extracting #7: cost 2 inf + 224579
1550699435.476 * * [misc]simplify:  Extracting #8: cost 0 inf + 227984
1550699435.491 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550699435.491 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699435.491 * * * * [misc]progress:  [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699435.492 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550699435.492 * * [misc]simplify:  iters left: 4 (8 enodes)
1550699435.495 * * [misc]simplify:  iters left: 3 (23 enodes)
1550699435.503 * * [misc]simplify:  iters left: 2 (45 enodes)
1550699435.519 * * [misc]simplify:  iters left: 1 (108 enodes)
1550699435.575 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699435.575 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699435.575 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550699435.575 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550699435.576 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550699435.576 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550699435.580 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550699435.589 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550699435.600 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550699435.612 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550699435.612 * [misc]simplify:  Simplified (2 1 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699435.612 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))
1550699435.612 * * [misc]simplify:  iters left: 4 (9 enodes)
1550699435.616 * * [misc]simplify:  iters left: 3 (25 enodes)
1550699435.625 * * [misc]simplify:  iters left: 2 (51 enodes)
1550699435.643 * * [misc]simplify:  iters left: 1 (118 enodes)
1550699435.702 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699435.702 * * [misc]simplify:  Extracting #1: cost 9 inf + 0
1550699435.702 * * [misc]simplify:  Extracting #2: cost 31 inf + 1
1550699435.702 * * [misc]simplify:  Extracting #3: cost 65 inf + 403
1550699435.703 * * [misc]simplify:  Extracting #4: cost 109 inf + 4971
1550699435.705 * * [misc]simplify:  Extracting #5: cost 145 inf + 16482
1550699435.712 * * [misc]simplify:  Extracting #6: cost 57 inf + 134951
1550699435.726 * * [misc]simplify:  Extracting #7: cost 2 inf + 224579
1550699435.741 * * [misc]simplify:  Extracting #8: cost 0 inf + 227984
1550699435.757 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550699435.757 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699435.757 * * * * [misc]progress:  [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2)) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699435.757 * * * * [misc]progress:  [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
1550699435.757 * * * * [misc]progress:  [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699435.757 * * * * [misc]progress:  [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699435.757 * * * * [misc]progress:  [ 7 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699435.757 * [enter]simplify:  Simplifying (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))
1550699435.758 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699435.762 * * [misc]simplify:  iters left: 4 (26 enodes)
1550699435.772 * * [misc]simplify:  iters left: 3 (56 enodes)
1550699435.792 * * [misc]simplify:  iters left: 2 (117 enodes)
1550699435.848 * * [misc]simplify:  iters left: 1 (404 enodes)
1550699436.228 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699436.229 * * [misc]simplify:  Extracting #1: cost 5 inf + 0
1550699436.229 * * [misc]simplify:  Extracting #2: cost 7 inf + 0
1550699436.229 * * [misc]simplify:  Extracting #3: cost 7 inf + 1
1550699436.229 * * [misc]simplify:  Extracting #4: cost 51 inf + 483
1550699436.230 * * [misc]simplify:  Extracting #5: cost 256 inf + 804
1550699436.242 * * [misc]simplify:  Extracting #6: cost 403 inf + 36487
1550699436.278 * * [misc]simplify:  Extracting #7: cost 236 inf + 480253
1550699436.345 * * [misc]simplify:  Extracting #8: cost 3 inf + 938234
1550699436.417 * * [misc]simplify:  Extracting #9: cost 0 inf + 943361
1550699436.493 * [exit]simplify:  Simplified to (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1550699436.493 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699436.494 * * * * [misc]progress:  [ 8 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699436.494 * [enter]simplify:  Simplifying (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))
1550699436.494 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699436.499 * * [misc]simplify:  iters left: 4 (26 enodes)
1550699436.508 * * [misc]simplify:  iters left: 3 (56 enodes)
1550699436.528 * * [misc]simplify:  iters left: 2 (117 enodes)
1550699436.587 * * [misc]simplify:  iters left: 1 (404 enodes)
1550699436.985 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699436.985 * * [misc]simplify:  Extracting #1: cost 5 inf + 0
1550699436.985 * * [misc]simplify:  Extracting #2: cost 7 inf + 0
1550699436.985 * * [misc]simplify:  Extracting #3: cost 7 inf + 1
1550699436.985 * * [misc]simplify:  Extracting #4: cost 51 inf + 483
1550699436.986 * * [misc]simplify:  Extracting #5: cost 256 inf + 804
1550699436.992 * * [misc]simplify:  Extracting #6: cost 403 inf + 36487
1550699437.027 * * [misc]simplify:  Extracting #7: cost 236 inf + 480253
1550699437.107 * * [misc]simplify:  Extracting #8: cost 3 inf + 938234
1550699437.189 * * [misc]simplify:  Extracting #9: cost 0 inf + 943361
1550699437.271 * [exit]simplify:  Simplified to (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1550699437.272 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699437.272 * * * * [misc]progress:  [ 9 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699437.272 * [enter]simplify:  Simplifying (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))
1550699437.273 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699437.276 * * [misc]simplify:  iters left: 4 (26 enodes)
1550699437.287 * * [misc]simplify:  iters left: 3 (56 enodes)
1550699437.305 * * [misc]simplify:  iters left: 2 (117 enodes)
1550699437.361 * * [misc]simplify:  iters left: 1 (404 enodes)
1550699437.749 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699437.749 * * [misc]simplify:  Extracting #1: cost 5 inf + 0
1550699437.749 * * [misc]simplify:  Extracting #2: cost 7 inf + 0
1550699437.749 * * [misc]simplify:  Extracting #3: cost 7 inf + 1
1550699437.749 * * [misc]simplify:  Extracting #4: cost 51 inf + 483
1550699437.751 * * [misc]simplify:  Extracting #5: cost 256 inf + 804
1550699437.761 * * [misc]simplify:  Extracting #6: cost 403 inf + 36487
1550699437.794 * * [misc]simplify:  Extracting #7: cost 236 inf + 480253
1550699437.869 * * [misc]simplify:  Extracting #8: cost 3 inf + 938234
1550699437.954 * * [misc]simplify:  Extracting #9: cost 0 inf + 943361
1550699438.036 * [exit]simplify:  Simplified to (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1550699438.036 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699438.037 * * * * [misc]progress:  [ 10 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1550699438.037 * [enter]simplify:  Simplifying (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))
1550699438.037 * * [misc]simplify:  iters left: 5 (10 enodes)
1550699438.041 * * [misc]simplify:  iters left: 4 (26 enodes)
1550699438.050 * * [misc]simplify:  iters left: 3 (56 enodes)
1550699438.070 * * [misc]simplify:  iters left: 2 (117 enodes)
1550699438.128 * * [misc]simplify:  iters left: 1 (404 enodes)
1550699438.526 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699438.526 * * [misc]simplify:  Extracting #1: cost 5 inf + 0
1550699438.526 * * [misc]simplify:  Extracting #2: cost 7 inf + 0
1550699438.526 * * [misc]simplify:  Extracting #3: cost 7 inf + 1
1550699438.527 * * [misc]simplify:  Extracting #4: cost 51 inf + 483
1550699438.528 * * [misc]simplify:  Extracting #5: cost 256 inf + 804
1550699438.533 * * [misc]simplify:  Extracting #6: cost 403 inf + 36487
1550699438.567 * * [misc]simplify:  Extracting #7: cost 236 inf + 480253
1550699438.651 * * [misc]simplify:  Extracting #8: cost 3 inf + 938234
1550699438.735 * * [misc]simplify:  Extracting #9: cost 0 inf + 943361
1550699438.817 * [exit]simplify:  Simplified to (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1550699438.817 * [misc]simplify:  Simplified (2 1 1 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (neg.p16 b_2) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))
1550699438.817 * * * [misc]progress:  adding candidates to table
1550699439.432 * [misc]progress:  [Phase 3 of 3] Extracting.
1550699439.433 * * [misc]regime:  Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>)
1550699439.441 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b_2)
1550699439.442 * * * * [misc]regimes:  Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>)
1550699439.977 * * * * [misc]regimes:  Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>)
1550699440.488 * * * * [misc]regimes:  Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>)
1550699441.021 * * * [misc]regime:  Found split indices: #<option (#s(si 6 256))>
1550699441.021 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550699441.021 * * [misc]simplify:  iters left: 5 (9 enodes)
1550699441.022 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550699441.022 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550699441.022 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1550699441.022 * * [misc]simplify:  Extracting #3: cost 4 inf + 2
1550699441.022 * * [misc]simplify:  Extracting #4: cost 6 inf + 2
1550699441.022 * * [misc]simplify:  Extracting #5: cost 6 inf + 323
1550699441.023 * * [misc]simplify:  Extracting #6: cost 0 inf + 4258
1550699441.023 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550699441.023 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1550699441.085 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1550699441.087 * * * * [misc]points:  Setting MPFR precision to 64
1550699441.089 * * * * [misc]points:  Setting MPFR precision to 320
1550699441.091 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1550699441.093 * * * * [misc]points:  Setting MPFR precision to 64
1550699441.097 * * * * [misc]points:  Setting MPFR precision to 320
1550699441.102 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1550699441.104 * * * * [misc]points:  Setting MPFR precision to 64
1550699441.112 * * * * [misc]points:  Setting MPFR precision to 320
1550699441.121 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1550699441.123 * * * * [misc]points:  Setting MPFR precision to 64
1550699441.158 * * * * [misc]points:  Setting MPFR precision to 320
1550699441.176 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1550699441.180 * * * * [misc]points:  Setting MPFR precision to 64
1550699441.208 * * * * [misc]points:  Setting MPFR precision to 320
1550699441.244 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1550699441.247 * * * * [misc]points:  Setting MPFR precision to 64
1550699441.305 * * * * [misc]points:  Setting MPFR precision to 320
1550699441.367 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1550699441.416 * * * * [misc]points:  Setting MPFR precision to 64
1550699441.527 * * * * [misc]points:  Setting MPFR precision to 320
1550699441.725 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1550699441.728 * * * * [misc]points:  Setting MPFR precision to 64
1550699442.033 * * * * [misc]points:  Setting MPFR precision to 320
1550699442.384 * * * * [misc]points:  Computing exacts for 8000 points
1550699442.386 * * * * [misc]points:  Setting MPFR precision to 64
1550699444.087 * * * * [misc]points:  Setting MPFR precision to 320
1550699445.626 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699446.429 * * * * [misc]points:  Sampling 1949 additional inputs, on iter 1 have 6051 / 8000
1550699446.444 * * * * [misc]points:  Computing exacts on every 121 of 1949 points to ramp up precision
1550699446.447 * * * * [misc]points:  Setting MPFR precision to 64
1550699446.449 * * * * [misc]points:  Setting MPFR precision to 320
1550699446.452 * * * * [misc]points:  Computing exacts on every 60 of 1949 points to ramp up precision
1550699446.453 * * * * [misc]points:  Setting MPFR precision to 64
1550699446.457 * * * * [misc]points:  Setting MPFR precision to 320
1550699446.462 * * * * [misc]points:  Computing exacts on every 30 of 1949 points to ramp up precision
1550699446.464 * * * * [misc]points:  Setting MPFR precision to 64
1550699446.472 * * * * [misc]points:  Setting MPFR precision to 320
1550699446.482 * * * * [misc]points:  Computing exacts on every 15 of 1949 points to ramp up precision
1550699446.484 * * * * [misc]points:  Setting MPFR precision to 64
1550699446.520 * * * * [misc]points:  Setting MPFR precision to 320
1550699446.539 * * * * [misc]points:  Computing exacts on every 7 of 1949 points to ramp up precision
1550699446.541 * * * * [misc]points:  Setting MPFR precision to 64
1550699446.571 * * * * [misc]points:  Setting MPFR precision to 320
1550699446.609 * * * * [misc]points:  Computing exacts on every 3 of 1949 points to ramp up precision
1550699446.611 * * * * [misc]points:  Setting MPFR precision to 64
1550699446.669 * * * * [misc]points:  Setting MPFR precision to 320
1550699446.744 * * * * [misc]points:  Computing exacts for 1949 points
1550699446.796 * * * * [misc]points:  Setting MPFR precision to 64
1550699447.103 * * * * [misc]points:  Setting MPFR precision to 320
1550699447.457 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699447.686 * * * * [misc]points:  Sampling 473 additional inputs, on iter 2 have 7527 / 8000
1550699447.690 * * * * [misc]points:  Computing exacts on every 29 of 473 points to ramp up precision
1550699447.692 * * * * [misc]points:  Setting MPFR precision to 64
1550699447.694 * * * * [misc]points:  Setting MPFR precision to 320
1550699447.697 * * * * [misc]points:  Computing exacts on every 14 of 473 points to ramp up precision
1550699447.699 * * * * [misc]points:  Setting MPFR precision to 64
1550699447.703 * * * * [misc]points:  Setting MPFR precision to 320
1550699447.708 * * * * [misc]points:  Computing exacts on every 7 of 473 points to ramp up precision
1550699447.710 * * * * [misc]points:  Setting MPFR precision to 64
1550699447.717 * * * * [misc]points:  Setting MPFR precision to 320
1550699447.727 * * * * [misc]points:  Computing exacts on every 3 of 473 points to ramp up precision
1550699447.729 * * * * [misc]points:  Setting MPFR precision to 64
1550699447.745 * * * * [misc]points:  Setting MPFR precision to 320
1550699447.764 * * * * [misc]points:  Computing exacts for 473 points
1550699447.766 * * * * [misc]points:  Setting MPFR precision to 64
1550699447.823 * * * * [misc]points:  Setting MPFR precision to 320
1550699447.935 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699447.987 * * * * [misc]points:  Sampling 109 additional inputs, on iter 3 have 7891 / 8000
1550699447.988 * * * * [misc]points:  Computing exacts on every 6 of 109 points to ramp up precision
1550699447.990 * * * * [misc]points:  Setting MPFR precision to 64
1550699447.993 * * * * [misc]points:  Setting MPFR precision to 320
1550699447.995 * * * * [misc]points:  Computing exacts on every 3 of 109 points to ramp up precision
1550699447.997 * * * * [misc]points:  Setting MPFR precision to 64
1550699448.001 * * * * [misc]points:  Setting MPFR precision to 320
1550699448.005 * * * * [misc]points:  Computing exacts for 109 points
1550699448.007 * * * * [misc]points:  Setting MPFR precision to 64
1550699448.020 * * * * [misc]points:  Setting MPFR precision to 320
1550699448.038 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699448.049 * * * * [misc]points:  Sampling 31 additional inputs, on iter 4 have 7969 / 8000
1550699448.050 * * * * [misc]points:  Computing exacts for 31 points
1550699448.052 * * * * [misc]points:  Setting MPFR precision to 64
1550699448.058 * * * * [misc]points:  Setting MPFR precision to 320
1550699448.063 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699448.067 * * * * [misc]points:  Sampling 11 additional inputs, on iter 5 have 7989 / 8000
1550699448.067 * * * * [misc]points:  Computing exacts for 11 points
1550699448.069 * * * * [misc]points:  Setting MPFR precision to 64
1550699448.071 * * * * [misc]points:  Setting MPFR precision to 320
1550699448.073 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699448.074 * * * * [misc]points:  Sampling 4 additional inputs, on iter 6 have 7997 / 8000
1550699448.074 * * * * [misc]points:  Computing exacts for 4 points
1550699448.076 * * * * [misc]points:  Setting MPFR precision to 64
1550699448.077 * * * * [misc]points:  Setting MPFR precision to 320
1550699448.078 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699448.078 * * * * [misc]points:  Sampling 4 additional inputs, on iter 7 have 7998 / 8000
1550699448.078 * * * * [misc]points:  Computing exacts for 4 points
1550699448.081 * * * * [misc]points:  Setting MPFR precision to 64
1550699448.081 * * * * [misc]points:  Setting MPFR precision to 320
1550699448.082 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550699448.083 * * * * [exit]points:  Sampled 8001 points with exact outputs
1550699452.715 * [misc]regime-testing:  Baseline error score: 64.0
1550699452.718 * [misc]regime-testing:  Oracle error score: 64.0
1550699452.728 * [misc]regime-testing:  End program error score: 2.2691139186249654