0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.003 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.004 * * * * [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.022 * * * * [points]: Setting MPFR precision to 320 0.025 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.032 * * * * [points]: Setting MPFR precision to 64 0.036 * * * * [points]: Setting MPFR precision to 320 0.041 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.048 * * * * [points]: Setting MPFR precision to 64 0.056 * * * * [points]: Setting MPFR precision to 320 0.064 * * * * [points]: Computing exacts for 256 points 0.071 * * * * [points]: Setting MPFR precision to 64 0.096 * * * * [points]: Setting MPFR precision to 320 0.120 * * * * [points]: Filtering points with unrepresentable outputs 0.121 * * * * [points]: Sampling 112 additional inputs, on iter 1 have 144 / 256 0.121 * * * * [points]: Computing exacts on every 7 of 112 points to ramp up precision 0.127 * * * * [points]: Setting MPFR precision to 64 0.128 * * * * [points]: Setting MPFR precision to 320 0.144 * * * * [points]: Computing exacts on every 3 of 112 points to ramp up precision 0.150 * * * * [points]: Setting MPFR precision to 64 0.152 * * * * [points]: Setting MPFR precision to 320 0.153 * * * * [points]: Computing exacts for 112 points 0.157 * * * * [points]: Setting MPFR precision to 64 0.165 * * * * [points]: Setting MPFR precision to 320 0.176 * * * * [points]: Filtering points with unrepresentable outputs 0.177 * * * * [points]: Sampling 45 additional inputs, on iter 2 have 211 / 256 0.177 * * * * [points]: Computing exacts on every 2 of 45 points to ramp up precision 0.184 * * * * [points]: Setting MPFR precision to 64 0.186 * * * * [points]: Setting MPFR precision to 320 0.188 * * * * [points]: Computing exacts for 45 points 0.195 * * * * [points]: Setting MPFR precision to 64 0.199 * * * * [points]: Setting MPFR precision to 320 0.204 * * * * [points]: Filtering points with unrepresentable outputs 0.204 * * * * [points]: Sampling 19 additional inputs, on iter 3 have 237 / 256 0.204 * * * * [points]: Computing exacts for 19 points 0.212 * * * * [points]: Setting MPFR precision to 64 0.214 * * * * [points]: Setting MPFR precision to 320 0.216 * * * * [points]: Filtering points with unrepresentable outputs 0.216 * * * * [points]: Sampling 7 additional inputs, on iter 4 have 249 / 256 0.216 * * * * [points]: Computing exacts for 7 points 0.223 * * * * [points]: Setting MPFR precision to 64 0.224 * * * * [points]: Setting MPFR precision to 320 0.225 * * * * [points]: Filtering points with unrepresentable outputs 0.225 * * * * [points]: Sampling 4 additional inputs, on iter 5 have 252 / 256 0.225 * * * * [points]: Computing exacts for 4 points 0.229 * * * * [points]: Setting MPFR precision to 64 0.230 * * * * [points]: Setting MPFR precision to 320 0.230 * * * * [points]: Filtering points with unrepresentable outputs 0.230 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 254 / 256 0.230 * * * * [points]: Computing exacts for 4 points 0.234 * * * * [points]: Setting MPFR precision to 64 0.234 * * * * [points]: Setting MPFR precision to 320 0.235 * * * * [points]: Filtering points with unrepresentable outputs 0.235 * * * * [points]: Sampling 4 additional inputs, on iter 7 have 255 / 256 0.235 * * * * [points]: Computing exacts for 4 points 0.239 * * * * [points]: Setting MPFR precision to 64 0.239 * * * * [points]: Setting MPFR precision to 320 0.239 * * * * [points]: Filtering points with unrepresentable outputs 0.239 * * * * [points]: Sampled 256 points with exact outputs 0.239 * * * [progress]: [2/2] Setting up program. 0.267 * [progress]: [Phase 2 of 3] Improving. 0.267 * * * * [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.267 * [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.267 * * [simplify]: iters left: 6 (18 enodes) 0.274 * * [simplify]: iters left: 5 (46 enodes) 0.288 * * [simplify]: iters left: 4 (118 enodes) 0.342 * * [simplify]: Extracting #0: cost 1 inf + 0 0.342 * * [simplify]: Extracting #1: cost 10 inf + 0 0.342 * * [simplify]: Extracting #2: cost 62 inf + 0 0.342 * * [simplify]: Extracting #3: cost 165 inf + 2 0.344 * * [simplify]: Extracting #4: cost 154 inf + 3708 0.345 * * [simplify]: Extracting #5: cost 131 inf + 9961 0.347 * * [simplify]: Extracting #6: cost 129 inf + 10365 0.352 * * [simplify]: Extracting #7: cost 82 inf + 46686 0.367 * * [simplify]: Extracting #8: cost 5 inf + 102245 0.382 * * [simplify]: Extracting #9: cost 0 inf + 105668 0.395 * [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.395 * [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.441 * * [progress]: iteration 1 / 4 0.441 * * * [progress]: picking best candidate 0.468 * * * * [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.468 * * * [progress]: localizing error 0.689 * * * [progress]: generating rewritten candidates 0.689 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 0.757 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1) 0.768 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 0.833 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 0.928 * * * [progress]: generating series expansions 0.929 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 0.929 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1) 0.929 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 0.929 * * * * [progress]: [ 4 / 4 ] generating series at (2) 0.929 * * * [progress]: simplifying candidates 0.929 * * * * [progress]: [ 1 / 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))))> 0.929 * * * * [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))))> 0.929 * * * * [progress]: [ 3 / 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))))> 0.929 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 0.929 * * [simplify]: iters left: 3 (8 enodes) 0.933 * * [simplify]: iters left: 2 (21 enodes) 0.939 * * [simplify]: iters left: 1 (43 enodes) 0.951 * * [simplify]: Extracting #0: cost 1 inf + 0 0.952 * * [simplify]: Extracting #1: cost 16 inf + 0 0.952 * * [simplify]: Extracting #2: cost 16 inf + 2 0.952 * * [simplify]: Extracting #3: cost 13 inf + 367 0.952 * * [simplify]: Extracting #4: cost 0 inf + 3718 0.953 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 0.953 * [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)))) 0.953 * * * * [progress]: [ 4 / 8 ] 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))))))> 0.953 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 0.953 * * [simplify]: iters left: 4 (15 enodes) 0.957 * * [simplify]: iters left: 3 (36 enodes) 0.963 * * [simplify]: iters left: 2 (66 enodes) 0.984 * * [simplify]: iters left: 1 (90 enodes) 1.003 * * [simplify]: Extracting #0: cost 1 inf + 0 1.003 * * [simplify]: Extracting #1: cost 3 inf + 0 1.003 * * [simplify]: Extracting #2: cost 20 inf + 0 1.003 * * [simplify]: Extracting #3: cost 23 inf + 2 1.004 * * [simplify]: Extracting #4: cost 19 inf + 1493 1.004 * * [simplify]: Extracting #5: cost 9 inf + 3152 1.005 * * [simplify]: Extracting #6: cost 2 inf + 4970 1.006 * * [simplify]: Extracting #7: cost 0 inf + 6578 1.008 * [simplify]: Simplified to (/.p16 (*.p16 (+.p16 beta (real->posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) (+.p16 beta alpha))) 1.008 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (/.p16 (*.p16 (+.p16 beta (real->posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) (+.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)))))) 1.008 * * * * [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))))> 1.008 * [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.008 * * [simplify]: iters left: 6 (18 enodes) 1.017 * * [simplify]: iters left: 5 (46 enodes) 1.033 * * [simplify]: iters left: 4 (118 enodes) 1.078 * * [simplify]: Extracting #0: cost 1 inf + 0 1.078 * * [simplify]: Extracting #1: cost 10 inf + 0 1.079 * * [simplify]: Extracting #2: cost 62 inf + 0 1.079 * * [simplify]: Extracting #3: cost 165 inf + 2 1.080 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.082 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.084 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.087 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.094 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.105 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.116 * [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.116 * [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.116 * * * * [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))))> 1.116 * [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.116 * * [simplify]: iters left: 6 (18 enodes) 1.123 * * [simplify]: iters left: 5 (46 enodes) 1.132 * * [simplify]: iters left: 4 (118 enodes) 1.183 * * [simplify]: Extracting #0: cost 1 inf + 0 1.183 * * [simplify]: Extracting #1: cost 10 inf + 0 1.183 * * [simplify]: Extracting #2: cost 62 inf + 0 1.184 * * [simplify]: Extracting #3: cost 165 inf + 2 1.185 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.187 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.190 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.196 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.206 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.215 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.223 * [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.224 * [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.224 * * * * [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))))> 1.224 * [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.224 * * [simplify]: iters left: 6 (18 enodes) 1.229 * * [simplify]: iters left: 5 (46 enodes) 1.238 * * [simplify]: iters left: 4 (118 enodes) 1.284 * * [simplify]: Extracting #0: cost 1 inf + 0 1.284 * * [simplify]: Extracting #1: cost 10 inf + 0 1.285 * * [simplify]: Extracting #2: cost 62 inf + 0 1.285 * * [simplify]: Extracting #3: cost 165 inf + 2 1.287 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.288 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.290 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.293 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.301 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.310 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.321 * [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.321 * [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.321 * * * * [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))))> 1.321 * [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.321 * * [simplify]: iters left: 6 (18 enodes) 1.330 * * [simplify]: iters left: 5 (46 enodes) 1.342 * * [simplify]: iters left: 4 (118 enodes) 1.390 * * [simplify]: Extracting #0: cost 1 inf + 0 1.390 * * [simplify]: Extracting #1: cost 10 inf + 0 1.390 * * [simplify]: Extracting #2: cost 62 inf + 0 1.391 * * [simplify]: Extracting #3: cost 165 inf + 2 1.392 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.393 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.394 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.397 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.405 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.413 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.424 * [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.424 * [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.424 * * * [progress]: adding candidates to table 1.756 * * [progress]: iteration 2 / 4 1.756 * * * [progress]: picking best candidate 1.846 * * * * [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))))> 1.846 * * * [progress]: localizing error 2.222 * * * [progress]: generating rewritten candidates 2.222 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 2.259 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 2.307 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 1) 2.314 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 1 1 2) 2.320 * * * [progress]: generating series expansions 2.320 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 2.320 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 2.320 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 1) 2.320 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 1 1 2) 2.320 * * * [progress]: simplifying candidates 2.320 * * * * [progress]: [ 1 / 8 ] simplifiying candidate #posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.320 * [simplify]: Simplifying (+.p16 (+.p16 alpha (+.p16 beta (*.p16 beta alpha))) (real->posit16 1.0)) 2.320 * * [simplify]: iters left: 4 (8 enodes) 2.324 * * [simplify]: iters left: 3 (21 enodes) 2.330 * * [simplify]: iters left: 2 (41 enodes) 2.337 * * [simplify]: iters left: 1 (61 enodes) 2.347 * * [simplify]: Extracting #0: cost 1 inf + 0 2.347 * * [simplify]: Extracting #1: cost 16 inf + 0 2.347 * * [simplify]: Extracting #2: cost 17 inf + 2 2.347 * * [simplify]: Extracting #3: cost 12 inf + 1091 2.347 * * [simplify]: Extracting #4: cost 3 inf + 3553 2.348 * * [simplify]: Extracting #5: cost 0 inf + 4280 2.349 * [simplify]: Simplified to (*.p16 (+.p16 beta (real->posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) 2.349 * [simplify]: Simplified (2 1 1) to (λ (alpha beta) (/.p16 (/.p16 (*.p16 (+.p16 beta (real->posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 2.349 * * * * [progress]: [ 2 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.349 * [simplify]: Simplifying (*.p16 beta alpha) 2.349 * * [simplify]: iters left: 1 (3 enodes) 2.351 * * [simplify]: Extracting #0: cost 1 inf + 0 2.351 * * [simplify]: Extracting #1: cost 3 inf + 0 2.351 * * [simplify]: Extracting #2: cost 1 inf + 2 2.351 * * [simplify]: Extracting #3: cost 0 inf + 324 2.351 * [simplify]: Simplified to (*.p16 alpha beta) 2.351 * [simplify]: Simplified (2 1 1 1 1 2) to (λ (alpha beta) (/.p16 (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 alpha beta)) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 2.351 * * * * [progress]: [ 3 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.351 * * * * [progress]: [ 4 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.351 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.351 * * * * [progress]: [ 6 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.351 * * * * [progress]: [ 7 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.351 * * * * [progress]: [ 8 / 8 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 2.351 * * * [progress]: adding candidates to table 2.608 * * [progress]: iteration 3 / 4 2.608 * * * [progress]: picking best candidate 2.700 * * * * [pick]: Picked #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.700 * * * [progress]: localizing error 3.077 * * * [progress]: generating rewritten candidates 3.077 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 3.152 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1) 3.161 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 3.178 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 3.281 * * * [progress]: generating series expansions 3.281 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 3.281 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1) 3.281 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 3.281 * * * * [progress]: [ 4 / 4 ] generating series at (2) 3.281 * * * [progress]: simplifying candidates 3.281 * * * * [progress]: [ 1 / 11 ] 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.281 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 3.281 * * [simplify]: iters left: 3 (9 enodes) 3.284 * * [simplify]: iters left: 2 (22 enodes) 3.290 * * [simplify]: iters left: 1 (30 enodes) 3.299 * * [simplify]: Extracting #0: cost 1 inf + 0 3.299 * * [simplify]: Extracting #1: cost 7 inf + 0 3.299 * * [simplify]: Extracting #2: cost 7 inf + 2 3.299 * * [simplify]: Extracting #3: cost 8 inf + 44 3.299 * * [simplify]: Extracting #4: cost 4 inf + 48 3.300 * * [simplify]: Extracting #5: cost 1 inf + 1137 3.300 * * [simplify]: Extracting #6: cost 0 inf + 1500 3.300 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 3.300 * [simplify]: Simplified (2 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 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.300 * * * * [progress]: [ 2 / 11 ] 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.300 * * * * [progress]: [ 3 / 11 ] 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.300 * * * * [progress]: [ 4 / 11 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 3.301 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 3.301 * * [simplify]: iters left: 4 (10 enodes) 3.303 * * [simplify]: iters left: 3 (26 enodes) 3.308 * * [simplify]: iters left: 2 (53 enodes) 3.319 * * [simplify]: iters left: 1 (150 enodes) 3.369 * * [simplify]: Extracting #0: cost 1 inf + 0 3.369 * * [simplify]: Extracting #1: cost 24 inf + 0 3.370 * * [simplify]: Extracting #2: cost 52 inf + 0 3.370 * * [simplify]: Extracting #3: cost 46 inf + 970 3.371 * * [simplify]: Extracting #4: cost 14 inf + 16705 3.375 * * [simplify]: Extracting #5: cost 0 inf + 25635 3.379 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 3.380 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) 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.380 * * * * [progress]: [ 5 / 11 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 alpha beta) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (*.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.380 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 3.380 * * [simplify]: iters left: 4 (10 enodes) 3.385 * * [simplify]: iters left: 3 (31 enodes) 3.393 * * [simplify]: iters left: 2 (85 enodes) 3.419 * * [simplify]: iters left: 1 (201 enodes) 3.475 * * [simplify]: Extracting #0: cost 1 inf + 0 3.475 * * [simplify]: Extracting #1: cost 27 inf + 0 3.476 * * [simplify]: Extracting #2: cost 61 inf + 0 3.476 * * [simplify]: Extracting #3: cost 50 inf + 1655 3.480 * * [simplify]: Extracting #4: cost 9 inf + 29980 3.485 * * [simplify]: Extracting #5: cost 0 inf + 35454 3.493 * [simplify]: Simplified to (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta) alpha)) 3.493 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (*.p16 (+.p16 alpha beta) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta) alpha)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 3.493 * * * * [progress]: [ 6 / 11 ] 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.493 * * * * [progress]: [ 7 / 11 ] simplifiying candidate #posit16 1.0)) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (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)))))))> 3.494 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 3.494 * * [simplify]: iters left: 3 (8 enodes) 3.498 * * [simplify]: iters left: 2 (21 enodes) 3.505 * * [simplify]: iters left: 1 (43 enodes) 3.514 * * [simplify]: Extracting #0: cost 1 inf + 0 3.514 * * [simplify]: Extracting #1: cost 16 inf + 0 3.514 * * [simplify]: Extracting #2: cost 16 inf + 2 3.514 * * [simplify]: Extracting #3: cost 13 inf + 367 3.515 * * [simplify]: Extracting #4: cost 0 inf + 3718 3.515 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 3.515 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) (*.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (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))))))) 3.515 * * * * [progress]: [ 8 / 11 ] 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.516 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 3.516 * * [simplify]: iters left: 3 (8 enodes) 3.518 * * [simplify]: iters left: 2 (21 enodes) 3.521 * * [simplify]: iters left: 1 (43 enodes) 3.529 * * [simplify]: Extracting #0: cost 1 inf + 0 3.529 * * [simplify]: Extracting #1: cost 16 inf + 0 3.529 * * [simplify]: Extracting #2: cost 16 inf + 2 3.529 * * [simplify]: Extracting #3: cost 13 inf + 367 3.530 * * [simplify]: Extracting #4: cost 0 inf + 3718 3.530 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 3.530 * [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)))) 3.530 * * * * [progress]: [ 9 / 11 ] 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.530 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 3.530 * * [simplify]: iters left: 3 (8 enodes) 3.532 * * [simplify]: iters left: 2 (21 enodes) 3.536 * * [simplify]: iters left: 1 (43 enodes) 3.544 * * [simplify]: Extracting #0: cost 1 inf + 0 3.544 * * [simplify]: Extracting #1: cost 16 inf + 0 3.544 * * [simplify]: Extracting #2: cost 16 inf + 2 3.544 * * [simplify]: Extracting #3: cost 13 inf + 367 3.545 * * [simplify]: Extracting #4: cost 0 inf + 3718 3.545 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 3.545 * [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)))) 3.545 * * * * [progress]: [ 10 / 11 ] 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.545 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 3.545 * * [simplify]: iters left: 3 (8 enodes) 3.547 * * [simplify]: iters left: 2 (21 enodes) 3.551 * * [simplify]: iters left: 1 (43 enodes) 3.559 * * [simplify]: Extracting #0: cost 1 inf + 0 3.559 * * [simplify]: Extracting #1: cost 16 inf + 0 3.559 * * [simplify]: Extracting #2: cost 16 inf + 2 3.559 * * [simplify]: Extracting #3: cost 13 inf + 367 3.559 * * [simplify]: Extracting #4: cost 0 inf + 3718 3.560 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 3.560 * [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)))) 3.560 * * * * [progress]: [ 11 / 11 ] 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.560 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 3.560 * * [simplify]: iters left: 3 (8 enodes) 3.562 * * [simplify]: iters left: 2 (21 enodes) 3.566 * * [simplify]: iters left: 1 (43 enodes) 3.580 * * [simplify]: Extracting #0: cost 1 inf + 0 3.580 * * [simplify]: Extracting #1: cost 16 inf + 0 3.580 * * [simplify]: Extracting #2: cost 16 inf + 2 3.580 * * [simplify]: Extracting #3: cost 13 inf + 367 3.581 * * [simplify]: Extracting #4: cost 0 inf + 3718 3.582 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 3.582 * [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)))) 3.582 * * * [progress]: adding candidates to table 4.150 * * [progress]: iteration 4 / 4 4.151 * * * [progress]: picking best candidate 4.283 * * * * [pick]: Picked #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 4.284 * * * [progress]: localizing error 4.782 * * * [progress]: generating rewritten candidates 4.782 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 4.869 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1) 4.889 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 1) 4.901 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2) 4.906 * * * [progress]: generating series expansions 4.906 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 4.906 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1) 4.906 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 1) 4.906 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2) 4.906 * * * [progress]: simplifying candidates 4.906 * * * * [progress]: [ 1 / 16 ] 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.907 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 4.907 * * [simplify]: iters left: 3 (9 enodes) 4.909 * * [simplify]: iters left: 2 (22 enodes) 4.913 * * [simplify]: iters left: 1 (30 enodes) 4.918 * * [simplify]: Extracting #0: cost 1 inf + 0 4.918 * * [simplify]: Extracting #1: cost 7 inf + 0 4.918 * * [simplify]: Extracting #2: cost 7 inf + 2 4.918 * * [simplify]: Extracting #3: cost 8 inf + 44 4.918 * * [simplify]: Extracting #4: cost 4 inf + 48 4.919 * * [simplify]: Extracting #5: cost 1 inf + 1137 4.919 * * [simplify]: Extracting #6: cost 0 inf + 1500 4.919 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 4.919 * [simplify]: Simplified (2 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 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 4.919 * * * * [progress]: [ 2 / 16 ] 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.919 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 4.919 * * [simplify]: iters left: 3 (9 enodes) 4.922 * * [simplify]: iters left: 2 (22 enodes) 4.925 * * [simplify]: iters left: 1 (30 enodes) 4.930 * * [simplify]: Extracting #0: cost 1 inf + 0 4.930 * * [simplify]: Extracting #1: cost 7 inf + 0 4.930 * * [simplify]: Extracting #2: cost 7 inf + 2 4.930 * * [simplify]: Extracting #3: cost 8 inf + 44 4.930 * * [simplify]: Extracting #4: cost 4 inf + 48 4.930 * * [simplify]: Extracting #5: cost 1 inf + 1137 4.931 * * [simplify]: Extracting #6: cost 0 inf + 1500 4.931 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 4.931 * [simplify]: Simplified (2 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 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 4.931 * * * * [progress]: [ 3 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 4.931 * * * * [progress]: [ 4 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 4.931 * * * * [progress]: [ 5 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) alpha) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 4.931 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) beta) 4.931 * * [simplify]: iters left: 4 (10 enodes) 4.934 * * [simplify]: iters left: 3 (24 enodes) 4.938 * * [simplify]: iters left: 2 (46 enodes) 4.946 * * [simplify]: iters left: 1 (73 enodes) 4.960 * * [simplify]: Extracting #0: cost 1 inf + 0 4.961 * * [simplify]: Extracting #1: cost 9 inf + 0 4.961 * * [simplify]: Extracting #2: cost 16 inf + 322 4.961 * * [simplify]: Extracting #3: cost 17 inf + 323 4.961 * * [simplify]: Extracting #4: cost 11 inf + 1052 4.962 * * [simplify]: Extracting #5: cost 3 inf + 5713 4.963 * * [simplify]: Extracting #6: cost 0 inf + 5883 4.964 * [simplify]: Simplified to (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) beta) 4.964 * [simplify]: Simplified (2 1 2 1 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) alpha) (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 4.964 * * * * [progress]: [ 6 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (+.p16 (*.p16 alpha (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 beta (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 4.964 * [simplify]: Simplifying (*.p16 beta (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 4.965 * * [simplify]: iters left: 4 (10 enodes) 4.970 * * [simplify]: iters left: 3 (30 enodes) 4.981 * * [simplify]: iters left: 2 (59 enodes) 5.003 * * [simplify]: iters left: 1 (80 enodes) 5.026 * * [simplify]: Extracting #0: cost 1 inf + 0 5.027 * * [simplify]: Extracting #1: cost 9 inf + 0 5.027 * * [simplify]: Extracting #2: cost 16 inf + 322 5.027 * * [simplify]: Extracting #3: cost 16 inf + 645 5.027 * * [simplify]: Extracting #4: cost 12 inf + 1051 5.028 * * [simplify]: Extracting #5: cost 3 inf + 5754 5.029 * * [simplify]: Extracting #6: cost 0 inf + 5883 5.030 * [simplify]: Simplified to (*.p16 beta (+.p16 beta (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) alpha))) 5.030 * [simplify]: Simplified (2 1 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 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 beta (+.p16 beta (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) alpha)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 5.030 * * * * [progress]: [ 7 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 alpha beta) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 5.030 * * * * [progress]: [ 8 / 16 ] 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.030 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 5.031 * * [simplify]: iters left: 3 (9 enodes) 5.035 * * [simplify]: iters left: 2 (22 enodes) 5.042 * * [simplify]: iters left: 1 (30 enodes) 5.051 * * [simplify]: Extracting #0: cost 1 inf + 0 5.051 * * [simplify]: Extracting #1: cost 7 inf + 0 5.051 * * [simplify]: Extracting #2: cost 7 inf + 2 5.052 * * [simplify]: Extracting #3: cost 8 inf + 44 5.052 * * [simplify]: Extracting #4: cost 4 inf + 48 5.052 * * [simplify]: Extracting #5: cost 1 inf + 1137 5.052 * * [simplify]: Extracting #6: cost 0 inf + 1500 5.053 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 5.053 * [simplify]: Simplified (2 1 2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 beta alpha) (*.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.053 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 5.053 * * [simplify]: iters left: 3 (9 enodes) 5.058 * * [simplify]: iters left: 2 (22 enodes) 5.065 * * [simplify]: iters left: 1 (30 enodes) 5.074 * * [simplify]: Extracting #0: cost 1 inf + 0 5.074 * * [simplify]: Extracting #1: cost 7 inf + 0 5.074 * * [simplify]: Extracting #2: cost 7 inf + 2 5.074 * * [simplify]: Extracting #3: cost 8 inf + 44 5.074 * * [simplify]: Extracting #4: cost 4 inf + 48 5.074 * * [simplify]: Extracting #5: cost 1 inf + 1137 5.075 * * [simplify]: Extracting #6: cost 0 inf + 1500 5.075 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 5.075 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 5.075 * * * * [progress]: [ 9 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) alpha) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) beta) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1)))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 5.076 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) alpha) 5.076 * * [simplify]: iters left: 4 (10 enodes) 5.081 * * [simplify]: iters left: 3 (24 enodes) 5.089 * * [simplify]: iters left: 2 (45 enodes) 5.106 * * [simplify]: iters left: 1 (73 enodes) 5.133 * * [simplify]: Extracting #0: cost 1 inf + 0 5.133 * * [simplify]: Extracting #1: cost 9 inf + 0 5.134 * * [simplify]: Extracting #2: cost 17 inf + 1 5.134 * * [simplify]: Extracting #3: cost 17 inf + 323 5.134 * * [simplify]: Extracting #4: cost 13 inf + 689 5.134 * * [simplify]: Extracting #5: cost 4 inf + 4709 5.135 * * [simplify]: Extracting #6: cost 0 inf + 5883 5.136 * [simplify]: Simplified to (*.p16 alpha (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1)))) 5.136 * [simplify]: Simplified (2 1 2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (*.p16 alpha (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) beta) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1)))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 5.137 * * * * [progress]: [ 10 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 alpha (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (*.p16 beta (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1)))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 5.137 * [simplify]: Simplifying (*.p16 alpha (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 5.137 * * [simplify]: iters left: 4 (10 enodes) 5.143 * * [simplify]: iters left: 3 (30 enodes) 5.155 * * [simplify]: iters left: 2 (59 enodes) 5.174 * * [simplify]: iters left: 1 (78 enodes) 5.200 * * [simplify]: Extracting #0: cost 1 inf + 0 5.200 * * [simplify]: Extracting #1: cost 9 inf + 0 5.200 * * [simplify]: Extracting #2: cost 17 inf + 1 5.200 * * [simplify]: Extracting #3: cost 16 inf + 645 5.201 * * [simplify]: Extracting #4: cost 12 inf + 1051 5.201 * * [simplify]: Extracting #5: cost 5 inf + 3747 5.202 * * [simplify]: Extracting #6: cost 0 inf + 6203 5.203 * * [simplify]: Extracting #7: cost 0 inf + 5883 5.204 * [simplify]: Simplified to (*.p16 alpha (+.p16 beta (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))))) 5.204 * [simplify]: Simplified (2 1 2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (*.p16 alpha (+.p16 beta (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (*.p16 beta (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1)))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 5.204 * * * * [progress]: [ 11 / 16 ] 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.205 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 5.205 * * [simplify]: iters left: 3 (9 enodes) 5.210 * * [simplify]: iters left: 2 (22 enodes) 5.218 * * [simplify]: iters left: 1 (30 enodes) 5.227 * * [simplify]: Extracting #0: cost 1 inf + 0 5.228 * * [simplify]: Extracting #1: cost 7 inf + 0 5.228 * * [simplify]: Extracting #2: cost 7 inf + 2 5.228 * * [simplify]: Extracting #3: cost 8 inf + 44 5.228 * * [simplify]: Extracting #4: cost 4 inf + 48 5.228 * * [simplify]: Extracting #5: cost 1 inf + 1137 5.229 * * [simplify]: Extracting #6: cost 0 inf + 1500 5.229 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 5.229 * [simplify]: Simplified (2 1 2 1) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 beta alpha) (*.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.229 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 5.229 * * [simplify]: iters left: 3 (9 enodes) 5.234 * * [simplify]: iters left: 2 (22 enodes) 5.242 * * [simplify]: iters left: 1 (30 enodes) 5.251 * * [simplify]: Extracting #0: cost 1 inf + 0 5.252 * * [simplify]: Extracting #1: cost 7 inf + 0 5.252 * * [simplify]: Extracting #2: cost 7 inf + 2 5.252 * * [simplify]: Extracting #3: cost 8 inf + 44 5.252 * * [simplify]: Extracting #4: cost 4 inf + 48 5.252 * * [simplify]: Extracting #5: cost 1 inf + 1137 5.252 * * [simplify]: Extracting #6: cost 0 inf + 1500 5.253 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 5.253 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0)))) 5.253 * * * * [progress]: [ 12 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 5.253 * * * * [progress]: [ 13 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 5.254 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 5.254 * * [simplify]: iters left: 4 (10 enodes) 5.259 * * [simplify]: iters left: 3 (26 enodes) 5.268 * * [simplify]: iters left: 2 (53 enodes) 5.295 * * [simplify]: iters left: 1 (150 enodes) 5.381 * * [simplify]: Extracting #0: cost 1 inf + 0 5.381 * * [simplify]: Extracting #1: cost 24 inf + 0 5.381 * * [simplify]: Extracting #2: cost 52 inf + 0 5.382 * * [simplify]: Extracting #3: cost 46 inf + 970 5.384 * * [simplify]: Extracting #4: cost 14 inf + 16705 5.389 * * [simplify]: Extracting #5: cost 0 inf + 25635 5.394 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 5.394 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) 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.394 * * * * [progress]: [ 14 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 5.395 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 5.395 * * [simplify]: iters left: 4 (10 enodes) 5.400 * * [simplify]: iters left: 3 (26 enodes) 5.412 * * [simplify]: iters left: 2 (53 enodes) 5.437 * * [simplify]: iters left: 1 (150 enodes) 5.522 * * [simplify]: Extracting #0: cost 1 inf + 0 5.522 * * [simplify]: Extracting #1: cost 24 inf + 0 5.523 * * [simplify]: Extracting #2: cost 52 inf + 0 5.523 * * [simplify]: Extracting #3: cost 46 inf + 970 5.528 * * [simplify]: Extracting #4: cost 14 inf + 16705 5.533 * * [simplify]: Extracting #5: cost 0 inf + 25635 5.537 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 5.537 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) 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.538 * * * * [progress]: [ 15 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 5.538 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 5.538 * * [simplify]: iters left: 4 (10 enodes) 5.544 * * [simplify]: iters left: 3 (26 enodes) 5.554 * * [simplify]: iters left: 2 (53 enodes) 5.577 * * [simplify]: iters left: 1 (150 enodes) 5.664 * * [simplify]: Extracting #0: cost 1 inf + 0 5.664 * * [simplify]: Extracting #1: cost 24 inf + 0 5.665 * * [simplify]: Extracting #2: cost 52 inf + 0 5.665 * * [simplify]: Extracting #3: cost 46 inf + 970 5.668 * * [simplify]: Extracting #4: cost 14 inf + 16705 5.672 * * [simplify]: Extracting #5: cost 0 inf + 25635 5.677 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 5.678 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) 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.678 * * * * [progress]: [ 16 / 16 ] simplifiying candidate #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> 5.678 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 5.678 * * [simplify]: iters left: 4 (10 enodes) 5.684 * * [simplify]: iters left: 3 (26 enodes) 5.693 * * [simplify]: iters left: 2 (53 enodes) 5.718 * * [simplify]: iters left: 1 (150 enodes) 5.802 * * [simplify]: Extracting #0: cost 1 inf + 0 5.803 * * [simplify]: Extracting #1: cost 24 inf + 0 5.803 * * [simplify]: Extracting #2: cost 52 inf + 0 5.803 * * [simplify]: Extracting #3: cost 46 inf + 970 5.806 * * [simplify]: Extracting #4: cost 14 inf + 16705 5.811 * * [simplify]: Extracting #5: cost 0 inf + 25635 5.816 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 5.816 * [simplify]: Simplified (2 1 2 2) to (λ (alpha beta) (/.p16 (/.p16 (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) 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.816 * * * [progress]: adding candidates to table 6.488 * [progress]: [Phase 3 of 3] Extracting. 6.488 * * [regime]: Finding splitpoints for: (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 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 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) alpha) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) beta) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 beta (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.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 (+.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.490 * * * [regime-changes]: Trying 2 branch expressions: (beta alpha) 6.490 * * * * [regimes]: Trying to branch on beta from (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 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 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) alpha) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) beta) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 beta (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.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 (+.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.727 * * * * [regimes]: Trying to branch on alpha from (#posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 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 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 alpha beta)) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) alpha) (+.p16 (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) beta) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (*.p16 beta (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.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 (+.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 (+.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.979 * * * [regime]: Found split indices: #