1552123016.580 * [progress]: [Phase 1 of 3] Setting up.
1552123016.581 * * * [progress]: [1/2] Preparing points
1552123016.583 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256
1552123016.591 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision
1552123016.672 * * * * [points]: Setting MPFR precision to 64
1552123016.677 * * * * [points]: Setting MPFR precision to 320
1552123016.679 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision
1552123016.680 * * * * [points]: Setting MPFR precision to 64
1552123016.682 * * * * [points]: Setting MPFR precision to 320
1552123016.685 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision
1552123016.686 * * * * [points]: Setting MPFR precision to 64
1552123016.690 * * * * [points]: Setting MPFR precision to 320
1552123016.694 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision
1552123016.695 * * * * [points]: Setting MPFR precision to 64
1552123016.703 * * * * [points]: Setting MPFR precision to 320
1552123016.710 * * * * [points]: Computing exacts for 256 points
1552123016.712 * * * * [points]: Setting MPFR precision to 64
1552123016.728 * * * * [points]: Setting MPFR precision to 320
1552123016.749 * * * * [points]: Filtering points with unrepresentable outputs
1552123016.762 * * * * [points]: Sampling 54 additional inputs, on iter 1 have 202 / 256
1552123017.151 * * * * [points]: Computing exacts on every 3 of 54 points to ramp up precision
1552123017.153 * * * * [points]: Setting MPFR precision to 64
1552123017.155 * * * * [points]: Setting MPFR precision to 320
1552123017.157 * * * * [points]: Computing exacts for 54 points
1552123017.159 * * * * [points]: Setting MPFR precision to 64
1552123017.168 * * * * [points]: Setting MPFR precision to 320
1552123017.176 * * * * [points]: Filtering points with unrepresentable outputs
1552123017.181 * * * * [points]: Sampling 14 additional inputs, on iter 2 have 242 / 256
1552123017.181 * * * * [points]: Computing exacts for 14 points
1552123017.184 * * * * [points]: Setting MPFR precision to 64
1552123017.185 * * * * [points]: Setting MPFR precision to 320
1552123017.188 * * * * [points]: Filtering points with unrepresentable outputs
1552123017.189 * * * * [points]: Sampling 4 additional inputs, on iter 3 have 252 / 256
1552123017.189 * * * * [points]: Computing exacts for 4 points
1552123017.191 * * * * [points]: Setting MPFR precision to 64
1552123017.191 * * * * [points]: Setting MPFR precision to 320
1552123017.192 * * * * [points]: Filtering points with unrepresentable outputs
1552123017.193 * * * * [points]: Sampled 256 points with exact outputs
1552123017.193 * * * [progress]: [2/2] Setting up program.
1552123017.230 * [progress]: [Phase 2 of 3] Improving.
1552123017.230 * * * * [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))>
1552123017.231 * [simplify]: Simplifying (/.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a)
1552123017.233 * * [simplify]: iters left: 5 (10 enodes)
1552123017.242 * * [simplify]: iters left: 4 (25 enodes)
1552123017.250 * * [simplify]: iters left: 3 (48 enodes)
1552123017.267 * * [simplify]: iters left: 2 (111 enodes)
1552123017.337 * * [simplify]: iters left: 1 (392 enodes)
1552123017.579 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123017.579 * * [simplify]: Extracting #1: cost 10 inf + 0
1552123017.579 * * [simplify]: Extracting #2: cost 35 inf + 1
1552123017.580 * * [simplify]: Extracting #3: cost 91 inf + 405
1552123017.580 * * [simplify]: Extracting #4: cost 331 inf + 2291
1552123017.584 * * [simplify]: Extracting #5: cost 455 inf + 80323
1552123017.603 * * [simplify]: Extracting #6: cost 250 inf + 579968
1552123017.641 * * [simplify]: Extracting #7: cost 28 inf + 1003440
1552123017.688 * * [simplify]: Extracting #8: cost 0 inf + 1069311
1552123017.732 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552123017.733 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))
1552123017.767 * * [progress]: iteration 1 / 4
1552123017.767 * * * [progress]: picking best candidate
1552123017.782 * * * * [pick]: Picked  #<alt (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a))>
1552123017.782 * * * [progress]: localizing error
1552123018.001 * * * [progress]: generating rewritten candidates
1552123018.001 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1)
1552123018.004 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1)
1552123018.004 * * * * [progress]: [ 3 / 4 ] rewriting at (2)
1552123018.006 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1)
1552123018.008 * * * [progress]: generating series expansions
1552123018.008 * * * * [progress]: [ 1 / 4 ] generating series at (2 1)
1552123018.009 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1)
1552123018.009 * * * * [progress]: [ 3 / 4 ] generating series at (2)
1552123018.009 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1)
1552123018.009 * * * [progress]: simplifying candidates
1552123018.009 * * * * [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))>
1552123018.009 * * * * [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))>
1552123018.009 * * * * [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))))>
1552123018.009 * [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))
1552123018.009 * * [simplify]: iters left: 5 (9 enodes)
1552123018.011 * * [simplify]: iters left: 4 (32 enodes)
1552123018.020 * * [simplify]: iters left: 3 (94 enodes)
1552123018.074 * * [simplify]: iters left: 2 (340 enodes)
1552123018.268 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123018.268 * * [simplify]: Extracting #1: cost 50 inf + 0
1552123018.269 * * [simplify]: Extracting #2: cost 240 inf + 0
1552123018.271 * * [simplify]: Extracting #3: cost 355 inf + 61800
1552123018.286 * * [simplify]: Extracting #4: cost 246 inf + 415499
1552123018.340 * * [simplify]: Extracting #5: cost 58 inf + 816216
1552123018.419 * * [simplify]: Extracting #6: cost 1 inf + 911482
1552123018.497 * * [simplify]: Extracting #7: cost 0 inf + 914765
1552123018.574 * [simplify]: Simplified to (-.p16 (real->posit16 0.0) (*.p16 a c))
1552123018.574 * [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))))
1552123018.574 * * * * [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))>
1552123018.574 * * * * [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))>
1552123018.574 * * * * [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))>
1552123018.575 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552123018.575 * * [simplify]: iters left: 5 (9 enodes)
1552123018.578 * * [simplify]: iters left: 4 (29 enodes)
1552123018.588 * * [simplify]: iters left: 3 (62 enodes)
1552123018.612 * * [simplify]: iters left: 2 (199 enodes)
1552123018.695 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123018.695 * * [simplify]: Extracting #1: cost 20 inf + 0
1552123018.695 * * [simplify]: Extracting #2: cost 94 inf + 1
1552123018.696 * * [simplify]: Extracting #3: cost 162 inf + 1046
1552123018.698 * * [simplify]: Extracting #4: cost 208 inf + 17818
1552123018.703 * * [simplify]: Extracting #5: cost 164 inf + 103714
1552123018.715 * * [simplify]: Extracting #6: cost 47 inf + 336456
1552123018.733 * * [simplify]: Extracting #7: cost 0 inf + 409081
1552123018.759 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1552123018.759 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1552123018.759 * * * * [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))>
1552123018.760 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552123018.760 * * [simplify]: iters left: 5 (9 enodes)
1552123018.763 * * [simplify]: iters left: 4 (29 enodes)
1552123018.773 * * [simplify]: iters left: 3 (62 enodes)
1552123018.797 * * [simplify]: iters left: 2 (199 enodes)
1552123018.870 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123018.870 * * [simplify]: Extracting #1: cost 20 inf + 0
1552123018.870 * * [simplify]: Extracting #2: cost 94 inf + 1
1552123018.871 * * [simplify]: Extracting #3: cost 162 inf + 1046
1552123018.873 * * [simplify]: Extracting #4: cost 208 inf + 17818
1552123018.880 * * [simplify]: Extracting #5: cost 164 inf + 103714
1552123018.902 * * [simplify]: Extracting #6: cost 47 inf + 336456
1552123018.929 * * [simplify]: Extracting #7: cost 0 inf + 409081
1552123018.944 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1552123018.944 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1552123018.944 * * * * [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))>
1552123018.945 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552123018.945 * * [simplify]: iters left: 5 (9 enodes)
1552123018.946 * * [simplify]: iters left: 4 (29 enodes)
1552123018.954 * * [simplify]: iters left: 3 (62 enodes)
1552123018.968 * * [simplify]: iters left: 2 (199 enodes)
1552123019.081 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123019.081 * * [simplify]: Extracting #1: cost 20 inf + 0
1552123019.082 * * [simplify]: Extracting #2: cost 94 inf + 1
1552123019.082 * * [simplify]: Extracting #3: cost 162 inf + 1046
1552123019.085 * * [simplify]: Extracting #4: cost 208 inf + 17818
1552123019.091 * * [simplify]: Extracting #5: cost 164 inf + 103714
1552123019.116 * * [simplify]: Extracting #6: cost 47 inf + 336456
1552123019.139 * * [simplify]: Extracting #7: cost 0 inf + 409081
1552123019.155 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1552123019.155 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1552123019.155 * * * * [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))>
1552123019.155 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552123019.155 * * [simplify]: iters left: 5 (9 enodes)
1552123019.157 * * [simplify]: iters left: 4 (29 enodes)
1552123019.162 * * [simplify]: iters left: 3 (62 enodes)
1552123019.173 * * [simplify]: iters left: 2 (199 enodes)
1552123019.241 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123019.241 * * [simplify]: Extracting #1: cost 20 inf + 0
1552123019.242 * * [simplify]: Extracting #2: cost 94 inf + 1
1552123019.243 * * [simplify]: Extracting #3: cost 162 inf + 1046
1552123019.245 * * [simplify]: Extracting #4: cost 208 inf + 17818
1552123019.252 * * [simplify]: Extracting #5: cost 164 inf + 103714
1552123019.276 * * [simplify]: Extracting #6: cost 47 inf + 336456
1552123019.291 * * [simplify]: Extracting #7: cost 0 inf + 409081
1552123019.307 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a)
1552123019.307 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2) a))
1552123019.307 * * * [progress]: adding candidates to table
1552123019.581 * * [progress]: iteration 2 / 4
1552123019.581 * * * [progress]: picking best candidate
1552123019.643 * * * * [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))>
1552123019.643 * * * [progress]: localizing error
1552123019.850 * * * [progress]: generating rewritten candidates
1552123019.850 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1)
1552123019.852 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1552123019.854 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1)
1552123019.865 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1)
1552123019.867 * * * [progress]: generating series expansions
1552123019.867 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1)
1552123019.867 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1552123019.867 * * * * [progress]: [ 3 / 4 ] generating series at (2 1)
1552123019.867 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1)
1552123019.867 * * * [progress]: simplifying candidates
1552123019.867 * * * * [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))>
1552123019.867 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123019.867 * * [simplify]: iters left: 4 (8 enodes)
1552123019.870 * * [simplify]: iters left: 3 (23 enodes)
1552123019.878 * * [simplify]: iters left: 2 (45 enodes)
1552123019.892 * * [simplify]: iters left: 1 (108 enodes)
1552123019.923 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123019.923 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123019.923 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123019.923 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123019.923 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123019.924 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123019.927 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123019.935 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123019.946 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123019.958 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123019.958 * [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))
1552123019.958 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123019.958 * * [simplify]: iters left: 4 (8 enodes)
1552123019.961 * * [simplify]: iters left: 3 (28 enodes)
1552123019.970 * * [simplify]: iters left: 2 (59 enodes)
1552123019.983 * * [simplify]: iters left: 1 (178 enodes)
1552123020.053 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123020.053 * * [simplify]: Extracting #1: cost 12 inf + 0
1552123020.053 * * [simplify]: Extracting #2: cost 64 inf + 1
1552123020.053 * * [simplify]: Extracting #3: cost 140 inf + 403
1552123020.055 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552123020.066 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552123020.087 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552123020.114 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552123020.142 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552123020.166 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552123020.166 * [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))
1552123020.166 * * * * [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))>
1552123020.166 * * * * [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))>
1552123020.166 * * * * [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))>
1552123020.166 * * * * [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))>
1552123020.167 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123020.167 * * [simplify]: iters left: 4 (8 enodes)
1552123020.168 * * [simplify]: iters left: 3 (23 enodes)
1552123020.172 * * [simplify]: iters left: 2 (45 enodes)
1552123020.180 * * [simplify]: iters left: 1 (108 enodes)
1552123020.217 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123020.217 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123020.217 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123020.217 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123020.218 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123020.219 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123020.222 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123020.233 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123020.245 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123020.257 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123020.257 * [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))
1552123020.257 * * * * [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))>
1552123020.258 * [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)))
1552123020.258 * * [simplify]: iters left: 6 (11 enodes)
1552123020.264 * * [simplify]: iters left: 5 (43 enodes)
1552123020.281 * * [simplify]: iters left: 4 (139 enodes)
1552123020.354 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123020.354 * * [simplify]: Extracting #1: cost 32 inf + 0
1552123020.354 * * [simplify]: Extracting #2: cost 85 inf + 0
1552123020.355 * * [simplify]: Extracting #3: cost 152 inf + 1364
1552123020.356 * * [simplify]: Extracting #4: cost 163 inf + 24483
1552123020.361 * * [simplify]: Extracting #5: cost 71 inf + 172897
1552123020.371 * * [simplify]: Extracting #6: cost 3 inf + 277964
1552123020.382 * * [simplify]: Extracting #7: cost 0 inf + 284573
1552123020.393 * [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))))
1552123020.393 * [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))
1552123020.393 * * * * [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))>
1552123020.393 * * * * [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))>
1552123020.393 * * * * [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))>
1552123020.393 * * * * [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))>
1552123020.393 * * * [progress]: adding candidates to table
1552123020.648 * * [progress]: iteration 3 / 4
1552123020.648 * * * [progress]: picking best candidate
1552123020.731 * * * * [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))>
1552123020.731 * * * [progress]: localizing error
1552123020.863 * * * [progress]: generating rewritten candidates
1552123020.863 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1 2)
1552123020.866 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2)
1552123020.869 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1)
1552123020.873 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
1552123020.880 * * * [progress]: generating series expansions
1552123020.880 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1 2)
1552123020.881 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2)
1552123020.881 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1)
1552123020.881 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
1552123020.881 * * * [progress]: simplifying candidates
1552123020.881 * * * * [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))>
1552123020.881 * * * * [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))>
1552123020.881 * * * * [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))>
1552123020.881 * * * * [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))>
1552123020.881 * * * * [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))>
1552123020.881 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123020.881 * * [simplify]: iters left: 4 (8 enodes)
1552123020.885 * * [simplify]: iters left: 3 (23 enodes)
1552123020.893 * * [simplify]: iters left: 2 (45 enodes)
1552123020.909 * * [simplify]: iters left: 1 (108 enodes)
1552123020.972 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123020.972 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123020.972 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123020.972 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123020.973 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123020.974 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123020.977 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123020.988 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123021.001 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123021.014 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123021.014 * [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))
1552123021.014 * * * * [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))>
1552123021.014 * [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)))
1552123021.014 * * [simplify]: iters left: 6 (11 enodes)
1552123021.019 * * [simplify]: iters left: 5 (35 enodes)
1552123021.032 * * [simplify]: iters left: 4 (111 enodes)
1552123021.081 * * [simplify]: iters left: 3 (448 enodes)
1552123021.438 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123021.438 * * [simplify]: Extracting #1: cost 64 inf + 0
1552123021.439 * * [simplify]: Extracting #2: cost 370 inf + 0
1552123021.441 * * [simplify]: Extracting #3: cost 522 inf + 6695
1552123021.450 * * [simplify]: Extracting #4: cost 536 inf + 237314
1552123021.493 * * [simplify]: Extracting #5: cost 132 inf + 950329
1552123021.600 * * [simplify]: Extracting #6: cost 26 inf + 1188087
1552123021.670 * * [simplify]: Extracting #7: cost 0 inf + 1213652
1552123021.744 * * [simplify]: Extracting #8: cost 0 inf + 1213496
1552123021.823 * [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)))))
1552123021.823 * [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))
1552123021.823 * * * * [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))>
1552123021.823 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123021.823 * * [simplify]: iters left: 4 (8 enodes)
1552123021.825 * * [simplify]: iters left: 3 (23 enodes)
1552123021.828 * * [simplify]: iters left: 2 (45 enodes)
1552123021.840 * * [simplify]: iters left: 1 (108 enodes)
1552123021.895 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123021.895 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123021.895 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123021.895 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123021.895 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123021.896 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123021.899 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123021.909 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123021.920 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123021.926 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123021.926 * [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))
1552123021.926 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123021.926 * * [simplify]: iters left: 4 (8 enodes)
1552123021.928 * * [simplify]: iters left: 3 (28 enodes)
1552123021.932 * * [simplify]: iters left: 2 (59 enodes)
1552123021.943 * * [simplify]: iters left: 1 (178 enodes)
1552123021.994 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123021.994 * * [simplify]: Extracting #1: cost 12 inf + 0
1552123021.994 * * [simplify]: Extracting #2: cost 64 inf + 1
1552123021.994 * * [simplify]: Extracting #3: cost 140 inf + 403
1552123021.995 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552123022.001 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552123022.012 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552123022.025 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552123022.039 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552123022.052 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552123022.053 * [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))
1552123022.053 * * * * [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))>
1552123022.053 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123022.053 * * [simplify]: iters left: 4 (8 enodes)
1552123022.054 * * [simplify]: iters left: 3 (23 enodes)
1552123022.058 * * [simplify]: iters left: 2 (45 enodes)
1552123022.065 * * [simplify]: iters left: 1 (108 enodes)
1552123022.092 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123022.092 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123022.092 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123022.092 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123022.093 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123022.093 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123022.097 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123022.106 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123022.118 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123022.131 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123022.131 * [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))
1552123022.132 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123022.132 * * [simplify]: iters left: 4 (8 enodes)
1552123022.135 * * [simplify]: iters left: 3 (28 enodes)
1552123022.144 * * [simplify]: iters left: 2 (59 enodes)
1552123022.160 * * [simplify]: iters left: 1 (178 enodes)
1552123022.225 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123022.225 * * [simplify]: Extracting #1: cost 12 inf + 0
1552123022.225 * * [simplify]: Extracting #2: cost 64 inf + 1
1552123022.225 * * [simplify]: Extracting #3: cost 140 inf + 403
1552123022.227 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552123022.235 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552123022.256 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552123022.284 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552123022.315 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552123022.342 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552123022.342 * [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))
1552123022.342 * * * * [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))>
1552123022.342 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123022.342 * * [simplify]: iters left: 4 (8 enodes)
1552123022.344 * * [simplify]: iters left: 3 (23 enodes)
1552123022.347 * * [simplify]: iters left: 2 (45 enodes)
1552123022.355 * * [simplify]: iters left: 1 (108 enodes)
1552123022.394 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123022.394 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123022.394 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123022.395 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123022.395 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123022.396 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123022.399 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123022.411 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123022.421 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123022.427 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123022.427 * [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))
1552123022.427 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123022.427 * * [simplify]: iters left: 4 (8 enodes)
1552123022.429 * * [simplify]: iters left: 3 (28 enodes)
1552123022.433 * * [simplify]: iters left: 2 (59 enodes)
1552123022.445 * * [simplify]: iters left: 1 (178 enodes)
1552123022.551 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123022.551 * * [simplify]: Extracting #1: cost 12 inf + 0
1552123022.551 * * [simplify]: Extracting #2: cost 64 inf + 1
1552123022.552 * * [simplify]: Extracting #3: cost 140 inf + 403
1552123022.554 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552123022.561 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552123022.582 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552123022.609 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552123022.636 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552123022.664 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552123022.664 * [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))
1552123022.664 * * * * [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))>
1552123022.665 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123022.665 * * [simplify]: iters left: 4 (8 enodes)
1552123022.668 * * [simplify]: iters left: 3 (23 enodes)
1552123022.676 * * [simplify]: iters left: 2 (45 enodes)
1552123022.695 * * [simplify]: iters left: 1 (108 enodes)
1552123022.749 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123022.749 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123022.749 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123022.749 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123022.750 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123022.751 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123022.754 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123022.764 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123022.776 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123022.790 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123022.790 * [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))
1552123022.790 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123022.791 * * [simplify]: iters left: 4 (8 enodes)
1552123022.793 * * [simplify]: iters left: 3 (28 enodes)
1552123022.802 * * [simplify]: iters left: 2 (59 enodes)
1552123022.827 * * [simplify]: iters left: 1 (178 enodes)
1552123022.934 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123022.934 * * [simplify]: Extracting #1: cost 12 inf + 0
1552123022.934 * * [simplify]: Extracting #2: cost 64 inf + 1
1552123022.935 * * [simplify]: Extracting #3: cost 140 inf + 403
1552123022.937 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552123022.944 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552123022.969 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552123022.997 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552123023.013 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552123023.027 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552123023.027 * [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))
1552123023.027 * * * [progress]: adding candidates to table
1552123023.272 * * [progress]: iteration 4 / 4
1552123023.272 * * * [progress]: picking best candidate
1552123023.366 * * * * [pick]: Picked  #<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))>
1552123023.366 * * * [progress]: localizing error
1552123023.493 * * * [progress]: generating rewritten candidates
1552123023.493 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2 2)
1552123023.496 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2 1)
1552123023.499 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1)
1552123023.502 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1)
1552123023.507 * * * [progress]: generating series expansions
1552123023.507 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2 2)
1552123023.508 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2 1)
1552123023.508 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1)
1552123023.508 * * * * [progress]: [ 4 / 4 ] generating series at (2 1)
1552123023.508 * * * [progress]: simplifying candidates
1552123023.508 * * * * [progress]: [ 1 / 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))) (neg.p16 b_2)))) a))>
1552123023.508 * * * * [progress]: [ 2 / 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 (-.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))>
1552123023.508 * * * * [progress]: [ 3 / 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 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))) a))>
1552123023.508 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))>
1552123023.508 * * * * [progress]: [ 5 / 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))) 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))>
1552123023.508 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123023.508 * * [simplify]: iters left: 4 (8 enodes)
1552123023.510 * * [simplify]: iters left: 3 (23 enodes)
1552123023.513 * * [simplify]: iters left: 2 (45 enodes)
1552123023.521 * * [simplify]: iters left: 1 (108 enodes)
1552123023.551 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123023.551 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123023.551 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123023.551 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123023.551 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123023.552 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123023.554 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123023.559 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123023.565 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123023.572 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123023.572 * [simplify]: Simplified (2 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 (+.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 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) a))
1552123023.572 * * * * [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 (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))>
1552123023.572 * [simplify]: Simplifying (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123023.572 * * [simplify]: iters left: 4 (8 enodes)
1552123023.574 * * [simplify]: iters left: 3 (28 enodes)
1552123023.578 * * [simplify]: iters left: 2 (59 enodes)
1552123023.588 * * [simplify]: iters left: 1 (178 enodes)
1552123023.654 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123023.654 * * [simplify]: Extracting #1: cost 12 inf + 0
1552123023.654 * * [simplify]: Extracting #2: cost 64 inf + 1
1552123023.655 * * [simplify]: Extracting #3: cost 140 inf + 403
1552123023.656 * * [simplify]: Extracting #4: cost 189 inf + 12881
1552123023.659 * * [simplify]: Extracting #5: cost 149 inf + 112868
1552123023.671 * * [simplify]: Extracting #6: cost 32 inf + 315911
1552123023.685 * * [simplify]: Extracting #7: cost 1 inf + 362422
1552123023.699 * * [simplify]: Extracting #8: cost 0 inf + 365106
1552123023.715 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)
1552123023.715 * [simplify]: Simplified (2 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 c a))) b_2)) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) b_2)) a))
1552123023.715 * * * * [progress]: [ 7 / 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))>
1552123023.716 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123023.716 * * [simplify]: iters left: 4 (8 enodes)
1552123023.717 * * [simplify]: iters left: 3 (23 enodes)
1552123023.720 * * [simplify]: iters left: 2 (45 enodes)
1552123023.728 * * [simplify]: iters left: 1 (108 enodes)
1552123023.754 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123023.754 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123023.754 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123023.754 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123023.755 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123023.755 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123023.757 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123023.762 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123023.768 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123023.774 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123023.774 * [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))
1552123023.775 * * * * [progress]: [ 8 / 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))>
1552123023.775 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123023.775 * * [simplify]: iters left: 4 (8 enodes)
1552123023.776 * * [simplify]: iters left: 3 (23 enodes)
1552123023.781 * * [simplify]: iters left: 2 (45 enodes)
1552123023.788 * * [simplify]: iters left: 1 (108 enodes)
1552123023.814 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123023.814 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123023.814 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123023.814 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123023.814 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123023.815 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123023.816 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123023.821 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123023.828 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123023.835 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123023.835 * [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))
1552123023.835 * * * * [progress]: [ 9 / 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))>
1552123023.835 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123023.835 * * [simplify]: iters left: 4 (8 enodes)
1552123023.837 * * [simplify]: iters left: 3 (23 enodes)
1552123023.840 * * [simplify]: iters left: 2 (45 enodes)
1552123023.847 * * [simplify]: iters left: 1 (108 enodes)
1552123023.874 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123023.874 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123023.874 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123023.874 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123023.875 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123023.875 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123023.877 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123023.882 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123023.888 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123023.895 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123023.895 * [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))
1552123023.895 * * * * [progress]: [ 10 / 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))>
1552123023.895 * [simplify]: Simplifying (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)
1552123023.895 * * [simplify]: iters left: 4 (8 enodes)
1552123023.897 * * [simplify]: iters left: 3 (23 enodes)
1552123023.900 * * [simplify]: iters left: 2 (45 enodes)
1552123023.907 * * [simplify]: iters left: 1 (108 enodes)
1552123023.938 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123023.938 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123023.938 * * [simplify]: Extracting #2: cost 3 inf + 1
1552123023.938 * * [simplify]: Extracting #3: cost 17 inf + 1
1552123023.938 * * [simplify]: Extracting #4: cost 55 inf + 322
1552123023.938 * * [simplify]: Extracting #5: cost 80 inf + 11197
1552123023.940 * * [simplify]: Extracting #6: cost 84 inf + 56173
1552123023.945 * * [simplify]: Extracting #7: cost 7 inf + 177856
1552123023.951 * * [simplify]: Extracting #8: cost 0 inf + 193436
1552123023.958 * [simplify]: Simplified to (+.p16 b_2 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))
1552123023.958 * [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))
1552123023.958 * * * [progress]: adding candidates to table
1552123024.394 * [progress]: [Phase 3 of 3] Extracting.
1552123024.395 * * [regime]: Finding splitpoints for: (#<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 (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (-.p16 (*.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))))) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (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))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.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 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (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 (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 (*.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))>)
1552123024.399 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2)
1552123024.400 * * * * [regimes]: Trying to branch on c from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.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)))) 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 (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))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.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 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (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 (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 (*.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))>)
1552123024.882 * * * * [regimes]: Trying to branch on a from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.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)))) 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 (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))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.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 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (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 (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 (*.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))>)
1552123025.294 * * * * [regimes]: Trying to branch on b_2 from (#<alt (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (/.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)))) 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 (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))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2)))) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.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 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 c a) (*.p16 c a))) (+.p16 (*.p16 b_2 b_2) (*.p16 c a)))) b_2) a))> #<alt (λ (a b_2 c) (/.p16 (/.p16 (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (-.p16 (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) (*.p16 b_2 b_2))) (*.p16 (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) (+.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) a))> #<alt (λ (a b_2 c) (/.p16 (-.p16 (*.p16 (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 (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 (*.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))>)
1552123025.745 * * * [regime]: Found split indices: #<option (#s(si 2 256))>
1552123025.745 * [simplify]: Simplifying (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552123025.746 * * [simplify]: iters left: 5 (9 enodes)
1552123025.746 * * [simplify]: Extracting #0: cost 1 inf + 0
1552123025.746 * * [simplify]: Extracting #1: cost 3 inf + 0
1552123025.746 * * [simplify]: Extracting #2: cost 4 inf + 1
1552123025.746 * * [simplify]: Extracting #3: cost 4 inf + 2
1552123025.746 * * [simplify]: Extracting #4: cost 6 inf + 2
1552123025.746 * * [simplify]: Extracting #5: cost 6 inf + 323
1552123025.747 * * [simplify]: Extracting #6: cost 0 inf + 4258
1552123025.747 * [simplify]: Simplified to (/.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) a)
1552123025.747 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000
1552123025.800 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision
1552123025.801 * * * * [points]: Setting MPFR precision to 64
1552123025.803 * * * * [points]: Setting MPFR precision to 320
1552123025.804 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision
1552123025.805 * * * * [points]: Setting MPFR precision to 64
1552123025.808 * * * * [points]: Setting MPFR precision to 320
1552123025.813 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision
1552123025.815 * * * * [points]: Setting MPFR precision to 64
1552123025.822 * * * * [points]: Setting MPFR precision to 320
1552123025.830 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision
1552123025.832 * * * * [points]: Setting MPFR precision to 64
1552123025.845 * * * * [points]: Setting MPFR precision to 320
1552123025.882 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision
1552123025.885 * * * * [points]: Setting MPFR precision to 64
1552123025.913 * * * * [points]: Setting MPFR precision to 320
1552123025.944 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision
1552123025.946 * * * * [points]: Setting MPFR precision to 64
1552123026.000 * * * * [points]: Setting MPFR precision to 320
1552123026.058 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision
1552123026.059 * * * * [points]: Setting MPFR precision to 64
1552123026.159 * * * * [points]: Setting MPFR precision to 320
1552123026.295 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision
1552123026.296 * * * * [points]: Setting MPFR precision to 64
1552123026.461 * * * * [points]: Setting MPFR precision to 320
1552123026.702 * * * * [points]: Computing exacts for 8000 points
1552123026.705 * * * * [points]: Setting MPFR precision to 64
1552123028.300 * * * * [points]: Setting MPFR precision to 320
1552123029.390 * * * * [points]: Filtering points with unrepresentable outputs
1552123029.837 * * * * [points]: Sampling 1986 additional inputs, on iter 1 have 6014 / 8000
1552123029.852 * * * * [points]: Computing exacts on every 124 of 1986 points to ramp up precision
1552123029.854 * * * * [points]: Setting MPFR precision to 64
1552123029.856 * * * * [points]: Setting MPFR precision to 320
1552123029.859 * * * * [points]: Computing exacts on every 62 of 1986 points to ramp up precision
1552123029.860 * * * * [points]: Setting MPFR precision to 64
1552123029.865 * * * * [points]: Setting MPFR precision to 320
1552123029.870 * * * * [points]: Computing exacts on every 31 of 1986 points to ramp up precision
1552123029.872 * * * * [points]: Setting MPFR precision to 64
1552123029.879 * * * * [points]: Setting MPFR precision to 320
1552123029.888 * * * * [points]: Computing exacts on every 15 of 1986 points to ramp up precision
1552123029.890 * * * * [points]: Setting MPFR precision to 64
1552123029.904 * * * * [points]: Setting MPFR precision to 320
1552123029.922 * * * * [points]: Computing exacts on every 7 of 1986 points to ramp up precision
1552123029.924 * * * * [points]: Setting MPFR precision to 64
1552123029.977 * * * * [points]: Setting MPFR precision to 320
1552123030.012 * * * * [points]: Computing exacts on every 3 of 1986 points to ramp up precision
1552123030.014 * * * * [points]: Setting MPFR precision to 64
1552123030.057 * * * * [points]: Setting MPFR precision to 320
1552123030.115 * * * * [points]: Computing exacts for 1986 points
1552123030.117 * * * * [points]: Setting MPFR precision to 64
1552123030.402 * * * * [points]: Setting MPFR precision to 320
1552123030.826 * * * * [points]: Filtering points with unrepresentable outputs
1552123031.045 * * * * [points]: Sampling 499 additional inputs, on iter 2 have 7501 / 8000
1552123031.049 * * * * [points]: Computing exacts on every 31 of 499 points to ramp up precision
1552123031.051 * * * * [points]: Setting MPFR precision to 64
1552123031.054 * * * * [points]: Setting MPFR precision to 320
1552123031.056 * * * * [points]: Computing exacts on every 15 of 499 points to ramp up precision
1552123031.058 * * * * [points]: Setting MPFR precision to 64
1552123031.062 * * * * [points]: Setting MPFR precision to 320
1552123031.067 * * * * [points]: Computing exacts on every 7 of 499 points to ramp up precision
1552123031.069 * * * * [points]: Setting MPFR precision to 64
1552123031.077 * * * * [points]: Setting MPFR precision to 320
1552123031.087 * * * * [points]: Computing exacts on every 3 of 499 points to ramp up precision
1552123031.089 * * * * [points]: Setting MPFR precision to 64
1552123031.104 * * * * [points]: Setting MPFR precision to 320
1552123031.122 * * * * [points]: Computing exacts for 499 points
1552123031.124 * * * * [points]: Setting MPFR precision to 64
1552123031.183 * * * * [points]: Setting MPFR precision to 320
1552123031.304 * * * * [points]: Filtering points with unrepresentable outputs
1552123031.352 * * * * [points]: Sampling 127 additional inputs, on iter 3 have 7873 / 8000
1552123031.354 * * * * [points]: Computing exacts on every 7 of 127 points to ramp up precision
1552123031.356 * * * * [points]: Setting MPFR precision to 64
1552123031.358 * * * * [points]: Setting MPFR precision to 320
1552123031.361 * * * * [points]: Computing exacts on every 3 of 127 points to ramp up precision
1552123031.362 * * * * [points]: Setting MPFR precision to 64
1552123031.366 * * * * [points]: Setting MPFR precision to 320
1552123031.371 * * * * [points]: Computing exacts for 127 points
1552123031.373 * * * * [points]: Setting MPFR precision to 64
1552123031.388 * * * * [points]: Setting MPFR precision to 320
1552123031.407 * * * * [points]: Filtering points with unrepresentable outputs
1552123031.420 * * * * [points]: Sampling 32 additional inputs, on iter 4 have 7968 / 8000
1552123031.420 * * * * [points]: Computing exacts on every 2 of 32 points to ramp up precision
1552123031.422 * * * * [points]: Setting MPFR precision to 64
1552123031.424 * * * * [points]: Setting MPFR precision to 320
1552123031.425 * * * * [points]: Computing exacts for 32 points
1552123031.426 * * * * [points]: Setting MPFR precision to 64
1552123031.430 * * * * [points]: Setting MPFR precision to 320
1552123031.435 * * * * [points]: Filtering points with unrepresentable outputs
1552123031.438 * * * * [points]: Sampling 10 additional inputs, on iter 5 have 7990 / 8000
1552123031.438 * * * * [points]: Computing exacts for 10 points
1552123031.440 * * * * [points]: Setting MPFR precision to 64
1552123031.441 * * * * [points]: Setting MPFR precision to 320
1552123031.443 * * * * [points]: Filtering points with unrepresentable outputs
1552123031.444 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 7997 / 8000
1552123031.444 * * * * [points]: Computing exacts for 4 points
1552123031.445 * * * * [points]: Setting MPFR precision to 64
1552123031.446 * * * * [points]: Setting MPFR precision to 320
1552123031.447 * * * * [points]: Filtering points with unrepresentable outputs
1552123031.447 * * * * [points]: Sampled 8001 points with exact outputs
1552123034.086 * [regime-testing]: Baseline error score: 64.0
1552123034.089 * [regime-testing]: Oracle error score: 64.0
1552123034.093 * [regime-testing]: End program error score: 2.3499374313572483