1554043358.014 * [progress]: [Phase 1 of 3] Setting up. 1554043358.014 * * * [progress]: [1/2] Preparing points 1554043358.014 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 1554043358.015 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 1554043358.017 * * * * [points]: Setting MPFR precision to 64 1554043358.018 * * * * [points]: Setting MPFR precision to 320 1554043358.019 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 1554043358.021 * * * * [points]: Setting MPFR precision to 64 1554043358.022 * * * * [points]: Setting MPFR precision to 320 1554043358.024 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 1554043358.025 * * * * [points]: Setting MPFR precision to 64 1554043358.028 * * * * [points]: Setting MPFR precision to 320 1554043358.031 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 1554043358.033 * * * * [points]: Setting MPFR precision to 64 1554043358.037 * * * * [points]: Setting MPFR precision to 320 1554043358.042 * * * * [points]: Computing exacts for 256 points 1554043358.044 * * * * [points]: Setting MPFR precision to 64 1554043358.056 * * * * [points]: Setting MPFR precision to 320 1554043358.073 * * * * [points]: Filtering points with unrepresentable outputs 1554043358.079 * * * * [points]: Sampling 133 additional inputs, on iter 1 have 123 / 256 1554043358.079 * * * * [points]: Computing exacts on every 8 of 133 points to ramp up precision 1554043358.081 * * * * [points]: Setting MPFR precision to 64 1554043358.082 * * * * [points]: Setting MPFR precision to 320 1554043358.083 * * * * [points]: Computing exacts on every 4 of 133 points to ramp up precision 1554043358.084 * * * * [points]: Setting MPFR precision to 64 1554043358.086 * * * * [points]: Setting MPFR precision to 320 1554043358.087 * * * * [points]: Computing exacts on every 2 of 133 points to ramp up precision 1554043358.089 * * * * [points]: Setting MPFR precision to 64 1554043358.091 * * * * [points]: Setting MPFR precision to 320 1554043358.094 * * * * [points]: Computing exacts for 133 points 1554043358.112 * * * * [points]: Setting MPFR precision to 64 1554043358.119 * * * * [points]: Setting MPFR precision to 320 1554043358.128 * * * * [points]: Filtering points with unrepresentable outputs 1554043358.133 * * * * [points]: Sampling 71 additional inputs, on iter 2 have 185 / 256 1554043358.133 * * * * [points]: Computing exacts on every 4 of 71 points to ramp up precision 1554043358.135 * * * * [points]: Setting MPFR precision to 64 1554043358.136 * * * * [points]: Setting MPFR precision to 320 1554043358.136 * * * * [points]: Computing exacts on every 2 of 71 points to ramp up precision 1554043358.138 * * * * [points]: Setting MPFR precision to 64 1554043358.139 * * * * [points]: Setting MPFR precision to 320 1554043358.141 * * * * [points]: Computing exacts for 71 points 1554043358.142 * * * * [points]: Setting MPFR precision to 64 1554043358.146 * * * * [points]: Setting MPFR precision to 320 1554043358.151 * * * * [points]: Filtering points with unrepresentable outputs 1554043358.152 * * * * [points]: Sampling 37 additional inputs, on iter 3 have 219 / 256 1554043358.153 * * * * [points]: Computing exacts on every 2 of 37 points to ramp up precision 1554043358.154 * * * * [points]: Setting MPFR precision to 64 1554043358.155 * * * * [points]: Setting MPFR precision to 320 1554043358.156 * * * * [points]: Computing exacts for 37 points 1554043358.157 * * * * [points]: Setting MPFR precision to 64 1554043358.159 * * * * [points]: Setting MPFR precision to 320 1554043358.161 * * * * [points]: Filtering points with unrepresentable outputs 1554043358.162 * * * * [points]: Sampling 19 additional inputs, on iter 4 have 237 / 256 1554043358.163 * * * * [points]: Computing exacts for 19 points 1554043358.164 * * * * [points]: Setting MPFR precision to 64 1554043358.165 * * * * [points]: Setting MPFR precision to 320 1554043358.166 * * * * [points]: Filtering points with unrepresentable outputs 1554043358.167 * * * * [points]: Sampling 11 additional inputs, on iter 5 have 245 / 256 1554043358.167 * * * * [points]: Computing exacts for 11 points 1554043358.168 * * * * [points]: Setting MPFR precision to 64 1554043358.169 * * * * [points]: Setting MPFR precision to 320 1554043358.170 * * * * [points]: Filtering points with unrepresentable outputs 1554043358.170 * * * * [points]: Sampling 6 additional inputs, on iter 6 have 250 / 256 1554043358.170 * * * * [points]: Computing exacts for 6 points 1554043358.172 * * * * [points]: Setting MPFR precision to 64 1554043358.172 * * * * [points]: Setting MPFR precision to 320 1554043358.173 * * * * [points]: Filtering points with unrepresentable outputs 1554043358.173 * * * * [points]: Sampling 4 additional inputs, on iter 7 have 253 / 256 1554043358.173 * * * * [points]: Computing exacts for 4 points 1554043358.174 * * * * [points]: Setting MPFR precision to 64 1554043358.175 * * * * [points]: Setting MPFR precision to 320 1554043358.175 * * * * [points]: Filtering points with unrepresentable outputs 1554043358.175 * * * * [points]: Sampled 256 points with exact outputs 1554043358.175 * * * [progress]: [2/2] Setting up program. 1554043358.193 * [progress]: [Phase 2 of 3] Improving. 1554043358.193 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1554043358.193 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043358.193 * * [simplify]: iters left: 5 (9 enodes) 1554043358.196 * * [simplify]: iters left: 4 (22 enodes) 1554043358.199 * * [simplify]: iters left: 3 (42 enodes) 1554043358.207 * * [simplify]: iters left: 2 (100 enodes) 1554043358.242 * * [simplify]: iters left: 1 (347 enodes) 1554043358.454 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043358.454 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043358.456 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043358.458 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043358.476 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043358.526 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043358.589 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043358.651 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043358.743 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043358.833 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043358.908 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043358.908 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1554043358.927 * * [progress]: iteration 1 / 4 1554043358.927 * * * [progress]: picking best candidate 1554043358.944 * * * * [pick]: Picked #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1554043358.944 * * * [progress]: localizing error 1554043359.139 * * * [progress]: generating rewritten candidates 1554043359.139 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 1554043359.142 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 1554043359.143 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 1554043359.144 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 1554043359.144 * * * [progress]: generating series expansions 1554043359.144 * * * * [progress]: [ 1 / 4 ] generating series at (2) 1554043359.144 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 1554043359.144 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 1554043359.144 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 1554043359.144 * * * [progress]: simplifying candidates 1554043359.144 * * * * [progress]: [ 1 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (neg.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043359.144 * * * * [progress]: [ 2 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043359.144 * * * * [progress]: [ 3 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1554043359.144 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043359.144 * * [simplify]: iters left: 5 (9 enodes) 1554043359.147 * * [simplify]: iters left: 4 (22 enodes) 1554043359.150 * * [simplify]: iters left: 3 (42 enodes) 1554043359.158 * * [simplify]: iters left: 2 (100 enodes) 1554043359.191 * * [simplify]: iters left: 1 (347 enodes) 1554043359.354 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043359.354 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043359.355 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043359.356 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043359.365 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043359.431 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043359.500 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043359.567 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043359.630 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043359.699 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043359.774 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043359.774 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1554043359.774 * * * * [progress]: [ 4 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1554043359.775 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043359.775 * * [simplify]: iters left: 5 (9 enodes) 1554043359.780 * * [simplify]: iters left: 4 (22 enodes) 1554043359.787 * * [simplify]: iters left: 3 (42 enodes) 1554043359.802 * * [simplify]: iters left: 2 (100 enodes) 1554043359.841 * * [simplify]: iters left: 1 (347 enodes) 1554043360.020 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043360.020 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043360.021 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043360.023 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043360.036 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043360.080 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043360.143 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043360.207 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043360.270 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043360.332 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043360.394 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043360.394 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1554043360.394 * * * * [progress]: [ 5 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1554043360.395 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043360.395 * * [simplify]: iters left: 5 (9 enodes) 1554043360.397 * * [simplify]: iters left: 4 (22 enodes) 1554043360.401 * * [simplify]: iters left: 3 (42 enodes) 1554043360.409 * * [simplify]: iters left: 2 (100 enodes) 1554043360.430 * * [simplify]: iters left: 1 (347 enodes) 1554043360.581 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043360.581 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043360.582 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043360.583 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043360.592 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043360.637 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043360.702 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043360.765 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043360.827 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043360.890 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043360.951 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043360.951 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1554043360.951 * * * * [progress]: [ 6 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1554043360.952 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043360.952 * * [simplify]: iters left: 5 (9 enodes) 1554043360.954 * * [simplify]: iters left: 4 (22 enodes) 1554043360.958 * * [simplify]: iters left: 3 (42 enodes) 1554043360.965 * * [simplify]: iters left: 2 (100 enodes) 1554043360.987 * * [simplify]: iters left: 1 (347 enodes) 1554043361.151 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043361.151 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043361.152 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043361.154 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043361.163 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043361.209 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043361.283 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043361.347 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043361.432 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043361.497 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043361.558 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043361.558 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1554043361.558 * * * [progress]: adding candidates to table 1554043361.819 * * [progress]: iteration 2 / 4 1554043361.819 * * * [progress]: picking best candidate 1554043361.846 * * * * [pick]: Picked #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043361.846 * * * [progress]: localizing error 1554043362.255 * * * [progress]: generating rewritten candidates 1554043362.255 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 1554043362.258 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1554043362.265 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 1554043362.267 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 1554043362.269 * * * [progress]: generating series expansions 1554043362.269 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 1554043362.269 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1554043362.269 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 1554043362.269 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 1554043362.269 * * * [progress]: simplifying candidates 1554043362.269 * * * * [progress]: [ 1 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043362.269 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043362.269 * * [simplify]: iters left: 5 (9 enodes) 1554043362.271 * * [simplify]: iters left: 4 (16 enodes) 1554043362.274 * * [simplify]: iters left: 3 (18 enodes) 1554043362.277 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043362.277 * * [simplify]: Extracting #1: cost 3 inf + 0 1554043362.277 * * [simplify]: Extracting #2: cost 6 inf + 0 1554043362.277 * * [simplify]: Extracting #3: cost 9 inf + 0 1554043362.277 * * [simplify]: Extracting #4: cost 6 inf + 43 1554043362.277 * * [simplify]: Extracting #5: cost 0 inf + 2214 1554043362.277 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043362.277 * [simplify]: Simplified (2 1 1) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043362.278 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043362.278 * * [simplify]: iters left: 5 (9 enodes) 1554043362.280 * * [simplify]: iters left: 4 (22 enodes) 1554043362.283 * * [simplify]: iters left: 3 (42 enodes) 1554043362.298 * * [simplify]: iters left: 2 (100 enodes) 1554043362.339 * * [simplify]: iters left: 1 (347 enodes) 1554043362.515 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043362.515 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043362.516 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043362.518 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043362.527 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043362.591 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043362.670 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043362.746 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043362.839 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043362.902 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043362.998 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043362.999 * [simplify]: Simplified (2 1 2) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043362.999 * * * * [progress]: [ 2 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (neg.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043362.999 * * * * [progress]: [ 3 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x)))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043362.999 * * * * [progress]: [ 4 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (/.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> 1554043362.999 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043362.999 * * [simplify]: iters left: 5 (9 enodes) 1554043363.003 * * [simplify]: iters left: 4 (16 enodes) 1554043363.009 * * [simplify]: iters left: 3 (18 enodes) 1554043363.014 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043363.014 * * [simplify]: Extracting #1: cost 3 inf + 0 1554043363.014 * * [simplify]: Extracting #2: cost 6 inf + 0 1554043363.014 * * [simplify]: Extracting #3: cost 9 inf + 0 1554043363.014 * * [simplify]: Extracting #4: cost 6 inf + 43 1554043363.015 * * [simplify]: Extracting #5: cost 0 inf + 2214 1554043363.015 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043363.015 * [simplify]: Simplified (2 1) to (λ (x) (/.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (/.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))) 1554043363.015 * * * * [progress]: [ 5 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x)))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))))> 1554043363.015 * [simplify]: Simplifying (-.p16 (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x)))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043363.016 * * [simplify]: iters left: 6 (13 enodes) 1554043363.022 * * [simplify]: iters left: 5 (45 enodes) 1554043363.042 * * [simplify]: iters left: 4 (144 enodes) 1554043363.110 * * [simplify]: iters left: 3 (446 enodes) 1554043363.554 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043363.555 * * [simplify]: Extracting #1: cost 41 inf + 0 1554043363.556 * * [simplify]: Extracting #2: cost 283 inf + 0 1554043363.559 * * [simplify]: Extracting #3: cost 446 inf + 44 1554043363.582 * * [simplify]: Extracting #4: cost 488 inf + 246749 1554043363.700 * * [simplify]: Extracting #5: cost 101 inf + 1165723 1554043363.878 * * [simplify]: Extracting #6: cost 2 inf + 1463482 1554043364.041 * * [simplify]: Extracting #7: cost 0 inf + 1419126 1554043364.126 * * [simplify]: Extracting #8: cost 0 inf + 1414206 1554043364.237 * [simplify]: Simplified to (*.p16 (*.p16 (real->posit16 1) (-.p16 (/.p16 (real->posit16 1) x) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) (*.p16 (real->posit16 1) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) x)))) 1554043364.237 * [simplify]: Simplified (2 1) to (λ (x) (/.p16 (*.p16 (*.p16 (real->posit16 1) (-.p16 (/.p16 (real->posit16 1) x) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) (*.p16 (real->posit16 1) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) x)))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))) 1554043364.237 * * * * [progress]: [ 6 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (real->posit16 1)) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.238 * [simplify]: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1554043364.238 * * [simplify]: iters left: 3 (5 enodes) 1554043364.240 * * [simplify]: iters left: 2 (11 enodes) 1554043364.244 * * [simplify]: iters left: 1 (13 enodes) 1554043364.247 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043364.248 * * [simplify]: Extracting #1: cost 2 inf + 0 1554043364.248 * * [simplify]: Extracting #2: cost 4 inf + 0 1554043364.248 * * [simplify]: Extracting #3: cost 4 inf + 1 1554043364.248 * * [simplify]: Extracting #4: cost 0 inf + 127 1554043364.248 * [simplify]: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1554043364.248 * [simplify]: Simplified (2 1 2 2) to (λ (x) (/.p16 (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (real->posit16 1)) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043364.248 * * * * [progress]: [ 7 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.248 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043364.249 * * [simplify]: iters left: 5 (7 enodes) 1554043364.252 * * [simplify]: iters left: 4 (16 enodes) 1554043364.258 * * [simplify]: iters left: 3 (20 enodes) 1554043364.264 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043364.264 * * [simplify]: Extracting #1: cost 6 inf + 0 1554043364.264 * * [simplify]: Extracting #2: cost 8 inf + 0 1554043364.264 * * [simplify]: Extracting #3: cost 8 inf + 1 1554043364.264 * * [simplify]: Extracting #4: cost 5 inf + 324 1554043364.264 * * [simplify]: Extracting #5: cost 0 inf + 2334 1554043364.265 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1554043364.265 * [simplify]: Simplified (2 1 2 1) to (λ (x) (/.p16 (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043364.265 * * * * [progress]: [ 8 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.265 * * * * [progress]: [ 9 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.265 * [simplify]: Simplifying (sqrt.p16 x) 1554043364.265 * * [simplify]: iters left: 1 (2 enodes) 1554043364.266 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043364.266 * * [simplify]: Extracting #1: cost 2 inf + 0 1554043364.266 * * [simplify]: Extracting #2: cost 1 inf + 1 1554043364.266 * * [simplify]: Extracting #3: cost 0 inf + 42 1554043364.266 * [simplify]: Simplified to (sqrt.p16 x) 1554043364.267 * [simplify]: Simplified (2 1 1 2) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043364.267 * * * * [progress]: [ 10 / 15 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.267 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1554043364.267 * * [simplify]: iters left: 3 (6 enodes) 1554043364.270 * * [simplify]: iters left: 2 (14 enodes) 1554043364.275 * * [simplify]: iters left: 1 (18 enodes) 1554043364.280 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043364.280 * * [simplify]: Extracting #1: cost 6 inf + 0 1554043364.280 * * [simplify]: Extracting #2: cost 8 inf + 0 1554043364.281 * * [simplify]: Extracting #3: cost 5 inf + 43 1554043364.281 * * [simplify]: Extracting #4: cost 0 inf + 2131 1554043364.281 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1554043364.281 * [simplify]: Simplified (2 1 1 1) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043364.281 * * * * [progress]: [ 11 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.281 * * * * [progress]: [ 12 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.281 * * * * [progress]: [ 13 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.281 * * * * [progress]: [ 14 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.281 * * * * [progress]: [ 15 / 15 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043364.281 * * * [progress]: adding candidates to table 1554043365.264 * * [progress]: iteration 3 / 4 1554043365.264 * * * [progress]: picking best candidate 1554043365.498 * * * * [pick]: Picked #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043365.498 * * * [progress]: localizing error 1554043366.062 * * * [progress]: generating rewritten candidates 1554043366.062 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 1554043366.068 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1554043366.084 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2) 1554043366.086 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2) 1554043366.089 * * * [progress]: generating series expansions 1554043366.089 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 1554043366.089 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1554043366.089 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2) 1554043366.089 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2) 1554043366.089 * * * [progress]: simplifying candidates 1554043366.089 * * * * [progress]: [ 1 / 8 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (neg.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043366.089 * * * * [progress]: [ 2 / 8 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (/.p16 (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043366.089 * * * * [progress]: [ 3 / 8 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (/.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> 1554043366.090 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043366.090 * * [simplify]: iters left: 5 (9 enodes) 1554043366.094 * * [simplify]: iters left: 4 (16 enodes) 1554043366.099 * * [simplify]: iters left: 3 (18 enodes) 1554043366.105 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043366.105 * * [simplify]: Extracting #1: cost 3 inf + 0 1554043366.105 * * [simplify]: Extracting #2: cost 6 inf + 0 1554043366.105 * * [simplify]: Extracting #3: cost 9 inf + 0 1554043366.105 * * [simplify]: Extracting #4: cost 6 inf + 43 1554043366.105 * * [simplify]: Extracting #5: cost 0 inf + 2214 1554043366.105 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043366.105 * [simplify]: Simplified (2 1) to (λ (x) (/.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (/.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))) 1554043366.106 * * * * [progress]: [ 4 / 8 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> 1554043366.106 * [simplify]: Simplifying (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043366.106 * * [simplify]: iters left: 6 (13 enodes) 1554043366.112 * * [simplify]: iters left: 5 (38 enodes) 1554043366.126 * * [simplify]: iters left: 4 (106 enodes) 1554043366.180 * * [simplify]: iters left: 3 (376 enodes) 1554043366.511 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043366.511 * * [simplify]: Extracting #1: cost 52 inf + 0 1554043366.512 * * [simplify]: Extracting #2: cost 302 inf + 0 1554043366.521 * * [simplify]: Extracting #3: cost 417 inf + 43 1554043366.543 * * [simplify]: Extracting #4: cost 351 inf + 302562 1554043366.632 * * [simplify]: Extracting #5: cost 35 inf + 1004993 1554043366.737 * * [simplify]: Extracting #6: cost 0 inf + 1083663 1554043366.843 * * [simplify]: Extracting #7: cost 0 inf + 1082583 1554043366.948 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))))) 1554043366.948 * [simplify]: Simplified (2 1) to (λ (x) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))) 1554043366.949 * * * * [progress]: [ 5 / 8 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043366.949 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043366.949 * * [simplify]: iters left: 5 (9 enodes) 1554043366.953 * * [simplify]: iters left: 4 (16 enodes) 1554043366.958 * * [simplify]: iters left: 3 (18 enodes) 1554043366.964 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043366.964 * * [simplify]: Extracting #1: cost 3 inf + 0 1554043366.964 * * [simplify]: Extracting #2: cost 6 inf + 0 1554043366.964 * * [simplify]: Extracting #3: cost 9 inf + 0 1554043366.964 * * [simplify]: Extracting #4: cost 6 inf + 43 1554043366.965 * * [simplify]: Extracting #5: cost 0 inf + 2214 1554043366.965 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043366.965 * [simplify]: Simplified (2 1 1) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043366.965 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043366.965 * * [simplify]: iters left: 5 (9 enodes) 1554043366.969 * * [simplify]: iters left: 4 (22 enodes) 1554043366.977 * * [simplify]: iters left: 3 (42 enodes) 1554043366.992 * * [simplify]: iters left: 2 (100 enodes) 1554043367.037 * * [simplify]: iters left: 1 (347 enodes) 1554043367.334 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043367.334 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043367.336 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043367.339 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043367.356 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043367.443 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043367.573 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043367.694 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043367.815 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043367.934 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043368.041 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043368.041 * [simplify]: Simplified (2 1 2) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043368.041 * * * * [progress]: [ 6 / 8 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043368.041 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043368.041 * * [simplify]: iters left: 5 (9 enodes) 1554043368.043 * * [simplify]: iters left: 4 (16 enodes) 1554043368.046 * * [simplify]: iters left: 3 (18 enodes) 1554043368.048 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043368.048 * * [simplify]: Extracting #1: cost 3 inf + 0 1554043368.048 * * [simplify]: Extracting #2: cost 6 inf + 0 1554043368.049 * * [simplify]: Extracting #3: cost 9 inf + 0 1554043368.049 * * [simplify]: Extracting #4: cost 6 inf + 43 1554043368.049 * * [simplify]: Extracting #5: cost 0 inf + 2214 1554043368.049 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043368.049 * [simplify]: Simplified (2 1 1) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043368.049 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043368.049 * * [simplify]: iters left: 5 (9 enodes) 1554043368.051 * * [simplify]: iters left: 4 (22 enodes) 1554043368.055 * * [simplify]: iters left: 3 (42 enodes) 1554043368.062 * * [simplify]: iters left: 2 (100 enodes) 1554043368.084 * * [simplify]: iters left: 1 (347 enodes) 1554043368.233 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043368.233 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043368.234 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043368.235 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043368.244 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043368.292 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043368.356 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043368.421 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043368.514 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043368.633 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043368.751 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043368.751 * [simplify]: Simplified (2 1 2) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043368.752 * * * * [progress]: [ 7 / 8 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043368.752 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043368.752 * * [simplify]: iters left: 5 (9 enodes) 1554043368.756 * * [simplify]: iters left: 4 (16 enodes) 1554043368.761 * * [simplify]: iters left: 3 (18 enodes) 1554043368.766 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043368.766 * * [simplify]: Extracting #1: cost 3 inf + 0 1554043368.766 * * [simplify]: Extracting #2: cost 6 inf + 0 1554043368.766 * * [simplify]: Extracting #3: cost 9 inf + 0 1554043368.767 * * [simplify]: Extracting #4: cost 6 inf + 43 1554043368.767 * * [simplify]: Extracting #5: cost 0 inf + 2214 1554043368.767 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043368.767 * [simplify]: Simplified (2 1 1) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043368.767 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043368.768 * * [simplify]: iters left: 5 (9 enodes) 1554043368.771 * * [simplify]: iters left: 4 (22 enodes) 1554043368.779 * * [simplify]: iters left: 3 (42 enodes) 1554043368.796 * * [simplify]: iters left: 2 (100 enodes) 1554043368.840 * * [simplify]: iters left: 1 (347 enodes) 1554043369.136 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043369.136 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043369.137 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043369.140 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043369.158 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043369.249 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043369.372 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043369.493 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043369.604 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043369.666 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043369.728 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043369.728 * [simplify]: Simplified (2 1 2) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043369.729 * * * * [progress]: [ 8 / 8 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043369.729 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043369.729 * * [simplify]: iters left: 5 (9 enodes) 1554043369.731 * * [simplify]: iters left: 4 (16 enodes) 1554043369.734 * * [simplify]: iters left: 3 (18 enodes) 1554043369.736 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043369.736 * * [simplify]: Extracting #1: cost 3 inf + 0 1554043369.736 * * [simplify]: Extracting #2: cost 6 inf + 0 1554043369.737 * * [simplify]: Extracting #3: cost 9 inf + 0 1554043369.737 * * [simplify]: Extracting #4: cost 6 inf + 43 1554043369.737 * * [simplify]: Extracting #5: cost 0 inf + 2214 1554043369.737 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043369.737 * [simplify]: Simplified (2 1 1) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043369.737 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043369.737 * * [simplify]: iters left: 5 (9 enodes) 1554043369.739 * * [simplify]: iters left: 4 (22 enodes) 1554043369.743 * * [simplify]: iters left: 3 (42 enodes) 1554043369.750 * * [simplify]: iters left: 2 (100 enodes) 1554043369.771 * * [simplify]: iters left: 1 (347 enodes) 1554043369.919 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043369.919 * * [simplify]: Extracting #1: cost 48 inf + 0 1554043369.920 * * [simplify]: Extracting #2: cost 269 inf + 0 1554043369.922 * * [simplify]: Extracting #3: cost 457 inf + 1 1554043369.931 * * [simplify]: Extracting #4: cost 422 inf + 210469 1554043369.975 * * [simplify]: Extracting #5: cost 77 inf + 915056 1554043370.042 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1554043370.104 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1554043370.187 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1554043370.250 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1554043370.315 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1554043370.315 * [simplify]: Simplified (2 1 2) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043370.315 * * * [progress]: adding candidates to table 1554043370.791 * * [progress]: iteration 4 / 4 1554043370.791 * * * [progress]: picking best candidate 1554043371.036 * * * * [pick]: Picked #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043371.036 * * * [progress]: localizing error 1554043371.748 * * * [progress]: generating rewritten candidates 1554043371.748 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 1554043371.754 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1554043371.768 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 1554043371.772 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 1554043371.775 * * * [progress]: generating series expansions 1554043371.775 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 1554043371.775 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1554043371.775 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 1554043371.775 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 1554043371.775 * * * [progress]: simplifying candidates 1554043371.775 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (neg.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043371.775 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043371.775 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))))> 1554043371.775 * [simplify]: Simplifying (-.p16 (*.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043371.776 * * [simplify]: iters left: 6 (14 enodes) 1554043371.782 * * [simplify]: iters left: 5 (47 enodes) 1554043371.809 * * [simplify]: iters left: 4 (140 enodes) 1554043371.874 * * [simplify]: iters left: 3 (480 enodes) 1554043372.364 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043372.365 * * [simplify]: Extracting #1: cost 36 inf + 0 1554043372.365 * * [simplify]: Extracting #2: cost 250 inf + 0 1554043372.367 * * [simplify]: Extracting #3: cost 413 inf + 725 1554043372.374 * * [simplify]: Extracting #4: cost 550 inf + 129982 1554043372.429 * * [simplify]: Extracting #5: cost 163 inf + 996596 1554043372.594 * * [simplify]: Extracting #6: cost 12 inf + 1471739 1554043372.763 * * [simplify]: Extracting #7: cost 0 inf + 1461963 1554043372.925 * * [simplify]: Extracting #8: cost 0 inf + 1441923 1554043373.088 * * [simplify]: Extracting #9: cost 0 inf + 1441523 1554043373.251 * [simplify]: Simplified to (*.p16 (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))))) 1554043373.251 * [simplify]: Simplified (2 1) to (λ (x) (/.p16 (*.p16 (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))) 1554043373.252 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (real->posit16 1)) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043373.252 * [simplify]: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1554043373.252 * * [simplify]: iters left: 3 (5 enodes) 1554043373.255 * * [simplify]: iters left: 2 (11 enodes) 1554043373.258 * * [simplify]: iters left: 1 (13 enodes) 1554043373.262 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043373.262 * * [simplify]: Extracting #1: cost 2 inf + 0 1554043373.262 * * [simplify]: Extracting #2: cost 4 inf + 0 1554043373.262 * * [simplify]: Extracting #3: cost 4 inf + 1 1554043373.262 * * [simplify]: Extracting #4: cost 0 inf + 127 1554043373.263 * [simplify]: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1554043373.263 * [simplify]: Simplified (2 1 2 2) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (real->posit16 1)) (sqrt.p16 (+.p16 (real->posit16 1) x)))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043373.263 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043373.263 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1554043373.263 * * [simplify]: iters left: 5 (7 enodes) 1554043373.266 * * [simplify]: iters left: 4 (16 enodes) 1554043373.272 * * [simplify]: iters left: 3 (20 enodes) 1554043373.278 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043373.278 * * [simplify]: Extracting #1: cost 6 inf + 0 1554043373.278 * * [simplify]: Extracting #2: cost 8 inf + 0 1554043373.279 * * [simplify]: Extracting #3: cost 8 inf + 1 1554043373.279 * * [simplify]: Extracting #4: cost 5 inf + 324 1554043373.279 * * [simplify]: Extracting #5: cost 0 inf + 2334 1554043373.279 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1554043373.279 * [simplify]: Simplified (2 1 2 1) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043373.280 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043373.280 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043373.280 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1554043373.280 * * [simplify]: iters left: 3 (6 enodes) 1554043373.283 * * [simplify]: iters left: 2 (14 enodes) 1554043373.288 * * [simplify]: iters left: 1 (18 enodes) 1554043373.293 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043373.293 * * [simplify]: Extracting #1: cost 6 inf + 0 1554043373.293 * * [simplify]: Extracting #2: cost 8 inf + 0 1554043373.293 * * [simplify]: Extracting #3: cost 5 inf + 43 1554043373.293 * * [simplify]: Extracting #4: cost 0 inf + 2131 1554043373.294 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1554043373.294 * [simplify]: Simplified (2 1 1 1) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043373.294 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043373.294 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1554043373.294 * * [simplify]: iters left: 3 (6 enodes) 1554043373.297 * * [simplify]: iters left: 2 (14 enodes) 1554043373.302 * * [simplify]: iters left: 1 (18 enodes) 1554043373.307 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043373.307 * * [simplify]: Extracting #1: cost 6 inf + 0 1554043373.307 * * [simplify]: Extracting #2: cost 8 inf + 0 1554043373.307 * * [simplify]: Extracting #3: cost 5 inf + 43 1554043373.308 * * [simplify]: Extracting #4: cost 0 inf + 2131 1554043373.308 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1554043373.308 * [simplify]: Simplified (2 1 1 1) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043373.308 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043373.308 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1554043373.308 * * [simplify]: iters left: 3 (6 enodes) 1554043373.311 * * [simplify]: iters left: 2 (14 enodes) 1554043373.316 * * [simplify]: iters left: 1 (18 enodes) 1554043373.322 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043373.322 * * [simplify]: Extracting #1: cost 6 inf + 0 1554043373.322 * * [simplify]: Extracting #2: cost 8 inf + 0 1554043373.322 * * [simplify]: Extracting #3: cost 5 inf + 43 1554043373.322 * * [simplify]: Extracting #4: cost 0 inf + 2131 1554043373.322 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1554043373.323 * [simplify]: Simplified (2 1 1 1) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043373.323 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1554043373.323 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1554043373.323 * * [simplify]: iters left: 3 (6 enodes) 1554043373.326 * * [simplify]: iters left: 2 (14 enodes) 1554043373.332 * * [simplify]: iters left: 1 (18 enodes) 1554043373.338 * * [simplify]: Extracting #0: cost 1 inf + 0 1554043373.338 * * [simplify]: Extracting #1: cost 6 inf + 0 1554043373.338 * * [simplify]: Extracting #2: cost 8 inf + 0 1554043373.338 * * [simplify]: Extracting #3: cost 5 inf + 43 1554043373.339 * * [simplify]: Extracting #4: cost 0 inf + 2131 1554043373.339 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1554043373.339 * [simplify]: Simplified (2 1 1 1) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) 1554043373.339 * * * [progress]: adding candidates to table 1554043374.179 * [progress]: [Phase 3 of 3] Extracting. 1554043374.179 * * [regime]: Finding splitpoints for: (#posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x)))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))))> #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (/.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))))>) 1554043374.184 * * * [regime-changes]: Trying 1 branch expressions: (x) 1554043374.184 * * * * [regimes]: Trying to branch on x from (#posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x)))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))))> #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (/.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))))>) 1554043374.740 * * * [regime]: Found split indices: #