1553862975.661 * [progress]: [Phase 1 of 3] Setting up.
1553862975.662 * * * [progress]: [1/2] Preparing points
1553862975.663 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
1553862975.667 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
1553862975.697 * * * * [points]: Setting MPFR precision to 64
1553862975.699 * * * * [points]: Setting MPFR precision to 320
1553862975.737 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
1553862975.738 * * * * [points]: Setting MPFR precision to 64
1553862975.740 * * * * [points]: Setting MPFR precision to 320
1553862975.743 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
1553862975.744 * * * * [points]: Setting MPFR precision to 64
1553862975.783 * * * * [points]: Setting MPFR precision to 320
1553862975.793 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
1553862975.795 * * * * [points]: Setting MPFR precision to 64
1553862975.806 * * * * [points]: Setting MPFR precision to 320
1553862975.850 * * * * [points]: Computing exacts for 256 points
1553862975.853 * * * * [points]: Setting MPFR precision to 64
1553862975.920 * * * * [points]: Setting MPFR precision to 320
1553862975.964 * * * * [points]: Filtering points with unrepresentable outputs
1553862975.977 * * * * [points]: Sampling 64 additional inputs, on iter 1 have 192 / 256
1553862975.978 * * * * [points]: Computing exacts on every 4 of 64 points to ramp up precision
1553862975.979 * * * * [points]: Setting MPFR precision to 64
1553862975.980 * * * * [points]: Setting MPFR precision to 320
1553862975.981 * * * * [points]: Computing exacts on every 2 of 64 points to ramp up precision
1553862975.982 * * * * [points]: Setting MPFR precision to 64
1553862975.984 * * * * [points]: Setting MPFR precision to 320
1553862975.985 * * * * [points]: Computing exacts for 64 points
1553862975.987 * * * * [points]: Setting MPFR precision to 64
1553862975.991 * * * * [points]: Setting MPFR precision to 320
1553862975.998 * * * * [points]: Filtering points with unrepresentable outputs
1553862976.002 * * * * [points]: Sampling 19 additional inputs, on iter 2 have 237 / 256
1553862976.002 * * * * [points]: Computing exacts for 19 points
1553862976.003 * * * * [points]: Setting MPFR precision to 64
1553862976.005 * * * * [points]: Setting MPFR precision to 320
1553862976.006 * * * * [points]: Filtering points with unrepresentable outputs
1553862976.008 * * * * [points]: Sampling 4 additional inputs, on iter 3 have 253 / 256
1553862976.008 * * * * [points]: Computing exacts for 4 points
1553862976.009 * * * * [points]: Setting MPFR precision to 64
1553862976.009 * * * * [points]: Setting MPFR precision to 320
1553862976.010 * * * * [points]: Filtering points with unrepresentable outputs
1553862976.010 * * * * [points]: Sampled 257 points with exact outputs
1553862976.010 * * * [progress]: [2/2] Setting up program.
1553862976.059 * [progress]: [Phase 2 of 3] Improving.
1553862976.059 * * * * [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))>
1553862976.060 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1553862976.061 * * [simplify]: iters left: 5 (10 enodes)
1553862976.066 * * [simplify]: iters left: 4 (25 enodes)
1553862976.071 * * [simplify]: iters left: 3 (48 enodes)
1553862976.080 * * [simplify]: iters left: 2 (111 enodes)
1553862976.109 * * [simplify]: iters left: 1 (392 enodes)
1553862976.310 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862976.311 * * [simplify]: Extracting #1: cost 10 inf + 0
1553862976.311 * * [simplify]: Extracting #2: cost 35 inf + 1
1553862976.311 * * [simplify]: Extracting #3: cost 91 inf + 405
1553862976.312 * * [simplify]: Extracting #4: cost 331 inf + 2291
1553862976.316 * * [simplify]: Extracting #5: cost 455 inf + 80323
1553862976.340 * * [simplify]: Extracting #6: cost 250 inf + 579968
1553862976.383 * * [simplify]: Extracting #7: cost 28 inf + 1003440
1553862976.430 * * [simplify]: Extracting #8: cost 0 inf + 1069311
1553862976.475 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1553862976.476 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
1553862976.505 * * [progress]: iteration 1 / 4
1553862976.505 * * * [progress]: picking best candidate
1553862976.518 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1553862976.518 * * * [progress]: localizing error
1553862976.745 * * * [progress]: generating rewritten candidates
1553862976.746 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1553862976.751 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1)
1553862976.752 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1553862976.757 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1553862976.770 * * * [progress]: generating series expansions
1553862976.770 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1553862976.771 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1)
1553862976.771 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1553862976.771 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1553862976.771 * * * [progress]: simplifying candidates
1553862976.771 * * * * [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))>
1553862976.771 * * * * [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))>
1553862976.771 * * * * [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))))>
1553862976.771 * [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))
1553862976.772 * * [simplify]: iters left: 5 (9 enodes)
1553862976.776 * * [simplify]: iters left: 4 (32 enodes)
1553862976.788 * * [simplify]: iters left: 3 (94 enodes)
1553862976.832 * * [simplify]: iters left: 2 (340 enodes)
1553862977.042 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862977.042 * * [simplify]: Extracting #1: cost 50 inf + 0
1553862977.043 * * [simplify]: Extracting #2: cost 240 inf + 0
1553862977.045 * * [simplify]: Extracting #3: cost 355 inf + 61800
1553862977.068 * * [simplify]: Extracting #4: cost 246 inf + 415499
1553862977.119 * * [simplify]: Extracting #5: cost 58 inf + 816216
1553862977.173 * * [simplify]: Extracting #6: cost 1 inf + 911482
1553862977.217 * * [simplify]: Extracting #7: cost 0 inf + 914765
1553862977.298 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1553862977.298 * [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))))
1553862977.298 * * * * [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))>
1553862977.298 * * * * [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))>
1553862977.298 * * * * [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))>
1553862977.299 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1553862977.299 * * [simplify]: iters left: 5 (9 enodes)
1553862977.303 * * [simplify]: iters left: 4 (29 enodes)
1553862977.313 * * [simplify]: iters left: 3 (62 enodes)
1553862977.338 * * [simplify]: iters left: 2 (199 enodes)
1553862977.447 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862977.447 * * [simplify]: Extracting #1: cost 20 inf + 0
1553862977.447 * * [simplify]: Extracting #2: cost 94 inf + 1
1553862977.448 * * [simplify]: Extracting #3: cost 162 inf + 1046
1553862977.449 * * [simplify]: Extracting #4: cost 208 inf + 17818
1553862977.452 * * [simplify]: Extracting #5: cost 164 inf + 103714
1553862977.464 * * [simplify]: Extracting #6: cost 47 inf + 336456
1553862977.480 * * [simplify]: Extracting #7: cost 0 inf + 409081
1553862977.498 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1553862977.499 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1553862977.499 * * * * [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))>
1553862977.499 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1553862977.499 * * [simplify]: iters left: 5 (9 enodes)
1553862977.501 * * [simplify]: iters left: 4 (29 enodes)
1553862977.505 * * [simplify]: iters left: 3 (62 enodes)
1553862977.526 * * [simplify]: iters left: 2 (199 enodes)
1553862977.642 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862977.642 * * [simplify]: Extracting #1: cost 20 inf + 0
1553862977.642 * * [simplify]: Extracting #2: cost 94 inf + 1
1553862977.643 * * [simplify]: Extracting #3: cost 162 inf + 1046
1553862977.645 * * [simplify]: Extracting #4: cost 208 inf + 17818
1553862977.652 * * [simplify]: Extracting #5: cost 164 inf + 103714
1553862977.675 * * [simplify]: Extracting #6: cost 47 inf + 336456
1553862977.701 * * [simplify]: Extracting #7: cost 0 inf + 409081
1553862977.717 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1553862977.717 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1553862977.717 * * * * [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))>
1553862977.718 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1553862977.718 * * [simplify]: iters left: 5 (9 enodes)
1553862977.719 * * [simplify]: iters left: 4 (29 enodes)
1553862977.725 * * [simplify]: iters left: 3 (62 enodes)
1553862977.738 * * [simplify]: iters left: 2 (199 enodes)
1553862977.841 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862977.841 * * [simplify]: Extracting #1: cost 20 inf + 0
1553862977.842 * * [simplify]: Extracting #2: cost 94 inf + 1
1553862977.843 * * [simplify]: Extracting #3: cost 162 inf + 1046
1553862977.845 * * [simplify]: Extracting #4: cost 208 inf + 17818
1553862977.852 * * [simplify]: Extracting #5: cost 164 inf + 103714
1553862977.876 * * [simplify]: Extracting #6: cost 47 inf + 336456
1553862977.908 * * [simplify]: Extracting #7: cost 0 inf + 409081
1553862977.939 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1553862977.939 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1553862977.940 * * * * [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))>
1553862977.940 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1553862977.940 * * [simplify]: iters left: 5 (9 enodes)
1553862977.944 * * [simplify]: iters left: 4 (29 enodes)
1553862977.949 * * [simplify]: iters left: 3 (62 enodes)
1553862977.963 * * [simplify]: iters left: 2 (199 enodes)
1553862978.026 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862978.026 * * [simplify]: Extracting #1: cost 20 inf + 0
1553862978.027 * * [simplify]: Extracting #2: cost 94 inf + 1
1553862978.027 * * [simplify]: Extracting #3: cost 162 inf + 1046
1553862978.029 * * [simplify]: Extracting #4: cost 208 inf + 17818
1553862978.035 * * [simplify]: Extracting #5: cost 164 inf + 103714
1553862978.061 * * [simplify]: Extracting #6: cost 47 inf + 336456
1553862978.092 * * [simplify]: Extracting #7: cost 0 inf + 409081
1553862978.114 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1553862978.114 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1553862978.115 * * * [progress]: adding candidates to table
1553862978.435 * * [progress]: iteration 2 / 4
1553862978.435 * * * [progress]: picking best candidate
1553862978.515 * * * * [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))>
1553862978.515 * * * [progress]: localizing error
1553862978.822 * * * [progress]: generating rewritten candidates
1553862978.822 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 1)
1553862978.857 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1)
1553862978.859 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
1553862978.859 * * * * [progress]: [ 4 / 4 ] rewriting at (2)
1553862978.862 * * * [progress]: generating series expansions
1553862978.862 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 1)
1553862978.862 * * * * [progress]: [ 2 / 4 ] generating series at (2 1)
1553862978.862 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
1553862978.863 * * * * [progress]: [ 4 / 4 ] generating series at (2)
1553862978.863 * * * [progress]: simplifying candidates
1553862978.863 * * * * [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))>
1553862978.863 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1553862978.863 * * [simplify]: iters left: 2 (6 enodes)
1553862978.864 * * [simplify]: iters left: 1 (14 enodes)
1553862978.866 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862978.866 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862978.866 * * [simplify]: Extracting #2: cost 6 inf + 0
1553862978.866 * * [simplify]: Extracting #3: cost 2 inf + 325
1553862978.866 * * [simplify]: Extracting #4: cost 0 inf + 1329
1553862978.866 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1553862978.866 * [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))
1553862978.866 * * * * [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))>
1553862978.866 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1553862978.866 * * [simplify]: iters left: 2 (6 enodes)
1553862978.868 * * [simplify]: iters left: 1 (14 enodes)
1553862978.869 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862978.869 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862978.869 * * [simplify]: Extracting #2: cost 6 inf + 0
1553862978.869 * * [simplify]: Extracting #3: cost 2 inf + 325
1553862978.870 * * [simplify]: Extracting #4: cost 0 inf + 1329
1553862978.870 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1553862978.870 * [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))
1553862978.870 * * * * [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))>
1553862978.870 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1553862978.870 * * [simplify]: iters left: 2 (6 enodes)
1553862978.871 * * [simplify]: iters left: 1 (14 enodes)
1553862978.873 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862978.873 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862978.873 * * [simplify]: Extracting #2: cost 6 inf + 0
1553862978.873 * * [simplify]: Extracting #3: cost 2 inf + 325
1553862978.873 * * [simplify]: Extracting #4: cost 0 inf + 1329
1553862978.873 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1553862978.873 * [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))
1553862978.873 * * * * [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))>
1553862978.873 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 c a))
1553862978.873 * * [simplify]: iters left: 2 (6 enodes)
1553862978.875 * * [simplify]: iters left: 1 (14 enodes)
1553862978.876 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862978.876 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862978.876 * * [simplify]: Extracting #2: cost 6 inf + 0
1553862978.877 * * [simplify]: Extracting #3: cost 2 inf + 325
1553862978.877 * * [simplify]: Extracting #4: cost 0 inf + 1329
1553862978.877 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 b_2 b_2))
1553862978.877 * [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))
1553862978.877 * * * * [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))>
1553862978.877 * [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))))
1553862978.877 * * [simplify]: iters left: 4 (10 enodes)
1553862978.879 * * [simplify]: iters left: 3 (43 enodes)
1553862978.891 * * [simplify]: iters left: 2 (121 enodes)
1553862978.938 * * [simplify]: iters left: 1 (429 enodes)
1553862979.171 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862979.172 * * [simplify]: Extracting #1: cost 46 inf + 0
1553862979.172 * * [simplify]: Extracting #2: cost 270 inf + 0
1553862979.175 * * [simplify]: Extracting #3: cost 354 inf + 59003
1553862979.188 * * [simplify]: Extracting #4: cost 345 inf + 369227
1553862979.253 * * [simplify]: Extracting #5: cost 22 inf + 1102360
1553862979.325 * * [simplify]: Extracting #6: cost 1 inf + 1150488
1553862979.379 * * [simplify]: Extracting #7: cost 0 inf + 1155051
1553862979.433 * [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))))
1553862979.433 * [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))
1553862979.433 * * * * [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))>
1553862979.433 * * * * [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))>
1553862979.434 * * * * [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))))>
1553862979.434 * [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))
1553862979.434 * * [simplify]: iters left: 6 (13 enodes)
1553862979.437 * * [simplify]: iters left: 5 (47 enodes)
1553862979.446 * * [simplify]: iters left: 4 (118 enodes)
1553862979.476 * * [simplify]: iters left: 3 (482 enodes)
1553862979.915 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862979.915 * * [simplify]: Extracting #1: cost 39 inf + 0
1553862979.916 * * [simplify]: Extracting #2: cost 255 inf + 0
1553862979.917 * * [simplify]: Extracting #3: cost 532 inf + 10719
1553862979.930 * * [simplify]: Extracting #4: cost 679 inf + 310118
1553862979.995 * * [simplify]: Extracting #5: cost 214 inf + 1310578
1553862980.112 * * [simplify]: Extracting #6: cost 5 inf + 1763746
1553862980.275 * * [simplify]: Extracting #7: cost 0 inf + 1773035
1553862980.438 * [simplify]: Simplified to (-.p16 (*.p16 b_2 b_2) (+.p16 (*.p16 a c) (*.p16 b_2 b_2)))
1553862980.439 * [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))))
1553862980.439 * * * * [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))>
1553862980.439 * * * * [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))>
1553862980.439 * * * * [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))>
1553862980.439 * * * * [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))>
1553862980.439 * * * [progress]: adding candidates to table
1553862981.036 * * [progress]: iteration 3 / 4
1553862981.036 * * * [progress]: picking best candidate
1553862981.116 * * * * [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))>
1553862981.116 * * * [progress]: localizing error
1553862981.613 * * * [progress]: generating rewritten candidates
1553862981.613 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
1553862981.625 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1553862982.083 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
1553862982.105 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
1553862982.106 * * * [progress]: generating series expansions
1553862982.106 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
1553862982.106 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1553862982.107 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
1553862982.107 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
1553862982.107 * * * [progress]: simplifying candidates
1553862982.107 * * * * [progress]: [ 1 / 16 ] 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))>
1553862982.107 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862982.107 * * [simplify]: iters left: 4 (8 enodes)
1553862982.111 * * [simplify]: iters left: 3 (23 enodes)
1553862982.119 * * [simplify]: iters left: 2 (45 enodes)
1553862982.136 * * [simplify]: iters left: 1 (108 enodes)
1553862982.190 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862982.190 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862982.190 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862982.190 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862982.190 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862982.191 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862982.193 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862982.198 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862982.209 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862982.215 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862982.216 * [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))
1553862982.216 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862982.216 * * [simplify]: iters left: 4 (8 enodes)
1553862982.217 * * [simplify]: iters left: 3 (28 enodes)
1553862982.222 * * [simplify]: iters left: 2 (59 enodes)
1553862982.233 * * [simplify]: iters left: 1 (178 enodes)
1553862982.289 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862982.289 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862982.289 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862982.289 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862982.290 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862982.294 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862982.305 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862982.320 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862982.334 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862982.349 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862982.349 * [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))
1553862982.349 * * * * [progress]: [ 2 / 16 ] 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))>
1553862982.349 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862982.349 * * [simplify]: iters left: 4 (8 enodes)
1553862982.351 * * [simplify]: iters left: 3 (23 enodes)
1553862982.355 * * [simplify]: iters left: 2 (45 enodes)
1553862982.365 * * [simplify]: iters left: 1 (108 enodes)
1553862982.394 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862982.394 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862982.394 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862982.394 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862982.394 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862982.395 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862982.396 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862982.402 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862982.409 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862982.416 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862982.416 * [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))
1553862982.416 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862982.416 * * [simplify]: iters left: 4 (8 enodes)
1553862982.418 * * [simplify]: iters left: 3 (28 enodes)
1553862982.423 * * [simplify]: iters left: 2 (59 enodes)
1553862982.435 * * [simplify]: iters left: 1 (178 enodes)
1553862982.538 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862982.538 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862982.538 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862982.539 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862982.541 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862982.548 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862982.573 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862982.599 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862982.627 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862982.654 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862982.654 * [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))
1553862982.654 * * * * [progress]: [ 3 / 16 ] 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))>
1553862982.654 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862982.654 * * [simplify]: iters left: 4 (8 enodes)
1553862982.658 * * [simplify]: iters left: 3 (23 enodes)
1553862982.665 * * [simplify]: iters left: 2 (45 enodes)
1553862982.681 * * [simplify]: iters left: 1 (108 enodes)
1553862982.736 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862982.736 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862982.736 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862982.736 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862982.736 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862982.737 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862982.741 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862982.751 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862982.764 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862982.776 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862982.776 * [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))
1553862982.777 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862982.777 * * [simplify]: iters left: 4 (8 enodes)
1553862982.780 * * [simplify]: iters left: 3 (28 enodes)
1553862982.789 * * [simplify]: iters left: 2 (59 enodes)
1553862982.812 * * [simplify]: iters left: 1 (178 enodes)
1553862982.911 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862982.911 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862982.911 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862982.912 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862982.914 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862982.921 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862982.944 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862982.971 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862983.003 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862983.031 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862983.031 * [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))
1553862983.031 * * * * [progress]: [ 4 / 16 ] 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))>
1553862983.032 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862983.032 * * [simplify]: iters left: 4 (8 enodes)
1553862983.035 * * [simplify]: iters left: 3 (23 enodes)
1553862983.043 * * [simplify]: iters left: 2 (45 enodes)
1553862983.060 * * [simplify]: iters left: 1 (108 enodes)
1553862983.116 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862983.116 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862983.116 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862983.116 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862983.116 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862983.117 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862983.120 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862983.130 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862983.143 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862983.158 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862983.158 * [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))
1553862983.158 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862983.159 * * [simplify]: iters left: 4 (8 enodes)
1553862983.162 * * [simplify]: iters left: 3 (28 enodes)
1553862983.171 * * [simplify]: iters left: 2 (59 enodes)
1553862983.195 * * [simplify]: iters left: 1 (178 enodes)
1553862983.304 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862983.304 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862983.304 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862983.305 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862983.307 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862983.315 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862983.336 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862983.363 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862983.392 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862983.419 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862983.419 * [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))
1553862983.420 * * * * [progress]: [ 5 / 16 ] 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))>
1553862983.420 * * * * [progress]: [ 6 / 16 ] 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))>
1553862983.420 * * * * [progress]: [ 7 / 16 ] 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))>
1553862983.420 * * * * [progress]: [ 8 / 16 ] 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))>
1553862983.420 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862983.420 * * [simplify]: iters left: 4 (8 enodes)
1553862983.424 * * [simplify]: iters left: 3 (23 enodes)
1553862983.428 * * [simplify]: iters left: 2 (45 enodes)
1553862983.438 * * [simplify]: iters left: 1 (108 enodes)
1553862983.465 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862983.465 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862983.465 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862983.465 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862983.465 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862983.466 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862983.468 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862983.473 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862983.479 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862983.486 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862983.486 * [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))
1553862983.486 * * * * [progress]: [ 9 / 16 ] 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))>
1553862983.486 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862983.486 * * [simplify]: iters left: 4 (8 enodes)
1553862983.488 * * [simplify]: iters left: 3 (23 enodes)
1553862983.491 * * [simplify]: iters left: 2 (45 enodes)
1553862983.499 * * [simplify]: iters left: 1 (108 enodes)
1553862983.530 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862983.530 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862983.530 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862983.530 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862983.530 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862983.530 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862983.532 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862983.537 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862983.544 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862983.550 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862983.551 * [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))
1553862983.551 * * * * [progress]: [ 10 / 16 ] 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))>
1553862983.551 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862983.551 * * [simplify]: iters left: 4 (8 enodes)
1553862983.553 * * [simplify]: iters left: 3 (23 enodes)
1553862983.556 * * [simplify]: iters left: 2 (45 enodes)
1553862983.565 * * [simplify]: iters left: 1 (108 enodes)
1553862983.595 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862983.595 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862983.595 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862983.595 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862983.596 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862983.596 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862983.598 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862983.603 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862983.609 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862983.616 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862983.616 * [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))
1553862983.616 * * * * [progress]: [ 11 / 16 ] 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))>
1553862983.616 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862983.616 * * [simplify]: iters left: 4 (8 enodes)
1553862983.618 * * [simplify]: iters left: 3 (23 enodes)
1553862983.622 * * [simplify]: iters left: 2 (45 enodes)
1553862983.631 * * [simplify]: iters left: 1 (108 enodes)
1553862983.660 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862983.660 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862983.660 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862983.660 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862983.660 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862983.661 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862983.662 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862983.668 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862983.674 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862983.681 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862983.681 * [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))
1553862983.681 * * * * [progress]: [ 12 / 16 ] 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))>
1553862983.681 * [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)))
1553862983.681 * * [simplify]: iters left: 6 (11 enodes)
1553862983.684 * * [simplify]: iters left: 5 (43 enodes)
1553862983.692 * * [simplify]: iters left: 4 (139 enodes)
1553862983.739 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862983.739 * * [simplify]: Extracting #1: cost 32 inf + 0
1553862983.739 * * [simplify]: Extracting #2: cost 85 inf + 0
1553862983.740 * * [simplify]: Extracting #3: cost 152 inf + 1364
1553862983.741 * * [simplify]: Extracting #4: cost 163 inf + 24483
1553862983.751 * * [simplify]: Extracting #5: cost 71 inf + 172897
1553862983.770 * * [simplify]: Extracting #6: cost 3 inf + 277964
1553862983.792 * * [simplify]: Extracting #7: cost 0 inf + 284573
1553862983.814 * [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))))
1553862983.814 * [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))
1553862983.814 * * * * [progress]: [ 13 / 16 ] 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))>
1553862983.814 * * * * [progress]: [ 14 / 16 ] 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))>
1553862983.814 * * * * [progress]: [ 15 / 16 ] 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))>
1553862983.814 * * * * [progress]: [ 16 / 16 ] 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))>
1553862983.815 * * * [progress]: adding candidates to table
1553862984.650 * * [progress]: iteration 4 / 4
1553862984.650 * * * [progress]: picking best candidate
1553862984.790 * * * * [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))>
1553862984.790 * * * [progress]: localizing error
1553862985.232 * * * [progress]: generating rewritten candidates
1553862985.232 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2)
1553862985.237 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1)
1553862985.242 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2)
1553862985.245 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
1553862985.263 * * * [progress]: generating series expansions
1553862985.263 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2)
1553862985.263 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1)
1553862985.263 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2)
1553862985.263 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
1553862985.263 * * * [progress]: simplifying candidates
1553862985.263 * * * * [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))>
1553862985.263 * * * * [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))>
1553862985.264 * * * * [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))>
1553862985.264 * * * * [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))>
1553862985.264 * * * * [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))>
1553862985.264 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862985.264 * * [simplify]: iters left: 4 (8 enodes)
1553862985.267 * * [simplify]: iters left: 3 (23 enodes)
1553862985.275 * * [simplify]: iters left: 2 (45 enodes)
1553862985.290 * * [simplify]: iters left: 1 (108 enodes)
1553862985.348 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862985.349 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862985.349 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862985.349 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862985.349 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862985.350 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862985.353 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862985.358 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862985.365 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862985.372 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862985.372 * [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))
1553862985.372 * * * * [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))>
1553862985.373 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862985.373 * * [simplify]: iters left: 4 (8 enodes)
1553862985.374 * * [simplify]: iters left: 3 (28 enodes)
1553862985.379 * * [simplify]: iters left: 2 (59 enodes)
1553862985.390 * * [simplify]: iters left: 1 (178 enodes)
1553862985.471 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862985.471 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862985.471 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862985.472 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862985.473 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862985.477 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862985.491 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862985.518 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862985.550 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862985.579 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862985.579 * [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))
1553862985.579 * * * * [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))>
1553862985.579 * [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)))
1553862985.580 * * [simplify]: iters left: 6 (11 enodes)
1553862985.585 * * [simplify]: iters left: 5 (35 enodes)
1553862985.598 * * [simplify]: iters left: 4 (111 enodes)
1553862985.655 * * [simplify]: iters left: 3 (448 enodes)
1553862986.032 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862986.032 * * [simplify]: Extracting #1: cost 64 inf + 0
1553862986.033 * * [simplify]: Extracting #2: cost 370 inf + 0
1553862986.035 * * [simplify]: Extracting #3: cost 522 inf + 6695
1553862986.045 * * [simplify]: Extracting #4: cost 536 inf + 237314
1553862986.116 * * [simplify]: Extracting #5: cost 132 inf + 950329
1553862986.208 * * [simplify]: Extracting #6: cost 26 inf + 1188087
1553862986.314 * * [simplify]: Extracting #7: cost 0 inf + 1213652
1553862986.383 * * [simplify]: Extracting #8: cost 0 inf + 1213496
1553862986.454 * [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)))))
1553862986.454 * [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))
1553862986.455 * * * * [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))>
1553862986.455 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862986.455 * * [simplify]: iters left: 4 (8 enodes)
1553862986.458 * * [simplify]: iters left: 3 (23 enodes)
1553862986.465 * * [simplify]: iters left: 2 (45 enodes)
1553862986.482 * * [simplify]: iters left: 1 (108 enodes)
1553862986.537 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862986.537 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862986.537 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862986.537 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862986.537 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862986.537 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862986.539 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862986.545 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862986.551 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862986.558 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862986.558 * [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))
1553862986.558 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862986.558 * * [simplify]: iters left: 4 (8 enodes)
1553862986.560 * * [simplify]: iters left: 3 (28 enodes)
1553862986.565 * * [simplify]: iters left: 2 (59 enodes)
1553862986.578 * * [simplify]: iters left: 1 (178 enodes)
1553862986.656 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862986.656 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862986.657 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862986.657 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862986.658 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862986.662 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862986.677 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862986.706 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862986.738 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862986.766 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862986.766 * [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))
1553862986.766 * * * * [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))>
1553862986.766 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862986.767 * * [simplify]: iters left: 4 (8 enodes)
1553862986.770 * * [simplify]: iters left: 3 (23 enodes)
1553862986.778 * * [simplify]: iters left: 2 (45 enodes)
1553862986.794 * * [simplify]: iters left: 1 (108 enodes)
1553862986.850 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862986.850 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862986.850 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862986.851 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862986.851 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862986.852 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862986.855 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862986.868 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862986.881 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862986.894 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862986.894 * [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))
1553862986.895 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862986.895 * * [simplify]: iters left: 4 (8 enodes)
1553862986.898 * * [simplify]: iters left: 3 (28 enodes)
1553862986.909 * * [simplify]: iters left: 2 (59 enodes)
1553862986.932 * * [simplify]: iters left: 1 (178 enodes)
1553862987.027 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862987.027 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862987.028 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862987.028 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862987.029 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862987.034 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862987.055 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862987.074 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862987.089 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862987.114 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862987.114 * [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))
1553862987.114 * * * * [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))>
1553862987.114 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862987.114 * * [simplify]: iters left: 4 (8 enodes)
1553862987.121 * * [simplify]: iters left: 3 (23 enodes)
1553862987.129 * * [simplify]: iters left: 2 (45 enodes)
1553862987.146 * * [simplify]: iters left: 1 (108 enodes)
1553862987.204 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862987.204 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862987.204 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862987.204 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862987.204 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862987.205 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862987.209 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862987.219 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862987.232 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862987.245 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862987.245 * [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))
1553862987.245 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862987.245 * * [simplify]: iters left: 4 (8 enodes)
1553862987.249 * * [simplify]: iters left: 3 (28 enodes)
1553862987.259 * * [simplify]: iters left: 2 (59 enodes)
1553862987.277 * * [simplify]: iters left: 1 (178 enodes)
1553862987.360 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862987.360 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862987.361 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862987.361 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862987.364 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862987.374 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862987.396 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862987.422 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862987.449 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862987.477 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862987.477 * [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))
1553862987.477 * * * * [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))>
1553862987.477 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862987.478 * * [simplify]: iters left: 4 (8 enodes)
1553862987.481 * * [simplify]: iters left: 3 (23 enodes)
1553862987.488 * * [simplify]: iters left: 2 (45 enodes)
1553862987.505 * * [simplify]: iters left: 1 (108 enodes)
1553862987.562 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862987.562 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862987.562 * * [simplify]: Extracting #2: cost 3 inf + 1
1553862987.562 * * [simplify]: Extracting #3: cost 17 inf + 1
1553862987.562 * * [simplify]: Extracting #4: cost 55 inf + 322
1553862987.563 * * [simplify]: Extracting #5: cost 80 inf + 11197
1553862987.567 * * [simplify]: Extracting #6: cost 84 inf + 56173
1553862987.578 * * [simplify]: Extracting #7: cost 7 inf + 177856
1553862987.591 * * [simplify]: Extracting #8: cost 0 inf + 193436
1553862987.604 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1553862987.604 * [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))
1553862987.604 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1553862987.604 * * [simplify]: iters left: 4 (8 enodes)
1553862987.608 * * [simplify]: iters left: 3 (28 enodes)
1553862987.618 * * [simplify]: iters left: 2 (59 enodes)
1553862987.642 * * [simplify]: iters left: 1 (178 enodes)
1553862987.744 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862987.744 * * [simplify]: Extracting #1: cost 12 inf + 0
1553862987.745 * * [simplify]: Extracting #2: cost 64 inf + 1
1553862987.745 * * [simplify]: Extracting #3: cost 140 inf + 403
1553862987.747 * * [simplify]: Extracting #4: cost 189 inf + 12881
1553862987.754 * * [simplify]: Extracting #5: cost 149 inf + 112868
1553862987.776 * * [simplify]: Extracting #6: cost 32 inf + 315911
1553862987.805 * * [simplify]: Extracting #7: cost 1 inf + 362422
1553862987.833 * * [simplify]: Extracting #8: cost 0 inf + 365106
1553862987.861 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1553862987.861 * [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))
1553862987.861 * * * [progress]: adding candidates to table
1553862988.320 * [progress]: [Phase 3 of 3] Extracting.
1553862988.321 * * [regime]: Finding splitpoints for: (#<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 (*.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 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 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 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (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))) 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))>)
1553862988.324 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
1553862988.324 * * * * [regimes]: Trying to branch on c from (#<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 (*.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 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 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 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (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))) 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))>)
1553862988.643 * * * * [regimes]: Trying to branch on a from (#<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 (*.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 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 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 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (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))) 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))>)
1553862989.140 * * * * [regimes]: Trying to branch on b_2 from (#<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 (*.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 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 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 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (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))) 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))>)
1553862989.639 * * * [regime]: Found split indices: #<option (#s(si 1 256))>
1553862989.640 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1553862989.640 * * [simplify]: iters left: 5 (9 enodes)
1553862989.640 * * [simplify]: Extracting #0: cost 1 inf + 0
1553862989.640 * * [simplify]: Extracting #1: cost 3 inf + 0
1553862989.641 * * [simplify]: Extracting #2: cost 4 inf + 1
1553862989.641 * * [simplify]: Extracting #3: cost 4 inf + 2
1553862989.641 * * [simplify]: Extracting #4: cost 6 inf + 2
1553862989.641 * * [simplify]: Extracting #5: cost 6 inf + 323
1553862989.641 * * [simplify]: Extracting #6: cost 0 inf + 4258
1553862989.641 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1553862989.641 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1553862989.703 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
1553862989.705 * * * * [points]: Setting MPFR precision to 64
1553862989.707 * * * * [points]: Setting MPFR precision to 320
1553862989.709 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
1553862989.711 * * * * [points]: Setting MPFR precision to 64
1553862989.714 * * * * [points]: Setting MPFR precision to 320
1553862989.716 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
1553862989.718 * * * * [points]: Setting MPFR precision to 64
1553862989.721 * * * * [points]: Setting MPFR precision to 320
1553862989.727 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
1553862989.728 * * * * [points]: Setting MPFR precision to 64
1553862989.753 * * * * [points]: Setting MPFR precision to 320
1553862989.773 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
1553862989.776 * * * * [points]: Setting MPFR precision to 64
1553862989.804 * * * * [points]: Setting MPFR precision to 320
1553862989.840 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
1553862989.842 * * * * [points]: Setting MPFR precision to 64
1553862989.898 * * * * [points]: Setting MPFR precision to 320
1553862989.985 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
1553862989.986 * * * * [points]: Setting MPFR precision to 64
1553862990.085 * * * * [points]: Setting MPFR precision to 320
1553862990.289 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
1553862990.291 * * * * [points]: Setting MPFR precision to 64
1553862990.566 * * * * [points]: Setting MPFR precision to 320
1553862990.919 * * * * [points]: Computing exacts for 8000 points
1553862990.921 * * * * [points]: Setting MPFR precision to 64
1553862991.932 * * * * [points]: Setting MPFR precision to 320
1553862993.555 * * * * [points]: Filtering points with unrepresentable outputs
1553862994.464 * * * * [points]: Sampling 1932 additional inputs, on iter 1 have 6068 / 8000
1553862994.478 * * * * [points]: Computing exacts on every 120 of 1932 points to ramp up precision
1553862994.480 * * * * [points]: Setting MPFR precision to 64
1553862994.482 * * * * [points]: Setting MPFR precision to 320
1553862994.485 * * * * [points]: Computing exacts on every 60 of 1932 points to ramp up precision
1553862994.486 * * * * [points]: Setting MPFR precision to 64
1553862994.490 * * * * [points]: Setting MPFR precision to 320
1553862994.495 * * * * [points]: Computing exacts on every 30 of 1932 points to ramp up precision
1553862994.496 * * * * [points]: Setting MPFR precision to 64
1553862994.504 * * * * [points]: Setting MPFR precision to 320
1553862994.513 * * * * [points]: Computing exacts on every 15 of 1932 points to ramp up precision
1553862994.515 * * * * [points]: Setting MPFR precision to 64
1553862994.529 * * * * [points]: Setting MPFR precision to 320
1553862994.547 * * * * [points]: Computing exacts on every 7 of 1932 points to ramp up precision
1553862994.549 * * * * [points]: Setting MPFR precision to 64
1553862994.602 * * * * [points]: Setting MPFR precision to 320
1553862994.639 * * * * [points]: Computing exacts on every 3 of 1932 points to ramp up precision
1553862994.641 * * * * [points]: Setting MPFR precision to 64
1553862994.696 * * * * [points]: Setting MPFR precision to 320
1553862994.770 * * * * [points]: Computing exacts for 1932 points
1553862994.771 * * * * [points]: Setting MPFR precision to 64
1553862995.038 * * * * [points]: Setting MPFR precision to 320
1553862995.353 * * * * [points]: Filtering points with unrepresentable outputs
1553862995.552 * * * * [points]: Sampling 484 additional inputs, on iter 2 have 7516 / 8000
1553862995.555 * * * * [points]: Computing exacts on every 30 of 484 points to ramp up precision
1553862995.557 * * * * [points]: Setting MPFR precision to 64
1553862995.559 * * * * [points]: Setting MPFR precision to 320
1553862995.561 * * * * [points]: Computing exacts on every 15 of 484 points to ramp up precision
1553862995.562 * * * * [points]: Setting MPFR precision to 64
1553862995.565 * * * * [points]: Setting MPFR precision to 320
1553862995.568 * * * * [points]: Computing exacts on every 7 of 484 points to ramp up precision
1553862995.569 * * * * [points]: Setting MPFR precision to 64
1553862995.572 * * * * [points]: Setting MPFR precision to 320
1553862995.577 * * * * [points]: Computing exacts on every 3 of 484 points to ramp up precision
1553862995.579 * * * * [points]: Setting MPFR precision to 64
1553862995.587 * * * * [points]: Setting MPFR precision to 320
1553862995.597 * * * * [points]: Computing exacts for 484 points
1553862995.599 * * * * [points]: Setting MPFR precision to 64
1553862995.629 * * * * [points]: Setting MPFR precision to 320
1553862995.696 * * * * [points]: Filtering points with unrepresentable outputs
1553862995.727 * * * * [points]: Sampling 127 additional inputs, on iter 3 have 7873 / 8000
1553862995.728 * * * * [points]: Computing exacts on every 7 of 127 points to ramp up precision
1553862995.729 * * * * [points]: Setting MPFR precision to 64
1553862995.730 * * * * [points]: Setting MPFR precision to 320
1553862995.731 * * * * [points]: Computing exacts on every 3 of 127 points to ramp up precision
1553862995.732 * * * * [points]: Setting MPFR precision to 64
1553862995.734 * * * * [points]: Setting MPFR precision to 320
1553862995.737 * * * * [points]: Computing exacts for 127 points
1553862995.738 * * * * [points]: Setting MPFR precision to 64
1553862995.746 * * * * [points]: Setting MPFR precision to 320
1553862995.758 * * * * [points]: Filtering points with unrepresentable outputs
1553862995.765 * * * * [points]: Sampling 37 additional inputs, on iter 4 have 7963 / 8000
1553862995.765 * * * * [points]: Computing exacts on every 2 of 37 points to ramp up precision
1553862995.766 * * * * [points]: Setting MPFR precision to 64
1553862995.767 * * * * [points]: Setting MPFR precision to 320
1553862995.768 * * * * [points]: Computing exacts for 37 points
1553862995.769 * * * * [points]: Setting MPFR precision to 64
1553862995.772 * * * * [points]: Setting MPFR precision to 320
1553862995.775 * * * * [points]: Filtering points with unrepresentable outputs
1553862995.777 * * * * [points]: Sampling 9 additional inputs, on iter 5 have 7991 / 8000
1553862995.777 * * * * [points]: Computing exacts for 9 points
1553862995.778 * * * * [points]: Setting MPFR precision to 64
1553862995.779 * * * * [points]: Setting MPFR precision to 320
1553862995.780 * * * * [points]: Filtering points with unrepresentable outputs
1553862995.780 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 7996 / 8000
1553862995.780 * * * * [points]: Computing exacts for 4 points
1553862995.781 * * * * [points]: Setting MPFR precision to 64
1553862995.782 * * * * [points]: Setting MPFR precision to 320
1553862995.782 * * * * [points]: Filtering points with unrepresentable outputs
1553862995.782 * * * * [points]: Sampled 8000 points with exact outputs
1553862997.730 * [regime-testing]: Baseline error score: 64.0
1553862997.734 * [regime-testing]: Oracle error score: 64.0
1553862997.741 * [regime-testing]: End program error score: 2.3092875478297596