0.003 * [progress]: [Phase 1 of 3] Setting up. 0.005 * * * [progress]: [1/2] Preparing points 0.037 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.042 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.150 * * * * [points]: Setting MPFR precision to 64 0.154 * * * * [points]: Setting MPFR precision to 320 0.156 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.158 * * * * [points]: Setting MPFR precision to 64 0.161 * * * * [points]: Setting MPFR precision to 320 0.164 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.167 * * * * [points]: Setting MPFR precision to 64 0.172 * * * * [points]: Setting MPFR precision to 320 0.178 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.180 * * * * [points]: Setting MPFR precision to 64 0.189 * * * * [points]: Setting MPFR precision to 320 0.247 * * * * [points]: Computing exacts for 256 points 0.251 * * * * [points]: Setting MPFR precision to 64 0.281 * * * * [points]: Setting MPFR precision to 320 0.311 * * * * [points]: Filtering points with unrepresentable outputs 0.313 * * * * [points]: Sampled 256 points with exact outputs 0.314 * * * [progress]: [2/2] Setting up program. 0.333 * [progress]: [Phase 2 of 3] Improving. 0.334 * * * * [progress]: [ 1 / 1 ] simplifiying candidate # 0.337 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a) 0.339 * * [simplify]: iters left: 5 (10 enodes) 0.350 * * [simplify]: iters left: 4 (31 enodes) 0.361 * * [simplify]: iters left: 3 (65 enodes) 0.386 * * [simplify]: iters left: 2 (207 enodes) 0.910 * * [simplify]: Extracting #0: cost 1 inf + 0 0.910 * * [simplify]: Extracting #1: cost 20 inf + 0 0.911 * * [simplify]: Extracting #2: cost 89 inf + 1 0.911 * * [simplify]: Extracting #3: cost 168 inf + 83 0.912 * * [simplify]: Extracting #4: cost 227 inf + 12401 0.916 * * [simplify]: Extracting #5: cost 180 inf + 98398 0.928 * * [simplify]: Extracting #6: cost 61 inf + 349602 0.950 * * [simplify]: Extracting #7: cost 2 inf + 436444 0.967 * * [simplify]: Extracting #8: cost 0 inf + 442330 0.986 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a) 0.986 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)) 1.009 * * [progress]: iteration 1 / 4 1.009 * * * [progress]: picking best candidate 1.027 * * * * [pick]: Picked # 1.027 * * * [progress]: localizing error 1.184 * * * [progress]: generating rewritten candidates 1.184 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 1.187 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 1.187 * * * * [progress]: [ 3 / 4 ] rewriting at (2) 1.190 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 1.194 * * * [progress]: generating series expansions 1.194 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 1.194 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 1.194 * * * * [progress]: [ 3 / 4 ] generating series at (2) 1.195 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 1.195 * * * [progress]: simplifying candidates 1.195 * * * * [progress]: [ 1 / 9 ] simplifiying candidate # 1.195 * * * * [progress]: [ 2 / 9 ] simplifiying candidate # 1.195 * * * * [progress]: [ 3 / 9 ] simplifiying candidate # 1.195 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))) 1.195 * * [simplify]: iters left: 5 (11 enodes) 1.198 * * [simplify]: iters left: 4 (35 enodes) 1.211 * * [simplify]: iters left: 3 (100 enodes) 1.264 * * [simplify]: iters left: 2 (360 enodes) 1.530 * * [simplify]: Extracting #0: cost 1 inf + 0 1.530 * * [simplify]: Extracting #1: cost 48 inf + 0 1.531 * * [simplify]: Extracting #2: cost 223 inf + 0 1.536 * * [simplify]: Extracting #3: cost 348 inf + 45039 1.567 * * [simplify]: Extracting #4: cost 315 inf + 336131 1.627 * * [simplify]: Extracting #5: cost 84 inf + 852438 1.687 * * [simplify]: Extracting #6: cost 1 inf + 990774 1.734 * * [simplify]: Extracting #7: cost 0 inf + 992777 1.816 * [simplify]: Simplified to (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) 1.817 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c))))))) 1.817 * * * * [progress]: [ 4 / 9 ] simplifiying candidate # 1.817 * * * * [progress]: [ 5 / 9 ] simplifiying candidate # 1.817 * * * * [progress]: [ 6 / 9 ] simplifiying candidate # 1.817 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a) 1.817 * * [simplify]: iters left: 5 (10 enodes) 1.822 * * [simplify]: iters left: 4 (31 enodes) 1.831 * * [simplify]: iters left: 3 (65 enodes) 1.845 * * [simplify]: iters left: 2 (207 enodes) 1.951 * * [simplify]: Extracting #0: cost 1 inf + 0 1.951 * * [simplify]: Extracting #1: cost 20 inf + 0 1.951 * * [simplify]: Extracting #2: cost 89 inf + 1 1.951 * * [simplify]: Extracting #3: cost 168 inf + 83 1.952 * * [simplify]: Extracting #4: cost 227 inf + 12401 1.957 * * [simplify]: Extracting #5: cost 180 inf + 98398 1.968 * * [simplify]: Extracting #6: cost 61 inf + 349602 1.986 * * [simplify]: Extracting #7: cost 2 inf + 436444 2.010 * * [simplify]: Extracting #8: cost 0 inf + 442330 2.027 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a) 2.027 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)) 2.027 * * * * [progress]: [ 7 / 9 ] simplifiying candidate # 2.028 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a) 2.028 * * [simplify]: iters left: 5 (10 enodes) 2.030 * * [simplify]: iters left: 4 (31 enodes) 2.037 * * [simplify]: iters left: 3 (65 enodes) 2.063 * * [simplify]: iters left: 2 (207 enodes) 2.175 * * [simplify]: Extracting #0: cost 1 inf + 0 2.175 * * [simplify]: Extracting #1: cost 20 inf + 0 2.175 * * [simplify]: Extracting #2: cost 89 inf + 1 2.176 * * [simplify]: Extracting #3: cost 168 inf + 83 2.182 * * [simplify]: Extracting #4: cost 227 inf + 12401 2.188 * * [simplify]: Extracting #5: cost 180 inf + 98398 2.211 * * [simplify]: Extracting #6: cost 61 inf + 349602 2.234 * * [simplify]: Extracting #7: cost 2 inf + 436444 2.251 * * [simplify]: Extracting #8: cost 0 inf + 442330 2.272 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a) 2.273 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)) 2.273 * * * * [progress]: [ 8 / 9 ] simplifiying candidate # 2.273 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a) 2.273 * * [simplify]: iters left: 5 (10 enodes) 2.275 * * [simplify]: iters left: 4 (31 enodes) 2.280 * * [simplify]: iters left: 3 (65 enodes) 2.293 * * [simplify]: iters left: 2 (207 enodes) 2.390 * * [simplify]: Extracting #0: cost 1 inf + 0 2.391 * * [simplify]: Extracting #1: cost 20 inf + 0 2.391 * * [simplify]: Extracting #2: cost 89 inf + 1 2.392 * * [simplify]: Extracting #3: cost 168 inf + 83 2.394 * * [simplify]: Extracting #4: cost 227 inf + 12401 2.403 * * [simplify]: Extracting #5: cost 180 inf + 98398 2.418 * * [simplify]: Extracting #6: cost 61 inf + 349602 2.434 * * [simplify]: Extracting #7: cost 2 inf + 436444 2.450 * * [simplify]: Extracting #8: cost 0 inf + 442330 2.467 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a) 2.467 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)) 2.467 * * * * [progress]: [ 9 / 9 ] simplifiying candidate # 2.467 * [simplify]: Simplifying (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a) 2.467 * * [simplify]: iters left: 5 (10 enodes) 2.469 * * [simplify]: iters left: 4 (31 enodes) 2.476 * * [simplify]: iters left: 3 (65 enodes) 2.499 * * [simplify]: iters left: 2 (207 enodes) 2.586 * * [simplify]: Extracting #0: cost 1 inf + 0 2.586 * * [simplify]: Extracting #1: cost 20 inf + 0 2.587 * * [simplify]: Extracting #2: cost 89 inf + 1 2.587 * * [simplify]: Extracting #3: cost 168 inf + 83 2.589 * * [simplify]: Extracting #4: cost 227 inf + 12401 2.599 * * [simplify]: Extracting #5: cost 180 inf + 98398 2.622 * * [simplify]: Extracting #6: cost 61 inf + 349602 2.656 * * [simplify]: Extracting #7: cost 2 inf + 436444 2.690 * * [simplify]: Extracting #8: cost 0 inf + 442330 2.723 * [simplify]: Simplified to (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a) 2.723 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a)))) a)) 2.723 * * * [progress]: adding candidates to table 2.935 * * [progress]: iteration 2 / 4 2.935 * * * [progress]: picking best candidate 2.975 * * * * [pick]: Picked # 2.975 * * * [progress]: localizing error 3.242 * * * [progress]: generating rewritten candidates 3.242 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2 2) 3.245 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 3.247 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2 2) 3.248 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2 2 1) 3.253 * * * [progress]: generating series expansions 3.253 * * * * [progress]: [ 1 / 4 ] generating series at (2 2 2) 3.253 * * * * [progress]: [ 2 / 4 ] generating series at (2) 3.253 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2 2) 3.253 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2 2 1) 3.253 * * * [progress]: simplifying candidates 3.253 * * * * [progress]: [ 1 / 8 ] simplifiying candidate # 3.254 * * * * [progress]: [ 2 / 8 ] simplifiying candidate # 3.254 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) 3.254 * * [simplify]: iters left: 4 (9 enodes) 3.258 * * [simplify]: iters left: 3 (24 enodes) 3.265 * * [simplify]: iters left: 2 (47 enodes) 3.281 * * [simplify]: iters left: 1 (110 enodes) 3.316 * * [simplify]: Extracting #0: cost 1 inf + 0 3.316 * * [simplify]: Extracting #1: cost 6 inf + 0 3.316 * * [simplify]: Extracting #2: cost 10 inf + 1 3.316 * * [simplify]: Extracting #3: cost 23 inf + 403 3.317 * * [simplify]: Extracting #4: cost 60 inf + 1445 3.318 * * [simplify]: Extracting #5: cost 79 inf + 13843 3.321 * * [simplify]: Extracting #6: cost 73 inf + 57826 3.330 * * [simplify]: Extracting #7: cost 3 inf + 171780 3.336 * * [simplify]: Extracting #8: cost 0 inf + 178629 3.342 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) 3.342 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 3.342 * * * * [progress]: [ 3 / 8 ] simplifiying candidate # 3.342 * * * * [progress]: [ 4 / 8 ] simplifiying candidate # 3.342 * * * * [progress]: [ 5 / 8 ] simplifiying candidate # 3.342 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) 3.342 * * [simplify]: iters left: 6 (15 enodes) 3.345 * * [simplify]: iters left: 5 (47 enodes) 3.354 * * [simplify]: iters left: 4 (100 enodes) 3.390 * * [simplify]: iters left: 3 (250 enodes) 3.560 * * [simplify]: Extracting #0: cost 1 inf + 0 3.560 * * [simplify]: Extracting #1: cost 7 inf + 0 3.560 * * [simplify]: Extracting #2: cost 38 inf + 0 3.561 * * [simplify]: Extracting #3: cost 89 inf + 404 3.562 * * [simplify]: Extracting #4: cost 105 inf + 13282 3.565 * * [simplify]: Extracting #5: cost 75 inf + 74603 3.571 * * [simplify]: Extracting #6: cost 45 inf + 171652 3.585 * * [simplify]: Extracting #7: cost 3 inf + 235044 3.601 * * [simplify]: Extracting #8: cost 0 inf + 242171 3.610 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 3.610 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))) 3.610 * * * * [progress]: [ 6 / 8 ] simplifiying candidate # 3.611 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) 3.611 * * [simplify]: iters left: 6 (15 enodes) 3.614 * * [simplify]: iters left: 5 (47 enodes) 3.623 * * [simplify]: iters left: 4 (100 enodes) 3.659 * * [simplify]: iters left: 3 (250 enodes) 3.835 * * [simplify]: Extracting #0: cost 1 inf + 0 3.835 * * [simplify]: Extracting #1: cost 7 inf + 0 3.835 * * [simplify]: Extracting #2: cost 38 inf + 0 3.836 * * [simplify]: Extracting #3: cost 89 inf + 404 3.837 * * [simplify]: Extracting #4: cost 105 inf + 13282 3.843 * * [simplify]: Extracting #5: cost 75 inf + 74603 3.856 * * [simplify]: Extracting #6: cost 45 inf + 171652 3.872 * * [simplify]: Extracting #7: cost 3 inf + 235044 3.890 * * [simplify]: Extracting #8: cost 0 inf + 242171 3.909 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 3.909 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))) 3.909 * * * * [progress]: [ 7 / 8 ] simplifiying candidate # 3.909 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) 3.909 * * [simplify]: iters left: 6 (15 enodes) 3.916 * * [simplify]: iters left: 5 (47 enodes) 3.936 * * [simplify]: iters left: 4 (100 enodes) 3.974 * * [simplify]: iters left: 3 (250 enodes) 4.143 * * [simplify]: Extracting #0: cost 1 inf + 0 4.143 * * [simplify]: Extracting #1: cost 7 inf + 0 4.143 * * [simplify]: Extracting #2: cost 38 inf + 0 4.144 * * [simplify]: Extracting #3: cost 89 inf + 404 4.146 * * [simplify]: Extracting #4: cost 105 inf + 13282 4.152 * * [simplify]: Extracting #5: cost 75 inf + 74603 4.165 * * [simplify]: Extracting #6: cost 45 inf + 171652 4.181 * * [simplify]: Extracting #7: cost 3 inf + 235044 4.200 * * [simplify]: Extracting #8: cost 0 inf + 242171 4.218 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 4.218 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))) 4.218 * * * * [progress]: [ 8 / 8 ] simplifiying candidate # 4.218 * [simplify]: Simplifying (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) 4.218 * * [simplify]: iters left: 6 (15 enodes) 4.225 * * [simplify]: iters left: 5 (47 enodes) 4.243 * * [simplify]: iters left: 4 (100 enodes) 4.285 * * [simplify]: iters left: 3 (250 enodes) 4.494 * * [simplify]: Extracting #0: cost 1 inf + 0 4.494 * * [simplify]: Extracting #1: cost 7 inf + 0 4.494 * * [simplify]: Extracting #2: cost 38 inf + 0 4.498 * * [simplify]: Extracting #3: cost 89 inf + 404 4.500 * * [simplify]: Extracting #4: cost 105 inf + 13282 4.506 * * [simplify]: Extracting #5: cost 75 inf + 74603 4.518 * * [simplify]: Extracting #6: cost 45 inf + 171652 4.528 * * [simplify]: Extracting #7: cost 3 inf + 235044 4.537 * * [simplify]: Extracting #8: cost 0 inf + 242171 4.546 * [simplify]: Simplified to (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 4.546 * [simplify]: Simplified (2) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2)))) 4.546 * * * [progress]: adding candidates to table 4.799 * * [progress]: iteration 3 / 4 4.799 * * * [progress]: picking best candidate 4.834 * * * * [pick]: Picked # 4.834 * * * [progress]: localizing error 5.092 * * * [progress]: generating rewritten candidates 5.092 * * * * [progress]: [ 1 / 4 ] rewriting at (2 2) 5.095 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 5.096 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2) 5.097 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 5.100 * * * [progress]: generating series expansions 5.100 * * * * [progress]: [ 1 / 4 ] generating series at (2 2) 5.100 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 5.100 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2) 5.100 * * * * [progress]: [ 4 / 4 ] generating series at (2) 5.100 * * * [progress]: simplifying candidates 5.100 * * * * [progress]: [ 1 / 6 ] simplifiying candidate # 5.100 * * * * [progress]: [ 2 / 6 ] simplifiying candidate # 5.101 * [simplify]: Simplifying (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) 5.101 * * [simplify]: iters left: 4 (9 enodes) 5.102 * * [simplify]: iters left: 3 (24 enodes) 5.107 * * [simplify]: iters left: 2 (53 enodes) 5.118 * * [simplify]: iters left: 1 (140 enodes) 5.232 * * [simplify]: Extracting #0: cost 1 inf + 0 5.232 * * [simplify]: Extracting #1: cost 24 inf + 0 5.233 * * [simplify]: Extracting #2: cost 70 inf + 0 5.233 * * [simplify]: Extracting #3: cost 62 inf + 3454 5.237 * * [simplify]: Extracting #4: cost 19 inf + 33897 5.239 * * [simplify]: Extracting #5: cost 0 inf + 53655 5.242 * [simplify]: Simplified to (+.p16 (*.p16 c a) (real->posit16 0.0)) 5.242 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 c a) (real->posit16 0.0)) (*.p16 (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) a))) 5.242 * * * * [progress]: [ 3 / 6 ] simplifiying candidate # 5.242 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) 5.242 * * [simplify]: iters left: 4 (9 enodes) 5.244 * * [simplify]: iters left: 3 (24 enodes) 5.248 * * [simplify]: iters left: 2 (47 enodes) 5.256 * * [simplify]: iters left: 1 (110 enodes) 5.282 * * [simplify]: Extracting #0: cost 1 inf + 0 5.283 * * [simplify]: Extracting #1: cost 6 inf + 0 5.283 * * [simplify]: Extracting #2: cost 10 inf + 1 5.283 * * [simplify]: Extracting #3: cost 23 inf + 403 5.283 * * [simplify]: Extracting #4: cost 60 inf + 1445 5.283 * * [simplify]: Extracting #5: cost 79 inf + 13843 5.285 * * [simplify]: Extracting #6: cost 73 inf + 57826 5.290 * * [simplify]: Extracting #7: cost 3 inf + 171780 5.295 * * [simplify]: Extracting #8: cost 0 inf + 178629 5.303 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) 5.303 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 5.303 * * * * [progress]: [ 4 / 6 ] simplifiying candidate # 5.304 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) 5.304 * * [simplify]: iters left: 4 (9 enodes) 5.305 * * [simplify]: iters left: 3 (24 enodes) 5.309 * * [simplify]: iters left: 2 (47 enodes) 5.319 * * [simplify]: iters left: 1 (110 enodes) 5.359 * * [simplify]: Extracting #0: cost 1 inf + 0 5.360 * * [simplify]: Extracting #1: cost 6 inf + 0 5.360 * * [simplify]: Extracting #2: cost 10 inf + 1 5.360 * * [simplify]: Extracting #3: cost 23 inf + 403 5.360 * * [simplify]: Extracting #4: cost 60 inf + 1445 5.360 * * [simplify]: Extracting #5: cost 79 inf + 13843 5.362 * * [simplify]: Extracting #6: cost 73 inf + 57826 5.367 * * [simplify]: Extracting #7: cost 3 inf + 171780 5.373 * * [simplify]: Extracting #8: cost 0 inf + 178629 5.379 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) 5.379 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 5.379 * * * * [progress]: [ 5 / 6 ] simplifiying candidate # 5.379 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) 5.379 * * [simplify]: iters left: 4 (9 enodes) 5.381 * * [simplify]: iters left: 3 (24 enodes) 5.384 * * [simplify]: iters left: 2 (47 enodes) 5.393 * * [simplify]: iters left: 1 (110 enodes) 5.419 * * [simplify]: Extracting #0: cost 1 inf + 0 5.419 * * [simplify]: Extracting #1: cost 6 inf + 0 5.419 * * [simplify]: Extracting #2: cost 10 inf + 1 5.419 * * [simplify]: Extracting #3: cost 23 inf + 403 5.419 * * [simplify]: Extracting #4: cost 60 inf + 1445 5.420 * * [simplify]: Extracting #5: cost 79 inf + 13843 5.421 * * [simplify]: Extracting #6: cost 73 inf + 57826 5.426 * * [simplify]: Extracting #7: cost 3 inf + 171780 5.432 * * [simplify]: Extracting #8: cost 0 inf + 178629 5.438 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) 5.438 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 5.438 * * * * [progress]: [ 6 / 6 ] simplifiying candidate # 5.438 * [simplify]: Simplifying (+.p16 (neg.p16 b_2) (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))) 5.438 * * [simplify]: iters left: 4 (9 enodes) 5.440 * * [simplify]: iters left: 3 (24 enodes) 5.443 * * [simplify]: iters left: 2 (47 enodes) 5.451 * * [simplify]: iters left: 1 (110 enodes) 5.478 * * [simplify]: Extracting #0: cost 1 inf + 0 5.478 * * [simplify]: Extracting #1: cost 6 inf + 0 5.478 * * [simplify]: Extracting #2: cost 10 inf + 1 5.479 * * [simplify]: Extracting #3: cost 23 inf + 403 5.479 * * [simplify]: Extracting #4: cost 60 inf + 1445 5.479 * * [simplify]: Extracting #5: cost 79 inf + 13843 5.481 * * [simplify]: Extracting #6: cost 73 inf + 57826 5.486 * * [simplify]: Extracting #7: cost 3 inf + 171780 5.492 * * [simplify]: Extracting #8: cost 0 inf + 178629 5.498 * [simplify]: Simplified to (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2) 5.498 * [simplify]: Simplified (2 2) to (λ (a b_2 c) (/.p16 (/.p16 (+.p16 (*.p16 a c) (*.p16 (+.p16 (neg.p16 b_2) b_2) (+.p16 (neg.p16 b_2) (neg.p16 b_2)))) a) (-.p16 (sqrt.p16 (-.p16 (*.p16 b_2 b_2) (*.p16 c a))) b_2))) 5.498 * * * [progress]: adding candidates to table 5.627 * * [progress]: iteration 4 / 4 5.627 * * * [progress]: picking best candidate 5.647 * * * * [pick]: Picked # 5.647 * * * [progress]: localizing error 5.868 * * * [progress]: generating rewritten candidates 5.868 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2 1) 5.876 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 5.878 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 5.878 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 5.881 * * * [progress]: generating series expansions 5.881 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2 1) 5.881 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 5.881 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 5.881 * * * * [progress]: [ 4 / 4 ] generating series at (2) 5.881 * * * [progress]: simplifying candidates 5.881 * * * * [progress]: [ 1 / 9 ] simplifiying candidate # 5.881 * [simplify]: Simplifying (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) 5.882 * * [simplify]: iters left: 2 (6 enodes) 5.883 * * [simplify]: iters left: 1 (14 enodes) 5.885 * * [simplify]: Extracting #0: cost 1 inf + 0 5.885 * * [simplify]: Extracting #1: cost 3 inf + 0 5.885 * * [simplify]: Extracting #2: cost 6 inf + 0 5.885 * * [simplify]: Extracting #3: cost 2 inf + 325 5.885 * * [simplify]: Extracting #4: cost 0 inf + 1329 5.885 * [simplify]: Simplified to (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) 5.885 * [simplify]: Simplified (2 1 2 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (+.p16 (*.p16 c a) (*.p16 b_2 b_2)) (/.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (-.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) a)) 5.885 * * * * [progress]: [ 2 / 9 ] simplifiying candidate # 5.885 * [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 a c) (*.p16 a c)) (*.p16 (*.p16 a c) (*.p16 a c)))) 5.885 * * [simplify]: iters left: 4 (10 enodes) 5.887 * * [simplify]: iters left: 3 (43 enodes) 5.896 * * [simplify]: iters left: 2 (121 enodes) 5.954 * * [simplify]: iters left: 1 (429 enodes) 6.247 * * [simplify]: Extracting #0: cost 1 inf + 0 6.248 * * [simplify]: Extracting #1: cost 46 inf + 0 6.249 * * [simplify]: Extracting #2: cost 270 inf + 0 6.253 * * [simplify]: Extracting #3: cost 354 inf + 59003 6.280 * * [simplify]: Extracting #4: cost 345 inf + 369227 6.347 * * [simplify]: Extracting #5: cost 22 inf + 1102360 6.452 * * [simplify]: Extracting #6: cost 1 inf + 1150488 6.559 * * [simplify]: Extracting #7: cost 0 inf + 1155051 6.667 * [simplify]: Simplified to (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) 6.668 * [simplify]: Simplified (2 1 2 1 1) to (λ (a b_2 c) (/.p16 (-.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (*.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 (*.p16 a c) (*.p16 a c)) (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)))) (*.p16 (+.p16 (*.p16 b_2 b_2) (*.p16 a c)) (+.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))))))) a)) 6.668 * * * * [progress]: [ 3 / 9 ] simplifiying candidate # 6.668 * * * * [progress]: [ 4 / 9 ] simplifiying candidate # 6.668 * * * * [progress]: [ 5 / 9 ] simplifiying candidate # 6.668 * [simplify]: Simplifying (-.p16 (*.p16 (neg.p16 b_2) (neg.p16 b_2)) (*.p16 (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))))) 6.669 * * [simplify]: iters left: 6 (15 enodes) 6.675 * * [simplify]: iters left: 5 (50 enodes) 6.693 * * [simplify]: iters left: 4 (126 enodes) 6.726 * * [simplify]: iters left: 3 (499 enodes) 7.212 * * [simplify]: Extracting #0: cost 1 inf + 0 7.212 * * [simplify]: Extracting #1: cost 42 inf + 0 7.213 * * [simplify]: Extracting #2: cost 280 inf + 0 7.217 * * [simplify]: Extracting #3: cost 597 inf + 12843 7.239 * * [simplify]: Extracting #4: cost 810 inf + 280829 7.324 * * [simplify]: Extracting #5: cost 230 inf + 1598730 7.439 * * [simplify]: Extracting #6: cost 4 inf + 2036734 7.586 * * [simplify]: Extracting #7: cost 0 inf + 2038740 7.723 * [simplify]: Simplified to (+.p16 (*.p16 (+.p16 (neg.p16 b_2) b_2) (-.p16 (neg.p16 b_2) b_2)) (*.p16 c a)) 7.723 * [simplify]: Simplified (2 1) to (λ (a b_2 c) (/.p16 (+.p16 (*.p16 (+.p16 (neg.p16 b_2) b_2) (-.p16 (neg.p16 b_2) b_2)) (*.p16 c a)) (*.p16 a (+.p16 (neg.p16 b_2) (sqrt.p16 (/.p16 (-.p16 (*.p16 (*.p16 b_2 b_2) (*.p16 b_2 b_2)) (*.p16 (*.p16 a c) (*.p16 a c))) (+.p16 (*.p16 b_2 b_2) (*.p16 a c)))))))) 7.723 * * * * [progress]: [ 6 / 9 ] simplifiying candidate # 7.723 * * * * [progress]: [ 7 / 9 ] simplifiying candidate # 7.723 * * * * [progress]: [ 8 / 9 ] simplifiying candidate # 7.723 * * * * [progress]: [ 9 / 9 ] simplifiying candidate # 7.723 * * * [progress]: adding candidates to table 7.964 * [progress]: [Phase 3 of 3] Extracting. 7.964 * * [regime]: Finding splitpoints for: (# # # # # #) 7.966 * * * [regime-changes]: Trying 3 branch expressions: (c a b_2) 7.967 * * * * [regimes]: Trying to branch on c from (# # # # # #) 8.140 * * * * [regimes]: Trying to branch on a from (# # # # # #) 8.368 * * * * [regimes]: Trying to branch on b_2 from (# # # # # #) 8.598 * * * [regime]: Found split indices: #