1554043184.128 * [progress]: [Phase 1 of 3] Setting up.
1554043184.130 * * * [progress]: [1/2] Preparing points
1554043184.131 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
1554043184.140 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
1554043184.874 * * * * [points]: Setting MPFR precision to 64
1554043184.879 * * * * [points]: Setting MPFR precision to 320
1554043184.882 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
1554043184.885 * * * * [points]: Setting MPFR precision to 64
1554043184.888 * * * * [points]: Setting MPFR precision to 320
1554043184.893 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
1554043184.895 * * * * [points]: Setting MPFR precision to 64
1554043184.901 * * * * [points]: Setting MPFR precision to 320
1554043184.909 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
1554043184.912 * * * * [points]: Setting MPFR precision to 64
1554043184.922 * * * * [points]: Setting MPFR precision to 320
1554043184.930 * * * * [points]: Computing exacts for 256 points
1554043184.932 * * * * [points]: Setting MPFR precision to 64
1554043184.961 * * * * [points]: Setting MPFR precision to 320
1554043184.983 * * * * [points]: Filtering points with unrepresentable outputs
1554043184.998 * * * * [points]: Sampling 65 additional inputs, on iter 1 have 191 / 256
1554043184.998 * * * * [points]: Computing exacts on every 4 of 65 points to ramp up precision
1554043185.000 * * * * [points]: Setting MPFR precision to 64
1554043185.001 * * * * [points]: Setting MPFR precision to 320
1554043185.002 * * * * [points]: Computing exacts on every 2 of 65 points to ramp up precision
1554043185.003 * * * * [points]: Setting MPFR precision to 64
1554043185.036 * * * * [points]: Setting MPFR precision to 320
1554043185.038 * * * * [points]: Computing exacts for 65 points
1554043185.039 * * * * [points]: Setting MPFR precision to 64
1554043185.043 * * * * [points]: Setting MPFR precision to 320
1554043185.050 * * * * [points]: Filtering points with unrepresentable outputs
1554043185.053 * * * * [points]: Sampling 22 additional inputs, on iter 2 have 234 / 256
1554043185.053 * * * * [points]: Computing exacts for 22 points
1554043185.054 * * * * [points]: Setting MPFR precision to 64
1554043185.055 * * * * [points]: Setting MPFR precision to 320
1554043185.057 * * * * [points]: Filtering points with unrepresentable outputs
1554043185.058 * * * * [points]: Sampling 4 additional inputs, on iter 3 have 252 / 256
1554043185.058 * * * * [points]: Computing exacts for 4 points
1554043185.060 * * * * [points]: Setting MPFR precision to 64
1554043185.060 * * * * [points]: Setting MPFR precision to 320
1554043185.061 * * * * [points]: Filtering points with unrepresentable outputs
1554043185.061 * * * * [points]: Sampling 4 additional inputs, on iter 4 have 254 / 256
1554043185.061 * * * * [points]: Computing exacts for 4 points
1554043185.062 * * * * [points]: Setting MPFR precision to 64
1554043185.062 * * * * [points]: Setting MPFR precision to 320
1554043185.063 * * * * [points]: Filtering points with unrepresentable outputs
1554043185.063 * * * * [points]: Sampled 257 points with exact outputs
1554043185.063 * * * [progress]: [2/2] Setting up program.
1554043185.083 * [progress]: [Phase 2 of 3] Improving.
1554043185.083 * * * * [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))>
1554043185.084 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1554043185.086 * * [simplify]: iters left: 5 (10 enodes)
1554043185.091 * * [simplify]: iters left: 4 (25 enodes)
1554043185.095 * * [simplify]: iters left: 3 (48 enodes)
1554043185.104 * * [simplify]: iters left: 2 (111 enodes)
1554043185.149 * * [simplify]: iters left: 1 (392 enodes)
1554043185.339 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043185.339 * * [simplify]: Extracting #1: cost 10 inf + 0
1554043185.340 * * [simplify]: Extracting #2: cost 35 inf + 1
1554043185.340 * * [simplify]: Extracting #3: cost 91 inf + 405
1554043185.341 * * [simplify]: Extracting #4: cost 331 inf + 2291
1554043185.344 * * [simplify]: Extracting #5: cost 455 inf + 80323
1554043185.363 * * [simplify]: Extracting #6: cost 250 inf + 579968
1554043185.402 * * [simplify]: Extracting #7: cost 28 inf + 1003440
1554043185.450 * * [simplify]: Extracting #8: cost 0 inf + 1069311
1554043185.494 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1554043185.494 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
1554043185.533 * * [progress]: iteration 1 / 4
1554043185.533 * * * [progress]: picking best candidate
1554043185.547 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1554043185.547 * * * [progress]: localizing error
1554043185.722 * * * [progress]: generating rewritten candidates
1554043185.722 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1554043185.725 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1)
1554043185.725 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1554043185.728 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1554043185.731 * * * [progress]: generating series expansions
1554043185.732 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1554043185.732 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1)
1554043185.732 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1554043185.732 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1554043185.732 * * * [progress]: simplifying candidates
1554043185.732 * * * * [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))>
1554043185.732 * * * * [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))>
1554043185.732 * * * * [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))))>
1554043185.732 * [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))
1554043185.732 * * [simplify]: iters left: 5 (9 enodes)
1554043185.734 * * [simplify]: iters left: 4 (32 enodes)
1554043185.740 * * [simplify]: iters left: 3 (94 enodes)
1554043185.771 * * [simplify]: iters left: 2 (340 enodes)
1554043185.926 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043185.926 * * [simplify]: Extracting #1: cost 50 inf + 0
1554043185.927 * * [simplify]: Extracting #2: cost 240 inf + 0
1554043185.929 * * [simplify]: Extracting #3: cost 355 inf + 61800
1554043185.944 * * [simplify]: Extracting #4: cost 246 inf + 415499
1554043185.980 * * [simplify]: Extracting #5: cost 58 inf + 816216
1554043186.033 * * [simplify]: Extracting #6: cost 1 inf + 911482
1554043186.112 * * [simplify]: Extracting #7: cost 0 inf + 914765
1554043186.191 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1554043186.191 * [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))))
1554043186.191 * * * * [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))>
1554043186.191 * * * * [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))>
1554043186.191 * * * * [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))>
1554043186.191 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1554043186.191 * * [simplify]: iters left: 5 (9 enodes)
1554043186.195 * * [simplify]: iters left: 4 (29 enodes)
1554043186.206 * * [simplify]: iters left: 3 (62 enodes)
1554043186.229 * * [simplify]: iters left: 2 (199 enodes)
1554043186.305 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043186.305 * * [simplify]: Extracting #1: cost 20 inf + 0
1554043186.305 * * [simplify]: Extracting #2: cost 94 inf + 1
1554043186.306 * * [simplify]: Extracting #3: cost 162 inf + 1046
1554043186.307 * * [simplify]: Extracting #4: cost 208 inf + 17818
1554043186.310 * * [simplify]: Extracting #5: cost 164 inf + 103714
1554043186.322 * * [simplify]: Extracting #6: cost 47 inf + 336456
1554043186.339 * * [simplify]: Extracting #7: cost 0 inf + 409081
1554043186.355 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1554043186.355 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1554043186.355 * * * * [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))>
1554043186.355 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1554043186.356 * * [simplify]: iters left: 5 (9 enodes)
1554043186.357 * * [simplify]: iters left: 4 (29 enodes)
1554043186.362 * * [simplify]: iters left: 3 (62 enodes)
1554043186.373 * * [simplify]: iters left: 2 (199 enodes)
1554043186.465 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043186.465 * * [simplify]: Extracting #1: cost 20 inf + 0
1554043186.465 * * [simplify]: Extracting #2: cost 94 inf + 1
1554043186.466 * * [simplify]: Extracting #3: cost 162 inf + 1046
1554043186.468 * * [simplify]: Extracting #4: cost 208 inf + 17818
1554043186.475 * * [simplify]: Extracting #5: cost 164 inf + 103714
1554043186.498 * * [simplify]: Extracting #6: cost 47 inf + 336456
1554043186.528 * * [simplify]: Extracting #7: cost 0 inf + 409081
1554043186.561 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1554043186.561 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1554043186.561 * * * * [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))>
1554043186.561 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1554043186.561 * * [simplify]: iters left: 5 (9 enodes)
1554043186.563 * * [simplify]: iters left: 4 (29 enodes)
1554043186.568 * * [simplify]: iters left: 3 (62 enodes)
1554043186.580 * * [simplify]: iters left: 2 (199 enodes)
1554043186.655 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043186.655 * * [simplify]: Extracting #1: cost 20 inf + 0
1554043186.656 * * [simplify]: Extracting #2: cost 94 inf + 1
1554043186.657 * * [simplify]: Extracting #3: cost 162 inf + 1046
1554043186.659 * * [simplify]: Extracting #4: cost 208 inf + 17818
1554043186.666 * * [simplify]: Extracting #5: cost 164 inf + 103714
1554043186.688 * * [simplify]: Extracting #6: cost 47 inf + 336456
1554043186.708 * * [simplify]: Extracting #7: cost 0 inf + 409081
1554043186.724 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1554043186.724 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1554043186.724 * * * * [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))>
1554043186.724 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1554043186.724 * * [simplify]: iters left: 5 (9 enodes)
1554043186.726 * * [simplify]: iters left: 4 (29 enodes)
1554043186.732 * * [simplify]: iters left: 3 (62 enodes)
1554043186.759 * * [simplify]: iters left: 2 (199 enodes)
1554043186.825 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043186.825 * * [simplify]: Extracting #1: cost 20 inf + 0
1554043186.826 * * [simplify]: Extracting #2: cost 94 inf + 1
1554043186.826 * * [simplify]: Extracting #3: cost 162 inf + 1046
1554043186.827 * * [simplify]: Extracting #4: cost 208 inf + 17818
1554043186.835 * * [simplify]: Extracting #5: cost 164 inf + 103714
1554043186.858 * * [simplify]: Extracting #6: cost 47 inf + 336456
1554043186.889 * * [simplify]: Extracting #7: cost 0 inf + 409081
1554043186.906 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1554043186.906 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1554043186.906 * * * [progress]: adding candidates to table
1554043187.301 * * [progress]: iteration 2 / 4
1554043187.301 * * * [progress]: picking best candidate
1554043187.379 * * * * [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))>
1554043187.379 * * * [progress]: localizing error
1554043187.678 * * * [progress]: generating rewritten candidates
1554043187.678 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
1554043187.686 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
1554043187.688 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
1554043187.688 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
1554043187.691 * * * [progress]: generating series expansions
1554043187.691 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
1554043187.691 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
1554043187.691 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
1554043187.691 * * * * [progress]: [ 4 / 4 ] generating series at (2)
1554043187.691 * * * [progress]: simplifying candidates
1554043187.691 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) b_2) a))>
1554043187.691 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1554043187.691 * * [simplify]: iters left: 2 (6 enodes)
1554043187.693 * * [simplify]: iters left: 1 (14 enodes)
1554043187.695 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043187.695 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043187.695 * * [simplify]: Extracting #2: cost 6 inf + 0
1554043187.695 * * [simplify]: Extracting #3: cost 2 inf + 325
1554043187.695 * * [simplify]: Extracting #4: cost 0 inf + 1329
1554043187.695 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1554043187.695 * [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))
1554043187.695 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 c a) (*.p16 c a)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>
1554043187.695 * [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))))
1554043187.695 * * [simplify]: iters left: 4 (10 enodes)
1554043187.698 * * [simplify]: iters left: 3 (43 enodes)
1554043187.706 * * [simplify]: iters left: 2 (121 enodes)
1554043187.735 * * [simplify]: iters left: 1 (429 enodes)
1554043187.982 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043187.982 * * [simplify]: Extracting #1: cost 46 inf + 0
1554043187.983 * * [simplify]: Extracting #2: cost 270 inf + 0
1554043187.988 * * [simplify]: Extracting #3: cost 354 inf + 59003
1554043188.013 * * [simplify]: Extracting #4: cost 345 inf + 369227
1554043188.092 * * [simplify]: Extracting #5: cost 22 inf + 1102360
1554043188.184 * * [simplify]: Extracting #6: cost 1 inf + 1150488
1554043188.246 * * [simplify]: Extracting #7: cost 0 inf + 1155051
1554043188.350 * [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))))
1554043188.350 * [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))
1554043188.350 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 b_2)) a))>
1554043188.351 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2)) a))>
1554043188.351 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2))))>
1554043188.351 * [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))
1554043188.351 * * [simplify]: iters left: 6 (13 enodes)
1554043188.357 * * [simplify]: iters left: 5 (47 enodes)
1554043188.374 * * [simplify]: iters left: 4 (118 enodes)
1554043188.431 * * [simplify]: iters left: 3 (482 enodes)
1554043188.914 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043188.914 * * [simplify]: Extracting #1: cost 39 inf + 0
1554043188.914 * * [simplify]: Extracting #2: cost 255 inf + 0
1554043188.916 * * [simplify]: Extracting #3: cost 532 inf + 10719
1554043188.928 * * [simplify]: Extracting #4: cost 679 inf + 310118
1554043189.022 * * [simplify]: Extracting #5: cost 214 inf + 1310578
1554043189.174 * * [simplify]: Extracting #6: cost 5 inf + 1763746
1554043189.260 * * [simplify]: Extracting #7: cost 0 inf + 1773035
1554043189.389 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
1554043189.389 * [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))))
1554043189.389 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
1554043189.389 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
1554043189.389 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
1554043189.389 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))>
1554043189.389 * * * [progress]: adding candidates to table
1554043189.704 * * [progress]: iteration 3 / 4
1554043189.704 * * * [progress]: picking best candidate
1554043189.845 * * * * [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))>
1554043189.845 * * * [progress]: localizing error
1554043190.272 * * * [progress]: generating rewritten candidates
1554043190.272 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
1554043190.275 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1554043190.277 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
1554043190.288 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
1554043190.289 * * * [progress]: generating series expansions
1554043190.289 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
1554043190.289 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1554043190.289 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
1554043190.289 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
1554043190.289 * * * [progress]: simplifying candidates
1554043190.289 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043190.290 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043190.290 * * [simplify]: iters left: 4 (8 enodes)
1554043190.291 * * [simplify]: iters left: 3 (23 enodes)
1554043190.295 * * [simplify]: iters left: 2 (45 enodes)
1554043190.302 * * [simplify]: iters left: 1 (108 enodes)
1554043190.330 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043190.330 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043190.330 * * [simplify]: Extracting #2: cost 3 inf + 1
1554043190.330 * * [simplify]: Extracting #3: cost 17 inf + 1
1554043190.330 * * [simplify]: Extracting #4: cost 55 inf + 322
1554043190.330 * * [simplify]: Extracting #5: cost 80 inf + 11197
1554043190.332 * * [simplify]: Extracting #6: cost 84 inf + 56173
1554043190.337 * * [simplify]: Extracting #7: cost 7 inf + 177856
1554043190.350 * * [simplify]: Extracting #8: cost 0 inf + 193436
1554043190.362 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554043190.362 * [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))
1554043190.363 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043190.363 * * [simplify]: iters left: 4 (8 enodes)
1554043190.366 * * [simplify]: iters left: 3 (28 enodes)
1554043190.376 * * [simplify]: iters left: 2 (59 enodes)
1554043190.400 * * [simplify]: iters left: 1 (178 enodes)
1554043190.478 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043190.478 * * [simplify]: Extracting #1: cost 12 inf + 0
1554043190.478 * * [simplify]: Extracting #2: cost 64 inf + 1
1554043190.478 * * [simplify]: Extracting #3: cost 140 inf + 403
1554043190.479 * * [simplify]: Extracting #4: cost 189 inf + 12881
1554043190.485 * * [simplify]: Extracting #5: cost 149 inf + 112868
1554043190.495 * * [simplify]: Extracting #6: cost 32 inf + 315911
1554043190.511 * * [simplify]: Extracting #7: cost 1 inf + 362422
1554043190.524 * * [simplify]: Extracting #8: cost 0 inf + 365106
1554043190.538 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1554043190.538 * [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))
1554043190.538 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (neg.p16 (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043190.538 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043190.538 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
1554043190.538 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
1554043190.539 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043190.539 * * [simplify]: iters left: 4 (8 enodes)
1554043190.540 * * [simplify]: iters left: 3 (23 enodes)
1554043190.544 * * [simplify]: iters left: 2 (45 enodes)
1554043190.552 * * [simplify]: iters left: 1 (108 enodes)
1554043190.593 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043190.594 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043190.594 * * [simplify]: Extracting #2: cost 3 inf + 1
1554043190.594 * * [simplify]: Extracting #3: cost 17 inf + 1
1554043190.594 * * [simplify]: Extracting #4: cost 55 inf + 322
1554043190.594 * * [simplify]: Extracting #5: cost 80 inf + 11197
1554043190.596 * * [simplify]: Extracting #6: cost 84 inf + 56173
1554043190.601 * * [simplify]: Extracting #7: cost 7 inf + 177856
1554043190.607 * * [simplify]: Extracting #8: cost 0 inf + 193436
1554043190.613 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554043190.613 * [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))
1554043190.613 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))>
1554043190.614 * [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)))
1554043190.614 * * [simplify]: iters left: 6 (11 enodes)
1554043190.616 * * [simplify]: iters left: 5 (43 enodes)
1554043190.624 * * [simplify]: iters left: 4 (139 enodes)
1554043190.669 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043190.669 * * [simplify]: Extracting #1: cost 32 inf + 0
1554043190.670 * * [simplify]: Extracting #2: cost 85 inf + 0
1554043190.670 * * [simplify]: Extracting #3: cost 152 inf + 1364
1554043190.671 * * [simplify]: Extracting #4: cost 163 inf + 24483
1554043190.676 * * [simplify]: Extracting #5: cost 71 inf + 172897
1554043190.686 * * [simplify]: Extracting #6: cost 3 inf + 277964
1554043190.697 * * [simplify]: Extracting #7: cost 0 inf + 284573
1554043190.708 * [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))))
1554043190.709 * [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))
1554043190.709 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043190.709 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043190.709 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043190.709 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043190.709 * * * [progress]: adding candidates to table
1554043191.016 * * [progress]: iteration 4 / 4
1554043191.016 * * * [progress]: picking best candidate
1554043191.109 * * * * [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))>
1554043191.109 * * * [progress]: localizing error
1554043191.478 * * * [progress]: generating rewritten candidates
1554043191.478 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2)
1554043191.482 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1554043191.486 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
1554043191.491 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
1554043191.513 * * * [progress]: generating series expansions
1554043191.513 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2)
1554043191.513 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1554043191.513 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
1554043191.513 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
1554043191.513 * * * [progress]: simplifying candidates
1554043191.513 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (neg.p16 b_2))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043191.513 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (-.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))>
1554043191.513 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) a))>
1554043191.513 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043191.513 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
1554043191.514 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043191.514 * * [simplify]: iters left: 4 (8 enodes)
1554043191.517 * * [simplify]: iters left: 3 (23 enodes)
1554043191.524 * * [simplify]: iters left: 2 (45 enodes)
1554043191.540 * * [simplify]: iters left: 1 (108 enodes)
1554043191.595 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043191.595 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043191.595 * * [simplify]: Extracting #2: cost 3 inf + 1
1554043191.595 * * [simplify]: Extracting #3: cost 17 inf + 1
1554043191.595 * * [simplify]: Extracting #4: cost 55 inf + 322
1554043191.596 * * [simplify]: Extracting #5: cost 80 inf + 11197
1554043191.599 * * [simplify]: Extracting #6: cost 84 inf + 56173
1554043191.609 * * [simplify]: Extracting #7: cost 7 inf + 177856
1554043191.622 * * [simplify]: Extracting #8: cost 0 inf + 193436
1554043191.634 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554043191.634 * [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))
1554043191.634 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
1554043191.635 * [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)))
1554043191.635 * * [simplify]: iters left: 6 (11 enodes)
1554043191.639 * * [simplify]: iters left: 5 (35 enodes)
1554043191.654 * * [simplify]: iters left: 4 (111 enodes)
1554043191.709 * * [simplify]: iters left: 3 (448 enodes)
1554043192.090 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043192.090 * * [simplify]: Extracting #1: cost 64 inf + 0
1554043192.091 * * [simplify]: Extracting #2: cost 370 inf + 0
1554043192.093 * * [simplify]: Extracting #3: cost 522 inf + 6695
1554043192.103 * * [simplify]: Extracting #4: cost 536 inf + 237314
1554043192.147 * * [simplify]: Extracting #5: cost 132 inf + 950329
1554043192.200 * * [simplify]: Extracting #6: cost 26 inf + 1188087
1554043192.258 * * [simplify]: Extracting #7: cost 0 inf + 1213652
1554043192.314 * * [simplify]: Extracting #8: cost 0 inf + 1213496
1554043192.425 * [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)))))
1554043192.425 * [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))
1554043192.425 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043192.426 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043192.426 * * [simplify]: iters left: 4 (8 enodes)
1554043192.429 * * [simplify]: iters left: 3 (23 enodes)
1554043192.436 * * [simplify]: iters left: 2 (45 enodes)
1554043192.452 * * [simplify]: iters left: 1 (108 enodes)
1554043192.508 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043192.508 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043192.508 * * [simplify]: Extracting #2: cost 3 inf + 1
1554043192.509 * * [simplify]: Extracting #3: cost 17 inf + 1
1554043192.509 * * [simplify]: Extracting #4: cost 55 inf + 322
1554043192.510 * * [simplify]: Extracting #5: cost 80 inf + 11197
1554043192.514 * * [simplify]: Extracting #6: cost 84 inf + 56173
1554043192.522 * * [simplify]: Extracting #7: cost 7 inf + 177856
1554043192.528 * * [simplify]: Extracting #8: cost 0 inf + 193436
1554043192.539 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554043192.539 * [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))
1554043192.539 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043192.539 * * [simplify]: iters left: 4 (8 enodes)
1554043192.542 * * [simplify]: iters left: 3 (28 enodes)
1554043192.546 * * [simplify]: iters left: 2 (59 enodes)
1554043192.557 * * [simplify]: iters left: 1 (178 enodes)
1554043192.658 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043192.659 * * [simplify]: Extracting #1: cost 12 inf + 0
1554043192.659 * * [simplify]: Extracting #2: cost 64 inf + 1
1554043192.660 * * [simplify]: Extracting #3: cost 140 inf + 403
1554043192.661 * * [simplify]: Extracting #4: cost 189 inf + 12881
1554043192.669 * * [simplify]: Extracting #5: cost 149 inf + 112868
1554043192.688 * * [simplify]: Extracting #6: cost 32 inf + 315911
1554043192.701 * * [simplify]: Extracting #7: cost 1 inf + 362422
1554043192.715 * * [simplify]: Extracting #8: cost 0 inf + 365106
1554043192.733 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1554043192.734 * [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))
1554043192.734 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043192.734 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043192.734 * * [simplify]: iters left: 4 (8 enodes)
1554043192.737 * * [simplify]: iters left: 3 (23 enodes)
1554043192.744 * * [simplify]: iters left: 2 (45 enodes)
1554043192.758 * * [simplify]: iters left: 1 (108 enodes)
1554043192.805 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043192.805 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043192.805 * * [simplify]: Extracting #2: cost 3 inf + 1
1554043192.805 * * [simplify]: Extracting #3: cost 17 inf + 1
1554043192.805 * * [simplify]: Extracting #4: cost 55 inf + 322
1554043192.806 * * [simplify]: Extracting #5: cost 80 inf + 11197
1554043192.809 * * [simplify]: Extracting #6: cost 84 inf + 56173
1554043192.818 * * [simplify]: Extracting #7: cost 7 inf + 177856
1554043192.829 * * [simplify]: Extracting #8: cost 0 inf + 193436
1554043192.841 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554043192.841 * [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))
1554043192.841 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043192.841 * * [simplify]: iters left: 4 (8 enodes)
1554043192.844 * * [simplify]: iters left: 3 (28 enodes)
1554043192.852 * * [simplify]: iters left: 2 (59 enodes)
1554043192.867 * * [simplify]: iters left: 1 (178 enodes)
1554043192.939 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043192.940 * * [simplify]: Extracting #1: cost 12 inf + 0
1554043192.940 * * [simplify]: Extracting #2: cost 64 inf + 1
1554043192.940 * * [simplify]: Extracting #3: cost 140 inf + 403
1554043192.942 * * [simplify]: Extracting #4: cost 189 inf + 12881
1554043192.953 * * [simplify]: Extracting #5: cost 149 inf + 112868
1554043192.976 * * [simplify]: Extracting #6: cost 32 inf + 315911
1554043193.003 * * [simplify]: Extracting #7: cost 1 inf + 362422
1554043193.032 * * [simplify]: Extracting #8: cost 0 inf + 365106
1554043193.060 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1554043193.060 * [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))
1554043193.060 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043193.061 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043193.061 * * [simplify]: iters left: 4 (8 enodes)
1554043193.064 * * [simplify]: iters left: 3 (23 enodes)
1554043193.072 * * [simplify]: iters left: 2 (45 enodes)
1554043193.088 * * [simplify]: iters left: 1 (108 enodes)
1554043193.117 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043193.117 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043193.117 * * [simplify]: Extracting #2: cost 3 inf + 1
1554043193.117 * * [simplify]: Extracting #3: cost 17 inf + 1
1554043193.117 * * [simplify]: Extracting #4: cost 55 inf + 322
1554043193.117 * * [simplify]: Extracting #5: cost 80 inf + 11197
1554043193.119 * * [simplify]: Extracting #6: cost 84 inf + 56173
1554043193.124 * * [simplify]: Extracting #7: cost 7 inf + 177856
1554043193.130 * * [simplify]: Extracting #8: cost 0 inf + 193436
1554043193.137 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554043193.137 * [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))
1554043193.137 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043193.137 * * [simplify]: iters left: 4 (8 enodes)
1554043193.139 * * [simplify]: iters left: 3 (28 enodes)
1554043193.144 * * [simplify]: iters left: 2 (59 enodes)
1554043193.155 * * [simplify]: iters left: 1 (178 enodes)
1554043193.248 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043193.248 * * [simplify]: Extracting #1: cost 12 inf + 0
1554043193.249 * * [simplify]: Extracting #2: cost 64 inf + 1
1554043193.249 * * [simplify]: Extracting #3: cost 140 inf + 403
1554043193.251 * * [simplify]: Extracting #4: cost 189 inf + 12881
1554043193.258 * * [simplify]: Extracting #5: cost 149 inf + 112868
1554043193.281 * * [simplify]: Extracting #6: cost 32 inf + 315911
1554043193.309 * * [simplify]: Extracting #7: cost 1 inf + 362422
1554043193.341 * * [simplify]: Extracting #8: cost 0 inf + 365106
1554043193.368 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1554043193.369 * [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))
1554043193.369 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))>
1554043193.369 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043193.369 * * [simplify]: iters left: 4 (8 enodes)
1554043193.372 * * [simplify]: iters left: 3 (23 enodes)
1554043193.380 * * [simplify]: iters left: 2 (45 enodes)
1554043193.396 * * [simplify]: iters left: 1 (108 enodes)
1554043193.444 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043193.444 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043193.444 * * [simplify]: Extracting #2: cost 3 inf + 1
1554043193.444 * * [simplify]: Extracting #3: cost 17 inf + 1
1554043193.445 * * [simplify]: Extracting #4: cost 55 inf + 322
1554043193.445 * * [simplify]: Extracting #5: cost 80 inf + 11197
1554043193.447 * * [simplify]: Extracting #6: cost 84 inf + 56173
1554043193.453 * * [simplify]: Extracting #7: cost 7 inf + 177856
1554043193.459 * * [simplify]: Extracting #8: cost 0 inf + 193436
1554043193.466 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1554043193.466 * [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))
1554043193.466 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1554043193.466 * * [simplify]: iters left: 4 (8 enodes)
1554043193.468 * * [simplify]: iters left: 3 (28 enodes)
1554043193.472 * * [simplify]: iters left: 2 (59 enodes)
1554043193.493 * * [simplify]: iters left: 1 (178 enodes)
1554043193.595 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043193.595 * * [simplify]: Extracting #1: cost 12 inf + 0
1554043193.595 * * [simplify]: Extracting #2: cost 64 inf + 1
1554043193.595 * * [simplify]: Extracting #3: cost 140 inf + 403
1554043193.596 * * [simplify]: Extracting #4: cost 189 inf + 12881
1554043193.600 * * [simplify]: Extracting #5: cost 149 inf + 112868
1554043193.610 * * [simplify]: Extracting #6: cost 32 inf + 315911
1554043193.624 * * [simplify]: Extracting #7: cost 1 inf + 362422
1554043193.651 * * [simplify]: Extracting #8: cost 0 inf + 365106
1554043193.678 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1554043193.678 * [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))
1554043193.678 * * * [progress]: adding candidates to table
1554043194.128 * [progress]: [Phase 3 of 3] Extracting.
1554043194.129 * * [regime]: Finding splitpoints for: (#<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.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))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 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 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>)
1554043194.137 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
1554043194.138 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.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))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 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 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>)
1554043194.730 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.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))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 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 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>)
1554043195.196 * * * * [regimes]: Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.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))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 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 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (*.p16 a (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 (*.p16 c a) (*.p16 c a)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 c a)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a)))))) b_2) a))>)
1554043195.619 * * * [regime]: Found split indices: #<option (#s(si 4 256))>
1554043195.619 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1554043195.619 * * [simplify]: iters left: 5 (9 enodes)
1554043195.620 * * [simplify]: Extracting #0: cost 1 inf + 0
1554043195.620 * * [simplify]: Extracting #1: cost 3 inf + 0
1554043195.620 * * [simplify]: Extracting #2: cost 4 inf + 1
1554043195.620 * * [simplify]: Extracting #3: cost 4 inf + 2
1554043195.620 * * [simplify]: Extracting #4: cost 6 inf + 2
1554043195.620 * * [simplify]: Extracting #5: cost 6 inf + 323
1554043195.620 * * [simplify]: Extracting #6: cost 0 inf + 4258
1554043195.621 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1554043195.621 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1554043195.683 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
1554043195.685 * * * * [points]: Setting MPFR precision to 64
1554043195.688 * * * * [points]: Setting MPFR precision to 320
1554043195.690 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
1554043195.692 * * * * [points]: Setting MPFR precision to 64
1554043195.694 * * * * [points]: Setting MPFR precision to 320
1554043195.697 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
1554043195.698 * * * * [points]: Setting MPFR precision to 64
1554043195.705 * * * * [points]: Setting MPFR precision to 320
1554043195.714 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
1554043195.716 * * * * [points]: Setting MPFR precision to 64
1554043195.730 * * * * [points]: Setting MPFR precision to 320
1554043195.742 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
1554043195.743 * * * * [points]: Setting MPFR precision to 64
1554043195.758 * * * * [points]: Setting MPFR precision to 320
1554043195.779 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
1554043195.780 * * * * [points]: Setting MPFR precision to 64
1554043195.840 * * * * [points]: Setting MPFR precision to 320
1554043195.912 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
1554043195.913 * * * * [points]: Setting MPFR precision to 64
1554043195.978 * * * * [points]: Setting MPFR precision to 320
1554043196.097 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
1554043196.098 * * * * [points]: Setting MPFR precision to 64
1554043196.255 * * * * [points]: Setting MPFR precision to 320
1554043196.743 * * * * [points]: Computing exacts for 8000 points
1554043196.745 * * * * [points]: Setting MPFR precision to 64
1554043197.703 * * * * [points]: Setting MPFR precision to 320
1554043198.922 * * * * [points]: Filtering points with unrepresentable outputs
1554043199.650 * * * * [points]: Sampling 1975 additional inputs, on iter 1 have 6025 / 8000
1554043199.666 * * * * [points]: Computing exacts on every 123 of 1975 points to ramp up precision
1554043199.668 * * * * [points]: Setting MPFR precision to 64
1554043199.669 * * * * [points]: Setting MPFR precision to 320
1554043199.671 * * * * [points]: Computing exacts on every 61 of 1975 points to ramp up precision
1554043199.673 * * * * [points]: Setting MPFR precision to 64
1554043199.676 * * * * [points]: Setting MPFR precision to 320
1554043199.699 * * * * [points]: Computing exacts on every 30 of 1975 points to ramp up precision
1554043199.701 * * * * [points]: Setting MPFR precision to 64
1554043199.710 * * * * [points]: Setting MPFR precision to 320
1554043199.719 * * * * [points]: Computing exacts on every 15 of 1975 points to ramp up precision
1554043199.721 * * * * [points]: Setting MPFR precision to 64
1554043199.736 * * * * [points]: Setting MPFR precision to 320
1554043199.751 * * * * [points]: Computing exacts on every 7 of 1975 points to ramp up precision
1554043199.753 * * * * [points]: Setting MPFR precision to 64
1554043199.777 * * * * [points]: Setting MPFR precision to 320
1554043199.798 * * * * [points]: Computing exacts on every 3 of 1975 points to ramp up precision
1554043199.799 * * * * [points]: Setting MPFR precision to 64
1554043199.830 * * * * [points]: Setting MPFR precision to 320
1554043199.933 * * * * [points]: Computing exacts for 1975 points
1554043199.934 * * * * [points]: Setting MPFR precision to 64
1554043200.097 * * * * [points]: Setting MPFR precision to 320
1554043200.299 * * * * [points]: Filtering points with unrepresentable outputs
1554043200.694 * * * * [points]: Sampling 506 additional inputs, on iter 2 have 7494 / 8000
1554043200.696 * * * * [points]: Computing exacts on every 31 of 506 points to ramp up precision
1554043200.698 * * * * [points]: Setting MPFR precision to 64
1554043200.699 * * * * [points]: Setting MPFR precision to 320
1554043200.700 * * * * [points]: Computing exacts on every 15 of 506 points to ramp up precision
1554043200.701 * * * * [points]: Setting MPFR precision to 64
1554043200.704 * * * * [points]: Setting MPFR precision to 320
1554043200.706 * * * * [points]: Computing exacts on every 7 of 506 points to ramp up precision
1554043200.707 * * * * [points]: Setting MPFR precision to 64
1554043200.712 * * * * [points]: Setting MPFR precision to 320
1554043200.717 * * * * [points]: Computing exacts on every 3 of 506 points to ramp up precision
1554043200.718 * * * * [points]: Setting MPFR precision to 64
1554043200.726 * * * * [points]: Setting MPFR precision to 320
1554043200.736 * * * * [points]: Computing exacts for 506 points
1554043200.737 * * * * [points]: Setting MPFR precision to 64
1554043200.787 * * * * [points]: Setting MPFR precision to 320
1554043200.830 * * * * [points]: Filtering points with unrepresentable outputs
1554043200.857 * * * * [points]: Sampling 146 additional inputs, on iter 3 have 7854 / 8000
1554043200.858 * * * * [points]: Computing exacts on every 9 of 146 points to ramp up precision
1554043200.859 * * * * [points]: Setting MPFR precision to 64
1554043200.860 * * * * [points]: Setting MPFR precision to 320
1554043200.861 * * * * [points]: Computing exacts on every 4 of 146 points to ramp up precision
1554043200.862 * * * * [points]: Setting MPFR precision to 64
1554043200.864 * * * * [points]: Setting MPFR precision to 320
1554043200.867 * * * * [points]: Computing exacts on every 2 of 146 points to ramp up precision
1554043200.868 * * * * [points]: Setting MPFR precision to 64
1554043200.871 * * * * [points]: Setting MPFR precision to 320
1554043200.875 * * * * [points]: Computing exacts for 146 points
1554043200.876 * * * * [points]: Setting MPFR precision to 64
1554043200.886 * * * * [points]: Setting MPFR precision to 320
1554043200.898 * * * * [points]: Filtering points with unrepresentable outputs
1554043200.906 * * * * [points]: Sampling 44 additional inputs, on iter 4 have 7956 / 8000
1554043200.907 * * * * [points]: Computing exacts on every 2 of 44 points to ramp up precision
1554043200.908 * * * * [points]: Setting MPFR precision to 64
1554043200.931 * * * * [points]: Setting MPFR precision to 320
1554043200.933 * * * * [points]: Computing exacts for 44 points
1554043200.934 * * * * [points]: Setting MPFR precision to 64
1554043200.937 * * * * [points]: Setting MPFR precision to 320
1554043200.942 * * * * [points]: Filtering points with unrepresentable outputs
1554043200.944 * * * * [points]: Sampling 8 additional inputs, on iter 5 have 7992 / 8000
1554043200.945 * * * * [points]: Computing exacts for 8 points
1554043200.946 * * * * [points]: Setting MPFR precision to 64
1554043200.947 * * * * [points]: Setting MPFR precision to 320
1554043200.948 * * * * [points]: Filtering points with unrepresentable outputs
1554043200.948 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 7998 / 8000
1554043200.948 * * * * [points]: Computing exacts for 4 points
1554043200.950 * * * * [points]: Setting MPFR precision to 64
1554043200.950 * * * * [points]: Setting MPFR precision to 320
1554043200.950 * * * * [points]: Filtering points with unrepresentable outputs
1554043200.951 * * * * [points]: Sampled 8000 points with exact outputs
1554043203.369 * [regime-testing]: Baseline error score: 64.0
1554043203.373 * [regime-testing]: Oracle error score: 64.0
1554043203.381 * [regime-testing]: End program error score: 2.284350792699524