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.010 * * * * [points]: Setting MPFR precision to 64 0.017 * * * * [points]: Setting MPFR precision to 320 0.018 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.025 * * * * [points]: Setting MPFR precision to 64 0.029 * * * * [points]: Setting MPFR precision to 320 0.030 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.035 * * * * [points]: Setting MPFR precision to 64 0.038 * * * * [points]: Setting MPFR precision to 320 0.041 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.045 * * * * [points]: Setting MPFR precision to 64 0.051 * * * * [points]: Setting MPFR precision to 320 0.056 * * * * [points]: Computing exacts for 256 points 0.061 * * * * [points]: Setting MPFR precision to 64 0.076 * * * * [points]: Setting MPFR precision to 320 0.091 * * * * [points]: Filtering points with unrepresentable outputs 0.091 * * * * [points]: Sampling 114 additional inputs, on iter 1 have 142 / 256 0.092 * * * * [points]: Computing exacts on every 7 of 114 points to ramp up precision 0.096 * * * * [points]: Setting MPFR precision to 64 0.097 * * * * [points]: Setting MPFR precision to 320 0.098 * * * * [points]: Computing exacts on every 3 of 114 points to ramp up precision 0.102 * * * * [points]: Setting MPFR precision to 64 0.104 * * * * [points]: Setting MPFR precision to 320 0.123 * * * * [points]: Computing exacts for 114 points 0.127 * * * * [points]: Setting MPFR precision to 64 0.136 * * * * [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.144 * * * * [points]: Computing exacts on every 3 of 55 points to ramp up precision 0.148 * * * * [points]: Setting MPFR precision to 64 0.149 * * * * [points]: Setting MPFR precision to 320 0.150 * * * * [points]: Computing exacts for 55 points 0.154 * * * * [points]: Setting MPFR precision to 64 0.157 * * * * [points]: Setting MPFR precision to 320 0.161 * * * * [points]: Filtering points with unrepresentable outputs 0.161 * * * * [points]: Sampling 24 additional inputs, on iter 3 have 232 / 256 0.161 * * * * [points]: Computing exacts for 24 points 0.165 * * * * [points]: Setting MPFR precision to 64 0.167 * * * * [points]: Setting MPFR precision to 320 0.168 * * * * [points]: Filtering points with unrepresentable outputs 0.168 * * * * [points]: Sampling 8 additional inputs, on iter 4 have 248 / 256 0.169 * * * * [points]: Computing exacts for 8 points 0.173 * * * * [points]: Setting MPFR precision to 64 0.174 * * * * [points]: Setting MPFR precision to 320 0.174 * * * * [points]: Filtering points with unrepresentable outputs 0.175 * * * * [points]: Sampling 7 additional inputs, on iter 5 have 249 / 256 0.175 * * * * [points]: Computing exacts for 7 points 0.179 * * * * [points]: Setting MPFR precision to 64 0.179 * * * * [points]: Setting MPFR precision to 320 0.180 * * * * [points]: Filtering points with unrepresentable outputs 0.180 * * * * [points]: Sampling 4 additional inputs, on iter 6 have 252 / 256 0.180 * * * * [points]: Computing exacts for 4 points 0.184 * * * * [points]: Setting MPFR precision to 64 0.185 * * * * [points]: Setting MPFR precision to 320 0.185 * * * * [points]: Filtering points with unrepresentable outputs 0.185 * * * * [points]: Sampling 4 additional inputs, on iter 7 have 254 / 256 0.185 * * * * [points]: Computing exacts for 4 points 0.189 * * * * [points]: Setting MPFR precision to 64 0.189 * * * * [points]: Setting MPFR precision to 320 0.190 * * * * [points]: Filtering points with unrepresentable outputs 0.190 * * * * [points]: Sampled 256 points with exact outputs 0.190 * * * [progress]: [2/2] Setting up program. 0.215 * [progress]: [Phase 2 of 3] Improving. 0.215 * * * * [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.216 * [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.216 * * [simplify]: iters left: 6 (18 enodes) 0.220 * * [simplify]: iters left: 5 (46 enodes) 0.228 * * [simplify]: iters left: 4 (118 enodes) 0.270 * * [simplify]: Extracting #0: cost 1 inf + 0 0.270 * * [simplify]: Extracting #1: cost 10 inf + 0 0.270 * * [simplify]: Extracting #2: cost 62 inf + 0 0.270 * * [simplify]: Extracting #3: cost 165 inf + 2 0.271 * * [simplify]: Extracting #4: cost 154 inf + 3708 0.272 * * [simplify]: Extracting #5: cost 131 inf + 9961 0.274 * * [simplify]: Extracting #6: cost 129 inf + 10365 0.277 * * [simplify]: Extracting #7: cost 82 inf + 46686 0.289 * * [simplify]: Extracting #8: cost 5 inf + 102245 0.304 * * [simplify]: Extracting #9: cost 0 inf + 105668 0.316 * [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.316 * [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.345 * * [progress]: iteration 1 / 4 0.345 * * * [progress]: picking best candidate 0.371 * * * * [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.371 * * * [progress]: localizing error 0.608 * * * [progress]: generating rewritten candidates 0.608 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 0.690 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1 1) 0.704 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 0.776 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 0.850 * * * [progress]: generating series expansions 0.850 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 0.850 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1 1) 0.850 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 0.850 * * * * [progress]: [ 4 / 4 ] generating series at (2) 0.850 * * * [progress]: simplifying candidates 0.850 * * * * [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.851 * * * * [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.851 * * * * [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.851 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 0.851 * * [simplify]: iters left: 3 (8 enodes) 0.853 * * [simplify]: iters left: 2 (21 enodes) 0.857 * * [simplify]: iters left: 1 (43 enodes) 0.865 * * [simplify]: Extracting #0: cost 1 inf + 0 0.865 * * [simplify]: Extracting #1: cost 16 inf + 0 0.865 * * [simplify]: Extracting #2: cost 16 inf + 2 0.865 * * [simplify]: Extracting #3: cost 13 inf + 367 0.866 * * [simplify]: Extracting #4: cost 0 inf + 3718 0.866 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 0.866 * [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.866 * * * * [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.867 * [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.867 * * [simplify]: iters left: 4 (15 enodes) 0.870 * * [simplify]: iters left: 3 (36 enodes) 0.877 * * [simplify]: iters left: 2 (66 enodes) 0.890 * * [simplify]: iters left: 1 (90 enodes) 0.912 * * [simplify]: Extracting #0: cost 1 inf + 0 0.913 * * [simplify]: Extracting #1: cost 3 inf + 0 0.913 * * [simplify]: Extracting #2: cost 20 inf + 0 0.913 * * [simplify]: Extracting #3: cost 23 inf + 2 0.913 * * [simplify]: Extracting #4: cost 19 inf + 1493 0.914 * * [simplify]: Extracting #5: cost 9 inf + 3152 0.915 * * [simplify]: Extracting #6: cost 2 inf + 4970 0.916 * * [simplify]: Extracting #7: cost 0 inf + 6578 0.917 * [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))) 0.917 * [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)))))) 0.917 * * * * [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))))> 0.918 * [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.918 * * [simplify]: iters left: 6 (18 enodes) 0.925 * * [simplify]: iters left: 5 (46 enodes) 0.941 * * [simplify]: iters left: 4 (118 enodes) 0.977 * * [simplify]: Extracting #0: cost 1 inf + 0 0.977 * * [simplify]: Extracting #1: cost 10 inf + 0 0.977 * * [simplify]: Extracting #2: cost 62 inf + 0 0.978 * * [simplify]: Extracting #3: cost 165 inf + 2 0.978 * * [simplify]: Extracting #4: cost 154 inf + 3708 0.980 * * [simplify]: Extracting #5: cost 131 inf + 9961 0.981 * * [simplify]: Extracting #6: cost 129 inf + 10365 0.984 * * [simplify]: Extracting #7: cost 82 inf + 46686 0.996 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.009 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.021 * [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.021 * [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.021 * * * * [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.021 * [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.021 * * [simplify]: iters left: 6 (18 enodes) 1.026 * * [simplify]: iters left: 5 (46 enodes) 1.034 * * [simplify]: iters left: 4 (118 enodes) 1.067 * * [simplify]: Extracting #0: cost 1 inf + 0 1.067 * * [simplify]: Extracting #1: cost 10 inf + 0 1.067 * * [simplify]: Extracting #2: cost 62 inf + 0 1.068 * * [simplify]: Extracting #3: cost 165 inf + 2 1.068 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.069 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.071 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.074 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.081 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.091 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.099 * [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.099 * [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.099 * * * * [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.099 * [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.099 * * [simplify]: iters left: 6 (18 enodes) 1.104 * * [simplify]: iters left: 5 (46 enodes) 1.112 * * [simplify]: iters left: 4 (118 enodes) 1.145 * * [simplify]: Extracting #0: cost 1 inf + 0 1.145 * * [simplify]: Extracting #1: cost 10 inf + 0 1.146 * * [simplify]: Extracting #2: cost 62 inf + 0 1.146 * * [simplify]: Extracting #3: cost 165 inf + 2 1.147 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.148 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.149 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.154 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.161 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.169 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.177 * [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.177 * [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.178 * * * * [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.178 * [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.178 * * [simplify]: iters left: 6 (18 enodes) 1.182 * * [simplify]: iters left: 5 (46 enodes) 1.192 * * [simplify]: iters left: 4 (118 enodes) 1.226 * * [simplify]: Extracting #0: cost 1 inf + 0 1.226 * * [simplify]: Extracting #1: cost 10 inf + 0 1.226 * * [simplify]: Extracting #2: cost 62 inf + 0 1.227 * * [simplify]: Extracting #3: cost 165 inf + 2 1.227 * * [simplify]: Extracting #4: cost 154 inf + 3708 1.229 * * [simplify]: Extracting #5: cost 131 inf + 9961 1.230 * * [simplify]: Extracting #6: cost 129 inf + 10365 1.233 * * [simplify]: Extracting #7: cost 82 inf + 46686 1.240 * * [simplify]: Extracting #8: cost 5 inf + 102245 1.248 * * [simplify]: Extracting #9: cost 0 inf + 105668 1.256 * [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.256 * [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.256 * * * [progress]: adding candidates to table 1.473 * * [progress]: iteration 2 / 4 1.473 * * * [progress]: picking best candidate 1.529 * * * * [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.530 * * * [progress]: localizing error 1.773 * * * [progress]: generating rewritten candidates 1.773 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 1.795 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 1.817 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1 1) 1.823 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 1.868 * * * [progress]: generating series expansions 1.868 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 1.868 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 1.868 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1 1) 1.868 * * * * [progress]: [ 4 / 4 ] generating series at (2) 1.868 * * * [progress]: simplifying candidates 1.868 * * * * [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))))> 1.868 * [simplify]: Simplifying (+.p16 (+.p16 alpha (+.p16 beta (*.p16 beta alpha))) (real->posit16 1.0)) 1.868 * * [simplify]: iters left: 4 (8 enodes) 1.871 * * [simplify]: iters left: 3 (21 enodes) 1.874 * * [simplify]: iters left: 2 (41 enodes) 1.881 * * [simplify]: iters left: 1 (61 enodes) 1.892 * * [simplify]: Extracting #0: cost 1 inf + 0 1.892 * * [simplify]: Extracting #1: cost 16 inf + 0 1.892 * * [simplify]: Extracting #2: cost 17 inf + 2 1.893 * * [simplify]: Extracting #3: cost 12 inf + 1091 1.893 * * [simplify]: Extracting #4: cost 3 inf + 3553 1.893 * * [simplify]: Extracting #5: cost 0 inf + 4280 1.894 * [simplify]: Simplified to (*.p16 (+.p16 beta (real->posit16 1.0)) (+.p16 alpha (real->posit16 1.0))) 1.894 * [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)))) 1.894 * * * * [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))))> 1.894 * [simplify]: Simplifying (*.p16 beta alpha) 1.894 * * [simplify]: iters left: 1 (3 enodes) 1.895 * * [simplify]: Extracting #0: cost 1 inf + 0 1.895 * * [simplify]: Extracting #1: cost 3 inf + 0 1.895 * * [simplify]: Extracting #2: cost 1 inf + 2 1.895 * * [simplify]: Extracting #3: cost 0 inf + 324 1.895 * [simplify]: Simplified to (*.p16 alpha beta) 1.895 * [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)))) 1.895 * * * * [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))))> 1.895 * * * * [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))))))> 1.895 * [simplify]: Simplifying (/.p16 (+.p16 (+.p16 alpha (+.p16 beta (*.p16 beta alpha))) (real->posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 1.896 * * [simplify]: iters left: 5 (16 enodes) 1.900 * * [simplify]: iters left: 4 (37 enodes) 1.906 * * [simplify]: iters left: 3 (65 enodes) 1.916 * * [simplify]: iters left: 2 (83 enodes) 1.930 * * [simplify]: iters left: 1 (118 enodes) 1.951 * * [simplify]: Extracting #0: cost 1 inf + 0 1.951 * * [simplify]: Extracting #1: cost 5 inf + 0 1.952 * * [simplify]: Extracting #2: cost 23 inf + 0 1.953 * * [simplify]: Extracting #3: cost 26 inf + 2 1.953 * * [simplify]: Extracting #4: cost 22 inf + 1493 1.953 * * [simplify]: Extracting #5: cost 9 inf + 3919 1.954 * * [simplify]: Extracting #6: cost 5 inf + 4927 1.955 * * [simplify]: Extracting #7: cost 0 inf + 8187 1.956 * [simplify]: Simplified to (/.p16 (*.p16 (+.p16 alpha (real->posit16 1.0)) (+.p16 (real->posit16 1.0) beta)) (+.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) beta) alpha)) 1.956 * [simplify]: Simplified (2 1) to (λ (alpha beta) (/.p16 (/.p16 (*.p16 (+.p16 alpha (real->posit16 1.0)) (+.p16 (real->posit16 1.0) beta)) (+.p16 (+.p16 (*.p16 (real->posit16 1) (real->posit16 2)) 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.956 * * * * [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.956 * * * * [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.956 * * * * [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.956 * * * * [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.956 * * * [progress]: adding candidates to table 2.114 * * [progress]: iteration 3 / 4 2.114 * * * [progress]: picking best candidate 2.171 * * * * [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.171 * * * [progress]: localizing error 2.414 * * * [progress]: generating rewritten candidates 2.414 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 2.472 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 2.492 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 1) 2.506 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 2.611 * * * [progress]: generating series expansions 2.611 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 2.611 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 2.611 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 1) 2.611 * * * * [progress]: [ 4 / 4 ] generating series at (2) 2.612 * * * [progress]: simplifying candidates 2.612 * * * * [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))))> 2.612 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 2.612 * * [simplify]: iters left: 3 (9 enodes) 2.616 * * [simplify]: iters left: 2 (22 enodes) 2.622 * * [simplify]: iters left: 1 (30 enodes) 2.630 * * [simplify]: Extracting #0: cost 1 inf + 0 2.630 * * [simplify]: Extracting #1: cost 7 inf + 0 2.630 * * [simplify]: Extracting #2: cost 7 inf + 2 2.630 * * [simplify]: Extracting #3: cost 8 inf + 44 2.630 * * [simplify]: Extracting #4: cost 4 inf + 48 2.630 * * [simplify]: Extracting #5: cost 1 inf + 1137 2.631 * * [simplify]: Extracting #6: cost 0 inf + 1500 2.631 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 2.631 * [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)))) 2.631 * * * * [progress]: [ 2 / 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))))> 2.631 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 2.632 * * [simplify]: iters left: 4 (10 enodes) 2.636 * * [simplify]: iters left: 3 (26 enodes) 2.643 * * [simplify]: iters left: 2 (53 enodes) 2.662 * * [simplify]: iters left: 1 (150 enodes) 2.714 * * [simplify]: Extracting #0: cost 1 inf + 0 2.715 * * [simplify]: Extracting #1: cost 24 inf + 0 2.715 * * [simplify]: Extracting #2: cost 52 inf + 0 2.715 * * [simplify]: Extracting #3: cost 46 inf + 970 2.716 * * [simplify]: Extracting #4: cost 14 inf + 16705 2.718 * * [simplify]: Extracting #5: cost 0 inf + 25635 2.721 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 2.721 * [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)))) 2.721 * * * * [progress]: [ 3 / 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))))> 2.721 * [simplify]: Simplifying (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 2.721 * * [simplify]: iters left: 4 (10 enodes) 2.724 * * [simplify]: iters left: 3 (31 enodes) 2.730 * * [simplify]: iters left: 2 (85 enodes) 2.754 * * [simplify]: iters left: 1 (201 enodes) 2.824 * * [simplify]: Extracting #0: cost 1 inf + 0 2.824 * * [simplify]: Extracting #1: cost 27 inf + 0 2.824 * * [simplify]: Extracting #2: cost 61 inf + 0 2.825 * * [simplify]: Extracting #3: cost 50 inf + 1655 2.827 * * [simplify]: Extracting #4: cost 9 inf + 29980 2.832 * * [simplify]: Extracting #5: cost 0 inf + 35454 2.836 * [simplify]: Simplified to (*.p16 (*.p16 (real->posit16 2) (real->posit16 1)) (+.p16 (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta) alpha)) 2.836 * [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)))) 2.837 * * * * [progress]: [ 4 / 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))))> 2.837 * * * * [progress]: [ 5 / 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))))> 2.837 * * * * [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))))> 2.837 * * * * [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)))))))> 2.837 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 2.837 * * [simplify]: iters left: 3 (8 enodes) 2.840 * * [simplify]: iters left: 2 (21 enodes) 2.846 * * [simplify]: iters left: 1 (43 enodes) 2.856 * * [simplify]: Extracting #0: cost 1 inf + 0 2.856 * * [simplify]: Extracting #1: cost 16 inf + 0 2.856 * * [simplify]: Extracting #2: cost 16 inf + 2 2.857 * * [simplify]: Extracting #3: cost 13 inf + 367 2.857 * * [simplify]: Extracting #4: cost 0 inf + 3718 2.857 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 2.857 * [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))))))) 2.858 * * * * [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))))> 2.858 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 2.858 * * [simplify]: iters left: 3 (8 enodes) 2.860 * * [simplify]: iters left: 2 (21 enodes) 2.863 * * [simplify]: iters left: 1 (43 enodes) 2.871 * * [simplify]: Extracting #0: cost 1 inf + 0 2.871 * * [simplify]: Extracting #1: cost 16 inf + 0 2.871 * * [simplify]: Extracting #2: cost 16 inf + 2 2.871 * * [simplify]: Extracting #3: cost 13 inf + 367 2.871 * * [simplify]: Extracting #4: cost 0 inf + 3718 2.872 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 2.872 * [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)))) 2.872 * * * * [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))))> 2.872 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 2.872 * * [simplify]: iters left: 3 (8 enodes) 2.874 * * [simplify]: iters left: 2 (21 enodes) 2.878 * * [simplify]: iters left: 1 (43 enodes) 2.886 * * [simplify]: Extracting #0: cost 1 inf + 0 2.886 * * [simplify]: Extracting #1: cost 16 inf + 0 2.886 * * [simplify]: Extracting #2: cost 16 inf + 2 2.886 * * [simplify]: Extracting #3: cost 13 inf + 367 2.886 * * [simplify]: Extracting #4: cost 0 inf + 3718 2.887 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 2.887 * [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)))) 2.887 * * * * [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))))> 2.887 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 2.887 * * [simplify]: iters left: 3 (8 enodes) 2.889 * * [simplify]: iters left: 2 (21 enodes) 2.895 * * [simplify]: iters left: 1 (43 enodes) 2.903 * * [simplify]: Extracting #0: cost 1 inf + 0 2.903 * * [simplify]: Extracting #1: cost 16 inf + 0 2.903 * * [simplify]: Extracting #2: cost 16 inf + 2 2.903 * * [simplify]: Extracting #3: cost 13 inf + 367 2.904 * * [simplify]: Extracting #4: cost 0 inf + 3718 2.904 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 2.904 * [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)))) 2.904 * * * * [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))))> 2.904 * [simplify]: Simplifying (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 beta alpha)) (real->posit16 1.0)) 2.904 * * [simplify]: iters left: 3 (8 enodes) 2.906 * * [simplify]: iters left: 2 (21 enodes) 2.910 * * [simplify]: iters left: 1 (43 enodes) 2.917 * * [simplify]: Extracting #0: cost 1 inf + 0 2.918 * * [simplify]: Extracting #1: cost 16 inf + 0 2.918 * * [simplify]: Extracting #2: cost 16 inf + 2 2.918 * * [simplify]: Extracting #3: cost 13 inf + 367 2.918 * * [simplify]: Extracting #4: cost 0 inf + 3718 2.919 * [simplify]: Simplified to (+.p16 (+.p16 (real->posit16 1.0) (*.p16 beta alpha)) (+.p16 beta alpha)) 2.919 * [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)))) 2.919 * * * [progress]: adding candidates to table 3.298 * * [progress]: iteration 4 / 4 3.298 * * * [progress]: picking best candidate 3.368 * * * * [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))))> 3.368 * * * [progress]: localizing error 3.709 * * * [progress]: generating rewritten candidates 3.709 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 3.791 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 1) 3.799 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 1) 3.806 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2) 3.811 * * * [progress]: generating series expansions 3.811 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 3.811 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 1) 3.811 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 1) 3.811 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2) 3.811 * * * [progress]: simplifying candidates 3.811 * * * * [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))))> 3.811 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 3.811 * * [simplify]: iters left: 3 (9 enodes) 3.814 * * [simplify]: iters left: 2 (22 enodes) 3.818 * * [simplify]: iters left: 1 (30 enodes) 3.823 * * [simplify]: Extracting #0: cost 1 inf + 0 3.823 * * [simplify]: Extracting #1: cost 7 inf + 0 3.823 * * [simplify]: Extracting #2: cost 7 inf + 2 3.823 * * [simplify]: Extracting #3: cost 8 inf + 44 3.824 * * [simplify]: Extracting #4: cost 4 inf + 48 3.824 * * [simplify]: Extracting #5: cost 1 inf + 1137 3.824 * * [simplify]: Extracting #6: cost 0 inf + 1500 3.824 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 3.825 * [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.825 * * * * [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))))> 3.825 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 3.825 * * [simplify]: iters left: 3 (9 enodes) 3.829 * * [simplify]: iters left: 2 (22 enodes) 3.836 * * [simplify]: iters left: 1 (30 enodes) 3.847 * * [simplify]: Extracting #0: cost 1 inf + 0 3.847 * * [simplify]: Extracting #1: cost 7 inf + 0 3.847 * * [simplify]: Extracting #2: cost 7 inf + 2 3.847 * * [simplify]: Extracting #3: cost 8 inf + 44 3.847 * * [simplify]: Extracting #4: cost 4 inf + 48 3.847 * * [simplify]: Extracting #5: cost 1 inf + 1137 3.848 * * [simplify]: Extracting #6: cost 0 inf + 1500 3.848 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 3.848 * [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.848 * * * * [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))))> 3.849 * * * * [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))))> 3.849 * * * * [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))))> 3.849 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) beta) 3.849 * * [simplify]: iters left: 4 (10 enodes) 3.854 * * [simplify]: iters left: 3 (24 enodes) 3.861 * * [simplify]: iters left: 2 (46 enodes) 3.869 * * [simplify]: iters left: 1 (73 enodes) 3.880 * * [simplify]: Extracting #0: cost 1 inf + 0 3.881 * * [simplify]: Extracting #1: cost 9 inf + 0 3.881 * * [simplify]: Extracting #2: cost 16 inf + 322 3.881 * * [simplify]: Extracting #3: cost 17 inf + 323 3.881 * * [simplify]: Extracting #4: cost 11 inf + 1052 3.881 * * [simplify]: Extracting #5: cost 3 inf + 5713 3.882 * * [simplify]: Extracting #6: cost 0 inf + 5883 3.882 * [simplify]: Simplified to (*.p16 (+.p16 (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))) beta) beta) 3.882 * [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)))) 3.882 * * * * [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))))> 3.883 * [simplify]: Simplifying (*.p16 beta (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 3.883 * * [simplify]: iters left: 4 (10 enodes) 3.885 * * [simplify]: iters left: 3 (30 enodes) 3.891 * * [simplify]: iters left: 2 (59 enodes) 3.900 * * [simplify]: iters left: 1 (80 enodes) 3.912 * * [simplify]: Extracting #0: cost 1 inf + 0 3.912 * * [simplify]: Extracting #1: cost 9 inf + 0 3.912 * * [simplify]: Extracting #2: cost 16 inf + 322 3.912 * * [simplify]: Extracting #3: cost 16 inf + 645 3.912 * * [simplify]: Extracting #4: cost 12 inf + 1051 3.912 * * [simplify]: Extracting #5: cost 3 inf + 5754 3.913 * * [simplify]: Extracting #6: cost 0 inf + 5883 3.913 * [simplify]: Simplified to (*.p16 beta (+.p16 beta (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) alpha))) 3.913 * [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)))) 3.914 * * * * [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))))> 3.914 * * * * [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))))> 3.914 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 3.914 * * [simplify]: iters left: 3 (9 enodes) 3.916 * * [simplify]: iters left: 2 (22 enodes) 3.921 * * [simplify]: iters left: 1 (30 enodes) 3.926 * * [simplify]: Extracting #0: cost 1 inf + 0 3.926 * * [simplify]: Extracting #1: cost 7 inf + 0 3.926 * * [simplify]: Extracting #2: cost 7 inf + 2 3.926 * * [simplify]: Extracting #3: cost 8 inf + 44 3.926 * * [simplify]: Extracting #4: cost 4 inf + 48 3.926 * * [simplify]: Extracting #5: cost 1 inf + 1137 3.927 * * [simplify]: Extracting #6: cost 0 inf + 1500 3.927 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 3.927 * [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)))) 3.927 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 3.927 * * [simplify]: iters left: 3 (9 enodes) 3.930 * * [simplify]: iters left: 2 (22 enodes) 3.933 * * [simplify]: iters left: 1 (30 enodes) 3.938 * * [simplify]: Extracting #0: cost 1 inf + 0 3.938 * * [simplify]: Extracting #1: cost 7 inf + 0 3.938 * * [simplify]: Extracting #2: cost 7 inf + 2 3.938 * * [simplify]: Extracting #3: cost 8 inf + 44 3.938 * * [simplify]: Extracting #4: cost 4 inf + 48 3.938 * * [simplify]: Extracting #5: cost 1 inf + 1137 3.938 * * [simplify]: Extracting #6: cost 0 inf + 1500 3.938 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 3.938 * [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)))) 3.938 * * * * [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))))> 3.939 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) alpha) 3.939 * * [simplify]: iters left: 4 (10 enodes) 3.941 * * [simplify]: iters left: 3 (24 enodes) 3.945 * * [simplify]: iters left: 2 (45 enodes) 3.953 * * [simplify]: iters left: 1 (73 enodes) 3.968 * * [simplify]: Extracting #0: cost 1 inf + 0 3.968 * * [simplify]: Extracting #1: cost 9 inf + 0 3.968 * * [simplify]: Extracting #2: cost 17 inf + 1 3.968 * * [simplify]: Extracting #3: cost 17 inf + 323 3.968 * * [simplify]: Extracting #4: cost 13 inf + 689 3.969 * * [simplify]: Extracting #5: cost 4 inf + 4709 3.970 * * [simplify]: Extracting #6: cost 0 inf + 5883 3.970 * [simplify]: Simplified to (*.p16 alpha (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1)))) 3.971 * [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)))) 3.971 * * * * [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))))> 3.971 * [simplify]: Simplifying (*.p16 alpha (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) 3.971 * * [simplify]: iters left: 4 (10 enodes) 3.975 * * [simplify]: iters left: 3 (30 enodes) 3.985 * * [simplify]: iters left: 2 (59 enodes) 4.001 * * [simplify]: iters left: 1 (78 enodes) 4.023 * * [simplify]: Extracting #0: cost 1 inf + 0 4.024 * * [simplify]: Extracting #1: cost 9 inf + 0 4.024 * * [simplify]: Extracting #2: cost 17 inf + 1 4.024 * * [simplify]: Extracting #3: cost 16 inf + 645 4.024 * * [simplify]: Extracting #4: cost 12 inf + 1051 4.024 * * [simplify]: Extracting #5: cost 5 inf + 3747 4.025 * * [simplify]: Extracting #6: cost 0 inf + 6203 4.025 * * [simplify]: Extracting #7: cost 0 inf + 5883 4.026 * [simplify]: Simplified to (*.p16 alpha (+.p16 beta (+.p16 alpha (*.p16 (real->posit16 2) (real->posit16 1))))) 4.026 * [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)))) 4.026 * * * * [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))))> 4.026 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 4.026 * * [simplify]: iters left: 3 (9 enodes) 4.029 * * [simplify]: iters left: 2 (22 enodes) 4.035 * * [simplify]: iters left: 1 (30 enodes) 4.043 * * [simplify]: Extracting #0: cost 1 inf + 0 4.043 * * [simplify]: Extracting #1: cost 7 inf + 0 4.043 * * [simplify]: Extracting #2: cost 7 inf + 2 4.044 * * [simplify]: Extracting #3: cost 8 inf + 44 4.044 * * [simplify]: Extracting #4: cost 4 inf + 48 4.044 * * [simplify]: Extracting #5: cost 1 inf + 1137 4.044 * * [simplify]: Extracting #6: cost 0 inf + 1500 4.045 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 4.045 * [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)))) 4.045 * [simplify]: Simplifying (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) 4.045 * * [simplify]: iters left: 3 (9 enodes) 4.049 * * [simplify]: iters left: 2 (22 enodes) 4.056 * * [simplify]: iters left: 1 (30 enodes) 4.063 * * [simplify]: Extracting #0: cost 1 inf + 0 4.063 * * [simplify]: Extracting #1: cost 7 inf + 0 4.064 * * [simplify]: Extracting #2: cost 7 inf + 2 4.064 * * [simplify]: Extracting #3: cost 8 inf + 44 4.064 * * [simplify]: Extracting #4: cost 4 inf + 48 4.064 * * [simplify]: Extracting #5: cost 1 inf + 1137 4.064 * * [simplify]: Extracting #6: cost 0 inf + 1500 4.065 * [simplify]: Simplified to (+.p16 (+.p16 beta alpha) (*.p16 (real->posit16 2) (real->posit16 1))) 4.065 * [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)))) 4.065 * * * * [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))))> 4.065 * * * * [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))))> 4.065 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 4.065 * * [simplify]: iters left: 4 (10 enodes) 4.070 * * [simplify]: iters left: 3 (26 enodes) 4.077 * * [simplify]: iters left: 2 (53 enodes) 4.096 * * [simplify]: iters left: 1 (150 enodes) 4.139 * * [simplify]: Extracting #0: cost 1 inf + 0 4.139 * * [simplify]: Extracting #1: cost 24 inf + 0 4.139 * * [simplify]: Extracting #2: cost 52 inf + 0 4.140 * * [simplify]: Extracting #3: cost 46 inf + 970 4.141 * * [simplify]: Extracting #4: cost 14 inf + 16705 4.143 * * [simplify]: Extracting #5: cost 0 inf + 25635 4.145 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 4.146 * [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)))) 4.146 * * * * [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))))> 4.146 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 4.146 * * [simplify]: iters left: 4 (10 enodes) 4.149 * * [simplify]: iters left: 3 (26 enodes) 4.155 * * [simplify]: iters left: 2 (53 enodes) 4.170 * * [simplify]: iters left: 1 (150 enodes) 4.242 * * [simplify]: Extracting #0: cost 1 inf + 0 4.242 * * [simplify]: Extracting #1: cost 24 inf + 0 4.243 * * [simplify]: Extracting #2: cost 52 inf + 0 4.243 * * [simplify]: Extracting #3: cost 46 inf + 970 4.244 * * [simplify]: Extracting #4: cost 14 inf + 16705 4.247 * * [simplify]: Extracting #5: cost 0 inf + 25635 4.249 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 4.249 * [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)))) 4.249 * * * * [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))))> 4.250 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 4.250 * * [simplify]: iters left: 4 (10 enodes) 4.252 * * [simplify]: iters left: 3 (26 enodes) 4.258 * * [simplify]: iters left: 2 (53 enodes) 4.271 * * [simplify]: iters left: 1 (150 enodes) 4.323 * * [simplify]: Extracting #0: cost 1 inf + 0 4.323 * * [simplify]: Extracting #1: cost 24 inf + 0 4.323 * * [simplify]: Extracting #2: cost 52 inf + 0 4.324 * * [simplify]: Extracting #3: cost 46 inf + 970 4.326 * * [simplify]: Extracting #4: cost 14 inf + 16705 4.329 * * [simplify]: Extracting #5: cost 0 inf + 25635 4.331 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 4.331 * [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)))) 4.331 * * * * [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))))> 4.332 * [simplify]: Simplifying (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (*.p16 (real->posit16 2) (real->posit16 1))) 4.332 * * [simplify]: iters left: 4 (10 enodes) 4.334 * * [simplify]: iters left: 3 (26 enodes) 4.339 * * [simplify]: iters left: 2 (53 enodes) 4.352 * * [simplify]: iters left: 1 (150 enodes) 4.393 * * [simplify]: Extracting #0: cost 1 inf + 0 4.394 * * [simplify]: Extracting #1: cost 24 inf + 0 4.394 * * [simplify]: Extracting #2: cost 52 inf + 0 4.394 * * [simplify]: Extracting #3: cost 46 inf + 970 4.395 * * [simplify]: Extracting #4: cost 14 inf + 16705 4.398 * * [simplify]: Extracting #5: cost 0 inf + 25635 4.400 * [simplify]: Simplified to (*.p16 (+.p16 alpha (+.p16 (*.p16 (real->posit16 2) (real->posit16 1)) beta)) (*.p16 (real->posit16 2) (real->posit16 1))) 4.400 * [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)))) 4.400 * * * [progress]: adding candidates to table 4.857 * [progress]: [Phase 3 of 3] Extracting. 4.857 * * [regime]: Finding splitpoints for: (#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)))))))> #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 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.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 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))))))>) 4.859 * * * [regime-changes]: Trying 2 branch expressions: (beta alpha) 4.859 * * * * [regimes]: Trying to branch on beta from (#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)))))))> #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 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.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 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))))))>) 5.055 * * * * [regimes]: Trying to branch on alpha from (#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)))))))> #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 alpha (real->posit16 1.0))) (*.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1)))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) (real->posit16 1))) (real->posit16 1.0))))> #posit16 1.0)) (+.p16 (*.p16 (+.p16 (+.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 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))))))>) 5.238 * * * [regime]: Found split indices: #