1552469842.147 * [progress]: [Phase 1 of 3] Setting up.
1552469842.150 * * * [progress]: [1/2] Preparing points
1552469842.151 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
1552469842.159 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
1552469842.214 * * * * [points]: Setting MPFR precision to 64
1552469842.219 * * * * [points]: Setting MPFR precision to 320
1552469842.222 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
1552469842.270 * * * * [points]: Setting MPFR precision to 64
1552469842.304 * * * * [points]: Setting MPFR precision to 320
1552469842.311 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
1552469842.314 * * * * [points]: Setting MPFR precision to 64
1552469842.323 * * * * [points]: Setting MPFR precision to 320
1552469842.332 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
1552469842.333 * * * * [points]: Setting MPFR precision to 64
1552469842.340 * * * * [points]: Setting MPFR precision to 320
1552469842.347 * * * * [points]: Computing exacts for 256 points
1552469842.348 * * * * [points]: Setting MPFR precision to 64
1552469842.409 * * * * [points]: Setting MPFR precision to 320
1552469842.481 * * * * [points]: Filtering points with unrepresentable outputs
1552469842.506 * * * * [points]: Sampling 49 additional inputs, on iter 1 have 207 / 256
1552469842.506 * * * * [points]: Computing exacts on every 3 of 49 points to ramp up precision
1552469842.508 * * * * [points]: Setting MPFR precision to 64
1552469842.510 * * * * [points]: Setting MPFR precision to 320
1552469842.511 * * * * [points]: Computing exacts for 49 points
1552469842.513 * * * * [points]: Setting MPFR precision to 64
1552469842.519 * * * * [points]: Setting MPFR precision to 320
1552469842.525 * * * * [points]: Filtering points with unrepresentable outputs
1552469842.529 * * * * [points]: Sampling 15 additional inputs, on iter 2 have 241 / 256
1552469842.529 * * * * [points]: Computing exacts for 15 points
1552469842.532 * * * * [points]: Setting MPFR precision to 64
1552469842.534 * * * * [points]: Setting MPFR precision to 320
1552469842.537 * * * * [points]: Filtering points with unrepresentable outputs
1552469842.538 * * * * [points]: Sampling 8 additional inputs, on iter 3 have 248 / 256
1552469842.538 * * * * [points]: Computing exacts for 8 points
1552469842.540 * * * * [points]: Setting MPFR precision to 64
1552469842.542 * * * * [points]: Setting MPFR precision to 320
1552469842.543 * * * * [points]: Filtering points with unrepresentable outputs
1552469842.544 * * * * [points]: Sampling 4 additional inputs, on iter 4 have 253 / 256
1552469842.544 * * * * [points]: Computing exacts for 4 points
1552469842.547 * * * * [points]: Setting MPFR precision to 64
1552469842.548 * * * * [points]: Setting MPFR precision to 320
1552469842.548 * * * * [points]: Filtering points with unrepresentable outputs
1552469842.549 * * * * [points]: Sampled 257 points with exact outputs
1552469842.550 * * * [progress]: [2/2] Setting up program.
1552469842.616 * [progress]: [Phase 2 of 3] Improving.
1552469842.616 * * * * [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))>
1552469842.617 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1552469842.618 * * [simplify]: iters left: 5 (10 enodes)
1552469842.625 * * [simplify]: iters left: 4 (25 enodes)
1552469842.630 * * [simplify]: iters left: 3 (48 enodes)
1552469842.639 * * [simplify]: iters left: 2 (111 enodes)
1552469842.668 * * [simplify]: iters left: 1 (392 enodes)
1552469843.586 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469843.587 * * [simplify]: Extracting #1: cost 10 inf + 0
1552469843.587 * * [simplify]: Extracting #2: cost 35 inf + 1
1552469843.588 * * [simplify]: Extracting #3: cost 91 inf + 405
1552469843.590 * * [simplify]: Extracting #4: cost 331 inf + 2291
1552469843.596 * * [simplify]: Extracting #5: cost 455 inf + 80323
1552469843.644 * * [simplify]: Extracting #6: cost 250 inf + 579968
1552469843.702 * * [simplify]: Extracting #7: cost 28 inf + 1003440
1552469843.781 * * [simplify]: Extracting #8: cost 0 inf + 1069311
1552469843.841 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552469843.842 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
1552469843.873 * * [progress]: iteration 1 / 4
1552469843.873 * * * [progress]: picking best candidate
1552469843.899 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1552469843.899 * * * [progress]: localizing error
1552469844.229 * * * [progress]: generating rewritten candidates
1552469844.229 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1552469844.234 * * * * [progress]: [ 2 / 4 ] rewriting at (2)
1552469844.237 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
1552469844.237 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1552469844.244 * * * [progress]: generating series expansions
1552469844.244 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1552469844.244 * * * * [progress]: [ 2 / 4 ] generating series at (2)
1552469844.244 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
1552469844.244 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1552469844.244 * * * [progress]: simplifying candidates
1552469844.244 * * * * [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))>
1552469844.245 * * * * [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))>
1552469844.245 * * * * [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))))>
1552469844.245 * [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))
1552469844.245 * * [simplify]: iters left: 5 (9 enodes)
1552469844.247 * * [simplify]: iters left: 4 (32 enodes)
1552469844.253 * * [simplify]: iters left: 3 (94 enodes)
1552469844.286 * * [simplify]: iters left: 2 (340 enodes)
1552469844.542 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469844.543 * * [simplify]: Extracting #1: cost 50 inf + 0
1552469844.544 * * [simplify]: Extracting #2: cost 240 inf + 0
1552469844.549 * * [simplify]: Extracting #3: cost 355 inf + 61800
1552469844.580 * * [simplify]: Extracting #4: cost 246 inf + 415499
1552469844.645 * * [simplify]: Extracting #5: cost 58 inf + 816216
1552469844.729 * * [simplify]: Extracting #6: cost 1 inf + 911482
1552469844.808 * * [simplify]: Extracting #7: cost 0 inf + 914765
1552469844.863 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1552469844.863 * [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))))
1552469844.863 * * * * [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))>
1552469844.863 * * * * [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))>
1552469844.863 * * * * [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))>
1552469844.863 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552469844.864 * * [simplify]: iters left: 5 (9 enodes)
1552469844.866 * * [simplify]: iters left: 4 (29 enodes)
1552469844.873 * * [simplify]: iters left: 3 (62 enodes)
1552469844.886 * * [simplify]: iters left: 2 (199 enodes)
1552469844.982 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469844.982 * * [simplify]: Extracting #1: cost 20 inf + 0
1552469844.983 * * [simplify]: Extracting #2: cost 94 inf + 1
1552469844.983 * * [simplify]: Extracting #3: cost 162 inf + 1046
1552469844.986 * * [simplify]: Extracting #4: cost 208 inf + 17818
1552469844.992 * * [simplify]: Extracting #5: cost 164 inf + 103714
1552469845.016 * * [simplify]: Extracting #6: cost 47 inf + 336456
1552469845.047 * * [simplify]: Extracting #7: cost 0 inf + 409081
1552469845.079 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1552469845.079 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1552469845.080 * * * * [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))>
1552469845.080 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552469845.080 * * [simplify]: iters left: 5 (9 enodes)
1552469845.084 * * [simplify]: iters left: 4 (29 enodes)
1552469845.098 * * [simplify]: iters left: 3 (62 enodes)
1552469845.123 * * [simplify]: iters left: 2 (199 enodes)
1552469845.233 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469845.233 * * [simplify]: Extracting #1: cost 20 inf + 0
1552469845.233 * * [simplify]: Extracting #2: cost 94 inf + 1
1552469845.234 * * [simplify]: Extracting #3: cost 162 inf + 1046
1552469845.236 * * [simplify]: Extracting #4: cost 208 inf + 17818
1552469845.240 * * [simplify]: Extracting #5: cost 164 inf + 103714
1552469845.251 * * [simplify]: Extracting #6: cost 47 inf + 336456
1552469845.267 * * [simplify]: Extracting #7: cost 0 inf + 409081
1552469845.296 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1552469845.296 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1552469845.296 * * * * [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))>
1552469845.297 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552469845.297 * * [simplify]: iters left: 5 (9 enodes)
1552469845.300 * * [simplify]: iters left: 4 (29 enodes)
1552469845.310 * * [simplify]: iters left: 3 (62 enodes)
1552469845.330 * * [simplify]: iters left: 2 (199 enodes)
1552469845.408 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469845.408 * * [simplify]: Extracting #1: cost 20 inf + 0
1552469845.408 * * [simplify]: Extracting #2: cost 94 inf + 1
1552469845.409 * * [simplify]: Extracting #3: cost 162 inf + 1046
1552469845.410 * * [simplify]: Extracting #4: cost 208 inf + 17818
1552469845.413 * * [simplify]: Extracting #5: cost 164 inf + 103714
1552469845.427 * * [simplify]: Extracting #6: cost 47 inf + 336456
1552469845.455 * * [simplify]: Extracting #7: cost 0 inf + 409081
1552469845.486 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1552469845.486 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1552469845.486 * * * * [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))>
1552469845.486 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552469845.486 * * [simplify]: iters left: 5 (9 enodes)
1552469845.490 * * [simplify]: iters left: 4 (29 enodes)
1552469845.500 * * [simplify]: iters left: 3 (62 enodes)
1552469845.524 * * [simplify]: iters left: 2 (199 enodes)
1552469845.604 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469845.604 * * [simplify]: Extracting #1: cost 20 inf + 0
1552469845.605 * * [simplify]: Extracting #2: cost 94 inf + 1
1552469845.605 * * [simplify]: Extracting #3: cost 162 inf + 1046
1552469845.608 * * [simplify]: Extracting #4: cost 208 inf + 17818
1552469845.614 * * [simplify]: Extracting #5: cost 164 inf + 103714
1552469845.638 * * [simplify]: Extracting #6: cost 47 inf + 336456
1552469845.673 * * [simplify]: Extracting #7: cost 0 inf + 409081
1552469845.704 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1552469845.704 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1552469845.704 * * * [progress]: adding candidates to table
1552469846.108 * * [progress]: iteration 2 / 4
1552469846.108 * * * [progress]: picking best candidate
1552469846.164 * * * * [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))>
1552469846.164 * * * [progress]: localizing error
1552469846.382 * * * [progress]: generating rewritten candidates
1552469846.382 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
1552469846.411 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
1552469846.412 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1552469846.416 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1)
1552469846.417 * * * [progress]: generating series expansions
1552469846.417 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
1552469846.418 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
1552469846.418 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1552469846.418 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1)
1552469846.418 * * * [progress]: simplifying candidates
1552469846.418 * * * * [progress]: [ 1 / 12 ] 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))>
1552469846.418 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1552469846.418 * * [simplify]: iters left: 2 (6 enodes)
1552469846.421 * * [simplify]: iters left: 1 (14 enodes)
1552469846.424 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469846.424 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469846.424 * * [simplify]: Extracting #2: cost 6 inf + 0
1552469846.424 * * [simplify]: Extracting #3: cost 2 inf + 325
1552469846.425 * * [simplify]: Extracting #4: cost 0 inf + 1329
1552469846.425 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1552469846.425 * [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))
1552469846.425 * * * * [progress]: [ 2 / 12 ] 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))>
1552469846.425 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1552469846.425 * * [simplify]: iters left: 2 (6 enodes)
1552469846.428 * * [simplify]: iters left: 1 (14 enodes)
1552469846.431 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469846.431 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469846.431 * * [simplify]: Extracting #2: cost 6 inf + 0
1552469846.431 * * [simplify]: Extracting #3: cost 2 inf + 325
1552469846.431 * * [simplify]: Extracting #4: cost 0 inf + 1329
1552469846.431 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1552469846.431 * [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))
1552469846.431 * * * * [progress]: [ 3 / 12 ] 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))>
1552469846.431 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1552469846.431 * * [simplify]: iters left: 2 (6 enodes)
1552469846.432 * * [simplify]: iters left: 1 (14 enodes)
1552469846.434 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469846.434 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469846.434 * * [simplify]: Extracting #2: cost 6 inf + 0
1552469846.434 * * [simplify]: Extracting #3: cost 2 inf + 325
1552469846.434 * * [simplify]: Extracting #4: cost 0 inf + 1329
1552469846.434 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1552469846.434 * [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))
1552469846.435 * * * * [progress]: [ 4 / 12 ] 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))>
1552469846.435 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1552469846.435 * * [simplify]: iters left: 2 (6 enodes)
1552469846.436 * * [simplify]: iters left: 1 (14 enodes)
1552469846.441 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469846.441 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469846.441 * * [simplify]: Extracting #2: cost 6 inf + 0
1552469846.441 * * [simplify]: Extracting #3: cost 2 inf + 325
1552469846.441 * * [simplify]: Extracting #4: cost 0 inf + 1329
1552469846.441 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1552469846.441 * [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))
1552469846.441 * * * * [progress]: [ 5 / 12 ] 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))>
1552469846.442 * [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))))
1552469846.442 * * [simplify]: iters left: 4 (10 enodes)
1552469846.444 * * [simplify]: iters left: 3 (43 enodes)
1552469846.453 * * [simplify]: iters left: 2 (121 enodes)
1552469846.508 * * [simplify]: iters left: 1 (429 enodes)
1552469846.761 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469846.761 * * [simplify]: Extracting #1: cost 46 inf + 0
1552469846.762 * * [simplify]: Extracting #2: cost 270 inf + 0
1552469846.764 * * [simplify]: Extracting #3: cost 354 inf + 59003
1552469846.777 * * [simplify]: Extracting #4: cost 345 inf + 369227
1552469846.821 * * [simplify]: Extracting #5: cost 22 inf + 1102360
1552469846.875 * * [simplify]: Extracting #6: cost 1 inf + 1150488
1552469846.927 * * [simplify]: Extracting #7: cost 0 inf + 1155051
1552469846.979 * [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))))
1552469846.979 * [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))
1552469846.979 * * * * [progress]: [ 6 / 12 ] 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))>
1552469846.980 * * * * [progress]: [ 7 / 12 ] 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))>
1552469846.980 * * * * [progress]: [ 8 / 12 ] 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))))>
1552469846.980 * [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))
1552469846.980 * * [simplify]: iters left: 6 (13 enodes)
1552469846.983 * * [simplify]: iters left: 5 (47 enodes)
1552469846.992 * * [simplify]: iters left: 4 (118 enodes)
1552469847.034 * * [simplify]: iters left: 3 (482 enodes)
1552469847.423 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469847.423 * * [simplify]: Extracting #1: cost 39 inf + 0
1552469847.424 * * [simplify]: Extracting #2: cost 255 inf + 0
1552469847.425 * * [simplify]: Extracting #3: cost 532 inf + 10719
1552469847.446 * * [simplify]: Extracting #4: cost 679 inf + 310118
1552469847.534 * * [simplify]: Extracting #5: cost 214 inf + 1310578
1552469847.689 * * [simplify]: Extracting #6: cost 5 inf + 1763746
1552469847.852 * * [simplify]: Extracting #7: cost 0 inf + 1773035
1552469848.014 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
1552469848.014 * [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))))
1552469848.014 * * * * [progress]: [ 9 / 12 ] 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))>
1552469848.014 * * * * [progress]: [ 10 / 12 ] 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))>
1552469848.014 * * * * [progress]: [ 11 / 12 ] 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))>
1552469848.014 * * * * [progress]: [ 12 / 12 ] 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))>
1552469848.014 * * * [progress]: adding candidates to table
1552469848.544 * * [progress]: iteration 3 / 4
1552469848.544 * * * [progress]: picking best candidate
1552469848.626 * * * * [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))>
1552469848.626 * * * [progress]: localizing error
1552469848.789 * * * [progress]: generating rewritten candidates
1552469848.789 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
1552469848.800 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1552469848.805 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
1552469848.825 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
1552469848.857 * * * [progress]: generating series expansions
1552469848.857 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
1552469848.857 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1552469848.858 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
1552469848.858 * * * * [progress]: [ 4 / 4 ] generating series at (2)
1552469848.858 * * * [progress]: simplifying candidates
1552469848.858 * * * * [progress]: [ 1 / 22 ] 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))>
1552469848.858 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469848.858 * * [simplify]: iters left: 4 (8 enodes)
1552469848.861 * * [simplify]: iters left: 3 (23 enodes)
1552469848.865 * * [simplify]: iters left: 2 (45 enodes)
1552469848.876 * * [simplify]: iters left: 1 (108 enodes)
1552469848.903 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469848.903 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469848.903 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469848.903 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469848.903 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469848.903 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469848.905 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469848.915 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469848.926 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469848.937 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469848.938 * [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))
1552469848.938 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469848.938 * * [simplify]: iters left: 4 (8 enodes)
1552469848.941 * * [simplify]: iters left: 3 (28 enodes)
1552469848.951 * * [simplify]: iters left: 2 (59 enodes)
1552469848.972 * * [simplify]: iters left: 1 (178 enodes)
1552469849.024 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469849.024 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469849.024 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469849.024 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469849.025 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469849.029 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469849.042 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469849.055 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469849.069 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469849.083 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469849.083 * [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))
1552469849.083 * * * * [progress]: [ 2 / 22 ] 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))>
1552469849.083 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469849.083 * * [simplify]: iters left: 4 (8 enodes)
1552469849.085 * * [simplify]: iters left: 3 (23 enodes)
1552469849.089 * * [simplify]: iters left: 2 (45 enodes)
1552469849.096 * * [simplify]: iters left: 1 (108 enodes)
1552469849.124 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469849.124 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469849.125 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469849.125 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469849.125 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469849.125 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469849.127 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469849.132 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469849.138 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469849.145 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469849.145 * [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))
1552469849.145 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469849.145 * * [simplify]: iters left: 4 (8 enodes)
1552469849.147 * * [simplify]: iters left: 3 (28 enodes)
1552469849.152 * * [simplify]: iters left: 2 (59 enodes)
1552469849.163 * * [simplify]: iters left: 1 (178 enodes)
1552469849.266 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469849.266 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469849.266 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469849.267 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469849.269 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469849.276 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469849.296 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469849.323 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469849.352 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469849.379 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469849.379 * [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))
1552469849.379 * * * * [progress]: [ 3 / 22 ] 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))>
1552469849.379 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469849.379 * * [simplify]: iters left: 4 (8 enodes)
1552469849.381 * * [simplify]: iters left: 3 (23 enodes)
1552469849.384 * * [simplify]: iters left: 2 (45 enodes)
1552469849.392 * * [simplify]: iters left: 1 (108 enodes)
1552469849.419 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469849.419 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469849.420 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469849.420 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469849.420 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469849.420 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469849.423 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469849.433 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469849.445 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469849.461 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469849.461 * [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))
1552469849.461 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469849.461 * * [simplify]: iters left: 4 (8 enodes)
1552469849.465 * * [simplify]: iters left: 3 (28 enodes)
1552469849.474 * * [simplify]: iters left: 2 (59 enodes)
1552469849.485 * * [simplify]: iters left: 1 (178 enodes)
1552469849.558 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469849.558 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469849.558 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469849.559 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469849.561 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469849.568 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469849.590 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469849.605 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469849.619 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469849.633 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469849.633 * [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))
1552469849.634 * * * * [progress]: [ 4 / 22 ] 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))>
1552469849.634 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469849.634 * * [simplify]: iters left: 4 (8 enodes)
1552469849.636 * * [simplify]: iters left: 3 (23 enodes)
1552469849.639 * * [simplify]: iters left: 2 (45 enodes)
1552469849.649 * * [simplify]: iters left: 1 (108 enodes)
1552469849.688 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469849.688 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469849.688 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469849.688 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469849.689 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469849.690 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469849.693 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469849.703 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469849.716 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469849.728 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469849.728 * [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))
1552469849.729 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469849.729 * * [simplify]: iters left: 4 (8 enodes)
1552469849.732 * * [simplify]: iters left: 3 (28 enodes)
1552469849.742 * * [simplify]: iters left: 2 (59 enodes)
1552469849.755 * * [simplify]: iters left: 1 (178 enodes)
1552469849.810 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469849.811 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469849.811 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469849.812 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469849.814 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469849.821 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469849.843 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469849.874 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469849.902 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469849.930 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469849.930 * [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))
1552469849.930 * * * * [progress]: [ 5 / 22 ] 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))>
1552469849.930 * * * * [progress]: [ 6 / 22 ] 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))>
1552469849.930 * * * * [progress]: [ 7 / 22 ] 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))>
1552469849.930 * * * * [progress]: [ 8 / 22 ] 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))>
1552469849.930 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469849.931 * * [simplify]: iters left: 4 (8 enodes)
1552469849.934 * * [simplify]: iters left: 3 (23 enodes)
1552469849.941 * * [simplify]: iters left: 2 (45 enodes)
1552469849.958 * * [simplify]: iters left: 1 (108 enodes)
1552469850.009 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469850.009 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469850.010 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469850.010 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469850.010 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469850.010 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469850.012 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469850.017 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469850.023 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469850.030 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469850.030 * [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))
1552469850.030 * * * * [progress]: [ 9 / 22 ] 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))>
1552469850.030 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469850.031 * * [simplify]: iters left: 4 (8 enodes)
1552469850.032 * * [simplify]: iters left: 3 (23 enodes)
1552469850.036 * * [simplify]: iters left: 2 (45 enodes)
1552469850.048 * * [simplify]: iters left: 1 (108 enodes)
1552469850.102 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469850.103 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469850.103 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469850.103 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469850.103 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469850.104 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469850.107 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469850.115 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469850.121 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469850.128 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469850.128 * [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))
1552469850.128 * * * * [progress]: [ 10 / 22 ] 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))>
1552469850.128 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469850.128 * * [simplify]: iters left: 4 (8 enodes)
1552469850.130 * * [simplify]: iters left: 3 (23 enodes)
1552469850.134 * * [simplify]: iters left: 2 (45 enodes)
1552469850.142 * * [simplify]: iters left: 1 (108 enodes)
1552469850.169 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469850.169 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469850.169 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469850.169 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469850.169 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469850.170 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469850.172 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469850.177 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469850.191 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469850.204 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469850.204 * [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))
1552469850.205 * * * * [progress]: [ 11 / 22 ] 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))>
1552469850.205 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469850.205 * * [simplify]: iters left: 4 (8 enodes)
1552469850.208 * * [simplify]: iters left: 3 (23 enodes)
1552469850.215 * * [simplify]: iters left: 2 (45 enodes)
1552469850.224 * * [simplify]: iters left: 1 (108 enodes)
1552469850.257 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469850.257 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469850.257 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469850.257 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469850.257 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469850.258 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469850.262 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469850.272 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469850.284 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469850.296 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469850.297 * [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))
1552469850.297 * * * * [progress]: [ 12 / 22 ] 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))>
1552469850.297 * [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)))
1552469850.297 * * [simplify]: iters left: 6 (11 enodes)
1552469850.302 * * [simplify]: iters left: 5 (43 enodes)
1552469850.320 * * [simplify]: iters left: 4 (139 enodes)
1552469850.408 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469850.409 * * [simplify]: Extracting #1: cost 32 inf + 0
1552469850.409 * * [simplify]: Extracting #2: cost 85 inf + 0
1552469850.410 * * [simplify]: Extracting #3: cost 152 inf + 1364
1552469850.412 * * [simplify]: Extracting #4: cost 163 inf + 24483
1552469850.420 * * [simplify]: Extracting #5: cost 71 inf + 172897
1552469850.431 * * [simplify]: Extracting #6: cost 3 inf + 277964
1552469850.442 * * [simplify]: Extracting #7: cost 0 inf + 284573
1552469850.454 * [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))))
1552469850.454 * [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))
1552469850.454 * * * * [progress]: [ 13 / 22 ] 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))))>
1552469850.454 * [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))
1552469850.454 * * [simplify]: iters left: 5 (9 enodes)
1552469850.456 * * [simplify]: iters left: 4 (32 enodes)
1552469850.462 * * [simplify]: iters left: 3 (94 enodes)
1552469850.498 * * [simplify]: iters left: 2 (340 enodes)
1552469850.784 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469850.784 * * [simplify]: Extracting #1: cost 50 inf + 0
1552469850.784 * * [simplify]: Extracting #2: cost 240 inf + 0
1552469850.787 * * [simplify]: Extracting #3: cost 355 inf + 61800
1552469850.801 * * [simplify]: Extracting #4: cost 246 inf + 415499
1552469850.834 * * [simplify]: Extracting #5: cost 58 inf + 816216
1552469850.876 * * [simplify]: Extracting #6: cost 1 inf + 911482
1552469850.919 * * [simplify]: Extracting #7: cost 0 inf + 914765
1552469850.967 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1552469850.967 * [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))))
1552469850.967 * * * * [progress]: [ 14 / 22 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (/.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)))))>
1552469850.967 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469850.967 * * [simplify]: iters left: 4 (8 enodes)
1552469850.969 * * [simplify]: iters left: 3 (23 enodes)
1552469850.973 * * [simplify]: iters left: 2 (45 enodes)
1552469850.980 * * [simplify]: iters left: 1 (108 enodes)
1552469851.007 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469851.007 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469851.007 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469851.007 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469851.008 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469851.008 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469851.010 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469851.015 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469851.021 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469851.029 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469851.029 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (*.p16 a (/.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)))))
1552469851.029 * * * * [progress]: [ 15 / 22 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (/.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)))))>
1552469851.029 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469851.029 * * [simplify]: iters left: 4 (8 enodes)
1552469851.031 * * [simplify]: iters left: 3 (23 enodes)
1552469851.035 * * [simplify]: iters left: 2 (45 enodes)
1552469851.043 * * [simplify]: iters left: 1 (108 enodes)
1552469851.070 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469851.070 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469851.070 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469851.070 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469851.070 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469851.071 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469851.073 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469851.077 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469851.084 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469851.090 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469851.090 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (*.p16 a (/.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)))))
1552469851.090 * * * * [progress]: [ 16 / 22 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (/.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)))))>
1552469851.090 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469851.090 * * [simplify]: iters left: 4 (8 enodes)
1552469851.092 * * [simplify]: iters left: 3 (23 enodes)
1552469851.096 * * [simplify]: iters left: 2 (45 enodes)
1552469851.106 * * [simplify]: iters left: 1 (108 enodes)
1552469851.133 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469851.133 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469851.133 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469851.133 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469851.133 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469851.133 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469851.135 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469851.140 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469851.146 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469851.152 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469851.153 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (*.p16 a (/.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)))))
1552469851.153 * * * * [progress]: [ 17 / 22 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (/.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)))))>
1552469851.153 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469851.153 * * [simplify]: iters left: 4 (8 enodes)
1552469851.155 * * [simplify]: iters left: 3 (23 enodes)
1552469851.158 * * [simplify]: iters left: 2 (45 enodes)
1552469851.166 * * [simplify]: iters left: 1 (108 enodes)
1552469851.195 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469851.195 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469851.195 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469851.195 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469851.195 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469851.195 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469851.197 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469851.202 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469851.208 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469851.215 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469851.215 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (*.p16 a (/.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)))))
1552469851.215 * * * * [progress]: [ 18 / 22 ] 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 (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 a (*.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))))))>
1552469851.215 * [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)))
1552469851.215 * * [simplify]: iters left: 6 (11 enodes)
1552469851.218 * * [simplify]: iters left: 5 (43 enodes)
1552469851.227 * * [simplify]: iters left: 4 (139 enodes)
1552469851.273 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469851.273 * * [simplify]: Extracting #1: cost 32 inf + 0
1552469851.273 * * [simplify]: Extracting #2: cost 85 inf + 0
1552469851.274 * * [simplify]: Extracting #3: cost 152 inf + 1364
1552469851.275 * * [simplify]: Extracting #4: cost 163 inf + 24483
1552469851.280 * * [simplify]: Extracting #5: cost 71 inf + 172897
1552469851.290 * * [simplify]: Extracting #6: cost 3 inf + 277964
1552469851.301 * * [simplify]: Extracting #7: cost 0 inf + 284573
1552469851.312 * [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))))
1552469851.312 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.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 a (*.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))))))
1552469851.313 * * * * [progress]: [ 19 / 22 ] 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))>
1552469851.313 * * * * [progress]: [ 20 / 22 ] 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))>
1552469851.313 * * * * [progress]: [ 21 / 22 ] 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))>
1552469851.313 * * * * [progress]: [ 22 / 22 ] 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))>
1552469851.313 * * * [progress]: adding candidates to table
1552469852.305 * * [progress]: iteration 4 / 4
1552469852.305 * * * [progress]: picking best candidate
1552469852.502 * * * * [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))>
1552469852.502 * * * [progress]: localizing error
1552469852.670 * * * [progress]: generating rewritten candidates
1552469852.670 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
1552469852.675 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
1552469852.680 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
1552469852.683 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
1552469852.700 * * * [progress]: generating series expansions
1552469852.700 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
1552469852.700 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
1552469852.700 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
1552469852.701 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
1552469852.701 * * * [progress]: simplifying candidates
1552469852.701 * * * * [progress]: [ 1 / 11 ] 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))>
1552469852.701 * * * * [progress]: [ 2 / 11 ] 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))>
1552469852.701 * * * * [progress]: [ 3 / 11 ] 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))>
1552469852.701 * * * * [progress]: [ 4 / 11 ] 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))>
1552469852.701 * * * * [progress]: [ 5 / 11 ] 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))>
1552469852.701 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469852.701 * * [simplify]: iters left: 4 (8 enodes)
1552469852.705 * * [simplify]: iters left: 3 (23 enodes)
1552469852.712 * * [simplify]: iters left: 2 (45 enodes)
1552469852.730 * * [simplify]: iters left: 1 (108 enodes)
1552469852.779 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469852.779 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469852.779 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469852.779 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469852.780 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469852.780 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469852.782 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469852.787 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469852.793 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469852.800 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469852.800 * [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))
1552469852.800 * * * * [progress]: [ 6 / 11 ] 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))>
1552469852.800 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469852.800 * * [simplify]: iters left: 4 (8 enodes)
1552469852.802 * * [simplify]: iters left: 3 (28 enodes)
1552469852.807 * * [simplify]: iters left: 2 (59 enodes)
1552469852.818 * * [simplify]: iters left: 1 (178 enodes)
1552469852.872 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469852.873 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469852.873 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469852.873 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469852.874 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469852.878 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469852.899 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469852.926 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469852.940 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469852.957 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469852.957 * [simplify]: Simplified (2 1 1) to (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) 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))
1552469852.957 * * * * [progress]: [ 7 / 11 ] 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))>
1552469852.957 * [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)))
1552469852.957 * * [simplify]: iters left: 6 (11 enodes)
1552469852.960 * * [simplify]: iters left: 5 (35 enodes)
1552469852.967 * * [simplify]: iters left: 4 (111 enodes)
1552469852.996 * * [simplify]: iters left: 3 (448 enodes)
1552469853.330 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469853.330 * * [simplify]: Extracting #1: cost 64 inf + 0
1552469853.332 * * [simplify]: Extracting #2: cost 370 inf + 0
1552469853.336 * * [simplify]: Extracting #3: cost 522 inf + 6695
1552469853.348 * * [simplify]: Extracting #4: cost 536 inf + 237314
1552469853.414 * * [simplify]: Extracting #5: cost 132 inf + 950329
1552469853.498 * * [simplify]: Extracting #6: cost 26 inf + 1188087
1552469853.600 * * [simplify]: Extracting #7: cost 0 inf + 1213652
1552469853.712 * * [simplify]: Extracting #8: cost 0 inf + 1213496
1552469853.797 * [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)))))
1552469853.798 * [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))
1552469853.798 * * * * [progress]: [ 8 / 11 ] 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))>
1552469853.798 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469853.798 * * [simplify]: iters left: 4 (8 enodes)
1552469853.800 * * [simplify]: iters left: 3 (23 enodes)
1552469853.804 * * [simplify]: iters left: 2 (45 enodes)
1552469853.813 * * [simplify]: iters left: 1 (108 enodes)
1552469853.856 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469853.856 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469853.856 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469853.856 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469853.856 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469853.857 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469853.858 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469853.864 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469853.870 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469853.878 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469853.878 * [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))
1552469853.879 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469853.879 * * [simplify]: iters left: 4 (8 enodes)
1552469853.881 * * [simplify]: iters left: 3 (28 enodes)
1552469853.885 * * [simplify]: iters left: 2 (59 enodes)
1552469853.897 * * [simplify]: iters left: 1 (178 enodes)
1552469853.967 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469853.967 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469853.967 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469853.968 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469853.970 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469853.977 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469853.999 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469854.027 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469854.056 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469854.071 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469854.071 * [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))
1552469854.071 * * * * [progress]: [ 9 / 11 ] 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))>
1552469854.071 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469854.071 * * [simplify]: iters left: 4 (8 enodes)
1552469854.073 * * [simplify]: iters left: 3 (23 enodes)
1552469854.077 * * [simplify]: iters left: 2 (45 enodes)
1552469854.084 * * [simplify]: iters left: 1 (108 enodes)
1552469854.111 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469854.111 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469854.111 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469854.111 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469854.111 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469854.112 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469854.114 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469854.119 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469854.125 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469854.133 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469854.133 * [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))
1552469854.133 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469854.133 * * [simplify]: iters left: 4 (8 enodes)
1552469854.135 * * [simplify]: iters left: 3 (28 enodes)
1552469854.139 * * [simplify]: iters left: 2 (59 enodes)
1552469854.151 * * [simplify]: iters left: 1 (178 enodes)
1552469854.205 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469854.205 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469854.205 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469854.205 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469854.206 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469854.211 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469854.222 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469854.236 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469854.250 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469854.265 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469854.265 * [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))
1552469854.265 * * * * [progress]: [ 10 / 11 ] 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))>
1552469854.265 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469854.265 * * [simplify]: iters left: 4 (8 enodes)
1552469854.267 * * [simplify]: iters left: 3 (23 enodes)
1552469854.270 * * [simplify]: iters left: 2 (45 enodes)
1552469854.280 * * [simplify]: iters left: 1 (108 enodes)
1552469854.316 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469854.316 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469854.316 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469854.316 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469854.316 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469854.317 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469854.320 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469854.330 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469854.342 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469854.355 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469854.355 * [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))
1552469854.355 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469854.355 * * [simplify]: iters left: 4 (8 enodes)
1552469854.359 * * [simplify]: iters left: 3 (28 enodes)
1552469854.368 * * [simplify]: iters left: 2 (59 enodes)
1552469854.390 * * [simplify]: iters left: 1 (178 enodes)
1552469854.498 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469854.498 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469854.499 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469854.499 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469854.501 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469854.508 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469854.530 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469854.559 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469854.588 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469854.618 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469854.618 * [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))
1552469854.618 * * * * [progress]: [ 11 / 11 ] 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))>
1552469854.618 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469854.619 * * [simplify]: iters left: 4 (8 enodes)
1552469854.622 * * [simplify]: iters left: 3 (23 enodes)
1552469854.630 * * [simplify]: iters left: 2 (45 enodes)
1552469854.646 * * [simplify]: iters left: 1 (108 enodes)
1552469854.699 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469854.699 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469854.699 * * [simplify]: Extracting #2: cost 3 inf + 1
1552469854.700 * * [simplify]: Extracting #3: cost 17 inf + 1
1552469854.700 * * [simplify]: Extracting #4: cost 55 inf + 322
1552469854.700 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552469854.702 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552469854.707 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552469854.714 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552469854.721 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552469854.721 * [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))
1552469854.721 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552469854.721 * * [simplify]: iters left: 4 (8 enodes)
1552469854.723 * * [simplify]: iters left: 3 (28 enodes)
1552469854.729 * * [simplify]: iters left: 2 (59 enodes)
1552469854.741 * * [simplify]: iters left: 1 (178 enodes)
1552469854.794 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469854.794 * * [simplify]: Extracting #1: cost 12 inf + 0
1552469854.795 * * [simplify]: Extracting #2: cost 64 inf + 1
1552469854.795 * * [simplify]: Extracting #3: cost 140 inf + 403
1552469854.796 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552469854.799 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552469854.810 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552469854.823 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552469854.841 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552469854.860 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552469854.860 * [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))
1552469854.860 * * * [progress]: adding candidates to table
1552469855.150 * [progress]: [Phase 3 of 3] Extracting.
1552469855.150 * * [regime]: Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.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 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (*.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 a (*.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))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (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 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 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (/.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)))))> #<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))>)
1552469855.155 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
1552469855.156 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.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 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (*.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 a (*.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))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (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 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 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (/.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)))))> #<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))>)
1552469855.665 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.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 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (*.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 a (*.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))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (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 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 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (/.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)))))> #<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))>)
1552469856.126 * * * * [regimes]: Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.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 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (*.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 a (*.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))))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (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 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 b_2 b_2) (*.p16 c a))) b_2) (*.p16 a (/.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)))))> #<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))>)
1552469856.436 * * * [regime]: Found split indices: #<option (#s(si 3 256))>
1552469856.436 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552469856.437 * * [simplify]: iters left: 5 (9 enodes)
1552469856.437 * * [simplify]: Extracting #0: cost 1 inf + 0
1552469856.437 * * [simplify]: Extracting #1: cost 3 inf + 0
1552469856.437 * * [simplify]: Extracting #2: cost 4 inf + 1
1552469856.437 * * [simplify]: Extracting #3: cost 4 inf + 2
1552469856.437 * * [simplify]: Extracting #4: cost 6 inf + 2
1552469856.437 * * [simplify]: Extracting #5: cost 6 inf + 323
1552469856.437 * * [simplify]: Extracting #6: cost 0 inf + 4258
1552469856.437 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552469856.437 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1552469856.499 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
1552469856.500 * * * * [points]: Setting MPFR precision to 64
1552469856.501 * * * * [points]: Setting MPFR precision to 320
1552469856.502 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
1552469856.503 * * * * [points]: Setting MPFR precision to 64
1552469856.505 * * * * [points]: Setting MPFR precision to 320
1552469856.508 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
1552469856.509 * * * * [points]: Setting MPFR precision to 64
1552469856.513 * * * * [points]: Setting MPFR precision to 320
1552469856.519 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
1552469856.520 * * * * [points]: Setting MPFR precision to 64
1552469856.527 * * * * [points]: Setting MPFR precision to 320
1552469856.537 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
1552469856.538 * * * * [points]: Setting MPFR precision to 64
1552469856.554 * * * * [points]: Setting MPFR precision to 320
1552469856.572 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
1552469856.574 * * * * [points]: Setting MPFR precision to 64
1552469856.604 * * * * [points]: Setting MPFR precision to 320
1552469856.676 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
1552469856.678 * * * * [points]: Setting MPFR precision to 64
1552469856.751 * * * * [points]: Setting MPFR precision to 320
1552469856.951 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
1552469856.953 * * * * [points]: Setting MPFR precision to 64
1552469857.163 * * * * [points]: Setting MPFR precision to 320
1552469857.357 * * * * [points]: Computing exacts for 8000 points
1552469857.668 * * * * [points]: Setting MPFR precision to 64
1552469858.541 * * * * [points]: Setting MPFR precision to 320
1552469859.747 * * * * [points]: Filtering points with unrepresentable outputs
1552469860.425 * * * * [points]: Sampling 2004 additional inputs, on iter 1 have 5996 / 8000
1552469860.442 * * * * [points]: Computing exacts on every 125 of 2004 points to ramp up precision
1552469860.444 * * * * [points]: Setting MPFR precision to 64
1552469860.446 * * * * [points]: Setting MPFR precision to 320
1552469860.448 * * * * [points]: Computing exacts on every 62 of 2004 points to ramp up precision
1552469860.450 * * * * [points]: Setting MPFR precision to 64
1552469860.454 * * * * [points]: Setting MPFR precision to 320
1552469860.458 * * * * [points]: Computing exacts on every 31 of 2004 points to ramp up precision
1552469860.460 * * * * [points]: Setting MPFR precision to 64
1552469860.467 * * * * [points]: Setting MPFR precision to 320
1552469860.500 * * * * [points]: Computing exacts on every 15 of 2004 points to ramp up precision
1552469860.502 * * * * [points]: Setting MPFR precision to 64
1552469860.515 * * * * [points]: Setting MPFR precision to 320
1552469860.525 * * * * [points]: Computing exacts on every 7 of 2004 points to ramp up precision
1552469860.526 * * * * [points]: Setting MPFR precision to 64
1552469860.541 * * * * [points]: Setting MPFR precision to 320
1552469860.562 * * * * [points]: Computing exacts on every 3 of 2004 points to ramp up precision
1552469860.563 * * * * [points]: Setting MPFR precision to 64
1552469860.593 * * * * [points]: Setting MPFR precision to 320
1552469860.687 * * * * [points]: Computing exacts for 2004 points
1552469860.689 * * * * [points]: Setting MPFR precision to 64
1552469860.971 * * * * [points]: Setting MPFR precision to 320
1552469861.274 * * * * [points]: Filtering points with unrepresentable outputs
1552469861.878 * * * * [points]: Sampling 463 additional inputs, on iter 2 have 7537 / 8000
1552469861.880 * * * * [points]: Computing exacts on every 28 of 463 points to ramp up precision
1552469861.881 * * * * [points]: Setting MPFR precision to 64
1552469861.882 * * * * [points]: Setting MPFR precision to 320
1552469861.883 * * * * [points]: Computing exacts on every 14 of 463 points to ramp up precision
1552469861.884 * * * * [points]: Setting MPFR precision to 64
1552469861.886 * * * * [points]: Setting MPFR precision to 320
1552469861.888 * * * * [points]: Computing exacts on every 7 of 463 points to ramp up precision
1552469861.890 * * * * [points]: Setting MPFR precision to 64
1552469861.894 * * * * [points]: Setting MPFR precision to 320
1552469861.898 * * * * [points]: Computing exacts on every 3 of 463 points to ramp up precision
1552469861.899 * * * * [points]: Setting MPFR precision to 64
1552469861.906 * * * * [points]: Setting MPFR precision to 320
1552469861.916 * * * * [points]: Computing exacts for 463 points
1552469861.917 * * * * [points]: Setting MPFR precision to 64
1552469861.961 * * * * [points]: Setting MPFR precision to 320
1552469862.018 * * * * [points]: Filtering points with unrepresentable outputs
1552469862.046 * * * * [points]: Sampling 109 additional inputs, on iter 3 have 7891 / 8000
1552469862.046 * * * * [points]: Computing exacts on every 6 of 109 points to ramp up precision
1552469862.047 * * * * [points]: Setting MPFR precision to 64
1552469862.048 * * * * [points]: Setting MPFR precision to 320
1552469862.049 * * * * [points]: Computing exacts on every 3 of 109 points to ramp up precision
1552469862.050 * * * * [points]: Setting MPFR precision to 64
1552469862.052 * * * * [points]: Setting MPFR precision to 320
1552469862.055 * * * * [points]: Computing exacts for 109 points
1552469862.056 * * * * [points]: Setting MPFR precision to 64
1552469862.062 * * * * [points]: Setting MPFR precision to 320
1552469862.074 * * * * [points]: Filtering points with unrepresentable outputs
1552469862.084 * * * * [points]: Sampling 38 additional inputs, on iter 4 have 7962 / 8000
1552469862.084 * * * * [points]: Computing exacts on every 2 of 38 points to ramp up precision
1552469862.086 * * * * [points]: Setting MPFR precision to 64
1552469862.087 * * * * [points]: Setting MPFR precision to 320
1552469862.089 * * * * [points]: Computing exacts for 38 points
1552469862.091 * * * * [points]: Setting MPFR precision to 64
1552469862.095 * * * * [points]: Setting MPFR precision to 320
1552469862.100 * * * * [points]: Filtering points with unrepresentable outputs
1552469862.104 * * * * [points]: Sampling 9 additional inputs, on iter 5 have 7991 / 8000
1552469862.104 * * * * [points]: Computing exacts for 9 points
1552469862.106 * * * * [points]: Setting MPFR precision to 64
1552469862.107 * * * * [points]: Setting MPFR precision to 320
1552469862.108 * * * * [points]: Filtering points with unrepresentable outputs
1552469862.109 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 7998 / 8000
1552469862.109 * * * * [points]: Computing exacts for 4 points
1552469862.111 * * * * [points]: Setting MPFR precision to 64
1552469862.111 * * * * [points]: Setting MPFR precision to 320
1552469862.112 * * * * [points]: Filtering points with unrepresentable outputs
1552469862.112 * * * * [points]: Sampled 8001 points with exact outputs
1552469865.504 * [regime-testing]: Baseline error score: 64.0
1552469865.508 * [regime-testing]: Oracle error score: 64.0
1552469865.516 * [regime-testing]: End program error score: 2.29992961421634