0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.004 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.005 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.011 * * * * [points]: Setting MPFR precision to 64 0.014 * * * * [points]: Setting MPFR precision to 320 0.015 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.024 * * * * [points]: Setting MPFR precision to 64 0.027 * * * * [points]: Setting MPFR precision to 320 0.030 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.045 * * * * [points]: Setting MPFR precision to 64 0.052 * * * * [points]: Setting MPFR precision to 320 0.057 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.067 * * * * [points]: Setting MPFR precision to 64 0.078 * * * * [points]: Setting MPFR precision to 320 0.087 * * * * [points]: Computing exacts for 256 points 0.097 * * * * [points]: Setting MPFR precision to 64 0.128 * * * * [points]: Setting MPFR precision to 320 0.158 * * * * [points]: Filtering points with unrepresentable outputs 0.158 * * * * [points]: Sampling 109 additional inputs, on iter 1 have 147 / 256 0.159 * * * * [points]: Computing exacts on every 6 of 109 points to ramp up precision 0.169 * * * * [points]: Setting MPFR precision to 64 0.171 * * * * [points]: Setting MPFR precision to 320 0.173 * * * * [points]: Computing exacts on every 3 of 109 points to ramp up precision 0.183 * * * * [points]: Setting MPFR precision to 64 0.187 * * * * [points]: Setting MPFR precision to 320 0.190 * * * * [points]: Computing exacts for 109 points 0.200 * * * * [points]: Setting MPFR precision to 64 0.213 * * * * [points]: Setting MPFR precision to 320 0.256 * * * * [points]: Filtering points with unrepresentable outputs 0.257 * * * * [points]: Sampling 48 additional inputs, on iter 2 have 208 / 256 0.257 * * * * [points]: Computing exacts on every 3 of 48 points to ramp up precision 0.267 * * * * [points]: Setting MPFR precision to 64 0.269 * * * * [points]: Setting MPFR precision to 320 0.270 * * * * [points]: Computing exacts for 48 points 0.274 * * * * [points]: Setting MPFR precision to 64 0.277 * * * * [points]: Setting MPFR precision to 320 0.280 * * * * [points]: Filtering points with unrepresentable outputs 0.280 * * * * [points]: Sampling 24 additional inputs, on iter 3 have 232 / 256 0.281 * * * * [points]: Computing exacts for 24 points 0.286 * * * * [points]: Setting MPFR precision to 64 0.288 * * * * [points]: Setting MPFR precision to 320 0.290 * * * * [points]: Filtering points with unrepresentable outputs 0.290 * * * * [points]: Sampling 12 additional inputs, on iter 4 have 244 / 256 0.290 * * * * [points]: Computing exacts for 12 points 0.296 * * * * [points]: Setting MPFR precision to 64 0.298 * * * * [points]: Setting MPFR precision to 320 0.299 * * * * [points]: Filtering points with unrepresentable outputs 0.299 * * * * [points]: Sampling 7 additional inputs, on iter 5 have 249 / 256 0.299 * * * * [points]: Computing exacts for 7 points 0.309 * * * * [points]: Setting MPFR precision to 64 0.311 * * * * [points]: Setting MPFR precision to 320 0.311 * * * * [points]: Filtering points with unrepresentable outputs 0.312 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 253 / 256 0.312 * * * * [points]: Computing exacts for 4 points 0.321 * * * * [points]: Setting MPFR precision to 64 0.322 * * * * [points]: Setting MPFR precision to 320 0.322 * * * * [points]: Filtering points with unrepresentable outputs 0.323 * * * * [points]: Sampled 257 points with exact outputs 0.323 * * * [progress]: [2/2] Setting up program. 0.350 * [progress]: [Phase 2 of 3] Improving. 0.350 * * * * [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.350 * [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.351 * * [simplify]: iters left: 6 (18 enodes) 0.359 * * [simplify]: iters left: 5 (46 enodes) 0.393 * * [simplify]: iters left: 4 (118 enodes) 0.433 * * [simplify]: Extracting #0: cost 1 inf + 0 0.433 * * [simplify]: Extracting #1: cost 10 inf + 0 0.433 * * [simplify]: Extracting #2: cost 62 inf + 0 0.434 * * [simplify]: Extracting #3: cost 165 inf + 2 0.434 * * [simplify]: Extracting #4: cost 154 inf + 3708 0.435 * * [simplify]: Extracting #5: cost 131 inf + 9961 0.436 * * [simplify]: Extracting #6: cost 129 inf + 10365 0.440 * * [simplify]: Extracting #7: cost 82 inf + 46686 0.446 * * [simplify]: Extracting #8: cost 5 inf + 102245 0.455 * * [simplify]: Extracting #9: cost 0 inf + 105668 0.477 * [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.477 * [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.529 * * [progress]: iteration 1 / 4 0.529 * * * [progress]: picking best candidate 0.555 * * * * [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.555 * * * [progress]: localizing error 0.867 * * * [progress]: generating rewritten candidates 0.867 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 0.975 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 1.089 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 1) 1.105 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1) 1.146 * * * [progress]: generating series expansions 1.146 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 1.146 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 1.146 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 1) 1.146 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1) 1.146 * * * [progress]: simplifying candidates 1.146 * * * * [progress]: [ 1 / 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.146 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 1.147 * * [simplify]: iters left: 3 (8 enodes) 1.151 * * [simplify]: iters left: 2 (21 enodes) 1.158 * * [simplify]: iters left: 1 (43 enodes) 1.173 * * [simplify]: Extracting #0: cost 1 inf + 0 1.173 * * [simplify]: Extracting #1: cost 16 inf + 0 1.174 * * [simplify]: Extracting #2: cost 16 inf + 2 1.174 * * [simplify]: Extracting #3: cost 13 inf + 367 1.175 * * [simplify]: Extracting #4: cost 0 inf + 3718 1.176 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 1.176 * [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.176 * * * * [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.176 * * * * [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))))> 1.176 * * * * [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.177 * [simplify]: Simplifying (+.p16 alpha beta) 1.177 * * [simplify]: iters left: 1 (3 enodes) 1.178 * * [simplify]: Extracting #0: cost 1 inf + 0 1.178 * * [simplify]: Extracting #1: cost 3 inf + 0 1.178 * * [simplify]: Extracting #2: cost 1 inf + 2 1.178 * * [simplify]: Extracting #3: cost 0 inf + 44 1.178 * [simplify]: Simplified to (+.p16 beta alpha) 1.178 * [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.178 * * * * [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.178 * * * * [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.179 * [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.179 * * [simplify]: iters left: 6 (18 enodes) 1.188 * * [simplify]: iters left: 5 (46 enodes) 1.205 * * [simplify]: iters left: 4 (118 enodes) 1.270 * * [simplify]: Extracting #0: cost 1 inf + 0 1.270 * * [simplify]: Extracting #1: cost 10 inf + 0 1.270 * * [simplify]: Extracting #2: cost 62 inf + 0 1.274 * * [simplify]: Extracting #3: cost 165 inf + 2 1.276 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.278 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.280 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.287 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.300 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.317 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.335 * [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.335 * [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.335 * * * * [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.335 * [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.336 * * [simplify]: iters left: 6 (18 enodes) 1.344 * * [simplify]: iters left: 5 (46 enodes) 1.361 * * [simplify]: iters left: 4 (118 enodes) 1.431 * * [simplify]: Extracting #0: cost 1 inf + 0 1.431 * * [simplify]: Extracting #1: cost 10 inf + 0 1.432 * * [simplify]: Extracting #2: cost 62 inf + 0 1.433 * * [simplify]: Extracting #3: cost 165 inf + 2 1.434 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.437 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.439 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.445 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.459 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.476 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.493 * [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.493 * [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.493 * * * * [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.494 * [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.494 * * [simplify]: iters left: 6 (18 enodes) 1.503 * * [simplify]: iters left: 5 (46 enodes) 1.521 * * [simplify]: iters left: 4 (118 enodes) 1.594 * * [simplify]: Extracting #0: cost 1 inf + 0 1.594 * * [simplify]: Extracting #1: cost 10 inf + 0 1.594 * * [simplify]: Extracting #2: cost 62 inf + 0 1.595 * * [simplify]: Extracting #3: cost 165 inf + 2 1.595 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.596 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.598 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.601 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.608 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.617 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.625 * [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.625 * [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.625 * * * * [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.625 * [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.626 * * [simplify]: iters left: 6 (18 enodes) 1.630 * * [simplify]: iters left: 5 (46 enodes) 1.639 * * [simplify]: iters left: 4 (118 enodes) 1.676 * * [simplify]: Extracting #0: cost 1 inf + 0 1.676 * * [simplify]: Extracting #1: cost 10 inf + 0 1.676 * * [simplify]: Extracting #2: cost 62 inf + 0 1.676 * * [simplify]: Extracting #3: cost 165 inf + 2 1.677 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.678 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.679 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.683 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.690 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.699 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.707 * [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.707 * [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.707 * * * [progress]: adding candidates to table 2.034 * * [progress]: iteration 2 / 4 2.034 * * * [progress]: picking best candidate 2.088 * * * * [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.088 * * * [progress]: localizing error 2.329 * * * [progress]: generating rewritten candidates 2.329 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 2.354 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1) 2.367 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 2.386 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 2.428 * * * [progress]: generating series expansions 2.428 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 2.428 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1) 2.428 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 2.428 * * * * [progress]: [ 4 / 4 ] generating series at (2) 2.428 * * * [progress]: simplifying candidates 2.428 * * * * [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))))> 2.428 * [simplify]: Simplifying (real->posit16 1.0) 2.428 * * [simplify]: iters left: 1 (2 enodes) 2.429 * * [simplify]: Extracting #0: cost 1 inf + 0 2.429 * * [simplify]: Extracting #1: cost 2 inf + 0 2.429 * * [simplify]: Extracting #2: cost 1 inf + 1 2.430 * * [simplify]: Extracting #3: cost 0 inf + 2 2.430 * [simplify]: Simplified to (real->posit16 1.0) 2.430 * [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)))) 2.430 * * * * [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))))> 2.430 * * * * [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))))> 2.430 * * * * [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))))> 2.430 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) 2.430 * * [simplify]: iters left: 3 (8 enodes) 2.432 * * [simplify]: iters left: 2 (21 enodes) 2.436 * * [simplify]: iters left: 1 (40 enodes) 2.442 * * [simplify]: Extracting #0: cost 1 inf + 0 2.443 * * [simplify]: Extracting #1: cost 15 inf + 0 2.443 * * [simplify]: Extracting #2: cost 15 inf + 2 2.443 * * [simplify]: Extracting #3: cost 9 inf + 772 2.443 * * [simplify]: Extracting #4: cost 0 inf + 3315 2.444 * [simplify]: Simplified to (+.p16 alpha (+.p16 (+.p16 (real->posit16 1.0) beta) (*.p16 beta alpha))) 2.444 * [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)))) 2.444 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 2.444 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 2.444 * * [simplify]: iters left: 4 (15 enodes) 2.448 * * [simplify]: iters left: 3 (36 enodes) 2.455 * * [simplify]: iters left: 2 (63 enodes) 2.467 * * [simplify]: iters left: 1 (88 enodes) 2.480 * * [simplify]: Extracting #0: cost 1 inf + 0 2.480 * * [simplify]: Extracting #1: cost 3 inf + 0 2.480 * * [simplify]: Extracting #2: cost 20 inf + 0 2.481 * * [simplify]: Extracting #3: cost 21 inf + 2 2.481 * * [simplify]: Extracting #4: cost 20 inf + 367 2.481 * * [simplify]: Extracting #5: cost 12 inf + 1498 2.482 * * [simplify]: Extracting #6: cost 3 inf + 4003 2.483 * * [simplify]: Extracting #7: cost 0 inf + 6014 2.485 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) 2.485 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))) 2.485 * * * * [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))))> 2.485 * [simplify]: Simplifying (+.p16 alpha beta) 2.485 * * [simplify]: iters left: 1 (3 enodes) 2.486 * * [simplify]: Extracting #0: cost 1 inf + 0 2.487 * * [simplify]: Extracting #1: cost 3 inf + 0 2.487 * * [simplify]: Extracting #2: cost 1 inf + 2 2.487 * * [simplify]: Extracting #3: cost 0 inf + 44 2.487 * [simplify]: Simplified to (+.p16 beta alpha) 2.487 * [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)))) 2.487 * * * * [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))))> 2.488 * [simplify]: Simplifying (+.p16 alpha beta) 2.489 * * [simplify]: iters left: 1 (3 enodes) 2.490 * * [simplify]: Extracting #0: cost 1 inf + 0 2.490 * * [simplify]: Extracting #1: cost 3 inf + 0 2.490 * * [simplify]: Extracting #2: cost 1 inf + 2 2.490 * * [simplify]: Extracting #3: cost 0 inf + 44 2.490 * [simplify]: Simplified to (+.p16 beta alpha) 2.490 * [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)))) 2.490 * * * * [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))))> 2.490 * [simplify]: Simplifying (+.p16 alpha beta) 2.491 * * [simplify]: iters left: 1 (3 enodes) 2.492 * * [simplify]: Extracting #0: cost 1 inf + 0 2.492 * * [simplify]: Extracting #1: cost 3 inf + 0 2.492 * * [simplify]: Extracting #2: cost 1 inf + 2 2.492 * * [simplify]: Extracting #3: cost 0 inf + 44 2.492 * [simplify]: Simplified to (+.p16 beta alpha) 2.492 * [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)))) 2.492 * * * * [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))))> 2.492 * [simplify]: Simplifying (+.p16 alpha beta) 2.492 * * [simplify]: iters left: 1 (3 enodes) 2.494 * * [simplify]: Extracting #0: cost 1 inf + 0 2.494 * * [simplify]: Extracting #1: cost 3 inf + 0 2.494 * * [simplify]: Extracting #2: cost 1 inf + 2 2.494 * * [simplify]: Extracting #3: cost 0 inf + 44 2.494 * [simplify]: Simplified to (+.p16 beta alpha) 2.494 * [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)))) 2.494 * * * [progress]: adding candidates to table 2.820 * * [progress]: iteration 3 / 4 2.820 * * * [progress]: picking best candidate 2.964 * * * * [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.965 * * * [progress]: localizing error 3.457 * * * [progress]: generating rewritten candidates 3.457 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 3.483 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 3.512 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1) 3.525 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 2) 3.533 * * * [progress]: generating series expansions 3.533 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 3.533 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 3.533 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1) 3.533 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 2) 3.534 * * * [progress]: simplifying candidates 3.534 * * * * [progress]: [ 1 / 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.534 * [simplify]: Simplifying (+.p16 alpha (+.p16 beta (+.p16 (*.p16 beta alpha) (real->posit16 1.0)))) 3.534 * * [simplify]: iters left: 4 (8 enodes) 3.538 * * [simplify]: iters left: 3 (21 enodes) 3.546 * * [simplify]: iters left: 2 (43 enodes) 3.561 * * [simplify]: iters left: 1 (66 enodes) 3.584 * * [simplify]: Extracting #0: cost 1 inf + 0 3.585 * * [simplify]: Extracting #1: cost 15 inf + 0 3.585 * * [simplify]: Extracting #2: cost 16 inf + 2 3.585 * * [simplify]: Extracting #3: cost 10 inf + 1493 3.585 * * [simplify]: Extracting #4: cost 1 inf + 3555 3.586 * * [simplify]: Extracting #5: cost 0 inf + 3877 3.586 * [simplify]: Simplified to (*.p16 (+.p16 (real->posit16 1.0) beta) (+.p16 alpha (real->posit16 1.0))) 3.587 * [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.587 * * * * [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.587 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (real->posit16 1.0)) 3.587 * * [simplify]: iters left: 2 (6 enodes) 3.588 * * [simplify]: iters left: 1 (13 enodes) 3.591 * * [simplify]: Extracting #0: cost 1 inf + 0 3.591 * * [simplify]: Extracting #1: cost 3 inf + 0 3.591 * * [simplify]: Extracting #2: cost 6 inf + 0 3.591 * * [simplify]: Extracting #3: cost 2 inf + 4 3.591 * * [simplify]: Extracting #4: cost 0 inf + 689 3.591 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) (real->posit16 1.0)) 3.591 * [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.591 * * * * [progress]: [ 3 / 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.591 * * * * [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))))> 3.591 * [simplify]: Simplifying (real->posit16 1.0) 3.591 * * [simplify]: iters left: 1 (2 enodes) 3.592 * * [simplify]: Extracting #0: cost 1 inf + 0 3.592 * * [simplify]: Extracting #1: cost 2 inf + 0 3.592 * * [simplify]: Extracting #2: cost 1 inf + 1 3.592 * * [simplify]: Extracting #3: cost 0 inf + 2 3.592 * [simplify]: Simplified to (real->posit16 1.0) 3.592 * [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.592 * * * * [progress]: [ 5 / 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.592 * * * * [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.592 * * * * [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.592 * * * * [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.592 * * * * [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.592 * * * [progress]: adding candidates to table 3.809 * * [progress]: iteration 4 / 4 3.809 * * * [progress]: picking best candidate 3.866 * * * * [pick]: Picked #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 3.866 * * * [progress]: localizing error 4.172 * * * [progress]: generating rewritten candidates 4.172 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 4.210 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1) 4.230 * * * * [progress]: [ 3 / 4 ] rewriting at (2) 4.260 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2) 4.298 * * * [progress]: generating series expansions 4.298 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 4.298 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1) 4.298 * * * * [progress]: [ 3 / 4 ] generating series at (2) 4.298 * * * * [progress]: [ 4 / 4 ] generating series at (2 2) 4.298 * * * [progress]: simplifying candidates 4.298 * * * * [progress]: [ 1 / 12 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 4.298 * [simplify]: Simplifying (real->posit16 1.0) 4.298 * * [simplify]: iters left: 1 (2 enodes) 4.300 * * [simplify]: Extracting #0: cost 1 inf + 0 4.300 * * [simplify]: Extracting #1: cost 2 inf + 0 4.300 * * [simplify]: Extracting #2: cost 1 inf + 1 4.300 * * [simplify]: Extracting #3: cost 0 inf + 2 4.300 * [simplify]: Simplified to (real->posit16 1.0) 4.300 * [simplify]: Simplified (2 1 1 2) to (λ (alpha beta) (/.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 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))) 4.300 * * * * [progress]: [ 2 / 12 ] simplifiying candidate #posit16 1.0)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 4.300 * * * * [progress]: [ 3 / 12 ] simplifiying candidate #posit16 1.0)) (+.p16 alpha beta)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 4.300 * * * * [progress]: [ 4 / 12 ] simplifiying candidate #posit16 1.0))) (+.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))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))> 4.301 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 4.301 * * [simplify]: iters left: 3 (9 enodes) 4.305 * * [simplify]: iters left: 2 (22 enodes) 4.313 * * [simplify]: iters left: 1 (30 enodes) 4.322 * * [simplify]: Extracting #0: cost 1 inf + 0 4.323 * * [simplify]: Extracting #1: cost 7 inf + 0 4.323 * * [simplify]: Extracting #2: cost 7 inf + 2 4.323 * * [simplify]: Extracting #3: cost 8 inf + 44 4.323 * * [simplify]: Extracting #4: cost 4 inf + 48 4.323 * * [simplify]: Extracting #5: cost 1 inf + 1137 4.323 * * [simplify]: Extracting #6: cost 0 inf + 1500 4.324 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 4.324 * [simplify]: Simplified (2 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.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))) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))))) 4.324 * * * * [progress]: [ 5 / 12 ] simplifiying candidate #posit16 1.0))) (*.p16 (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (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))))))> 4.325 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) 4.325 * * [simplify]: iters left: 3 (8 enodes) 4.329 * * [simplify]: iters left: 2 (21 enodes) 4.333 * * [simplify]: iters left: 1 (40 enodes) 4.342 * * [simplify]: Extracting #0: cost 1 inf + 0 4.342 * * [simplify]: Extracting #1: cost 15 inf + 0 4.342 * * [simplify]: Extracting #2: cost 15 inf + 2 4.343 * * [simplify]: Extracting #3: cost 9 inf + 772 4.343 * * [simplify]: Extracting #4: cost 0 inf + 3315 4.343 * [simplify]: Simplified to (+.p16 alpha (+.p16 (+.p16 (real->posit16 1.0) beta) (*.p16 beta alpha))) 4.343 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (+.p16 alpha (+.p16 (+.p16 (real->posit16 1.0) beta) (*.p16 beta alpha))) (*.p16 (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (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)))))) 4.344 * * * * [progress]: [ 6 / 12 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (*.p16 (real->posit16 2) (real->posit16 1))))))> 4.344 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (*.p16 (real->posit16 2) (real->posit16 1))) 4.344 * * [simplify]: iters left: 5 (13 enodes) 4.348 * * [simplify]: iters left: 4 (33 enodes) 4.354 * * [simplify]: iters left: 3 (75 enodes) 4.377 * * [simplify]: iters left: 2 (299 enodes) 4.802 * * [simplify]: Extracting #0: cost 1 inf + 0 4.802 * * [simplify]: Extracting #1: cost 150 inf + 0 4.805 * * [simplify]: Extracting #2: cost 497 inf + 0 4.810 * * [simplify]: Extracting #3: cost 531 inf + 3559 4.819 * * [simplify]: Extracting #4: cost 402 inf + 72063 4.852 * * [simplify]: Extracting #5: cost 50 inf + 307373 4.901 * * [simplify]: Extracting #6: cost 0 inf + 355493 4.947 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) alpha)) (*.p16 (real->posit16 2) (real->posit16 1)))) 4.947 * [simplify]: Simplified (2 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 alpha beta)) (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (*.p16 (+.p16 beta (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) alpha)) (*.p16 (real->posit16 2) (real->posit16 1))))))) 4.947 * * * * [progress]: [ 7 / 12 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 (+.p16 alpha beta) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))))> 4.948 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) 4.948 * * [simplify]: iters left: 5 (13 enodes) 4.955 * * [simplify]: iters left: 4 (39 enodes) 4.973 * * [simplify]: iters left: 3 (119 enodes) 5.120 * * [simplify]: Extracting #0: cost 1 inf + 0 5.120 * * [simplify]: Extracting #1: cost 54 inf + 0 5.121 * * [simplify]: Extracting #2: cost 200 inf + 0 5.122 * * [simplify]: Extracting #3: cost 214 inf + 2271 5.126 * * [simplify]: Extracting #4: cost 155 inf + 33806 5.139 * * [simplify]: Extracting #5: cost 20 inf + 120375 5.156 * * [simplify]: Extracting #6: cost 0 inf + 134925 5.174 * [simplify]: Simplified to (+.p16 (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (real->posit16 2) (real->posit16 1))) 5.174 * [simplify]: Simplified (2 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 (+.p16 alpha beta) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) (+.p16 (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (real->posit16 2) (real->posit16 1)))))) 5.174 * * * * [progress]: [ 8 / 12 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.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)))))> 5.174 * * * * [progress]: [ 9 / 12 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 5.175 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 5.175 * * [simplify]: iters left: 4 (15 enodes) 5.183 * * [simplify]: iters left: 3 (36 enodes) 5.195 * * [simplify]: iters left: 2 (63 enodes) 5.216 * * [simplify]: iters left: 1 (88 enodes) 5.240 * * [simplify]: Extracting #0: cost 1 inf + 0 5.241 * * [simplify]: Extracting #1: cost 3 inf + 0 5.241 * * [simplify]: Extracting #2: cost 20 inf + 0 5.241 * * [simplify]: Extracting #3: cost 21 inf + 2 5.241 * * [simplify]: Extracting #4: cost 20 inf + 367 5.241 * * [simplify]: Extracting #5: cost 12 inf + 1498 5.245 * * [simplify]: Extracting #6: cost 3 inf + 4003 5.246 * * [simplify]: Extracting #7: cost 0 inf + 6014 5.247 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) 5.248 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))) 5.248 * * * * [progress]: [ 10 / 12 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 5.248 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 5.248 * * [simplify]: iters left: 4 (15 enodes) 5.256 * * [simplify]: iters left: 3 (36 enodes) 5.269 * * [simplify]: iters left: 2 (63 enodes) 5.290 * * [simplify]: iters left: 1 (88 enodes) 5.315 * * [simplify]: Extracting #0: cost 1 inf + 0 5.315 * * [simplify]: Extracting #1: cost 3 inf + 0 5.316 * * [simplify]: Extracting #2: cost 20 inf + 0 5.316 * * [simplify]: Extracting #3: cost 21 inf + 2 5.316 * * [simplify]: Extracting #4: cost 20 inf + 367 5.316 * * [simplify]: Extracting #5: cost 12 inf + 1498 5.317 * * [simplify]: Extracting #6: cost 3 inf + 4003 5.318 * * [simplify]: Extracting #7: cost 0 inf + 6014 5.320 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) 5.320 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))) 5.320 * * * * [progress]: [ 11 / 12 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 5.320 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 5.321 * * [simplify]: iters left: 4 (15 enodes) 5.328 * * [simplify]: iters left: 3 (36 enodes) 5.340 * * [simplify]: iters left: 2 (63 enodes) 5.361 * * [simplify]: iters left: 1 (88 enodes) 5.387 * * [simplify]: Extracting #0: cost 1 inf + 0 5.387 * * [simplify]: Extracting #1: cost 3 inf + 0 5.387 * * [simplify]: Extracting #2: cost 20 inf + 0 5.388 * * [simplify]: Extracting #3: cost 21 inf + 2 5.388 * * [simplify]: Extracting #4: cost 20 inf + 367 5.388 * * [simplify]: Extracting #5: cost 12 inf + 1498 5.389 * * [simplify]: Extracting #6: cost 3 inf + 4003 5.390 * * [simplify]: Extracting #7: cost 0 inf + 6014 5.391 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) 5.391 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))) 5.392 * * * * [progress]: [ 12 / 12 ] simplifiying candidate #posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> 5.392 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 5.392 * * [simplify]: iters left: 4 (15 enodes) 5.399 * * [simplify]: iters left: 3 (36 enodes) 5.412 * * [simplify]: iters left: 2 (63 enodes) 5.434 * * [simplify]: iters left: 1 (88 enodes) 5.459 * * [simplify]: Extracting #0: cost 1 inf + 0 5.459 * * [simplify]: Extracting #1: cost 3 inf + 0 5.459 * * [simplify]: Extracting #2: cost 20 inf + 0 5.459 * * [simplify]: Extracting #3: cost 21 inf + 2 5.459 * * [simplify]: Extracting #4: cost 20 inf + 367 5.460 * * [simplify]: Extracting #5: cost 12 inf + 1498 5.461 * * [simplify]: Extracting #6: cost 3 inf + 4003 5.462 * * [simplify]: Extracting #7: cost 0 inf + 6014 5.463 * [simplify]: Simplified to (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) 5.463 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 (*.p16 beta alpha) beta) (real->posit16 1.0)) alpha) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))) 5.464 * * * [progress]: adding candidates to table 6.114 * [progress]: [Phase 3 of 3] Extracting. 6.115 * * [regime]: Finding splitpoints for: (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> #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))))> #posit16 1.0))) (+.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))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))> #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 beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 (+.p16 alpha beta) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) (*.p16 (*.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))))))>) 6.118 * * * [regime-changes]: Trying 2 branch expressions: (beta alpha) 6.118 * * * * [regimes]: Trying to branch on beta from (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> #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))))> #posit16 1.0))) (+.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))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))> #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 beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 (+.p16 alpha beta) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) (*.p16 (*.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))))))>) 6.282 * * * * [regimes]: Trying to branch on alpha from (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))))> #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))))> #posit16 1.0))) (+.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))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))))> #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 beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 (+.p16 alpha beta) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))) (*.p16 (*.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))))))>) 6.492 * * * [regime]: Found split indices: #