1550842780.487 * [misc]progress:  [Phase 1 of 3] Setting up.
1550842780.488 * * * [misc]progress:  [1/2] Preparing points
1550842780.490 * * * * [misc]points:  Sampling 256 additional inputs, on iter 0 have 0 / 256
1550842780.498 * * * * [misc]points:  Computing exacts on every 16 of 256 points to ramp up precision
1550842780.549 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.552 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.554 * * * * [misc]points:  Computing exacts on every 8 of 256 points to ramp up precision
1550842780.555 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.557 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.563 * * * * [misc]points:  Computing exacts on every 4 of 256 points to ramp up precision
1550842780.565 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.571 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.579 * * * * [misc]points:  Computing exacts on every 2 of 256 points to ramp up precision
1550842780.581 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.591 * * * * [misc]points:  Setting MPFR precision to 320
1550842780.605 * * * * [misc]points:  Computing exacts for 256 points
1550842780.607 * * * * [misc]points:  Setting MPFR precision to 64
1550842780.637 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.424 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.453 * * * * [misc]points:  Sampling 62 additional inputs, on iter 1 have 194 / 256
1550842781.453 * * * * [misc]points:  Computing exacts on every 3 of 62 points to ramp up precision
1550842781.455 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.457 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.460 * * * * [misc]points:  Computing exacts for 62 points
1550842781.462 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.470 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.479 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.486 * * * * [misc]points:  Sampling 13 additional inputs, on iter 2 have 243 / 256
1550842781.486 * * * * [misc]points:  Computing exacts for 13 points
1550842781.488 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.490 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.493 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.495 * * * * [misc]points:  Sampling 5 additional inputs, on iter 3 have 251 / 256
1550842781.496 * * * * [misc]points:  Computing exacts for 5 points
1550842781.498 * * * * [misc]points:  Setting MPFR precision to 64
1550842781.498 * * * * [misc]points:  Setting MPFR precision to 320
1550842781.499 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842781.500 * * * * [exit]points:  Sampled 256 points with exact outputs
1550842781.501 * * * [misc]progress:  [2/2] Setting up program.
1550842781.540 * [misc]progress:  [Phase 2 of 3] Improving.
1550842781.540 * * * * [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))>
1550842781.542 * [enter]simplify:  Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1550842781.543 * * [misc]simplify:  iters left: 5 (10 enodes)
1550842781.552 * * [misc]simplify:  iters left: 4 (25 enodes)
1550842781.561 * * [misc]simplify:  iters left: 3 (48 enodes)
1550842781.579 * * [misc]simplify:  iters left: 2 (111 enodes)
1550842781.666 * * [misc]simplify:  iters left: 1 (392 enodes)
1550842782.024 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842782.024 * * [misc]simplify:  Extracting #1: cost 10 inf + 0
1550842782.025 * * [misc]simplify:  Extracting #2: cost 35 inf + 1
1550842782.026 * * [misc]simplify:  Extracting #3: cost 91 inf + 405
1550842782.026 * * [misc]simplify:  Extracting #4: cost 331 inf + 2291
1550842782.030 * * [misc]simplify:  Extracting #5: cost 455 inf + 80323
1550842782.050 * * [misc]simplify:  Extracting #6: cost 250 inf + 579968
1550842782.092 * * [misc]simplify:  Extracting #7: cost 28 inf + 1003440
1550842782.137 * * [misc]simplify:  Extracting #8: cost 0 inf + 1069311
1550842782.181 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550842782.182 * [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))
1550842782.217 * * [misc]progress:  iteration 1 / 4
1550842782.218 * * * [misc]progress:  picking best candidate
1550842782.232 * * * * [misc]pick:  Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1550842782.232 * * * [misc]progress:  localizing error
1550842782.405 * * * [misc]progress:  generating rewritten candidates
1550842782.406 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1)
1550842782.409 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1)
1550842782.409 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2)
1550842782.411 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 1 1)
1550842782.413 * * * [misc]progress:  generating series expansions
1550842782.414 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1)
1550842782.414 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1)
1550842782.414 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2)
1550842782.414 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 1 1)
1550842782.414 * * * [misc]progress:  simplifying candidates
1550842782.414 * * * * [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))>
1550842782.414 * * * * [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))>
1550842782.414 * * * * [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))))>
1550842782.414 * [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))
1550842782.414 * * [misc]simplify:  iters left: 5 (9 enodes)
1550842782.416 * * [misc]simplify:  iters left: 4 (32 enodes)
1550842782.422 * * [misc]simplify:  iters left: 3 (94 enodes)
1550842782.453 * * [misc]simplify:  iters left: 2 (340 enodes)
1550842782.647 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842782.647 * * [misc]simplify:  Extracting #1: cost 50 inf + 0
1550842782.648 * * [misc]simplify:  Extracting #2: cost 240 inf + 0
1550842782.654 * * [misc]simplify:  Extracting #3: cost 355 inf + 61800
1550842782.689 * * [misc]simplify:  Extracting #4: cost 246 inf + 415499
1550842782.753 * * [misc]simplify:  Extracting #5: cost 58 inf + 816216
1550842782.811 * * [misc]simplify:  Extracting #6: cost 1 inf + 911482
1550842782.865 * * [misc]simplify:  Extracting #7: cost 0 inf + 914765
1550842782.946 * [exit]simplify:  Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1550842782.946 * [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))))
1550842782.946 * * * * [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))>
1550842782.946 * * * * [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))>
1550842782.946 * * * * [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))>
1550842782.946 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550842782.946 * * [misc]simplify:  iters left: 5 (9 enodes)
1550842782.951 * * [misc]simplify:  iters left: 4 (29 enodes)
1550842782.960 * * [misc]simplify:  iters left: 3 (62 enodes)
1550842782.986 * * [misc]simplify:  iters left: 2 (199 enodes)
1550842783.090 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.090 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550842783.090 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550842783.091 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550842783.092 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550842783.095 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550842783.114 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550842783.139 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550842783.155 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550842783.155 * [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))
1550842783.155 * * * * [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))>
1550842783.155 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550842783.155 * * [misc]simplify:  iters left: 5 (9 enodes)
1550842783.157 * * [misc]simplify:  iters left: 4 (29 enodes)
1550842783.162 * * [misc]simplify:  iters left: 3 (62 enodes)
1550842783.174 * * [misc]simplify:  iters left: 2 (199 enodes)
1550842783.247 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.248 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550842783.248 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550842783.249 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550842783.251 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550842783.257 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550842783.281 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550842783.316 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550842783.331 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550842783.332 * [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))
1550842783.332 * * * * [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))>
1550842783.332 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550842783.332 * * [misc]simplify:  iters left: 5 (9 enodes)
1550842783.334 * * [misc]simplify:  iters left: 4 (29 enodes)
1550842783.341 * * [misc]simplify:  iters left: 3 (62 enodes)
1550842783.364 * * [misc]simplify:  iters left: 2 (199 enodes)
1550842783.429 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.429 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550842783.429 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550842783.430 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550842783.432 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550842783.439 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550842783.462 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550842783.493 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550842783.524 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550842783.524 * [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))
1550842783.525 * * * * [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))>
1550842783.525 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550842783.525 * * [misc]simplify:  iters left: 5 (9 enodes)
1550842783.529 * * [misc]simplify:  iters left: 4 (29 enodes)
1550842783.540 * * [misc]simplify:  iters left: 3 (62 enodes)
1550842783.552 * * [misc]simplify:  iters left: 2 (199 enodes)
1550842783.618 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842783.618 * * [misc]simplify:  Extracting #1: cost 20 inf + 0
1550842783.618 * * [misc]simplify:  Extracting #2: cost 94 inf + 1
1550842783.619 * * [misc]simplify:  Extracting #3: cost 162 inf + 1046
1550842783.622 * * [misc]simplify:  Extracting #4: cost 208 inf + 17818
1550842783.626 * * [misc]simplify:  Extracting #5: cost 164 inf + 103714
1550842783.645 * * [misc]simplify:  Extracting #6: cost 47 inf + 336456
1550842783.677 * * [misc]simplify:  Extracting #7: cost 0 inf + 409081
1550842783.708 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1550842783.708 * [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))
1550842783.708 * * * [misc]progress:  adding candidates to table
1550842783.979 * * [misc]progress:  iteration 2 / 4
1550842783.979 * * * [misc]progress:  picking best candidate
1550842784.051 * * * * [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))>
1550842784.051 * * * [misc]progress:  localizing error
1550842784.361 * * * [misc]progress:  generating rewritten candidates
1550842784.361 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1 1)
1550842784.368 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1)
1550842784.370 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 1)
1550842784.371 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2)
1550842784.375 * * * [misc]progress:  generating series expansions
1550842784.375 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1 1)
1550842784.375 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1)
1550842784.375 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 1)
1550842784.375 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2)
1550842784.376 * * * [misc]progress:  simplifying candidates
1550842784.376 * * * * [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))>
1550842784.376 * [enter]simplify:  Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1550842784.376 * * [misc]simplify:  iters left: 2 (6 enodes)
1550842784.379 * * [misc]simplify:  iters left: 1 (14 enodes)
1550842784.383 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842784.383 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842784.383 * * [misc]simplify:  Extracting #2: cost 6 inf + 0
1550842784.383 * * [misc]simplify:  Extracting #3: cost 2 inf + 325
1550842784.383 * * [misc]simplify:  Extracting #4: cost 0 inf + 1329
1550842784.383 * [exit]simplify:  Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1550842784.383 * [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))
1550842784.383 * * * * [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))>
1550842784.383 * [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))))
1550842784.384 * * [misc]simplify:  iters left: 4 (10 enodes)
1550842784.388 * * [misc]simplify:  iters left: 3 (43 enodes)
1550842784.414 * * [misc]simplify:  iters left: 2 (121 enodes)
1550842784.450 * * [misc]simplify:  iters left: 1 (429 enodes)
1550842784.725 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842784.725 * * [misc]simplify:  Extracting #1: cost 46 inf + 0
1550842784.727 * * [misc]simplify:  Extracting #2: cost 270 inf + 0
1550842784.736 * * [misc]simplify:  Extracting #3: cost 354 inf + 59003
1550842784.762 * * [misc]simplify:  Extracting #4: cost 345 inf + 369227
1550842784.821 * * [misc]simplify:  Extracting #5: cost 22 inf + 1102360
1550842784.922 * * [misc]simplify:  Extracting #6: cost 1 inf + 1150488
1550842785.023 * * [misc]simplify:  Extracting #7: cost 0 inf + 1155051
1550842785.095 * [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))))
1550842785.096 * [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))
1550842785.096 * * * * [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))>
1550842785.096 * * * * [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))>
1550842785.096 * * * * [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))))>
1550842785.096 * [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))
1550842785.096 * * [misc]simplify:  iters left: 6 (13 enodes)
1550842785.102 * * [misc]simplify:  iters left: 5 (47 enodes)
1550842785.119 * * [misc]simplify:  iters left: 4 (118 enodes)
1550842785.171 * * [misc]simplify:  iters left: 3 (482 enodes)
1550842785.739 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842785.739 * * [misc]simplify:  Extracting #1: cost 39 inf + 0
1550842785.741 * * [misc]simplify:  Extracting #2: cost 255 inf + 0
1550842785.744 * * [misc]simplify:  Extracting #3: cost 532 inf + 10719
1550842785.766 * * [misc]simplify:  Extracting #4: cost 679 inf + 310118
1550842785.872 * * [misc]simplify:  Extracting #5: cost 214 inf + 1310578
1550842786.025 * * [misc]simplify:  Extracting #6: cost 5 inf + 1763746
1550842786.187 * * [misc]simplify:  Extracting #7: cost 0 inf + 1773035
1550842786.310 * [exit]simplify:  Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
1550842786.311 * [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))))
1550842786.311 * * * * [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))>
1550842786.311 * * * * [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))>
1550842786.311 * * * * [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))>
1550842786.311 * * * * [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))>
1550842786.311 * * * [misc]progress:  adding candidates to table
1550842786.736 * * [misc]progress:  iteration 3 / 4
1550842786.736 * * * [misc]progress:  picking best candidate
1550842786.858 * * * * [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))>
1550842786.858 * * * [misc]progress:  localizing error
1550842787.010 * * * [misc]progress:  generating rewritten candidates
1550842787.010 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 1)
1550842787.012 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 2)
1550842787.015 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1)
1550842787.022 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1 2 1)
1550842787.023 * * * [misc]progress:  generating series expansions
1550842787.023 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 1)
1550842787.023 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 2)
1550842787.023 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1)
1550842787.023 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1 2 1)
1550842787.023 * * * [misc]progress:  simplifying candidates
1550842787.023 * * * * [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))>
1550842787.023 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842787.024 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842787.027 * * [misc]simplify:  iters left: 3 (23 enodes)
1550842787.035 * * [misc]simplify:  iters left: 2 (45 enodes)
1550842787.051 * * [misc]simplify:  iters left: 1 (108 enodes)
1550842787.096 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842787.096 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842787.096 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550842787.096 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550842787.096 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550842787.096 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550842787.098 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550842787.104 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550842787.111 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550842787.117 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550842787.117 * [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))
1550842787.117 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842787.117 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842787.119 * * [misc]simplify:  iters left: 3 (28 enodes)
1550842787.124 * * [misc]simplify:  iters left: 2 (59 enodes)
1550842787.139 * * [misc]simplify:  iters left: 1 (178 enodes)
1550842787.217 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842787.217 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550842787.217 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550842787.217 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550842787.218 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550842787.222 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550842787.234 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550842787.247 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550842787.264 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550842787.278 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550842787.278 * [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))
1550842787.278 * * * * [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))>
1550842787.278 * * * * [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))>
1550842787.278 * * * * [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))>
1550842787.278 * * * * [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))>
1550842787.278 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842787.278 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842787.280 * * [misc]simplify:  iters left: 3 (23 enodes)
1550842787.284 * * [misc]simplify:  iters left: 2 (45 enodes)
1550842787.292 * * [misc]simplify:  iters left: 1 (108 enodes)
1550842787.323 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842787.323 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842787.323 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550842787.323 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550842787.323 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550842787.323 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550842787.325 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550842787.332 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550842787.339 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550842787.346 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550842787.346 * [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))
1550842787.346 * * * * [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))>
1550842787.346 * [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)))
1550842787.346 * * [misc]simplify:  iters left: 6 (11 enodes)
1550842787.350 * * [misc]simplify:  iters left: 5 (43 enodes)
1550842787.367 * * [misc]simplify:  iters left: 4 (139 enodes)
1550842787.421 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842787.421 * * [misc]simplify:  Extracting #1: cost 32 inf + 0
1550842787.422 * * [misc]simplify:  Extracting #2: cost 85 inf + 0
1550842787.422 * * [misc]simplify:  Extracting #3: cost 152 inf + 1364
1550842787.424 * * [misc]simplify:  Extracting #4: cost 163 inf + 24483
1550842787.435 * * [misc]simplify:  Extracting #5: cost 71 inf + 172897
1550842787.448 * * [misc]simplify:  Extracting #6: cost 3 inf + 277964
1550842787.459 * * [misc]simplify:  Extracting #7: cost 0 inf + 284573
1550842787.481 * [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))))
1550842787.481 * [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))
1550842787.481 * * * * [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))>
1550842787.481 * * * * [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))>
1550842787.481 * * * * [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))>
1550842787.481 * * * * [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))>
1550842787.482 * * * [misc]progress:  adding candidates to table
1550842787.799 * * [misc]progress:  iteration 4 / 4
1550842787.799 * * * [misc]progress:  picking best candidate
1550842787.955 * * * * [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))>
1550842787.955 * * * [misc]progress:  localizing error
1550842788.062 * * * [misc]progress:  generating rewritten candidates
1550842788.062 * * * * [misc]progress:  [ 1 / 4 ] rewriting at (2 1 2)
1550842788.064 * * * * [misc]progress:  [ 2 / 4 ] rewriting at (2 1 1 1)
1550842788.065 * * * * [misc]progress:  [ 3 / 4 ] rewriting at (2 1 1 2)
1550842788.066 * * * * [misc]progress:  [ 4 / 4 ] rewriting at (2 1)
1550842788.070 * * * [misc]progress:  generating series expansions
1550842788.070 * * * * [misc]progress:  [ 1 / 4 ] generating series at (2 1 2)
1550842788.070 * * * * [misc]progress:  [ 2 / 4 ] generating series at (2 1 1 1)
1550842788.070 * * * * [misc]progress:  [ 3 / 4 ] generating series at (2 1 1 2)
1550842788.070 * * * * [misc]progress:  [ 4 / 4 ] generating series at (2 1)
1550842788.071 * * * [misc]progress:  simplifying candidates
1550842788.071 * * * * [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))>
1550842788.071 * * * * [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))>
1550842788.071 * * * * [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))>
1550842788.071 * * * * [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))>
1550842788.071 * * * * [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))>
1550842788.071 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842788.071 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842788.073 * * [misc]simplify:  iters left: 3 (23 enodes)
1550842788.077 * * [misc]simplify:  iters left: 2 (45 enodes)
1550842788.086 * * [misc]simplify:  iters left: 1 (108 enodes)
1550842788.126 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842788.126 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842788.126 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550842788.126 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550842788.126 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550842788.126 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550842788.128 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550842788.134 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550842788.141 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550842788.147 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550842788.147 * [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))
1550842788.148 * * * * [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))>
1550842788.148 * [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)))
1550842788.148 * * [misc]simplify:  iters left: 6 (11 enodes)
1550842788.150 * * [misc]simplify:  iters left: 5 (35 enodes)
1550842788.157 * * [misc]simplify:  iters left: 4 (111 enodes)
1550842788.201 * * [misc]simplify:  iters left: 3 (448 enodes)
1550842788.557 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842788.558 * * [misc]simplify:  Extracting #1: cost 64 inf + 0
1550842788.560 * * [misc]simplify:  Extracting #2: cost 370 inf + 0
1550842788.563 * * [misc]simplify:  Extracting #3: cost 522 inf + 6695
1550842788.586 * * [misc]simplify:  Extracting #4: cost 536 inf + 237314
1550842788.655 * * [misc]simplify:  Extracting #5: cost 132 inf + 950329
1550842788.750 * * [misc]simplify:  Extracting #6: cost 26 inf + 1188087
1550842788.846 * * [misc]simplify:  Extracting #7: cost 0 inf + 1213652
1550842788.959 * * [misc]simplify:  Extracting #8: cost 0 inf + 1213496
1550842789.073 * [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)))))
1550842789.073 * [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))
1550842789.073 * * * * [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))>
1550842789.073 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842789.073 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842789.077 * * [misc]simplify:  iters left: 3 (23 enodes)
1550842789.086 * * [misc]simplify:  iters left: 2 (45 enodes)
1550842789.103 * * [misc]simplify:  iters left: 1 (108 enodes)
1550842789.159 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.159 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842789.159 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550842789.159 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550842789.159 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550842789.160 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550842789.164 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550842789.174 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550842789.187 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550842789.200 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550842789.200 * [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))
1550842789.201 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842789.201 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842789.204 * * [misc]simplify:  iters left: 3 (28 enodes)
1550842789.214 * * [misc]simplify:  iters left: 2 (59 enodes)
1550842789.240 * * [misc]simplify:  iters left: 1 (178 enodes)
1550842789.345 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.345 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550842789.345 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550842789.346 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550842789.348 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550842789.357 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550842789.382 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550842789.401 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550842789.415 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550842789.435 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550842789.435 * [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))
1550842789.435 * * * * [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))>
1550842789.436 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842789.436 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842789.439 * * [misc]simplify:  iters left: 3 (23 enodes)
1550842789.447 * * [misc]simplify:  iters left: 2 (45 enodes)
1550842789.464 * * [misc]simplify:  iters left: 1 (108 enodes)
1550842789.521 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.521 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842789.521 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550842789.521 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550842789.521 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550842789.522 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550842789.526 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550842789.537 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550842789.547 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550842789.553 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550842789.553 * [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))
1550842789.554 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842789.554 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842789.555 * * [misc]simplify:  iters left: 3 (28 enodes)
1550842789.560 * * [misc]simplify:  iters left: 2 (59 enodes)
1550842789.574 * * [misc]simplify:  iters left: 1 (178 enodes)
1550842789.643 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.643 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550842789.643 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550842789.644 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550842789.646 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550842789.651 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550842789.662 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550842789.676 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550842789.696 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550842789.724 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550842789.724 * [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))
1550842789.724 * * * * [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))>
1550842789.725 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842789.725 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842789.728 * * [misc]simplify:  iters left: 3 (23 enodes)
1550842789.736 * * [misc]simplify:  iters left: 2 (45 enodes)
1550842789.752 * * [misc]simplify:  iters left: 1 (108 enodes)
1550842789.809 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.809 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842789.810 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550842789.810 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550842789.810 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550842789.811 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550842789.814 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550842789.825 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550842789.838 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550842789.853 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550842789.853 * [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))
1550842789.853 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842789.854 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842789.857 * * [misc]simplify:  iters left: 3 (28 enodes)
1550842789.867 * * [misc]simplify:  iters left: 2 (59 enodes)
1550842789.889 * * [misc]simplify:  iters left: 1 (178 enodes)
1550842789.999 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842789.999 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550842789.999 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550842790.000 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550842790.002 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550842790.009 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550842790.030 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550842790.043 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550842790.058 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550842790.072 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550842790.072 * [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))
1550842790.072 * * * * [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))>
1550842790.072 * [enter]simplify:  Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842790.072 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842790.074 * * [misc]simplify:  iters left: 3 (23 enodes)
1550842790.078 * * [misc]simplify:  iters left: 2 (45 enodes)
1550842790.088 * * [misc]simplify:  iters left: 1 (108 enodes)
1550842790.135 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842790.135 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842790.136 * * [misc]simplify:  Extracting #2: cost 3 inf + 1
1550842790.136 * * [misc]simplify:  Extracting #3: cost 17 inf + 1
1550842790.136 * * [misc]simplify:  Extracting #4: cost 55 inf + 322
1550842790.137 * * [misc]simplify:  Extracting #5: cost 80 inf + 11197
1550842790.140 * * [misc]simplify:  Extracting #6: cost 84 inf + 56173
1550842790.151 * * [misc]simplify:  Extracting #7: cost 7 inf + 177856
1550842790.164 * * [misc]simplify:  Extracting #8: cost 0 inf + 193436
1550842790.177 * [exit]simplify:  Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1550842790.177 * [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))
1550842790.177 * [enter]simplify:  Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1550842790.177 * * [misc]simplify:  iters left: 4 (8 enodes)
1550842790.181 * * [misc]simplify:  iters left: 3 (28 enodes)
1550842790.191 * * [misc]simplify:  iters left: 2 (59 enodes)
1550842790.213 * * [misc]simplify:  iters left: 1 (178 enodes)
1550842790.275 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842790.275 * * [misc]simplify:  Extracting #1: cost 12 inf + 0
1550842790.276 * * [misc]simplify:  Extracting #2: cost 64 inf + 1
1550842790.276 * * [misc]simplify:  Extracting #3: cost 140 inf + 403
1550842790.278 * * [misc]simplify:  Extracting #4: cost 189 inf + 12881
1550842790.286 * * [misc]simplify:  Extracting #5: cost 149 inf + 112868
1550842790.311 * * [misc]simplify:  Extracting #6: cost 32 inf + 315911
1550842790.340 * * [misc]simplify:  Extracting #7: cost 1 inf + 362422
1550842790.358 * * [misc]simplify:  Extracting #8: cost 0 inf + 365106
1550842790.372 * [exit]simplify:  Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1550842790.372 * [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))
1550842790.372 * * * [misc]progress:  adding candidates to table
1550842790.833 * [misc]progress:  [Phase 3 of 3] Extracting.
1550842790.833 * * [misc]regime:  Finding splitpoints for: (#<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 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (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 (*.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 (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 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.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))) (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 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (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))>)
1550842790.838 * * * [misc]regime-changes:  Trying 3 branch expressions: (c a b_2)
1550842790.839 * * * * [misc]regimes:  Trying to branch on c from (#<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 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (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 (*.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 (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 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.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))) (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 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (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))>)
1550842791.331 * * * * [misc]regimes:  Trying to branch on a from (#<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 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (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 (*.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 (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 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.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))) (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 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (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))>)
1550842791.832 * * * * [misc]regimes:  Trying to branch on b_2 from (#<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 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (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 (*.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 (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 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.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))) (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 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (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))>)
1550842792.226 * * * [misc]regime:  Found split indices: #<option (#s(si 7 256))>
1550842792.227 * [enter]simplify:  Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550842792.227 * * [misc]simplify:  iters left: 5 (9 enodes)
1550842792.227 * * [misc]simplify:  Extracting #0: cost 1 inf + 0
1550842792.227 * * [misc]simplify:  Extracting #1: cost 3 inf + 0
1550842792.227 * * [misc]simplify:  Extracting #2: cost 4 inf + 1
1550842792.227 * * [misc]simplify:  Extracting #3: cost 4 inf + 2
1550842792.227 * * [misc]simplify:  Extracting #4: cost 6 inf + 2
1550842792.227 * * [misc]simplify:  Extracting #5: cost 6 inf + 323
1550842792.227 * * [misc]simplify:  Extracting #6: cost 0 inf + 4258
1550842792.227 * [exit]simplify:  Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1550842792.227 * * * * [misc]points:  Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1550842792.263 * * * * [misc]points:  Computing exacts on every 500 of 8000 points to ramp up precision
1550842792.264 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.265 * * * * [misc]points:  Setting MPFR precision to 320
1550842792.267 * * * * [misc]points:  Computing exacts on every 250 of 8000 points to ramp up precision
1550842792.268 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.270 * * * * [misc]points:  Setting MPFR precision to 320
1550842792.272 * * * * [misc]points:  Computing exacts on every 125 of 8000 points to ramp up precision
1550842792.273 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.277 * * * * [misc]points:  Setting MPFR precision to 320
1550842792.282 * * * * [misc]points:  Computing exacts on every 62 of 8000 points to ramp up precision
1550842792.284 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.293 * * * * [misc]points:  Setting MPFR precision to 320
1550842792.303 * * * * [misc]points:  Computing exacts on every 31 of 8000 points to ramp up precision
1550842792.304 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.320 * * * * [misc]points:  Setting MPFR precision to 320
1550842792.342 * * * * [misc]points:  Computing exacts on every 15 of 8000 points to ramp up precision
1550842792.343 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.400 * * * * [misc]points:  Setting MPFR precision to 320
1550842792.442 * * * * [misc]points:  Computing exacts on every 7 of 8000 points to ramp up precision
1550842792.443 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.541 * * * * [misc]points:  Setting MPFR precision to 320
1550842792.637 * * * * [misc]points:  Computing exacts on every 3 of 8000 points to ramp up precision
1550842792.638 * * * * [misc]points:  Setting MPFR precision to 64
1550842792.795 * * * * [misc]points:  Setting MPFR precision to 320
1550842793.164 * * * * [misc]points:  Computing exacts for 8000 points
1550842793.167 * * * * [misc]points:  Setting MPFR precision to 64
1550842794.266 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.223 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842795.798 * * * * [misc]points:  Sampling 2064 additional inputs, on iter 1 have 5936 / 8000
1550842795.807 * * * * [misc]points:  Computing exacts on every 129 of 2064 points to ramp up precision
1550842795.808 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.810 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.826 * * * * [misc]points:  Computing exacts on every 64 of 2064 points to ramp up precision
1550842795.828 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.832 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.835 * * * * [misc]points:  Computing exacts on every 32 of 2064 points to ramp up precision
1550842795.836 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.840 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.845 * * * * [misc]points:  Computing exacts on every 16 of 2064 points to ramp up precision
1550842795.847 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.854 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.864 * * * * [misc]points:  Computing exacts on every 8 of 2064 points to ramp up precision
1550842795.865 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.879 * * * * [misc]points:  Setting MPFR precision to 320
1550842795.915 * * * * [misc]points:  Computing exacts on every 4 of 2064 points to ramp up precision
1550842795.917 * * * * [misc]points:  Setting MPFR precision to 64
1550842795.960 * * * * [misc]points:  Setting MPFR precision to 320
1550842796.059 * * * * [misc]points:  Computing exacts on every 2 of 2064 points to ramp up precision
1550842796.061 * * * * [misc]points:  Setting MPFR precision to 64
1550842796.131 * * * * [misc]points:  Setting MPFR precision to 320
1550842796.218 * * * * [misc]points:  Computing exacts for 2064 points
1550842796.220 * * * * [misc]points:  Setting MPFR precision to 64
1550842796.524 * * * * [misc]points:  Setting MPFR precision to 320
1550842796.791 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.027 * * * * [misc]points:  Sampling 532 additional inputs, on iter 2 have 7468 / 8000
1550842797.031 * * * * [misc]points:  Computing exacts on every 33 of 532 points to ramp up precision
1550842797.033 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.035 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.038 * * * * [misc]points:  Computing exacts on every 16 of 532 points to ramp up precision
1550842797.040 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.043 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.048 * * * * [misc]points:  Computing exacts on every 8 of 532 points to ramp up precision
1550842797.050 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.057 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.065 * * * * [misc]points:  Computing exacts on every 4 of 532 points to ramp up precision
1550842797.067 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.080 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.093 * * * * [misc]points:  Computing exacts on every 2 of 532 points to ramp up precision
1550842797.094 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.106 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.125 * * * * [misc]points:  Computing exacts for 532 points
1550842797.127 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.219 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.283 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.333 * * * * [misc]points:  Sampling 129 additional inputs, on iter 3 have 7871 / 8000
1550842797.334 * * * * [misc]points:  Computing exacts on every 8 of 129 points to ramp up precision
1550842797.335 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.337 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.339 * * * * [misc]points:  Computing exacts on every 4 of 129 points to ramp up precision
1550842797.341 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.344 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.347 * * * * [misc]points:  Computing exacts on every 2 of 129 points to ramp up precision
1550842797.349 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.354 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.360 * * * * [misc]points:  Computing exacts for 129 points
1550842797.362 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.844 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.866 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.880 * * * * [misc]points:  Sampling 32 additional inputs, on iter 4 have 7968 / 8000
1550842797.880 * * * * [misc]points:  Computing exacts on every 2 of 32 points to ramp up precision
1550842797.882 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.883 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.885 * * * * [misc]points:  Computing exacts for 32 points
1550842797.887 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.891 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.895 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.899 * * * * [misc]points:  Sampling 5 additional inputs, on iter 5 have 7995 / 8000
1550842797.899 * * * * [misc]points:  Computing exacts for 5 points
1550842797.902 * * * * [misc]points:  Setting MPFR precision to 64
1550842797.902 * * * * [misc]points:  Setting MPFR precision to 320
1550842797.903 * * * * [misc]points:  Filtering points with unrepresentable outputs
1550842797.904 * * * * [exit]points:  Sampled 8000 points with exact outputs
1550842801.133 * [misc]regime-testing:  Baseline error score: 64.0
1550842801.137 * [misc]regime-testing:  Oracle error score: 64.0
1550842801.145 * [misc]regime-testing:  End program error score: 2.3145939968047435