1550842780.485 * [misc]progress:  [Phase 1 of 3] Setting up.
1550842780.508 * * * [misc]progress:  [1/2] Preparing points
1550842780.509 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1550842780.514 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1550842780.559 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.564 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.567 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1550842780.573 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.576 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.579 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1550842780.582 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.586 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.590 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1550842780.593 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.599 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.609 * * * * [misc]points:  Computing exacts for 256 points
1550842780.611 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.337 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.373 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.397 * * * * [misc]points:  Sampling 80 additional inputs, on iter 1 have 176 / 256
1550842781.398 * * * * [misc]points:  Computing exacts on every 5 of 80 points to ramp up precision
1550842781.404 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.406 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.408 * * * * [misc]points:  Computing exacts on every 2 of 80 points to ramp up precision
1550842781.413 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.417 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.421 * * * * [misc]points:  Computing exacts for 80 points
1550842781.427 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.439 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.453 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.461 * * * * [misc]points:  Sampling 19 additional inputs, on iter 2 have 237 / 256
1550842781.461 * * * * [misc]points:  Computing exacts for 19 points
1550842781.467 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.470 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.473 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.475 * * * * [misc]points:  Sampling 4 additional inputs, on iter 3 have 253 / 256
1550842781.475 * * * * [misc]points:  Computing exacts for 4 points
1550842781.480 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.481 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.482 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.483 * * * * [exit]points:  Sampled 256 points with exact outputs
1550842781.483 * * * [misc]progress:  [2/2] Setting up program.
1550842781.572 * [misc]progress:  [Phase 2 of 3] Improving.
1550842781.573 * * * * [misc]progress:  [ 1 / 1 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))>
1550842781.574 * [enter]simplify:  Simplifying (/.p16 (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a))
1550842781.576 * * [misc]simplify:  iters left: 6 (16 enodes)
1550842781.591 * * [misc]simplify:  iters left: 5 (39 enodes)
1550842781.605 * * [misc]simplify:  iters left: 4 (72 enodes)
1550842781.634 * * [misc]simplify:  iters left: 3 (196 enodes)
1550842781.726 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842781.726 * * [misc]simplify:  Extracting #1: cost 5 inf + 0
1550842781.727 * * [misc]simplify:  Extracting #2: cost 11 inf + 1
1550842781.727 * * [misc]simplify:  Extracting #3: cost 16 inf + 2
1550842781.727 * * [misc]simplify:  Extracting #4: cost 26 inf + 807
1550842781.727 * * [misc]simplify:  Extracting #5: cost 66 inf + 1770
1550842781.728 * * [misc]simplify:  Extracting #6: cost 135 inf + 3695
1550842781.729 * * [misc]simplify:  Extracting #7: cost 209 inf + 14082
1550842781.732 * * [misc]simplify:  Extracting #8: cost 138 inf + 107732
1550842781.742 * * [misc]simplify:  Extracting #9: cost 36 inf + 289941
1550842781.756 * * [misc]simplify:  Extracting #10: cost 2 inf + 355093
1550842781.770 * * [misc]simplify:  Extracting #11: cost 1 inf + 357016
1550842781.790 * * [misc]simplify:  Extracting #12: cost 0 inf + 360620
1550842781.805 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
1550842781.805 * [misc]simplify:  Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))
1550842781.851 * * [misc]progress:  iteration 1 / 4
1550842781.851 * * * [misc]progress:  picking best candidate
1550842781.872 * * * * [misc]pick:  Picked  #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
1550842781.872 * * * [misc]progress:  localizing error
1550842782.230 * * * [misc]progress:  generating rewritten candidates
1550842782.230 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1550842782.235 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1)
1550842782.235 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550842782.254 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1 1 2)
1550842782.259 * * * [misc]progress:  generating series expansions
1550842782.259 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1550842782.259 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1)
1550842782.259 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550842782.260 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1 1 2)
1550842782.260 * * * [misc]progress:  simplifying candidates
1550842782.260 * * * * [misc]progress:  [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))>
1550842782.260 * * * * [misc]progress:  [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (*.p16 (real->posit16 2) a)))>
1550842782.260 * * * * [misc]progress:  [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
1550842782.260 * * * * [misc]progress:  [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))>
1550842782.260 * [enter]simplify:  Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b))
1550842782.260 * * [misc]simplify:  iters left: 6 (12 enodes)
1550842782.267 * * [misc]simplify:  iters left: 5 (39 enodes)
1550842782.282 * * [misc]simplify:  iters left: 4 (111 enodes)
1550842782.335 * * [misc]simplify:  iters left: 3 (427 enodes)
1550842782.690 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842782.690 * * [misc]simplify:  Extracting #1: cost 47 inf + 0
1550842782.690 * * [misc]simplify:  Extracting #2: cost 231 inf + 0
1550842782.691 * * [misc]simplify:  Extracting #3: cost 400 inf + 3216
1550842782.699 * * [misc]simplify:  Extracting #4: cost 473 inf + 191470
1550842782.745 * * [misc]simplify:  Extracting #5: cost 180 inf + 866467
1550842782.834 * * [misc]simplify:  Extracting #6: cost 4 inf + 1232579
1550842782.892 * * [misc]simplify:  Extracting #7: cost 0 inf + 1241757
1550842782.966 * [exit]simplify:  Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4)))
1550842782.966 * [misc]simplify:  Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 a c) (real->posit16 4))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))
1550842782.966 * * * * [misc]progress:  [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
1550842782.966 * * * * [misc]progress:  [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (*.p16 (real->posit16 2) a)))>
1550842782.967 * * * * [misc]progress:  [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
1550842782.967 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
1550842782.967 * * [misc]simplify:  iters left: 6 (15 enodes)
1550842782.974 * * [misc]simplify:  iters left: 5 (43 enodes)
1550842782.985 * * [misc]simplify:  iters left: 4 (88 enodes)
1550842783.004 * * [misc]simplify:  iters left: 3 (307 enodes)
1550842783.190 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.190 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842783.190 * * [misc]simplify:  Extracting #2: cost 125 inf + 1
1550842783.191 * * [misc]simplify:  Extracting #3: cost 193 inf + 2734
1550842783.193 * * [misc]simplify:  Extracting #4: cost 253 inf + 8433
1550842783.198 * * [misc]simplify:  Extracting #5: cost 273 inf + 63950
1550842783.225 * * [misc]simplify:  Extracting #6: cost 175 inf + 356651
1550842783.281 * * [misc]simplify:  Extracting #7: cost 6 inf + 666712
1550842783.314 * * [misc]simplify:  Extracting #8: cost 0 inf + 674735
1550842783.367 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
1550842783.367 * [misc]simplify:  Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
1550842783.367 * * * * [misc]progress:  [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
1550842783.368 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
1550842783.368 * * [misc]simplify:  iters left: 6 (15 enodes)
1550842783.375 * * [misc]simplify:  iters left: 5 (43 enodes)
1550842783.390 * * [misc]simplify:  iters left: 4 (88 enodes)
1550842783.429 * * [misc]simplify:  iters left: 3 (307 enodes)
1550842783.610 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.611 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842783.611 * * [misc]simplify:  Extracting #2: cost 125 inf + 1
1550842783.612 * * [misc]simplify:  Extracting #3: cost 193 inf + 2734
1550842783.614 * * [misc]simplify:  Extracting #4: cost 253 inf + 8433
1550842783.619 * * [misc]simplify:  Extracting #5: cost 273 inf + 63950
1550842783.649 * * [misc]simplify:  Extracting #6: cost 175 inf + 356651
1550842783.692 * * [misc]simplify:  Extracting #7: cost 6 inf + 666712
1550842783.721 * * [misc]simplify:  Extracting #8: cost 0 inf + 674735
1550842783.775 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
1550842783.775 * [misc]simplify:  Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
1550842783.775 * * * * [misc]progress:  [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
1550842783.776 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
1550842783.776 * * [misc]simplify:  iters left: 6 (15 enodes)
1550842783.780 * * [misc]simplify:  iters left: 5 (43 enodes)
1550842783.788 * * [misc]simplify:  iters left: 4 (88 enodes)
1550842783.818 * * [misc]simplify:  iters left: 3 (307 enodes)
1550842783.976 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.976 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842783.976 * * [misc]simplify:  Extracting #2: cost 125 inf + 1
1550842783.978 * * [misc]simplify:  Extracting #3: cost 193 inf + 2734
1550842783.979 * * [misc]simplify:  Extracting #4: cost 253 inf + 8433
1550842783.984 * * [misc]simplify:  Extracting #5: cost 273 inf + 63950
1550842784.011 * * [misc]simplify:  Extracting #6: cost 175 inf + 356651
1550842784.054 * * [misc]simplify:  Extracting #7: cost 6 inf + 666712
1550842784.093 * * [misc]simplify:  Extracting #8: cost 0 inf + 674735
1550842784.139 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
1550842784.139 * [misc]simplify:  Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
1550842784.139 * * * * [misc]progress:  [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a)))>
1550842784.139 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 (real->posit16 2) a))
1550842784.139 * * [misc]simplify:  iters left: 6 (15 enodes)
1550842784.143 * * [misc]simplify:  iters left: 5 (43 enodes)
1550842784.150 * * [misc]simplify:  iters left: 4 (88 enodes)
1550842784.179 * * [misc]simplify:  iters left: 3 (307 enodes)
1550842784.343 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842784.343 * * [misc]simplify:  Extracting #1: cost 31 inf + 0
1550842784.343 * * [misc]simplify:  Extracting #2: cost 125 inf + 1
1550842784.344 * * [misc]simplify:  Extracting #3: cost 193 inf + 2734
1550842784.345 * * [misc]simplify:  Extracting #4: cost 253 inf + 8433
1550842784.347 * * [misc]simplify:  Extracting #5: cost 273 inf + 63950
1550842784.362 * * [misc]simplify:  Extracting #6: cost 175 inf + 356651
1550842784.400 * * [misc]simplify:  Extracting #7: cost 6 inf + 666712
1550842784.440 * * [misc]simplify:  Extracting #8: cost 0 inf + 674735
1550842784.477 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2)))
1550842784.477 * [misc]simplify:  Simplified (2) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
1550842784.477 * * * [misc]progress:  adding candidates to table
1550842784.972 * * [misc]progress:  iteration 2 / 4
1550842784.972 * * * [misc]progress:  picking best candidate
1550842785.064 * * * * [misc]pick:  Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
1550842785.064 * * * [misc]progress:  localizing error
1550842785.123 * * * [misc]progress:  generating rewritten candidates
1550842785.123 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1)
1550842785.124 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1 1)
1550842785.125 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550842785.127 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1 1 1 2)
1550842785.129 * * * [misc]progress:  generating series expansions
1550842785.129 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1)
1550842785.129 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1 1)
1550842785.129 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550842785.129 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1 1 1 2)
1550842785.129 * * * [misc]progress:  simplifying candidates
1550842785.129 * * * * [misc]progress:  [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (neg.p16 b)) (real->posit16 2)) a))>
1550842785.129 * * * * [misc]progress:  [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))>
1550842785.129 * * * * [misc]progress:  [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))>
1550842785.130 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)
1550842785.130 * * [misc]simplify:  iters left: 5 (11 enodes)
1550842785.132 * * [misc]simplify:  iters left: 4 (35 enodes)
1550842785.141 * * [misc]simplify:  iters left: 3 (76 enodes)
1550842785.166 * * [misc]simplify:  iters left: 2 (261 enodes)
1550842785.303 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842785.303 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550842785.304 * * [misc]simplify:  Extracting #2: cost 66 inf + 1
1550842785.304 * * [misc]simplify:  Extracting #3: cost 146 inf + 403
1550842785.305 * * [misc]simplify:  Extracting #4: cost 205 inf + 4899
1550842785.306 * * [misc]simplify:  Extracting #5: cost 241 inf + 36908
1550842785.320 * * [misc]simplify:  Extracting #6: cost 176 inf + 271128
1550842785.347 * * [misc]simplify:  Extracting #7: cost 10 inf + 555810
1550842785.386 * * [misc]simplify:  Extracting #8: cost 0 inf + 573768
1550842785.426 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b)
1550842785.426 * [misc]simplify:  Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 2))))
1550842785.426 * * * * [misc]progress:  [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
1550842785.426 * * * * [misc]progress:  [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 c a)))) b) (real->posit16 2)) a))>
1550842785.426 * * * * [misc]progress:  [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
1550842785.426 * * * * [misc]progress:  [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
1550842785.426 * * * * [misc]progress:  [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
1550842785.426 * * * * [misc]progress:  [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b) (real->posit16 2)) a))>
1550842785.426 * * * [misc]progress:  adding candidates to table
1550842785.972 * * [misc]progress:  iteration 3 / 4
1550842785.972 * * * [misc]progress:  picking best candidate
1550842786.103 * * * * [misc]pick:  Picked  #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
1550842786.103 * * * [misc]progress:  localizing error
1550842786.358 * * * [misc]progress:  generating rewritten candidates
1550842786.358 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1)
1550842786.360 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1 1)
1550842786.361 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550842786.366 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1 1 1)
1550842786.373 * * * [misc]progress:  generating series expansions
1550842786.373 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1)
1550842786.373 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1 1)
1550842786.373 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550842786.373 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1 1 1)
1550842786.373 * * * [misc]progress:  simplifying candidates
1550842786.373 * * * * [misc]progress:  [ 1 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (real->posit16 2)) a))>
1550842786.373 * * * * [misc]progress:  [ 2 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (real->posit16 2)) a))>
1550842786.373 * * * * [misc]progress:  [ 3 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2))))>
1550842786.374 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)
1550842786.374 * * [misc]simplify:  iters left: 6 (11 enodes)
1550842786.379 * * [misc]simplify:  iters left: 5 (35 enodes)
1550842786.392 * * [misc]simplify:  iters left: 4 (76 enodes)
1550842786.424 * * [misc]simplify:  iters left: 3 (256 enodes)
1550842786.598 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842786.598 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550842786.599 * * [misc]simplify:  Extracting #2: cost 66 inf + 1
1550842786.599 * * [misc]simplify:  Extracting #3: cost 146 inf + 403
1550842786.601 * * [misc]simplify:  Extracting #4: cost 206 inf + 4977
1550842786.604 * * [misc]simplify:  Extracting #5: cost 248 inf + 24473
1550842786.625 * * [misc]simplify:  Extracting #6: cost 211 inf + 217933
1550842786.663 * * [misc]simplify:  Extracting #7: cost 16 inf + 561609
1550842786.712 * * [misc]simplify:  Extracting #8: cost 0 inf + 595514
1550842786.761 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) b)
1550842786.761 * [misc]simplify:  Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) b) (*.p16 a (real->posit16 2))))
1550842786.762 * * * * [misc]progress:  [ 4 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))>
1550842786.762 * * * * [misc]progress:  [ 5 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (real->posit16 2)) a))>
1550842786.762 * * * * [misc]progress:  [ 6 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
1550842786.762 * * * * [misc]progress:  [ 7 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
1550842786.762 * * * * [misc]progress:  [ 8 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
1550842786.762 * * * * [misc]progress:  [ 9 / 9 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
1550842786.762 * * * [misc]progress:  adding candidates to table
1550842787.196 * * [misc]progress:  iteration 4 / 4
1550842787.196 * * * [misc]progress:  picking best candidate
1550842787.345 * * * * [misc]pick:  Picked  #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
1550842787.345 * * * [misc]progress:  localizing error
1550842787.383 * * * [misc]progress:  generating rewritten candidates
1550842787.383 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1550842787.385 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1)
1550842787.386 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550842787.391 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1 1)
1550842787.397 * * * [misc]progress:  generating series expansions
1550842787.397 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1550842787.397 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1)
1550842787.397 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550842787.397 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1 1)
1550842787.397 * * * [misc]progress:  simplifying candidates
1550842787.397 * * * * [misc]progress:  [ 1 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (neg.p16 b)) (*.p16 (real->posit16 2) a)))>
1550842787.397 * * * * [misc]progress:  [ 2 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 (real->posit16 2) a)))>
1550842787.397 * * * * [misc]progress:  [ 3 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))>
1550842787.397 * * * * [misc]progress:  [ 4 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))>
1550842787.397 * [enter]simplify:  Simplifying (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b))
1550842787.397 * * [misc]simplify:  iters left: 6 (12 enodes)
1550842787.400 * * [misc]simplify:  iters left: 5 (39 enodes)
1550842787.408 * * [misc]simplify:  iters left: 4 (111 enodes)
1550842787.444 * * [misc]simplify:  iters left: 3 (424 enodes)
1550842787.736 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842787.736 * * [misc]simplify:  Extracting #1: cost 47 inf + 0
1550842787.737 * * [misc]simplify:  Extracting #2: cost 231 inf + 0
1550842787.740 * * [misc]simplify:  Extracting #3: cost 400 inf + 3615
1550842787.755 * * [misc]simplify:  Extracting #4: cost 466 inf + 182833
1550842787.820 * * [misc]simplify:  Extracting #5: cost 208 inf + 789169
1550842787.936 * * [misc]simplify:  Extracting #6: cost 3 inf + 1219441
1550842788.052 * * [misc]simplify:  Extracting #7: cost 0 inf + 1225733
1550842788.172 * [exit]simplify:  Simplified to (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c))
1550842788.172 * [misc]simplify:  Simplified (2 1) to (λ (a b c) (/.p16 (-.p16 (real->posit16 0.0) (*.p16 (*.p16 (real->posit16 4) a) c)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))
1550842788.173 * * * * [misc]progress:  [ 5 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (+.p16 (*.p16 b b) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))>
1550842788.173 * * * * [misc]progress:  [ 6 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))>
1550842788.173 * * * * [misc]progress:  [ 7 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
1550842788.173 * * * * [misc]progress:  [ 8 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
1550842788.173 * * * * [misc]progress:  [ 9 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
1550842788.173 * * * * [misc]progress:  [ 10 / 10 ] simplifiying candidate #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>
1550842788.173 * * * [misc]progress:  adding candidates to table
1550842788.839 * [misc]progress:  [Phase 3 of 3] Extracting.
1550842788.839 * * [misc]regime:  Finding splitpoints for: (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>)
1550842788.845 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b)
1550842788.846 * * * * [misc]regimes:  Trying to branch on c from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>)
1550842789.370 * * * * [misc]regimes:  Trying to branch on a from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>)
1550842789.727 * * * * [misc]regimes:  Trying to branch on b from (#<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b))))> #<alt (λ (a b c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b))))> #<alt (λ (a b c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4)))) b)) (real->posit16 2)) a))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 c (*.p16 a (real->posit16 4))))) (+.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) b) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (*.p16 b b)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b)) (*.p16 (real->posit16 2) a)))> #<alt (λ (a b c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)))>)
1550842790.200 * * * [misc]regime:  Found split indices: #<option (#s(si 0 256))>
1550842790.201 * [enter]simplify:  Simplifying (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a)
1550842790.201 * * [misc]simplify:  iters left: 6 (15 enodes)
1550842790.202 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842790.202 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842790.202 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1550842790.202 * * [misc]simplify:  Extracting #3: cost 7 inf + 1
1550842790.202 * * [misc]simplify:  Extracting #4: cost 5 inf + 4
1550842790.202 * * [misc]simplify:  Extracting #5: cost 7 inf + 4
1550842790.202 * * [misc]simplify:  Extracting #6: cost 8 inf + 325
1550842790.202 * * [misc]simplify:  Extracting #7: cost 8 inf + 326
1550842790.202 * * [misc]simplify:  Extracting #8: cost 9 inf + 326
1550842790.203 * * [misc]simplify:  Extracting #9: cost 7 inf + 328
1550842790.203 * * [misc]simplify:  Extracting #10: cost 5 inf + 1293
1550842790.203 * * [misc]simplify:  Extracting #11: cost 3 inf + 3421
1550842790.203 * * [misc]simplify:  Extracting #12: cost 1 inf + 6190
1550842790.203 * * [misc]simplify:  Extracting #13: cost 0 inf + 8235
1550842790.203 * [exit]simplify:  Simplified to (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (real->posit16 2)) a)
1550842790.203 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1550842790.251 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1550842790.257 * * * * [misc]points:  Setting MPFR precision to 64
1550842790.259 * * * * [misc]points:  Setting MPFR precision to 320
1550842790.261 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1550842790.265 * * * * [misc]points:  Setting MPFR precision to 64
1550842790.268 * * * * [misc]points:  Setting MPFR precision to 320
1550842790.270 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1550842790.273 * * * * [misc]points:  Setting MPFR precision to 64
1550842790.277 * * * * [misc]points:  Setting MPFR precision to 320
1550842790.282 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1550842790.297 * * * * [misc]points:  Setting MPFR precision to 64
1550842790.307 * * * * [misc]points:  Setting MPFR precision to 320
1550842790.318 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1550842790.321 * * * * [misc]points:  Setting MPFR precision to 64
1550842790.338 * * * * [misc]points:  Setting MPFR precision to 320
1550842790.369 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1550842790.374 * * * * [misc]points:  Setting MPFR precision to 64
1550842790.413 * * * * [misc]points:  Setting MPFR precision to 320
1550842790.511 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1550842790.516 * * * * [misc]points:  Setting MPFR precision to 64
1550842790.597 * * * * [misc]points:  Setting MPFR precision to 320
1550842790.796 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1550842790.801 * * * * [misc]points:  Setting MPFR precision to 64
1550842791.024 * * * * [misc]points:  Setting MPFR precision to 320
1550842791.403 * * * * [misc]points:  Computing exacts for 8000 points
1550842791.408 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.894 * * * * [misc]points:  Setting MPFR precision to 320
1550842794.410 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842795.162 * * * * [misc]points:  Sampling 2397 additional inputs, on iter 1 have 5603 / 8000
1550842795.180 * * * * [misc]points:  Computing exacts on every 149 of 2397 points to ramp up precision
1550842795.185 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.187 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.205 * * * * [misc]points:  Computing exacts on every 74 of 2397 points to ramp up precision
1550842795.210 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.215 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.220 * * * * [misc]points:  Computing exacts on every 37 of 2397 points to ramp up precision
1550842795.224 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.233 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.243 * * * * [misc]points:  Computing exacts on every 18 of 2397 points to ramp up precision
1550842795.248 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.264 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.285 * * * * [misc]points:  Computing exacts on every 9 of 2397 points to ramp up precision
1550842795.291 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.322 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.360 * * * * [misc]points:  Computing exacts on every 4 of 2397 points to ramp up precision
1550842795.365 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.422 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.466 * * * * [misc]points:  Computing exacts on every 2 of 2397 points to ramp up precision
1550842795.468 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.558 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.690 * * * * [misc]points:  Computing exacts for 2397 points
1550842795.695 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.931 * * * * [misc]points:  Setting MPFR precision to 320
1550842796.782 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842796.983 * * * * [misc]points:  Sampling 717 additional inputs, on iter 2 have 7283 / 8000
1550842796.989 * * * * [misc]points:  Computing exacts on every 44 of 717 points to ramp up precision
1550842796.994 * * * * [misc]points:  Setting MPFR precision to 64
1550842796.996 * * * * [misc]points:  Setting MPFR precision to 320
1550842796.998 * * * * [misc]points:  Computing exacts on every 22 of 717 points to ramp up precision
1550842797.003 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.007 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.012 * * * * [misc]points:  Computing exacts on every 11 of 717 points to ramp up precision
1550842797.017 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.026 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.057 * * * * [misc]points:  Computing exacts on every 5 of 717 points to ramp up precision
1550842797.063 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.079 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.097 * * * * [misc]points:  Computing exacts on every 2 of 717 points to ramp up precision
1550842797.103 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.132 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.169 * * * * [misc]points:  Computing exacts for 717 points
1550842797.175 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.257 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.338 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.370 * * * * [misc]points:  Sampling 204 additional inputs, on iter 3 have 7796 / 8000
1550842797.371 * * * * [misc]points:  Computing exacts on every 12 of 204 points to ramp up precision
1550842797.374 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.377 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.378 * * * * [misc]points:  Computing exacts on every 6 of 204 points to ramp up precision
1550842797.381 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.383 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.409 * * * * [misc]points:  Computing exacts on every 3 of 204 points to ramp up precision
1550842797.411 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.415 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.420 * * * * [misc]points:  Computing exacts for 204 points
1550842797.423 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.437 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.454 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.463 * * * * [misc]points:  Sampling 57 additional inputs, on iter 4 have 7943 / 8000
1550842797.464 * * * * [misc]points:  Computing exacts on every 3 of 57 points to ramp up precision
1550842797.468 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.469 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.470 * * * * [misc]points:  Computing exacts for 57 points
1550842797.473 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.477 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.482 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.484 * * * * [misc]points:  Sampling 21 additional inputs, on iter 5 have 7979 / 8000
1550842797.484 * * * * [misc]points:  Computing exacts for 21 points
1550842797.487 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.489 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.491 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.492 * * * * [misc]points:  Sampling 5 additional inputs, on iter 6 have 7995 / 8000
1550842797.493 * * * * [misc]points:  Computing exacts for 5 points
1550842797.496 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.496 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.497 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.497 * * * * [misc]points:  Sampling 4 additional inputs, on iter 7 have 7998 / 8000
1550842797.497 * * * * [misc]points:  Computing exacts for 4 points
1550842797.500 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.501 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.501 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.501 * * * * [exit]points:  Sampled 8001 points with exact outputs
1550842804.481 * [misc]regime-testing:  Baseline error score: 64.0
1550842804.485 * [misc]regime-testing:  Oracle error score: 64.0
1550842804.489 * [misc]regime-testing:  End program error score: 2.20118363957485