1550698888.471 * [misc]progress:  [Phase 1 of 3] Setting up.
1550698888.474 * * * [misc]progress:  [1/2] Preparing points
1550698888.475 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1550698888.480 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1550698888.551 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.556 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.558 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1550698888.559 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.561 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.564 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1550698888.565 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.568 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.574 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1550698888.575 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.581 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.588 * * * * [misc]points:  Computing exacts for 256 points
1550698888.589 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.606 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.629 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698888.683 * * * * [misc]points:  Sampling 66 additional inputs, on iter 1 have 190 / 256
1550698888.683 * * * * [misc]points:  Computing exacts on every 4 of 66 points to ramp up precision
1550698888.684 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.685 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.686 * * * * [misc]points:  Computing exacts on every 2 of 66 points to ramp up precision
1550698888.688 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.690 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.692 * * * * [misc]points:  Computing exacts for 66 points
1550698888.693 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.697 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.703 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698888.706 * * * * [misc]points:  Sampling 19 additional inputs, on iter 2 have 237 / 256
1550698888.706 * * * * [misc]points:  Computing exacts for 19 points
1550698888.707 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.709 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.710 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698888.711 * * * * [misc]points:  Sampling 4 additional inputs, on iter 3 have 253 / 256
1550698888.711 * * * * [misc]points:  Computing exacts for 4 points
1550698888.713 * * * * [misc]points:  Setting MPFR precision to 64
1550698888.713 * * * * [misc]points:  Setting MPFR precision to 320
1550698888.713 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698888.714 * * * * [exit]points:  Sampled 256 points with exact outputs
1550698888.714 * * * [misc]progress:  [2/2] Setting up program.
1550698888.739 * [misc]progress:  [Phase 2 of 3] Improving.
1550698888.739 * * * * [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))>
1550698888.740 * [enter]simplify:  Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550698888.741 * * [misc]simplify:  iters left: 5 (10 enodes)
1550698888.747 * * [misc]simplify:  iters left: 4 (25 enodes)
1550698888.751 * * [misc]simplify:  iters left: 3 (48 enodes)
1550698888.760 * * [misc]simplify:  iters left: 2 (111 enodes)
1550698888.927 * * [misc]simplify:  iters left: 1 (392 enodes)
1550698889.433 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698889.433 * * [misc]simplify:  Extracting #1: cost 10 inf + 0
1550698889.434 * * [misc]simplify:  Extracting #2: cost 35 inf + 1
1550698889.435 * * [misc]simplify:  Extracting #3: cost 91 inf + 405
1550698889.438 * * [misc]simplify:  Extracting #4: cost 331 inf + 2291
1550698889.449 * * [misc]simplify:  Extracting #5: cost 455 inf + 80323
1550698889.519 * * [misc]simplify:  Extracting #6: cost 250 inf + 579968
1550698889.571 * * [misc]simplify:  Extracting #7: cost 28 inf + 1003440
1550698889.637 * * [misc]simplify:  Extracting #8: cost 0 inf + 1069311
1550698889.724 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550698889.725 * [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))
1550698889.789 * * [misc]progress:  iteration 1 / 4
1550698889.789 * * * [misc]progress:  picking best candidate
1550698889.817 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1550698889.817 * * * [misc]progress:  localizing error
1550698890.138 * * * [misc]progress:  generating rewritten candidates
1550698890.139 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1550698890.143 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1)
1550698890.144 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550698890.148 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1 1)
1550698890.152 * * * [misc]progress:  generating series expansions
1550698890.153 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1550698890.153 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1)
1550698890.153 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550698890.153 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1 1)
1550698890.153 * * * [misc]progress:  simplifying candidates
1550698890.153 * * * * [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))>
1550698890.153 * * * * [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))>
1550698890.153 * * * * [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))))>
1550698890.154 * [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))
1550698890.154 * * [misc]simplify:  iters left: 5 (9 enodes)
1550698890.158 * * [misc]simplify:  iters left: 4 (32 enodes)
1550698890.169 * * [misc]simplify:  iters left: 3 (94 enodes)
1550698890.224 * * [misc]simplify:  iters left: 2 (340 enodes)
1550698890.531 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698890.531 * * [misc]simplify:  Extracting #1: cost 50 inf + 0
1550698890.532 * * [misc]simplify:  Extracting #2: cost 240 inf + 0
1550698890.537 * * [misc]simplify:  Extracting #3: cost 355 inf + 61800
1550698890.566 * * [misc]simplify:  Extracting #4: cost 246 inf + 415499
1550698890.637 * * [misc]simplify:  Extracting #5: cost 58 inf + 816216
1550698890.715 * * [misc]simplify:  Extracting #6: cost 1 inf + 911482
1550698890.797 * * [misc]simplify:  Extracting #7: cost 0 inf + 914765
1550698890.875 * [exit]simplify:  Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1550698890.875 * [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))))
1550698890.875 * * * * [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))>
1550698890.875 * * * * [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))>
1550698890.875 * * * * [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))>
1550698890.876 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550698890.876 * * [misc]simplify:  iters left: 5 (9 enodes)
1550698890.879 * * [misc]simplify:  iters left: 4 (29 enodes)
1550698890.890 * * [misc]simplify:  iters left: 3 (62 enodes)
1550698890.913 * * [misc]simplify:  iters left: 2 (199 enodes)
1550698891.032 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698891.032 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698891.033 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550698891.034 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550698891.036 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550698891.042 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550698891.062 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550698891.096 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550698891.128 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550698891.128 * [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))
1550698891.128 * * * * [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))>
1550698891.128 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550698891.129 * * [misc]simplify:  iters left: 5 (9 enodes)
1550698891.132 * * [misc]simplify:  iters left: 4 (29 enodes)
1550698891.142 * * [misc]simplify:  iters left: 3 (62 enodes)
1550698891.166 * * [misc]simplify:  iters left: 2 (199 enodes)
1550698891.282 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698891.282 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698891.282 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550698891.283 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550698891.285 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550698891.292 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550698891.315 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550698891.347 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550698891.382 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550698891.383 * [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))
1550698891.383 * * * * [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))>
1550698891.383 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550698891.383 * * [misc]simplify:  iters left: 5 (9 enodes)
1550698891.387 * * [misc]simplify:  iters left: 4 (29 enodes)
1550698891.397 * * [misc]simplify:  iters left: 3 (62 enodes)
1550698891.421 * * [misc]simplify:  iters left: 2 (199 enodes)
1550698891.536 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698891.536 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698891.537 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550698891.537 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550698891.538 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550698891.541 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550698891.553 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550698891.569 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550698891.585 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550698891.585 * [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))
1550698891.585 * * * * [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))>
1550698891.585 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550698891.585 * * [misc]simplify:  iters left: 5 (9 enodes)
1550698891.587 * * [misc]simplify:  iters left: 4 (29 enodes)
1550698891.592 * * [misc]simplify:  iters left: 3 (62 enodes)
1550698891.609 * * [misc]simplify:  iters left: 2 (199 enodes)
1550698891.718 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698891.718 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550698891.718 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550698891.719 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550698891.721 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550698891.732 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550698891.755 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550698891.785 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550698891.816 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550698891.816 * [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))
1550698891.816 * * * [misc]progress:  adding candidates to table
1550698892.174 * * [misc]progress:  iteration 2 / 4
1550698892.175 * * * [misc]progress:  picking best candidate
1550698892.250 * * * * [misc]pick:  Picked  #<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))>
1550698892.250 * * * [misc]progress:  localizing error
1550698892.576 * * * [misc]progress:  generating rewritten candidates
1550698892.576 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1 1)
1550698892.583 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1550698892.585 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 1)
1550698892.586 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1550698892.590 * * * [misc]progress:  generating series expansions
1550698892.590 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1 1)
1550698892.590 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1550698892.590 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 1)
1550698892.590 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1550698892.590 * * * [misc]progress:  simplifying candidates
1550698892.590 * * * * [misc]progress:  [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
1550698892.591 * [enter]simplify:  Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1550698892.591 * * [misc]simplify:  iters left: 2 (6 enodes)
1550698892.593 * * [misc]simplify:  iters left: 1 (14 enodes)
1550698892.597 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698892.597 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698892.597 * * [misc]simplify:  Extracting #2: cost 6 inf + 0
1550698892.597 * * [misc]simplify:  Extracting #3: cost 2 inf + 325
1550698892.597 * * [misc]simplify:  Extracting #4: cost 0 inf + 1329
1550698892.597 * [exit]simplify:  Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1550698892.597 * [misc]simplify:  Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 b_2 b_2)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))
1550698892.597 * * * * [misc]progress:  [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (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 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>
1550698892.598 * [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 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a))))
1550698892.598 * * [misc]simplify:  iters left: 4 (10 enodes)
1550698892.602 * * [misc]simplify:  iters left: 3 (43 enodes)
1550698892.619 * * [misc]simplify:  iters left: 2 (121 enodes)
1550698892.676 * * [misc]simplify:  iters left: 1 (429 enodes)
1550698893.042 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698893.043 * * [misc]simplify:  Extracting #1: cost 46 inf + 0
1550698893.044 * * [misc]simplify:  Extracting #2: cost 270 inf + 0
1550698893.049 * * [misc]simplify:  Extracting #3: cost 354 inf + 59003
1550698893.080 * * [misc]simplify:  Extracting #4: cost 345 inf + 369227
1550698893.165 * * [misc]simplify:  Extracting #5: cost 22 inf + 1102360
1550698893.265 * * [misc]simplify:  Extracting #6: cost 1 inf + 1150488
1550698893.369 * * [misc]simplify:  Extracting #7: cost 0 inf + 1155051
1550698893.470 * [exit]simplify:  Simplified to (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))))
1550698893.470 * [misc]simplify:  Simplified (2 1 1 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))
1550698893.470 * * * * [misc]progress:  [ 3 / 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)))) (neg.p16 b_2)) a))>
1550698893.470 * * * * [misc]progress:  [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.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)))) (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))))) (*.p16 b_2 b_2)) (+.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))>
1550698893.470 * * * * [misc]progress:  [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.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)))) (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))))) (*.p16 b_2 b_2)) (*.p16 a (+.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))))>
1550698893.470 * [enter]simplify:  Simplifying (-.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)))) (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))))) (*.p16 b_2 b_2))
1550698893.471 * * [misc]simplify:  iters left: 6 (13 enodes)
1550698893.476 * * [misc]simplify:  iters left: 5 (47 enodes)
1550698893.494 * * [misc]simplify:  iters left: 4 (118 enodes)
1550698893.551 * * [misc]simplify:  iters left: 3 (482 enodes)
1550698894.161 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698894.161 * * [misc]simplify:  Extracting #1: cost 39 inf + 0
1550698894.162 * * [misc]simplify:  Extracting #2: cost 255 inf + 0
1550698894.166 * * [misc]simplify:  Extracting #3: cost 532 inf + 10719
1550698894.189 * * [misc]simplify:  Extracting #4: cost 679 inf + 310118
1550698894.292 * * [misc]simplify:  Extracting #5: cost 214 inf + 1310578
1550698894.444 * * [misc]simplify:  Extracting #6: cost 5 inf + 1763746
1550698894.606 * * [misc]simplify:  Extracting #7: cost 0 inf + 1773035
1550698894.766 * [exit]simplify:  Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
1550698894.766 * [misc]simplify:  Simplified (2 1) to (λ (a b_2 c) (/.p16 (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2))) (*.p16 a (+.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))))
1550698894.766 * * * * [misc]progress:  [ 6 / 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))>
1550698894.766 * * * * [misc]progress:  [ 7 / 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))>
1550698894.766 * * * * [misc]progress:  [ 8 / 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))>
1550698894.766 * * * * [misc]progress:  [ 9 / 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))>
1550698894.766 * * * [misc]progress:  adding candidates to table
1550698895.050 * * [misc]progress:  iteration 3 / 4
1550698895.050 * * * [misc]progress:  picking best candidate
1550698895.172 * * * * [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))>
1550698895.172 * * * [misc]progress:  localizing error
1550698895.462 * * * [misc]progress:  generating rewritten candidates
1550698895.462 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1)
1550698895.465 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1550698895.469 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1)
1550698895.475 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1)
1550698895.476 * * * [misc]progress:  generating series expansions
1550698895.477 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1)
1550698895.477 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1550698895.477 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1)
1550698895.477 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1)
1550698895.477 * * * [misc]progress:  simplifying candidates
1550698895.477 * * * * [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))>
1550698895.477 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698895.477 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698895.481 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698895.488 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698895.503 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698895.562 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698895.562 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698895.562 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698895.562 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698895.563 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550698895.564 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550698895.567 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550698895.578 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550698895.592 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550698895.604 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698895.604 * [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))
1550698895.605 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698895.605 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698895.608 * * [misc]simplify:  iters left: 3 (28 enodes)
1550698895.617 * * [misc]simplify:  iters left: 2 (59 enodes)
1550698895.639 * * [misc]simplify:  iters left: 1 (178 enodes)
1550698895.746 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698895.746 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550698895.746 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550698895.747 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550698895.749 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550698895.756 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550698895.777 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550698895.804 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550698895.832 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550698895.862 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550698895.862 * [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))
1550698895.863 * * * * [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))>
1550698895.863 * * * * [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))>
1550698895.863 * * * * [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))>
1550698895.863 * * * * [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))>
1550698895.863 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698895.863 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698895.866 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698895.874 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698895.890 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698895.942 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698895.942 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698895.942 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698895.942 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698895.943 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550698895.943 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550698895.947 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550698895.957 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550698895.970 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550698895.984 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698895.985 * [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))
1550698895.985 * * * * [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))>
1550698895.985 * [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)))
1550698895.985 * * [misc]simplify:  iters left: 6 (11 enodes)
1550698895.991 * * [misc]simplify:  iters left: 5 (43 enodes)
1550698896.008 * * [misc]simplify:  iters left: 4 (139 enodes)
1550698896.098 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698896.098 * * [misc]simplify:  Extracting #1: cost 32 inf + 0
1550698896.099 * * [misc]simplify:  Extracting #2: cost 85 inf + 0
1550698896.099 * * [misc]simplify:  Extracting #3: cost 152 inf + 1364
1550698896.101 * * [misc]simplify:  Extracting #4: cost 163 inf + 24483
1550698896.112 * * [misc]simplify:  Extracting #5: cost 71 inf + 172897
1550698896.134 * * [misc]simplify:  Extracting #6: cost 3 inf + 277964
1550698896.155 * * [misc]simplify:  Extracting #7: cost 0 inf + 284573
1550698896.176 * [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))))
1550698896.176 * [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))
1550698896.176 * * * * [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))>
1550698896.177 * * * * [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))>
1550698896.177 * * * * [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))>
1550698896.177 * * * * [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))>
1550698896.177 * * * [misc]progress:  adding candidates to table
1550698896.669 * * [misc]progress:  iteration 4 / 4
1550698896.669 * * * [misc]progress:  picking best candidate
1550698896.819 * * * * [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))>
1550698896.819 * * * [misc]progress:  localizing error
1550698896.925 * * * [misc]progress:  generating rewritten candidates
1550698896.925 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 2)
1550698896.927 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1 1)
1550698896.928 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 1 2)
1550698896.929 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1)
1550698896.934 * * * [misc]progress:  generating series expansions
1550698896.934 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 2)
1550698896.934 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1 1)
1550698896.934 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 1 2)
1550698896.934 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1)
1550698896.934 * * * [misc]progress:  simplifying candidates
1550698896.934 * * * * [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 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
1550698896.934 * * * * [misc]progress:  [ 2 / 10 ] 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))>
1550698896.934 * * * * [misc]progress:  [ 3 / 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))>
1550698896.934 * * * * [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))) 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))>
1550698896.934 * * * * [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))>
1550698896.934 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698896.934 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698896.936 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698896.939 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698896.947 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698896.973 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698896.973 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698896.973 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698896.973 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698896.974 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550698896.974 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550698896.976 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550698896.981 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550698896.990 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550698896.996 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698896.996 * [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))
1550698896.996 * * * * [misc]progress:  [ 6 / 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 (*.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 (+.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))>
1550698896.997 * [enter]simplify:  Simplifying (*.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)))
1550698896.997 * * [misc]simplify:  iters left: 6 (11 enodes)
1550698896.999 * * [misc]simplify:  iters left: 5 (35 enodes)
1550698897.007 * * [misc]simplify:  iters left: 4 (111 enodes)
1550698897.034 * * [misc]simplify:  iters left: 3 (448 enodes)
1550698897.266 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698897.266 * * [misc]simplify:  Extracting #1: cost 64 inf + 0
1550698897.268 * * [misc]simplify:  Extracting #2: cost 370 inf + 0
1550698897.270 * * [misc]simplify:  Extracting #3: cost 522 inf + 6695
1550698897.280 * * [misc]simplify:  Extracting #4: cost 536 inf + 237314
1550698897.359 * * [misc]simplify:  Extracting #5: cost 132 inf + 950329
1550698897.467 * * [misc]simplify:  Extracting #6: cost 26 inf + 1188087
1550698897.576 * * [misc]simplify:  Extracting #7: cost 0 inf + 1213652
1550698897.687 * * [misc]simplify:  Extracting #8: cost 0 inf + 1213496
1550698897.796 * [exit]simplify:  Simplified to (*.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))
1550698897.796 * [misc]simplify:  Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (-.p16 (real->posit16 0.0) (*.p16 a c)) (+.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))
1550698897.797 * * * * [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))) 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))>
1550698897.797 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698897.797 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698897.800 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698897.808 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698897.824 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698897.880 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698897.880 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698897.880 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698897.880 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698897.880 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550698897.881 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550698897.885 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550698897.895 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550698897.907 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550698897.920 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698897.920 * [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))
1550698897.920 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698897.920 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698897.924 * * [misc]simplify:  iters left: 3 (28 enodes)
1550698897.933 * * [misc]simplify:  iters left: 2 (59 enodes)
1550698897.956 * * [misc]simplify:  iters left: 1 (178 enodes)
1550698898.058 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698898.058 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550698898.059 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550698898.059 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550698898.061 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550698898.067 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550698898.086 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550698898.110 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550698898.138 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550698898.162 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550698898.163 * [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))
1550698898.163 * * * * [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))) 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))>
1550698898.163 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698898.163 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698898.166 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698898.173 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698898.187 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698898.233 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698898.233 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698898.233 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698898.234 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698898.234 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550698898.234 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550698898.237 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550698898.246 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550698898.260 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550698898.270 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698898.270 * [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))
1550698898.270 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698898.270 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698898.273 * * [misc]simplify:  iters left: 3 (28 enodes)
1550698898.281 * * [misc]simplify:  iters left: 2 (59 enodes)
1550698898.301 * * [misc]simplify:  iters left: 1 (178 enodes)
1550698898.390 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698898.391 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550698898.391 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550698898.391 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550698898.393 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550698898.399 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550698898.412 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550698898.426 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550698898.440 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550698898.467 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550698898.467 * [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))
1550698898.468 * * * * [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))) 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))>
1550698898.468 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698898.468 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698898.471 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698898.478 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698898.497 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698898.551 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698898.551 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698898.551 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698898.551 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698898.551 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550698898.552 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550698898.556 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550698898.566 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550698898.579 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550698898.591 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698898.591 * [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))
1550698898.591 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698898.591 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698898.595 * * [misc]simplify:  iters left: 3 (28 enodes)
1550698898.605 * * [misc]simplify:  iters left: 2 (59 enodes)
1550698898.628 * * [misc]simplify:  iters left: 1 (178 enodes)
1550698898.728 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698898.728 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550698898.728 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550698898.729 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550698898.731 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550698898.739 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550698898.764 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550698898.792 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550698898.820 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550698898.847 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550698898.848 * [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))
1550698898.848 * * * * [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))) 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))>
1550698898.848 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698898.848 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698898.851 * * [misc]simplify:  iters left: 3 (23 enodes)
1550698898.859 * * [misc]simplify:  iters left: 2 (45 enodes)
1550698898.876 * * [misc]simplify:  iters left: 1 (108 enodes)
1550698899.338 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698899.338 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698899.338 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550698899.338 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550698899.338 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550698899.338 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550698899.340 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550698899.345 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550698899.351 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550698899.358 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550698899.358 * [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))
1550698899.358 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550698899.358 * * [misc]simplify:  iters left: 4 (8 enodes)
1550698899.360 * * [misc]simplify:  iters left: 3 (28 enodes)
1550698899.364 * * [misc]simplify:  iters left: 2 (59 enodes)
1550698899.375 * * [misc]simplify:  iters left: 1 (178 enodes)
1550698899.437 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698899.437 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550698899.437 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550698899.437 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550698899.438 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550698899.442 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550698899.453 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550698899.467 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550698899.483 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550698899.497 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550698899.497 * [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))
1550698899.497 * * * [misc]progress:  adding candidates to table
1550698899.773 * [misc]progress:  [Phase 3 of 3] Extracting.
1550698899.774 * * [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))) (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 (*.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 (+.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 (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 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.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 (+.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 (*.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 (*.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)))) (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))))) (*.p16 b_2 b_2)) (*.p16 a (+.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))))> #<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))>)
1550698899.782 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b_2)
1550698899.783 * * * * [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))) (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 (*.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 (+.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 (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 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.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 (+.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 (*.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 (*.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)))) (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))))) (*.p16 b_2 b_2)) (*.p16 a (+.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))))> #<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))>)
1550698900.308 * * * * [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))) (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 (*.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 (+.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 (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 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.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 (+.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 (*.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 (*.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)))) (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))))) (*.p16 b_2 b_2)) (*.p16 a (+.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))))> #<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))>)
1550698900.833 * * * * [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))) (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 (*.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 (+.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 (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 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.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 (+.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 (*.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 (*.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)))) (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))))) (*.p16 b_2 b_2)) (*.p16 a (+.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))))> #<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))>)
1550698901.376 * * * [misc]regime:  Found split indices: #<option (#s(si 5 256))>
1550698901.377 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550698901.377 * * [misc]simplify:  iters left: 5 (9 enodes)
1550698901.377 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550698901.377 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550698901.378 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1550698901.378 * * [misc]simplify:  Extracting #3: cost 4 inf + 2
1550698901.378 * * [misc]simplify:  Extracting #4: cost 6 inf + 2
1550698901.378 * * [misc]simplify:  Extracting #5: cost 6 inf + 323
1550698901.378 * * [misc]simplify:  Extracting #6: cost 0 inf + 4258
1550698901.378 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550698901.378 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1550698901.442 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1550698901.444 * * * * [misc]points:  Setting MPFR precision to 64
1550698901.446 * * * * [misc]points:  Setting MPFR precision to 320
1550698901.448 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1550698901.450 * * * * [misc]points:  Setting MPFR precision to 64
1550698901.453 * * * * [misc]points:  Setting MPFR precision to 320
1550698901.458 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1550698901.459 * * * * [misc]points:  Setting MPFR precision to 64
1550698901.466 * * * * [misc]points:  Setting MPFR precision to 320
1550698901.475 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1550698901.477 * * * * [misc]points:  Setting MPFR precision to 64
1550698901.490 * * * * [misc]points:  Setting MPFR precision to 320
1550698901.507 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1550698901.509 * * * * [misc]points:  Setting MPFR precision to 64
1550698901.537 * * * * [misc]points:  Setting MPFR precision to 320
1550698901.599 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1550698901.603 * * * * [misc]points:  Setting MPFR precision to 64
1550698901.661 * * * * [misc]points:  Setting MPFR precision to 320
1550698901.736 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1550698901.738 * * * * [misc]points:  Setting MPFR precision to 64
1550698901.890 * * * * [misc]points:  Setting MPFR precision to 320
1550698902.038 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1550698902.041 * * * * [misc]points:  Setting MPFR precision to 64
1550698902.379 * * * * [misc]points:  Setting MPFR precision to 320
1550698902.736 * * * * [misc]points:  Computing exacts for 8000 points
1550698902.738 * * * * [misc]points:  Setting MPFR precision to 64
1550698903.822 * * * * [misc]points:  Setting MPFR precision to 320
1550698905.682 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698906.396 * * * * [misc]points:  Sampling 1963 additional inputs, on iter 1 have 6037 / 8000
1550698906.411 * * * * [misc]points:  Computing exacts on every 122 of 1963 points to ramp up precision
1550698906.413 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.415 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.418 * * * * [misc]points:  Computing exacts on every 61 of 1963 points to ramp up precision
1550698906.419 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.423 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.428 * * * * [misc]points:  Computing exacts on every 30 of 1963 points to ramp up precision
1550698906.430 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.438 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.448 * * * * [misc]points:  Computing exacts on every 15 of 1963 points to ramp up precision
1550698906.450 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.465 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.477 * * * * [misc]points:  Computing exacts on every 7 of 1963 points to ramp up precision
1550698906.478 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.494 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.516 * * * * [misc]points:  Computing exacts on every 3 of 1963 points to ramp up precision
1550698906.541 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.575 * * * * [misc]points:  Setting MPFR precision to 320
1550698906.617 * * * * [misc]points:  Computing exacts for 1963 points
1550698906.618 * * * * [misc]points:  Setting MPFR precision to 64
1550698906.780 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.077 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698907.284 * * * * [misc]points:  Sampling 509 additional inputs, on iter 2 have 7491 / 8000
1550698907.288 * * * * [misc]points:  Computing exacts on every 31 of 509 points to ramp up precision
1550698907.290 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.292 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.295 * * * * [misc]points:  Computing exacts on every 15 of 509 points to ramp up precision
1550698907.296 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.300 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.305 * * * * [misc]points:  Computing exacts on every 7 of 509 points to ramp up precision
1550698907.306 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.314 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.343 * * * * [misc]points:  Computing exacts on every 3 of 509 points to ramp up precision
1550698907.345 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.361 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.381 * * * * [misc]points:  Computing exacts for 509 points
1550698907.383 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.445 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.514 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698907.592 * * * * [misc]points:  Sampling 133 additional inputs, on iter 3 have 7867 / 8000
1550698907.593 * * * * [misc]points:  Computing exacts on every 8 of 133 points to ramp up precision
1550698907.595 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.599 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.602 * * * * [misc]points:  Computing exacts on every 4 of 133 points to ramp up precision
1550698907.604 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.607 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.611 * * * * [misc]points:  Computing exacts on every 2 of 133 points to ramp up precision
1550698907.613 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.619 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.625 * * * * [misc]points:  Computing exacts for 133 points
1550698907.627 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.642 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.663 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698907.681 * * * * [misc]points:  Sampling 30 additional inputs, on iter 4 have 7970 / 8000
1550698907.682 * * * * [misc]points:  Computing exacts for 30 points
1550698907.684 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.688 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.693 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698907.695 * * * * [misc]points:  Sampling 6 additional inputs, on iter 5 have 7994 / 8000
1550698907.695 * * * * [misc]points:  Computing exacts for 6 points
1550698907.697 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.698 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.699 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698907.699 * * * * [misc]points:  Sampling 4 additional inputs, on iter 6 have 7999 / 8000
1550698907.699 * * * * [misc]points:  Computing exacts for 4 points
1550698907.701 * * * * [misc]points:  Setting MPFR precision to 64
1550698907.702 * * * * [misc]points:  Setting MPFR precision to 320
1550698907.702 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550698907.703 * * * * [exit]points:  Sampled 8001 points with exact outputs
1550698910.791 * [misc]regime-testing:  Baseline error score: 64.0
1550698910.795 * [misc]regime-testing:  Oracle error score: 64.0
1550698910.806 * [misc]regime-testing:  End program error score: 2.303245789264322