0.001 * [progress]: [Phase 1 of 3] Setting up. 0.001 * * * [progress]: [1/2] Preparing points 0.002 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.003 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.007 * * * * [points]: Setting MPFR precision to 64 0.008 * * * * [points]: Setting MPFR precision to 320 0.009 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.014 * * * * [points]: Setting MPFR precision to 64 0.016 * * * * [points]: Setting MPFR precision to 320 0.019 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.027 * * * * [points]: Setting MPFR precision to 64 0.033 * * * * [points]: Setting MPFR precision to 320 0.048 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.059 * * * * [points]: Setting MPFR precision to 64 0.070 * * * * [points]: Setting MPFR precision to 320 0.080 * * * * [points]: Computing exacts for 256 points 0.090 * * * * [points]: Setting MPFR precision to 64 0.120 * * * * [points]: Setting MPFR precision to 320 0.150 * * * * [points]: Filtering points with unrepresentable outputs 0.151 * * * * [points]: Sampling 96 additional inputs, on iter 1 have 160 / 256 0.151 * * * * [points]: Computing exacts on every 6 of 96 points to ramp up precision 0.160 * * * * [points]: Setting MPFR precision to 64 0.162 * * * * [points]: Setting MPFR precision to 320 0.163 * * * * [points]: Computing exacts on every 3 of 96 points to ramp up precision 0.171 * * * * [points]: Setting MPFR precision to 64 0.174 * * * * [points]: Setting MPFR precision to 320 0.177 * * * * [points]: Computing exacts for 96 points 0.185 * * * * [points]: Setting MPFR precision to 64 0.191 * * * * [points]: Setting MPFR precision to 320 0.197 * * * * [points]: Filtering points with unrepresentable outputs 0.197 * * * * [points]: Sampling 33 additional inputs, on iter 2 have 223 / 256 0.197 * * * * [points]: Computing exacts on every 2 of 33 points to ramp up precision 0.220 * * * * [points]: Setting MPFR precision to 64 0.222 * * * * [points]: Setting MPFR precision to 320 0.223 * * * * [points]: Computing exacts for 33 points 0.234 * * * * [points]: Setting MPFR precision to 64 0.238 * * * * [points]: Setting MPFR precision to 320 0.242 * * * * [points]: Filtering points with unrepresentable outputs 0.242 * * * * [points]: Sampling 13 additional inputs, on iter 3 have 243 / 256 0.242 * * * * [points]: Computing exacts for 13 points 0.252 * * * * [points]: Setting MPFR precision to 64 0.254 * * * * [points]: Setting MPFR precision to 320 0.255 * * * * [points]: Filtering points with unrepresentable outputs 0.255 * * * * [points]: Sampling 6 additional inputs, on iter 4 have 250 / 256 0.255 * * * * [points]: Computing exacts for 6 points 0.263 * * * * [points]: Setting MPFR precision to 64 0.263 * * * * [points]: Setting MPFR precision to 320 0.264 * * * * [points]: Filtering points with unrepresentable outputs 0.264 * * * * [points]: Sampling 4 additional inputs, on iter 5 have 252 / 256 0.264 * * * * [points]: Computing exacts for 4 points 0.268 * * * * [points]: Setting MPFR precision to 64 0.268 * * * * [points]: Setting MPFR precision to 320 0.269 * * * * [points]: Filtering points with unrepresentable outputs 0.269 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 254 / 256 0.269 * * * * [points]: Computing exacts for 4 points 0.273 * * * * [points]: Setting MPFR precision to 64 0.274 * * * * [points]: Setting MPFR precision to 320 0.274 * * * * [points]: Filtering points with unrepresentable outputs 0.274 * * * * [points]: Sampled 257 points with exact outputs 0.274 * * * [progress]: [2/2] Setting up program. 0.288 * [progress]: [Phase 2 of 3] Improving. 0.288 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 0.288 * [simplify]: Simplifying (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) 0.288 * * [simplify]: iters left: 6 (18 enodes) 0.294 * * [simplify]: iters left: 5 (46 enodes) 0.311 * * [simplify]: iters left: 4 (118 enodes) 0.377 * * [simplify]: Extracting #0: cost 1 inf + 0 0.377 * * [simplify]: Extracting #1: cost 10 inf + 0 0.377 * * [simplify]: Extracting #2: cost 62 inf + 0 0.378 * * [simplify]: Extracting #3: cost 165 inf + 2 0.378 * * [simplify]: Extracting #4: cost 154 inf + 3708 0.380 * * [simplify]: Extracting #5: cost 131 inf + 9961 0.381 * * [simplify]: Extracting #6: cost 129 inf + 10365 0.384 * * [simplify]: Extracting #7: cost 82 inf + 46686 0.392 * * [simplify]: Extracting #8: cost 5 inf + 102245 0.411 * * [simplify]: Extracting #9: cost 0 inf + 105668 0.429 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))))) 0.429 * [simplify]: Simplified (2) to (λ (alpha beta) (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)))))) 0.490 * * [progress]: iteration 1 / 4 0.490 * * * [progress]: picking best candidate 0.518 * * * * [pick]: Picked #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 0.518 * * * [progress]: localizing error 1.130 * * * [progress]: generating rewritten candidates 1.130 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 1.211 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1) 1.221 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 1.294 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1) 1.350 * * * [progress]: generating series expansions 1.350 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 1.350 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1) 1.350 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 1.350 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1) 1.350 * * * [progress]: simplifying candidates 1.350 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.350 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.350 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.350 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 1.350 * * [simplify]: iters left: 3 (8 enodes) 1.352 * * [simplify]: iters left: 2 (21 enodes) 1.356 * * [simplify]: iters left: 1 (43 enodes) 1.364 * * [simplify]: Extracting #0: cost 1 inf + 0 1.364 * * [simplify]: Extracting #1: cost 16 inf + 0 1.364 * * [simplify]: Extracting #2: cost 16 inf + 2 1.365 * * [simplify]: Extracting #3: cost 13 inf + 367 1.365 * * [simplify]: Extracting #4: cost 0 inf + 3718 1.365 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 1.366 * [simplify]: Simplified (2 1 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 1.366 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.366 * [simplify]: Simplifying (+.p16 alpha beta) 1.366 * * [simplify]: iters left: 1 (3 enodes) 1.366 * * [simplify]: Extracting #0: cost 1 inf + 0 1.366 * * [simplify]: Extracting #1: cost 3 inf + 0 1.367 * * [simplify]: Extracting #2: cost 1 inf + 2 1.367 * * [simplify]: Extracting #3: cost 0 inf + 44 1.367 * [simplify]: Simplified to (+.p16 beta alpha) 1.367 * [simplify]: Simplified (2 1 1 1 1) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 beta alpha) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 1.367 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 1.0) (+.p16 (+.p16 alpha beta) (*.p16 beta alpha))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.367 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.367 * [simplify]: Simplifying (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) 1.367 * * [simplify]: iters left: 6 (18 enodes) 1.371 * * [simplify]: iters left: 5 (46 enodes) 1.380 * * [simplify]: iters left: 4 (118 enodes) 1.426 * * [simplify]: Extracting #0: cost 1 inf + 0 1.426 * * [simplify]: Extracting #1: cost 10 inf + 0 1.426 * * [simplify]: Extracting #2: cost 62 inf + 0 1.426 * * [simplify]: Extracting #3: cost 165 inf + 2 1.427 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.429 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.431 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.437 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.453 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.463 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.476 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))))) 1.476 * [simplify]: Simplified (2) to (λ (alpha beta) (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)))))) 1.476 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.476 * [simplify]: Simplifying (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) 1.476 * * [simplify]: iters left: 6 (18 enodes) 1.484 * * [simplify]: iters left: 5 (46 enodes) 1.499 * * [simplify]: iters left: 4 (118 enodes) 1.539 * * [simplify]: Extracting #0: cost 1 inf + 0 1.540 * * [simplify]: Extracting #1: cost 10 inf + 0 1.540 * * [simplify]: Extracting #2: cost 62 inf + 0 1.540 * * [simplify]: Extracting #3: cost 165 inf + 2 1.543 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.544 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.545 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.548 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.556 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.565 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.574 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))))) 1.574 * [simplify]: Simplified (2) to (λ (alpha beta) (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)))))) 1.574 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.574 * [simplify]: Simplifying (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) 1.574 * * [simplify]: iters left: 6 (18 enodes) 1.579 * * [simplify]: iters left: 5 (46 enodes) 1.589 * * [simplify]: iters left: 4 (118 enodes) 1.634 * * [simplify]: Extracting #0: cost 1 inf + 0 1.634 * * [simplify]: Extracting #1: cost 10 inf + 0 1.634 * * [simplify]: Extracting #2: cost 62 inf + 0 1.635 * * [simplify]: Extracting #3: cost 165 inf + 2 1.635 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.636 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.638 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.641 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.652 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.661 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.670 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))))) 1.670 * [simplify]: Simplified (2) to (λ (alpha beta) (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)))))) 1.670 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 1.671 * [simplify]: Simplifying (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) 1.671 * * [simplify]: iters left: 6 (18 enodes) 1.675 * * [simplify]: iters left: 5 (46 enodes) 1.684 * * [simplify]: iters left: 4 (118 enodes) 1.720 * * [simplify]: Extracting #0: cost 1 inf + 0 1.720 * * [simplify]: Extracting #1: cost 10 inf + 0 1.720 * * [simplify]: Extracting #2: cost 62 inf + 0 1.720 * * [simplify]: Extracting #3: cost 165 inf + 2 1.721 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.722 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.723 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.727 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.734 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.743 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.758 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))))) 1.758 * [simplify]: Simplified (2) to (λ (alpha beta) (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)))))) 1.758 * * * [progress]: adding candidates to table 2.119 * * [progress]: iteration 2 / 4 2.119 * * * [progress]: picking best candidate 2.172 * * * * [pick]: Picked #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.172 * * * [progress]: localizing error 2.454 * * * [progress]: generating rewritten candidates 2.454 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 2.483 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 2.506 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 1) 2.510 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 1 2) 2.513 * * * [progress]: generating series expansions 2.513 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 2.513 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 2.513 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 1) 2.513 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 1 2) 2.513 * * * [progress]: simplifying candidates 2.513 * * * * [progress]: [ 1 / 8 ] simplifiying candidate #posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.513 * [simplify]: Simplifying (+.p16 (+.p16 alpha (+.p16 beta (*.p16 beta alpha))) (real->posit16 1.0)) 2.513 * * [simplify]: iters left: 4 (8 enodes) 2.516 * * [simplify]: iters left: 3 (21 enodes) 2.520 * * [simplify]: iters left: 2 (41 enodes) 2.526 * * [simplify]: iters left: 1 (61 enodes) 2.537 * * [simplify]: Extracting #0: cost 1 inf + 0 2.537 * * [simplify]: Extracting #1: cost 16 inf + 0 2.537 * * [simplify]: Extracting #2: cost 17 inf + 2 2.538 * * [simplify]: Extracting #3: cost 12 inf + 1091 2.538 * * [simplify]: Extracting #4: cost 3 inf + 3553 2.539 * * [simplify]: Extracting #5: cost 0 inf + 4280 2.539 * [simplify]: Simplified to (*.p16 (+.p16 beta (real->posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) 2.539 * [simplify]: Simplified (2 1 1) to (λ (alpha beta) (/.p16 (/.p16 (*.p16 (+.p16 beta (real->posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 2.539 * * * * [progress]: [ 2 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.539 * [simplify]: Simplifying (*.p16 beta alpha) 2.540 * * [simplify]: iters left: 1 (3 enodes) 2.540 * * [simplify]: Extracting #0: cost 1 inf + 0 2.540 * * [simplify]: Extracting #1: cost 3 inf + 0 2.540 * * [simplify]: Extracting #2: cost 1 inf + 2 2.540 * * [simplify]: Extracting #3: cost 0 inf + 324 2.540 * [simplify]: Simplified to (*.p16 alpha beta) 2.540 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 alpha beta)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 2.540 * * * * [progress]: [ 3 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.540 * * * * [progress]: [ 4 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.541 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.541 * * * * [progress]: [ 6 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.541 * * * * [progress]: [ 7 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.541 * * * * [progress]: [ 8 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.541 * * * [progress]: adding candidates to table 2.713 * * [progress]: iteration 3 / 4 2.713 * * * [progress]: picking best candidate 2.798 * * * * [pick]: Picked #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.798 * * * [progress]: localizing error 3.200 * * * [progress]: generating rewritten candidates 3.200 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 3.220 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1) 3.229 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 3.248 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 2) 3.251 * * * [progress]: generating series expansions 3.251 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 3.251 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1) 3.251 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 3.251 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 2) 3.251 * * * [progress]: simplifying candidates 3.251 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.251 * [simplify]: Simplifying (real->posit16 1.0) 3.251 * * [simplify]: iters left: 1 (2 enodes) 3.252 * * [simplify]: Extracting #0: cost 1 inf + 0 3.252 * * [simplify]: Extracting #1: cost 2 inf + 0 3.252 * * [simplify]: Extracting #2: cost 1 inf + 1 3.252 * * [simplify]: Extracting #3: cost 0 inf + 2 3.252 * [simplify]: Simplified to (real->posit16 1.0) 3.252 * [simplify]: Simplified (2 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.253 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.253 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #posit16 1.0)) (+.p16 alpha beta)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.253 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.253 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) 3.253 * * [simplify]: iters left: 3 (8 enodes) 3.255 * * [simplify]: iters left: 2 (21 enodes) 3.258 * * [simplify]: iters left: 1 (40 enodes) 3.266 * * [simplify]: Extracting #0: cost 1 inf + 0 3.266 * * [simplify]: Extracting #1: cost 15 inf + 0 3.266 * * [simplify]: Extracting #2: cost 15 inf + 2 3.267 * * [simplify]: Extracting #3: cost 9 inf + 772 3.267 * * [simplify]: Extracting #4: cost 0 inf + 3315 3.268 * [simplify]: Simplified to (+.p16 alpha (+.p16 (+.p16 (real->posit16 1.0) beta) (*.p16 beta alpha))) 3.268 * [simplify]: Simplified (2 1 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 alpha (+.p16 (+.p16 (real->posit16 1.0) beta) (*.p16 beta alpha))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.268 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 1.0) (*.p16 beta alpha))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.268 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.268 * [simplify]: Simplifying (+.p16 alpha beta) 3.268 * * [simplify]: iters left: 1 (3 enodes) 3.269 * * [simplify]: Extracting #0: cost 1 inf + 0 3.269 * * [simplify]: Extracting #1: cost 3 inf + 0 3.269 * * [simplify]: Extracting #2: cost 1 inf + 2 3.269 * * [simplify]: Extracting #3: cost 0 inf + 44 3.269 * [simplify]: Simplified to (+.p16 beta alpha) 3.269 * [simplify]: Simplified (2 1 1 1 1) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 beta alpha) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.269 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.269 * [simplify]: Simplifying (+.p16 alpha beta) 3.269 * * [simplify]: iters left: 1 (3 enodes) 3.270 * * [simplify]: Extracting #0: cost 1 inf + 0 3.270 * * [simplify]: Extracting #1: cost 3 inf + 0 3.270 * * [simplify]: Extracting #2: cost 1 inf + 2 3.270 * * [simplify]: Extracting #3: cost 0 inf + 44 3.270 * [simplify]: Simplified to (+.p16 beta alpha) 3.270 * [simplify]: Simplified (2 1 1 1 1) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 beta alpha) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.270 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.270 * [simplify]: Simplifying (+.p16 alpha beta) 3.270 * * [simplify]: iters left: 1 (3 enodes) 3.271 * * [simplify]: Extracting #0: cost 1 inf + 0 3.271 * * [simplify]: Extracting #1: cost 3 inf + 0 3.271 * * [simplify]: Extracting #2: cost 1 inf + 2 3.271 * * [simplify]: Extracting #3: cost 0 inf + 44 3.271 * [simplify]: Simplified to (+.p16 beta alpha) 3.271 * [simplify]: Simplified (2 1 1 1 1) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 beta alpha) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.271 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.271 * [simplify]: Simplifying (+.p16 alpha beta) 3.271 * * [simplify]: iters left: 1 (3 enodes) 3.272 * * [simplify]: Extracting #0: cost 1 inf + 0 3.272 * * [simplify]: Extracting #1: cost 3 inf + 0 3.272 * * [simplify]: Extracting #2: cost 1 inf + 2 3.272 * * [simplify]: Extracting #3: cost 0 inf + 44 3.272 * [simplify]: Simplified to (+.p16 beta alpha) 3.272 * [simplify]: Simplified (2 1 1 1 1) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 beta alpha) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.272 * * * [progress]: adding candidates to table 3.479 * * [progress]: iteration 4 / 4 3.479 * * * [progress]: picking best candidate 3.534 * * * * [pick]: Picked #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.534 * * * [progress]: localizing error 3.799 * * * [progress]: generating rewritten candidates 3.799 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 3.811 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 2) 3.815 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1) 3.821 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1) 3.838 * * * [progress]: generating series expansions 3.838 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 3.838 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 2) 3.838 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1) 3.838 * * * * [progress]: [ 4 / 4 ] generating series at (2 1) 3.839 * * * [progress]: simplifying candidates 3.839 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.839 * [simplify]: Simplifying (real->posit16 1.0) 3.839 * * [simplify]: iters left: 1 (2 enodes) 3.840 * * [simplify]: Extracting #0: cost 1 inf + 0 3.840 * * [simplify]: Extracting #1: cost 2 inf + 0 3.840 * * [simplify]: Extracting #2: cost 1 inf + 1 3.840 * * [simplify]: Extracting #3: cost 0 inf + 2 3.840 * [simplify]: Simplified to (real->posit16 1.0) 3.840 * [simplify]: Simplified (2 1 1 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 alpha (+.p16 (+.p16 beta (*.p16 beta alpha)) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.840 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #posit16 1.0)) beta)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.840 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.840 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (real->posit16 1.0)) 3.840 * * [simplify]: iters left: 2 (6 enodes) 3.842 * * [simplify]: iters left: 1 (13 enodes) 3.843 * * [simplify]: Extracting #0: cost 1 inf + 0 3.843 * * [simplify]: Extracting #1: cost 3 inf + 0 3.843 * * [simplify]: Extracting #2: cost 6 inf + 0 3.844 * * [simplify]: Extracting #3: cost 2 inf + 4 3.844 * * [simplify]: Extracting #4: cost 0 inf + 689 3.844 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) (real->posit16 1.0)) 3.844 * [simplify]: Simplified (2 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 alpha beta) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.844 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #posit16 1.0))) alpha) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.844 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 1.0)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.844 * [simplify]: Simplifying (+.p16 alpha (+.p16 beta (+.p16 (*.p16 beta alpha) (real->posit16 1.0)))) 3.844 * * [simplify]: iters left: 4 (8 enodes) 3.846 * * [simplify]: iters left: 3 (21 enodes) 3.849 * * [simplify]: iters left: 2 (43 enodes) 3.857 * * [simplify]: iters left: 1 (66 enodes) 3.867 * * [simplify]: Extracting #0: cost 1 inf + 0 3.867 * * [simplify]: Extracting #1: cost 15 inf + 0 3.867 * * [simplify]: Extracting #2: cost 16 inf + 2 3.867 * * [simplify]: Extracting #3: cost 10 inf + 1493 3.867 * * [simplify]: Extracting #4: cost 1 inf + 3555 3.868 * * [simplify]: Extracting #5: cost 0 inf + 3877 3.869 * [simplify]: Simplified to (*.p16 (+.p16 (real->posit16 1.0) beta) (+.p16 alpha (real->posit16 1.0))) 3.869 * [simplify]: Simplified (2 1 1) to (λ (alpha beta) (/.p16 (/.p16 (*.p16 (+.p16 (real->posit16 1.0) beta) (+.p16 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.869 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.869 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.869 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.869 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.869 * * * [progress]: adding candidates to table 4.083 * [progress]: [Phase 3 of 3] Extracting. 4.084 * * [regime]: Finding splitpoints for: (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))))))> #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))>) 4.085 * * * [regime-changes]: Trying 2 branch expressions: (beta alpha) 4.085 * * * * [regimes]: Trying to branch on beta from (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))))))> #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))>) 4.230 * * * * [regimes]: Trying to branch on alpha from (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (*.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 (real->posit16 1) (real->posit16 2)))) (*.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha)) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))))))> #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))>) 4.369 * * * [regime]: Found split indices: #