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.009 * * * * [points]: Setting MPFR precision to 64 0.011 * * * * [points]: Setting MPFR precision to 320 0.013 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.020 * * * * [points]: Setting MPFR precision to 64 0.024 * * * * [points]: Setting MPFR precision to 320 0.027 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.031 * * * * [points]: Setting MPFR precision to 64 0.035 * * * * [points]: Setting MPFR precision to 320 0.038 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.043 * * * * [points]: Setting MPFR precision to 64 0.056 * * * * [points]: Setting MPFR precision to 320 0.061 * * * * [points]: Computing exacts for 256 points 0.066 * * * * [points]: Setting MPFR precision to 64 0.084 * * * * [points]: Setting MPFR precision to 320 0.105 * * * * [points]: Filtering points with unrepresentable outputs 0.106 * * * * [points]: Sampling 119 additional inputs, on iter 1 have 137 / 256 0.106 * * * * [points]: Computing exacts on every 7 of 119 points to ramp up precision 0.111 * * * * [points]: Setting MPFR precision to 64 0.112 * * * * [points]: Setting MPFR precision to 320 0.113 * * * * [points]: Computing exacts on every 3 of 119 points to ramp up precision 0.117 * * * * [points]: Setting MPFR precision to 64 0.119 * * * * [points]: Setting MPFR precision to 320 0.121 * * * * [points]: Computing exacts for 119 points 0.125 * * * * [points]: Setting MPFR precision to 64 0.133 * * * * [points]: Setting MPFR precision to 320 0.143 * * * * [points]: Filtering points with unrepresentable outputs 0.143 * * * * [points]: Sampling 55 additional inputs, on iter 2 have 201 / 256 0.143 * * * * [points]: Computing exacts on every 3 of 55 points to ramp up precision 0.147 * * * * [points]: Setting MPFR precision to 64 0.148 * * * * [points]: Setting MPFR precision to 320 0.149 * * * * [points]: Computing exacts for 55 points 0.153 * * * * [points]: Setting MPFR precision to 64 0.176 * * * * [points]: Setting MPFR precision to 320 0.180 * * * * [points]: Filtering points with unrepresentable outputs 0.180 * * * * [points]: Sampling 19 additional inputs, on iter 3 have 237 / 256 0.180 * * * * [points]: Computing exacts for 19 points 0.185 * * * * [points]: Setting MPFR precision to 64 0.187 * * * * [points]: Setting MPFR precision to 320 0.188 * * * * [points]: Filtering points with unrepresentable outputs 0.188 * * * * [points]: Sampling 10 additional inputs, on iter 4 have 246 / 256 0.188 * * * * [points]: Computing exacts for 10 points 0.192 * * * * [points]: Setting MPFR precision to 64 0.193 * * * * [points]: Setting MPFR precision to 320 0.194 * * * * [points]: Filtering points with unrepresentable outputs 0.194 * * * * [points]: Sampling 4 additional inputs, on iter 5 have 253 / 256 0.194 * * * * [points]: Computing exacts for 4 points 0.198 * * * * [points]: Setting MPFR precision to 64 0.199 * * * * [points]: Setting MPFR precision to 320 0.199 * * * * [points]: Filtering points with unrepresentable outputs 0.199 * * * * [points]: Sampled 256 points with exact outputs 0.199 * * * [progress]: [2/2] Setting up program. 0.220 * [progress]: [Phase 2 of 3] Improving. 0.220 * * * * [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.220 * [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.220 * * [simplify]: iters left: 6 (18 enodes) 0.228 * * [simplify]: iters left: 5 (46 enodes) 0.237 * * [simplify]: iters left: 4 (118 enodes) 0.277 * * [simplify]: Extracting #0: cost 1 inf + 0 0.277 * * [simplify]: Extracting #1: cost 10 inf + 0 0.277 * * [simplify]: Extracting #2: cost 61 inf + 0 0.277 * * [simplify]: Extracting #3: cost 163 inf + 2 0.278 * * [simplify]: Extracting #4: cost 151 inf + 3750 0.279 * * [simplify]: Extracting #5: cost 129 inf + 9961 0.280 * * [simplify]: Extracting #6: cost 127 inf + 10365 0.283 * * [simplify]: Extracting #7: cost 80 inf + 46686 0.291 * * [simplify]: Extracting #8: cost 5 inf + 100676 0.299 * * [simplify]: Extracting #9: cost 0 inf + 104099 0.308 * [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.308 * [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.337 * * [progress]: iteration 1 / 4 0.337 * * * [progress]: picking best candidate 0.367 * * * * [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.367 * * * [progress]: localizing error 0.663 * * * [progress]: generating rewritten candidates 0.663 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 0.722 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1) 0.732 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 0.789 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1) 0.827 * * * [progress]: generating series expansions 0.827 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 0.827 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1) 0.827 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 0.827 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1) 0.827 * * * [progress]: simplifying candidates 0.827 * * * * [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))))> 0.828 * [simplify]: Simplifying (+.p16 beta (*.p16 beta alpha)) 0.828 * * [simplify]: iters left: 2 (4 enodes) 0.829 * * [simplify]: iters left: 1 (10 enodes) 0.830 * * [simplify]: Extracting #0: cost 1 inf + 0 0.831 * * [simplify]: Extracting #1: cost 4 inf + 0 0.831 * * [simplify]: Extracting #2: cost 5 inf + 1 0.831 * * [simplify]: Extracting #3: cost 3 inf + 686 0.831 * * [simplify]: Extracting #4: cost 0 inf + 730 0.831 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) beta) 0.831 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha (+.p16 (*.p16 alpha beta) 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)))) 0.831 * * * * [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))))> 0.831 * * * * [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))))> 0.831 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 0.832 * * [simplify]: iters left: 4 (10 enodes) 0.836 * * [simplify]: iters left: 3 (29 enodes) 0.844 * * [simplify]: iters left: 2 (81 enodes) 0.875 * * [simplify]: iters left: 1 (321 enodes) 1.069 * * [simplify]: Extracting #0: cost 1 inf + 0 1.069 * * [simplify]: Extracting #1: cost 64 inf + 0 1.070 * * [simplify]: Extracting #2: cost 254 inf + 0 1.071 * * [simplify]: Extracting #3: cost 250 inf + 2816 1.073 * * [simplify]: Extracting #4: cost 212 inf + 33771 1.085 * * [simplify]: Extracting #5: cost 61 inf + 193913 1.107 * * [simplify]: Extracting #6: cost 1 inf + 237431 1.133 * * [simplify]: Extracting #7: cost 0 inf + 235555 1.155 * [simplify]: Simplified to (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta)) 1.155 * [simplify]: Simplified (2 1 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 1.155 * * * * [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.155 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (real->posit16 1.0)) 1.155 * * [simplify]: iters left: 2 (6 enodes) 1.157 * * [simplify]: iters left: 1 (13 enodes) 1.159 * * [simplify]: Extracting #0: cost 1 inf + 0 1.159 * * [simplify]: Extracting #1: cost 3 inf + 0 1.159 * * [simplify]: Extracting #2: cost 6 inf + 0 1.159 * * [simplify]: Extracting #3: cost 2 inf + 4 1.159 * * [simplify]: Extracting #4: cost 0 inf + 689 1.159 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) (real->posit16 1.0)) 1.159 * [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)))) 1.159 * * * * [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.159 * * * * [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.160 * [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.160 * * [simplify]: iters left: 6 (18 enodes) 1.164 * * [simplify]: iters left: 5 (46 enodes) 1.173 * * [simplify]: iters left: 4 (118 enodes) 1.222 * * [simplify]: Extracting #0: cost 1 inf + 0 1.222 * * [simplify]: Extracting #1: cost 10 inf + 0 1.223 * * [simplify]: Extracting #2: cost 61 inf + 0 1.223 * * [simplify]: Extracting #3: cost 163 inf + 2 1.226 * * [simplify]: Extracting #4: cost 151 inf + 3750 1.227 * * [simplify]: Extracting #5: cost 129 inf + 9961 1.228 * * [simplify]: Extracting #6: cost 127 inf + 10365 1.231 * * [simplify]: Extracting #7: cost 80 inf + 46686 1.238 * * [simplify]: Extracting #8: cost 5 inf + 100676 1.246 * * [simplify]: Extracting #9: cost 0 inf + 104099 1.261 * [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.261 * [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.261 * * * * [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.262 * [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.262 * * [simplify]: iters left: 6 (18 enodes) 1.269 * * [simplify]: iters left: 5 (46 enodes) 1.285 * * [simplify]: iters left: 4 (118 enodes) 1.344 * * [simplify]: Extracting #0: cost 1 inf + 0 1.344 * * [simplify]: Extracting #1: cost 10 inf + 0 1.344 * * [simplify]: Extracting #2: cost 61 inf + 0 1.345 * * [simplify]: Extracting #3: cost 163 inf + 2 1.346 * * [simplify]: Extracting #4: cost 151 inf + 3750 1.348 * * [simplify]: Extracting #5: cost 129 inf + 9961 1.349 * * [simplify]: Extracting #6: cost 127 inf + 10365 1.353 * * [simplify]: Extracting #7: cost 80 inf + 46686 1.365 * * [simplify]: Extracting #8: cost 5 inf + 100676 1.380 * * [simplify]: Extracting #9: cost 0 inf + 104099 1.394 * [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.394 * [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.394 * * * * [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.395 * [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.395 * * [simplify]: iters left: 6 (18 enodes) 1.403 * * [simplify]: iters left: 5 (46 enodes) 1.415 * * [simplify]: iters left: 4 (118 enodes) 1.476 * * [simplify]: Extracting #0: cost 1 inf + 0 1.477 * * [simplify]: Extracting #1: cost 10 inf + 0 1.477 * * [simplify]: Extracting #2: cost 61 inf + 0 1.478 * * [simplify]: Extracting #3: cost 163 inf + 2 1.479 * * [simplify]: Extracting #4: cost 151 inf + 3750 1.481 * * [simplify]: Extracting #5: cost 129 inf + 9961 1.484 * * [simplify]: Extracting #6: cost 127 inf + 10365 1.490 * * [simplify]: Extracting #7: cost 80 inf + 46686 1.503 * * [simplify]: Extracting #8: cost 5 inf + 100676 1.520 * * [simplify]: Extracting #9: cost 0 inf + 104099 1.536 * [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.536 * [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.536 * * * * [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.536 * [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.536 * * [simplify]: iters left: 6 (18 enodes) 1.544 * * [simplify]: iters left: 5 (46 enodes) 1.562 * * [simplify]: iters left: 4 (118 enodes) 1.617 * * [simplify]: Extracting #0: cost 1 inf + 0 1.617 * * [simplify]: Extracting #1: cost 10 inf + 0 1.618 * * [simplify]: Extracting #2: cost 61 inf + 0 1.618 * * [simplify]: Extracting #3: cost 163 inf + 2 1.619 * * [simplify]: Extracting #4: cost 151 inf + 3750 1.620 * * [simplify]: Extracting #5: cost 129 inf + 9961 1.621 * * [simplify]: Extracting #6: cost 127 inf + 10365 1.624 * * [simplify]: Extracting #7: cost 80 inf + 46686 1.632 * * [simplify]: Extracting #8: cost 5 inf + 100676 1.645 * * [simplify]: Extracting #9: cost 0 inf + 104099 1.663 * [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.663 * [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.664 * * * [progress]: adding candidates to table 2.092 * * [progress]: iteration 2 / 4 2.092 * * * [progress]: picking best candidate 2.190 * * * * [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.190 * * * [progress]: localizing error 2.579 * * * [progress]: generating rewritten candidates 2.579 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 2.612 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 2.639 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1) 2.648 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 2) 2.651 * * * [progress]: generating series expansions 2.651 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 2.652 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 2.652 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1) 2.652 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 2) 2.652 * * * [progress]: simplifying candidates 2.652 * * * * [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))))> 2.652 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 2.652 * * [simplify]: iters left: 4 (10 enodes) 2.655 * * [simplify]: iters left: 3 (29 enodes) 2.661 * * [simplify]: iters left: 2 (81 enodes) 2.690 * * [simplify]: iters left: 1 (321 enodes) 2.964 * * [simplify]: Extracting #0: cost 1 inf + 0 2.964 * * [simplify]: Extracting #1: cost 64 inf + 0 2.965 * * [simplify]: Extracting #2: cost 254 inf + 0 2.967 * * [simplify]: Extracting #3: cost 250 inf + 2816 2.969 * * [simplify]: Extracting #4: cost 212 inf + 33771 2.981 * * [simplify]: Extracting #5: cost 61 inf + 193913 2.999 * * [simplify]: Extracting #6: cost 1 inf + 237431 3.026 * * [simplify]: Extracting #7: cost 0 inf + 235555 3.063 * [simplify]: Simplified to (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta)) 3.063 * [simplify]: Simplified (2 1 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 alpha beta) (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.063 * * * * [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.063 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) 3.064 * * [simplify]: iters left: 2 (5 enodes) 3.065 * * [simplify]: iters left: 1 (14 enodes) 3.067 * * [simplify]: Extracting #0: cost 1 inf + 0 3.067 * * [simplify]: Extracting #1: cost 8 inf + 0 3.068 * * [simplify]: Extracting #2: cost 7 inf + 2 3.068 * * [simplify]: Extracting #3: cost 2 inf + 1854 3.068 * * [simplify]: Extracting #4: cost 3 inf + 1854 3.068 * * [simplify]: Extracting #5: cost 1 inf + 1856 3.068 * * [simplify]: Extracting #6: cost 0 inf + 1898 3.068 * [simplify]: Simplified to (+.p16 alpha (+.p16 (*.p16 beta alpha) beta)) 3.068 * [simplify]: Simplified (2 1 1 1 1) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha (+.p16 (*.p16 beta 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.068 * * * * [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.069 * [simplify]: Simplifying (+.p16 beta (+.p16 (*.p16 beta alpha) (real->posit16 1.0))) 3.069 * * [simplify]: iters left: 3 (7 enodes) 3.071 * * [simplify]: iters left: 2 (17 enodes) 3.073 * * [simplify]: iters left: 1 (25 enodes) 3.077 * * [simplify]: Extracting #0: cost 1 inf + 0 3.077 * * [simplify]: Extracting #1: cost 7 inf + 0 3.077 * * [simplify]: Extracting #2: cost 9 inf + 1 3.077 * * [simplify]: Extracting #3: cost 5 inf + 687 3.077 * * [simplify]: Extracting #4: cost 1 inf + 1496 3.078 * * [simplify]: Extracting #5: cost 0 inf + 1538 3.078 * [simplify]: Simplified to (+.p16 beta (+.p16 (*.p16 alpha beta) (real->posit16 1.0))) 3.078 * [simplify]: Simplified (2 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 alpha (+.p16 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.078 * * * * [progress]: [ 4 / 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.078 * * * * [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.078 * * * * [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.078 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (real->posit16 1.0)) 3.078 * * [simplify]: iters left: 2 (6 enodes) 3.080 * * [simplify]: iters left: 1 (13 enodes) 3.082 * * [simplify]: Extracting #0: cost 1 inf + 0 3.082 * * [simplify]: Extracting #1: cost 3 inf + 0 3.082 * * [simplify]: Extracting #2: cost 6 inf + 0 3.082 * * [simplify]: Extracting #3: cost 2 inf + 4 3.082 * * [simplify]: Extracting #4: cost 0 inf + 689 3.082 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) (real->posit16 1.0)) 3.082 * [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.082 * * * * [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.082 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (real->posit16 1.0)) 3.082 * * [simplify]: iters left: 2 (6 enodes) 3.084 * * [simplify]: iters left: 1 (13 enodes) 3.086 * * [simplify]: Extracting #0: cost 1 inf + 0 3.086 * * [simplify]: Extracting #1: cost 3 inf + 0 3.086 * * [simplify]: Extracting #2: cost 6 inf + 0 3.086 * * [simplify]: Extracting #3: cost 2 inf + 4 3.086 * * [simplify]: Extracting #4: cost 0 inf + 689 3.086 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) (real->posit16 1.0)) 3.086 * [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.086 * * * * [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.086 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (real->posit16 1.0)) 3.086 * * [simplify]: iters left: 2 (6 enodes) 3.088 * * [simplify]: iters left: 1 (13 enodes) 3.092 * * [simplify]: Extracting #0: cost 1 inf + 0 3.092 * * [simplify]: Extracting #1: cost 3 inf + 0 3.092 * * [simplify]: Extracting #2: cost 6 inf + 0 3.092 * * [simplify]: Extracting #3: cost 2 inf + 4 3.092 * * [simplify]: Extracting #4: cost 0 inf + 689 3.092 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) (real->posit16 1.0)) 3.092 * [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.092 * * * * [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.092 * [simplify]: Simplifying (+.p16 (*.p16 beta alpha) (real->posit16 1.0)) 3.093 * * [simplify]: iters left: 2 (6 enodes) 3.095 * * [simplify]: iters left: 1 (13 enodes) 3.099 * * [simplify]: Extracting #0: cost 1 inf + 0 3.099 * * [simplify]: Extracting #1: cost 3 inf + 0 3.099 * * [simplify]: Extracting #2: cost 6 inf + 0 3.099 * * [simplify]: Extracting #3: cost 2 inf + 4 3.099 * * [simplify]: Extracting #4: cost 0 inf + 689 3.099 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) (real->posit16 1.0)) 3.100 * [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.100 * * * [progress]: adding candidates to table 3.332 * * [progress]: iteration 3 / 4 3.332 * * * [progress]: picking best candidate 3.372 * * * * [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.373 * * * [progress]: localizing error 3.733 * * * [progress]: generating rewritten candidates 3.733 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 3.768 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 3.807 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 1) 3.811 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1) 3.823 * * * [progress]: generating series expansions 3.823 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 3.823 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 3.823 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 1) 3.823 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1) 3.823 * * * [progress]: simplifying candidates 3.823 * * * * [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.824 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 3.824 * * [simplify]: iters left: 4 (10 enodes) 3.827 * * [simplify]: iters left: 3 (29 enodes) 3.837 * * [simplify]: iters left: 2 (81 enodes) 3.866 * * [simplify]: iters left: 1 (321 enodes) 4.120 * * [simplify]: Extracting #0: cost 1 inf + 0 4.120 * * [simplify]: Extracting #1: cost 64 inf + 0 4.122 * * [simplify]: Extracting #2: cost 254 inf + 0 4.124 * * [simplify]: Extracting #3: cost 250 inf + 2816 4.129 * * [simplify]: Extracting #4: cost 212 inf + 33771 4.147 * * [simplify]: Extracting #5: cost 61 inf + 193913 4.176 * * [simplify]: Extracting #6: cost 1 inf + 237431 4.213 * * [simplify]: Extracting #7: cost 0 inf + 235555 4.244 * [simplify]: Simplified to (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta)) 4.245 * [simplify]: Simplified (2 1 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 alpha (+.p16 beta (*.p16 beta alpha))) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 4.245 * * * * [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))))> 4.245 * [simplify]: Simplifying (+.p16 alpha beta) 4.245 * * [simplify]: iters left: 1 (3 enodes) 4.246 * * [simplify]: Extracting #0: cost 1 inf + 0 4.246 * * [simplify]: Extracting #1: cost 3 inf + 0 4.246 * * [simplify]: Extracting #2: cost 1 inf + 2 4.246 * * [simplify]: Extracting #3: cost 0 inf + 44 4.246 * [simplify]: Simplified to (+.p16 beta alpha) 4.246 * [simplify]: Simplified (2 1 1 1 1 1) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 beta alpha) (*.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)))) 4.246 * * * * [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))))> 4.246 * * * * [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))))> 4.246 * [simplify]: Simplifying (+.p16 (+.p16 beta (*.p16 beta alpha)) (real->posit16 1.0)) 4.246 * * [simplify]: iters left: 3 (7 enodes) 4.248 * * [simplify]: iters left: 2 (17 enodes) 4.251 * * [simplify]: iters left: 1 (25 enodes) 4.255 * * [simplify]: Extracting #0: cost 1 inf + 0 4.255 * * [simplify]: Extracting #1: cost 7 inf + 0 4.255 * * [simplify]: Extracting #2: cost 9 inf + 1 4.255 * * [simplify]: Extracting #3: cost 5 inf + 687 4.255 * * [simplify]: Extracting #4: cost 1 inf + 1496 4.255 * * [simplify]: Extracting #5: cost 0 inf + 1538 4.255 * [simplify]: Simplified to (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 alpha beta)) 4.255 * [simplify]: Simplified (2 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->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)))) 4.255 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 1.0) (+.p16 alpha (+.p16 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))))> 4.255 * * * * [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))))> 4.256 * [simplify]: Simplifying (+.p16 beta (*.p16 beta alpha)) 4.256 * * [simplify]: iters left: 2 (4 enodes) 4.256 * * [simplify]: iters left: 1 (10 enodes) 4.258 * * [simplify]: Extracting #0: cost 1 inf + 0 4.258 * * [simplify]: Extracting #1: cost 4 inf + 0 4.258 * * [simplify]: Extracting #2: cost 5 inf + 1 4.258 * * [simplify]: Extracting #3: cost 3 inf + 686 4.258 * * [simplify]: Extracting #4: cost 0 inf + 730 4.258 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) beta) 4.258 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha (+.p16 (*.p16 alpha beta) 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)))) 4.258 * * * * [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))))> 4.259 * [simplify]: Simplifying (+.p16 beta (*.p16 beta alpha)) 4.259 * * [simplify]: iters left: 2 (4 enodes) 4.260 * * [simplify]: iters left: 1 (10 enodes) 4.261 * * [simplify]: Extracting #0: cost 1 inf + 0 4.261 * * [simplify]: Extracting #1: cost 4 inf + 0 4.261 * * [simplify]: Extracting #2: cost 5 inf + 1 4.261 * * [simplify]: Extracting #3: cost 3 inf + 686 4.261 * * [simplify]: Extracting #4: cost 0 inf + 730 4.261 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) beta) 4.261 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha (+.p16 (*.p16 alpha beta) 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)))) 4.262 * * * * [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))))> 4.262 * [simplify]: Simplifying (+.p16 beta (*.p16 beta alpha)) 4.262 * * [simplify]: iters left: 2 (4 enodes) 4.263 * * [simplify]: iters left: 1 (10 enodes) 4.264 * * [simplify]: Extracting #0: cost 1 inf + 0 4.264 * * [simplify]: Extracting #1: cost 4 inf + 0 4.264 * * [simplify]: Extracting #2: cost 5 inf + 1 4.264 * * [simplify]: Extracting #3: cost 3 inf + 686 4.264 * * [simplify]: Extracting #4: cost 0 inf + 730 4.265 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) beta) 4.265 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha (+.p16 (*.p16 alpha beta) 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)))) 4.265 * * * * [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))))> 4.265 * [simplify]: Simplifying (+.p16 beta (*.p16 beta alpha)) 4.265 * * [simplify]: iters left: 2 (4 enodes) 4.266 * * [simplify]: iters left: 1 (10 enodes) 4.267 * * [simplify]: Extracting #0: cost 1 inf + 0 4.267 * * [simplify]: Extracting #1: cost 4 inf + 0 4.267 * * [simplify]: Extracting #2: cost 5 inf + 1 4.267 * * [simplify]: Extracting #3: cost 3 inf + 686 4.268 * * [simplify]: Extracting #4: cost 0 inf + 730 4.268 * [simplify]: Simplified to (+.p16 (*.p16 alpha beta) beta) 4.268 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha (+.p16 (*.p16 alpha beta) 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)))) 4.268 * * * [progress]: adding candidates to table 4.621 * * [progress]: iteration 4 / 4 4.621 * * * [progress]: picking best candidate 4.700 * * * * [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))))> 4.700 * * * [progress]: localizing error 5.126 * * * [progress]: generating rewritten candidates 5.126 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 5.152 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 5.186 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1) 5.204 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 2 1) 5.210 * * * [progress]: generating series expansions 5.210 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 5.210 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 5.210 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1) 5.210 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 2 1) 5.210 * * * [progress]: simplifying candidates 5.210 * * * * [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))))> 5.210 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 5.210 * * [simplify]: iters left: 4 (10 enodes) 5.215 * * [simplify]: iters left: 3 (29 enodes) 5.225 * * [simplify]: iters left: 2 (81 enodes) 5.265 * * [simplify]: iters left: 1 (321 enodes) 5.515 * * [simplify]: Extracting #0: cost 1 inf + 0 5.515 * * [simplify]: Extracting #1: cost 64 inf + 0 5.517 * * [simplify]: Extracting #2: cost 254 inf + 0 5.519 * * [simplify]: Extracting #3: cost 250 inf + 2816 5.523 * * [simplify]: Extracting #4: cost 212 inf + 33771 5.546 * * [simplify]: Extracting #5: cost 61 inf + 193913 5.578 * * [simplify]: Extracting #6: cost 1 inf + 237431 5.600 * * [simplify]: Extracting #7: cost 0 inf + 235555 5.631 * [simplify]: Simplified to (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta)) 5.632 * [simplify]: Simplified (2 1 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 alpha (+.p16 (+.p16 beta (*.p16 beta alpha)) (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 5.632 * * * * [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))))> 5.632 * [simplify]: Simplifying (+.p16 alpha (+.p16 beta (*.p16 beta alpha))) 5.632 * * [simplify]: iters left: 3 (5 enodes) 5.634 * * [simplify]: iters left: 2 (14 enodes) 5.638 * * [simplify]: iters left: 1 (24 enodes) 5.644 * * [simplify]: Extracting #0: cost 1 inf + 0 5.645 * * [simplify]: Extracting #1: cost 7 inf + 0 5.645 * * [simplify]: Extracting #2: cost 7 inf + 2 5.645 * * [simplify]: Extracting #3: cost 3 inf + 1492 5.645 * * [simplify]: Extracting #4: cost 4 inf + 1492 5.645 * * [simplify]: Extracting #5: cost 2 inf + 1494 5.645 * * [simplify]: Extracting #6: cost 0 inf + 1578 5.646 * [simplify]: Simplified to (+.p16 alpha (+.p16 beta (*.p16 beta alpha))) 5.646 * [simplify]: Simplified (2 1 1 1 1) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 alpha (+.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)))) 5.646 * * * * [progress]: [ 3 / 8 ] 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))))> 5.646 * * * * [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))))> 5.646 * * * * [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))))> 5.646 * [simplify]: Simplifying (+.p16 (+.p16 beta (*.p16 beta alpha)) (real->posit16 1.0)) 5.646 * * [simplify]: iters left: 3 (7 enodes) 5.649 * * [simplify]: iters left: 2 (17 enodes) 5.654 * * [simplify]: iters left: 1 (25 enodes) 5.661 * * [simplify]: Extracting #0: cost 1 inf + 0 5.661 * * [simplify]: Extracting #1: cost 7 inf + 0 5.662 * * [simplify]: Extracting #2: cost 9 inf + 1 5.662 * * [simplify]: Extracting #3: cost 5 inf + 687 5.662 * * [simplify]: Extracting #4: cost 1 inf + 1496 5.663 * * [simplify]: Extracting #5: cost 0 inf + 1538 5.663 * [simplify]: Simplified to (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 alpha beta)) 5.663 * [simplify]: Simplified (2 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->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)))) 5.663 * * * * [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))))> 5.664 * [simplify]: Simplifying (+.p16 (+.p16 beta (*.p16 beta alpha)) (real->posit16 1.0)) 5.664 * * [simplify]: iters left: 3 (7 enodes) 5.667 * * [simplify]: iters left: 2 (17 enodes) 5.671 * * [simplify]: iters left: 1 (25 enodes) 5.678 * * [simplify]: Extracting #0: cost 1 inf + 0 5.678 * * [simplify]: Extracting #1: cost 7 inf + 0 5.678 * * [simplify]: Extracting #2: cost 9 inf + 1 5.678 * * [simplify]: Extracting #3: cost 5 inf + 687 5.678 * * [simplify]: Extracting #4: cost 1 inf + 1496 5.679 * * [simplify]: Extracting #5: cost 0 inf + 1538 5.679 * [simplify]: Simplified to (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 alpha beta)) 5.679 * [simplify]: Simplified (2 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->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)))) 5.679 * * * * [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))))> 5.679 * [simplify]: Simplifying (+.p16 (+.p16 beta (*.p16 beta alpha)) (real->posit16 1.0)) 5.679 * * [simplify]: iters left: 3 (7 enodes) 5.682 * * [simplify]: iters left: 2 (17 enodes) 5.687 * * [simplify]: iters left: 1 (25 enodes) 5.693 * * [simplify]: Extracting #0: cost 1 inf + 0 5.693 * * [simplify]: Extracting #1: cost 7 inf + 0 5.693 * * [simplify]: Extracting #2: cost 9 inf + 1 5.693 * * [simplify]: Extracting #3: cost 5 inf + 687 5.693 * * [simplify]: Extracting #4: cost 1 inf + 1496 5.694 * * [simplify]: Extracting #5: cost 0 inf + 1538 5.694 * [simplify]: Simplified to (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 alpha beta)) 5.694 * [simplify]: Simplified (2 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->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)))) 5.694 * * * * [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))))> 5.694 * [simplify]: Simplifying (+.p16 (+.p16 beta (*.p16 beta alpha)) (real->posit16 1.0)) 5.694 * * [simplify]: iters left: 3 (7 enodes) 5.697 * * [simplify]: iters left: 2 (17 enodes) 5.702 * * [simplify]: iters left: 1 (25 enodes) 5.708 * * [simplify]: Extracting #0: cost 1 inf + 0 5.708 * * [simplify]: Extracting #1: cost 7 inf + 0 5.708 * * [simplify]: Extracting #2: cost 9 inf + 1 5.708 * * [simplify]: Extracting #3: cost 5 inf + 687 5.708 * * [simplify]: Extracting #4: cost 1 inf + 1496 5.709 * * [simplify]: Extracting #5: cost 0 inf + 1538 5.709 * [simplify]: Simplified to (+.p16 (+.p16 beta (real->posit16 1.0)) (*.p16 alpha beta)) 5.709 * [simplify]: Simplified (2 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 alpha (+.p16 (+.p16 beta (real->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)))) 5.709 * * * [progress]: adding candidates to table 6.032 * [progress]: [Phase 3 of 3] Extracting. 6.032 * * [regime]: Finding splitpoints for: (#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 (+.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 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))))))>) 6.035 * * * [regime-changes]: Trying 2 branch expressions: (beta alpha) 6.035 * * * * [regimes]: Trying to branch on beta from (#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 (+.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 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))))))>) 6.192 * * * * [regimes]: Trying to branch on alpha from (#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 (+.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 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))))))>) 6.369 * * * [regime]: Found split indices: #