1552126665.630 * [progress]: [Phase 1 of 3] Setting up. 1552126665.630 * * * [progress]: [1/2] Preparing points 1552126665.630 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 1552126665.631 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 1552126665.633 * * * * [points]: Setting MPFR precision to 64 1552126665.635 * * * * [points]: Setting MPFR precision to 320 1552126665.636 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 1552126665.639 * * * * [points]: Setting MPFR precision to 64 1552126665.642 * * * * [points]: Setting MPFR precision to 320 1552126665.645 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 1552126665.648 * * * * [points]: Setting MPFR precision to 64 1552126665.652 * * * * [points]: Setting MPFR precision to 320 1552126665.657 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 1552126665.660 * * * * [points]: Setting MPFR precision to 64 1552126665.665 * * * * [points]: Setting MPFR precision to 320 1552126665.670 * * * * [points]: Computing exacts for 256 points 1552126665.672 * * * * [points]: Setting MPFR precision to 64 1552126665.684 * * * * [points]: Setting MPFR precision to 320 1552126665.700 * * * * [points]: Filtering points with unrepresentable outputs 1552126665.709 * * * * [points]: Sampling 134 additional inputs, on iter 1 have 122 / 256 1552126665.709 * * * * [points]: Computing exacts on every 8 of 134 points to ramp up precision 1552126665.712 * * * * [points]: Setting MPFR precision to 64 1552126665.713 * * * * [points]: Setting MPFR precision to 320 1552126665.715 * * * * [points]: Computing exacts on every 4 of 134 points to ramp up precision 1552126665.718 * * * * [points]: Setting MPFR precision to 64 1552126665.720 * * * * [points]: Setting MPFR precision to 320 1552126665.723 * * * * [points]: Computing exacts on every 2 of 134 points to ramp up precision 1552126665.725 * * * * [points]: Setting MPFR precision to 64 1552126665.729 * * * * [points]: Setting MPFR precision to 320 1552126665.734 * * * * [points]: Computing exacts for 134 points 1552126665.737 * * * * [points]: Setting MPFR precision to 64 1552126665.769 * * * * [points]: Setting MPFR precision to 320 1552126665.781 * * * * [points]: Filtering points with unrepresentable outputs 1552126665.784 * * * * [points]: Sampling 65 additional inputs, on iter 2 have 191 / 256 1552126665.784 * * * * [points]: Computing exacts on every 4 of 65 points to ramp up precision 1552126665.786 * * * * [points]: Setting MPFR precision to 64 1552126665.787 * * * * [points]: Setting MPFR precision to 320 1552126665.787 * * * * [points]: Computing exacts on every 2 of 65 points to ramp up precision 1552126665.789 * * * * [points]: Setting MPFR precision to 64 1552126665.790 * * * * [points]: Setting MPFR precision to 320 1552126665.792 * * * * [points]: Computing exacts for 65 points 1552126665.793 * * * * [points]: Setting MPFR precision to 64 1552126665.796 * * * * [points]: Setting MPFR precision to 320 1552126665.803 * * * * [points]: Filtering points with unrepresentable outputs 1552126665.806 * * * * [points]: Sampling 37 additional inputs, on iter 3 have 219 / 256 1552126665.806 * * * * [points]: Computing exacts on every 2 of 37 points to ramp up precision 1552126665.809 * * * * [points]: Setting MPFR precision to 64 1552126665.810 * * * * [points]: Setting MPFR precision to 320 1552126665.812 * * * * [points]: Computing exacts for 37 points 1552126665.815 * * * * [points]: Setting MPFR precision to 64 1552126665.818 * * * * [points]: Setting MPFR precision to 320 1552126665.822 * * * * [points]: Filtering points with unrepresentable outputs 1552126665.823 * * * * [points]: Sampling 18 additional inputs, on iter 4 have 238 / 256 1552126665.823 * * * * [points]: Computing exacts for 18 points 1552126665.826 * * * * [points]: Setting MPFR precision to 64 1552126665.827 * * * * [points]: Setting MPFR precision to 320 1552126665.828 * * * * [points]: Filtering points with unrepresentable outputs 1552126665.829 * * * * [points]: Sampling 12 additional inputs, on iter 5 have 244 / 256 1552126665.829 * * * * [points]: Computing exacts for 12 points 1552126665.830 * * * * [points]: Setting MPFR precision to 64 1552126665.831 * * * * [points]: Setting MPFR precision to 320 1552126665.832 * * * * [points]: Filtering points with unrepresentable outputs 1552126665.832 * * * * [points]: Sampling 5 additional inputs, on iter 6 have 251 / 256 1552126665.832 * * * * [points]: Computing exacts for 5 points 1552126665.834 * * * * [points]: Setting MPFR precision to 64 1552126665.834 * * * * [points]: Setting MPFR precision to 320 1552126665.835 * * * * [points]: Filtering points with unrepresentable outputs 1552126665.835 * * * * [points]: Sampling 4 additional inputs, on iter 7 have 255 / 256 1552126665.835 * * * * [points]: Computing exacts for 4 points 1552126665.837 * * * * [points]: Setting MPFR precision to 64 1552126665.837 * * * * [points]: Setting MPFR precision to 320 1552126665.837 * * * * [points]: Filtering points with unrepresentable outputs 1552126665.837 * * * * [points]: Sampled 256 points with exact outputs 1552126665.837 * * * [progress]: [2/2] Setting up program. 1552126665.855 * [progress]: [Phase 2 of 3] Improving. 1552126665.855 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552126665.855 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126665.856 * * [simplify]: iters left: 5 (9 enodes) 1552126665.858 * * [simplify]: iters left: 4 (22 enodes) 1552126665.862 * * [simplify]: iters left: 3 (42 enodes) 1552126665.870 * * [simplify]: iters left: 2 (100 enodes) 1552126665.911 * * [simplify]: iters left: 1 (347 enodes) 1552126666.134 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126666.134 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126666.134 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126666.136 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126666.144 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126666.201 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126666.277 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126666.371 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126666.436 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126666.514 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126666.623 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126666.623 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552126666.658 * * [progress]: iteration 1 / 4 1552126666.658 * * * [progress]: picking best candidate 1552126666.694 * * * * [pick]: Picked #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552126666.694 * * * [progress]: localizing error 1552126666.936 * * * [progress]: generating rewritten candidates 1552126666.936 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 1552126666.940 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 1552126666.941 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 1552126666.942 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 1552126666.942 * * * [progress]: generating series expansions 1552126666.942 * * * * [progress]: [ 1 / 4 ] generating series at (2) 1552126666.942 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 1552126666.942 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 1552126666.942 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 1552126666.942 * * * [progress]: simplifying candidates 1552126666.942 * * * * [progress]: [ 1 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (neg.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1552126666.942 * * * * [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)))))))> 1552126666.943 * * * * [progress]: [ 3 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552126666.943 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126666.943 * * [simplify]: iters left: 5 (9 enodes) 1552126666.945 * * [simplify]: iters left: 4 (22 enodes) 1552126666.949 * * [simplify]: iters left: 3 (42 enodes) 1552126666.956 * * [simplify]: iters left: 2 (100 enodes) 1552126666.985 * * [simplify]: iters left: 1 (347 enodes) 1552126667.208 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126667.209 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126667.210 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126667.211 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126667.220 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126667.284 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126667.368 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126667.486 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126667.608 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126667.711 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126667.793 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126667.793 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552126667.793 * * * * [progress]: [ 4 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552126667.793 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126667.793 * * [simplify]: iters left: 5 (9 enodes) 1552126667.796 * * [simplify]: iters left: 4 (22 enodes) 1552126667.800 * * [simplify]: iters left: 3 (42 enodes) 1552126667.810 * * [simplify]: iters left: 2 (100 enodes) 1552126667.849 * * [simplify]: iters left: 1 (347 enodes) 1552126668.034 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126668.034 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126668.035 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126668.038 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126668.060 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126668.121 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126668.201 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126668.282 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126668.391 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126668.481 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126668.603 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126668.603 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552126668.603 * * * * [progress]: [ 5 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552126668.603 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126668.603 * * [simplify]: iters left: 5 (9 enodes) 1552126668.608 * * [simplify]: iters left: 4 (22 enodes) 1552126668.616 * * [simplify]: iters left: 3 (42 enodes) 1552126668.631 * * [simplify]: iters left: 2 (100 enodes) 1552126668.677 * * [simplify]: iters left: 1 (347 enodes) 1552126668.976 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126668.976 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126668.978 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126668.981 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126668.997 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126669.085 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126669.545 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126669.606 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126669.670 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126669.784 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126669.871 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126669.871 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552126669.871 * * * * [progress]: [ 6 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552126669.872 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126669.872 * * [simplify]: iters left: 5 (9 enodes) 1552126669.874 * * [simplify]: iters left: 4 (22 enodes) 1552126669.882 * * [simplify]: iters left: 3 (42 enodes) 1552126669.898 * * [simplify]: iters left: 2 (100 enodes) 1552126669.938 * * [simplify]: iters left: 1 (347 enodes) 1552126670.211 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126670.212 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126670.212 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126670.214 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126670.223 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126670.305 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126670.435 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126670.523 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126670.586 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126670.648 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126670.732 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126670.732 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552126670.732 * * * [progress]: adding candidates to table 1552126671.023 * * [progress]: iteration 2 / 4 1552126671.023 * * * [progress]: picking best candidate 1552126671.057 * * * * [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)))))))> 1552126671.057 * * * [progress]: localizing error 1552126671.321 * * * [progress]: generating rewritten candidates 1552126671.321 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 1552126671.323 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1552126671.331 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 1552126671.333 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 1552126671.335 * * * [progress]: generating series expansions 1552126671.335 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 1552126671.335 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1552126671.335 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 1552126671.335 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 1552126671.335 * * * [progress]: simplifying candidates 1552126671.335 * * * * [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)))))))> 1552126671.335 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126671.335 * * [simplify]: iters left: 5 (9 enodes) 1552126671.338 * * [simplify]: iters left: 4 (16 enodes) 1552126671.341 * * [simplify]: iters left: 3 (18 enodes) 1552126671.343 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126671.343 * * [simplify]: Extracting #1: cost 3 inf + 0 1552126671.343 * * [simplify]: Extracting #2: cost 6 inf + 0 1552126671.344 * * [simplify]: Extracting #3: cost 9 inf + 0 1552126671.344 * * [simplify]: Extracting #4: cost 6 inf + 43 1552126671.344 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552126671.344 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126671.344 * [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))))))) 1552126671.344 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126671.344 * * [simplify]: iters left: 5 (9 enodes) 1552126671.346 * * [simplify]: iters left: 4 (22 enodes) 1552126671.350 * * [simplify]: iters left: 3 (42 enodes) 1552126671.358 * * [simplify]: iters left: 2 (100 enodes) 1552126671.379 * * [simplify]: iters left: 1 (347 enodes) 1552126671.547 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126671.547 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126671.548 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126671.550 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126671.559 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126671.617 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126671.744 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126671.864 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126671.987 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126672.108 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126672.228 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126672.228 * [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))))))) 1552126672.229 * * * * [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)))))))> 1552126672.229 * * * * [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)))))))> 1552126672.229 * * * * [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))))))))> 1552126672.229 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126672.229 * * [simplify]: iters left: 5 (9 enodes) 1552126672.233 * * [simplify]: iters left: 4 (16 enodes) 1552126672.238 * * [simplify]: iters left: 3 (18 enodes) 1552126672.244 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126672.244 * * [simplify]: Extracting #1: cost 3 inf + 0 1552126672.244 * * [simplify]: Extracting #2: cost 6 inf + 0 1552126672.244 * * [simplify]: Extracting #3: cost 9 inf + 0 1552126672.244 * * [simplify]: Extracting #4: cost 6 inf + 43 1552126672.245 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552126672.245 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126672.245 * [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)))))))) 1552126672.245 * * * * [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)))))))))> 1552126672.245 * [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))))))) 1552126672.246 * * [simplify]: iters left: 6 (13 enodes) 1552126672.253 * * [simplify]: iters left: 5 (45 enodes) 1552126672.272 * * [simplify]: iters left: 4 (144 enodes) 1552126672.337 * * [simplify]: iters left: 3 (446 enodes) 1552126672.779 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126672.779 * * [simplify]: Extracting #1: cost 41 inf + 0 1552126672.780 * * [simplify]: Extracting #2: cost 283 inf + 0 1552126672.783 * * [simplify]: Extracting #3: cost 446 inf + 44 1552126672.804 * * [simplify]: Extracting #4: cost 488 inf + 246749 1552126672.924 * * [simplify]: Extracting #5: cost 101 inf + 1165723 1552126673.061 * * [simplify]: Extracting #6: cost 2 inf + 1463482 1552126673.226 * * [simplify]: Extracting #7: cost 0 inf + 1419126 1552126673.393 * * [simplify]: Extracting #8: cost 0 inf + 1414206 1552126673.533 * [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)))) 1552126673.533 * [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))))))))) 1552126673.533 * * * * [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)))))))> 1552126673.534 * [simplify]: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1552126673.534 * * [simplify]: iters left: 3 (5 enodes) 1552126673.535 * * [simplify]: iters left: 2 (11 enodes) 1552126673.537 * * [simplify]: iters left: 1 (13 enodes) 1552126673.540 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126673.540 * * [simplify]: Extracting #1: cost 2 inf + 0 1552126673.540 * * [simplify]: Extracting #2: cost 4 inf + 0 1552126673.540 * * [simplify]: Extracting #3: cost 4 inf + 1 1552126673.540 * * [simplify]: Extracting #4: cost 0 inf + 127 1552126673.541 * [simplify]: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1552126673.541 * [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))))))) 1552126673.541 * * * * [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)))))))> 1552126673.541 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126673.541 * * [simplify]: iters left: 5 (7 enodes) 1552126673.544 * * [simplify]: iters left: 4 (16 enodes) 1552126673.550 * * [simplify]: iters left: 3 (20 enodes) 1552126673.555 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126673.555 * * [simplify]: Extracting #1: cost 6 inf + 0 1552126673.556 * * [simplify]: Extracting #2: cost 8 inf + 0 1552126673.556 * * [simplify]: Extracting #3: cost 8 inf + 1 1552126673.556 * * [simplify]: Extracting #4: cost 5 inf + 324 1552126673.556 * * [simplify]: Extracting #5: cost 0 inf + 2334 1552126673.556 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1552126673.556 * [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))))))) 1552126673.557 * * * * [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)))))))> 1552126673.557 * * * * [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)))))))> 1552126673.557 * [simplify]: Simplifying (sqrt.p16 x) 1552126673.557 * * [simplify]: iters left: 1 (2 enodes) 1552126673.558 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126673.558 * * [simplify]: Extracting #1: cost 2 inf + 0 1552126673.558 * * [simplify]: Extracting #2: cost 1 inf + 1 1552126673.558 * * [simplify]: Extracting #3: cost 0 inf + 42 1552126673.558 * [simplify]: Simplified to (sqrt.p16 x) 1552126673.558 * [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))))))) 1552126673.558 * * * * [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)))))))> 1552126673.558 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552126673.558 * * [simplify]: iters left: 3 (6 enodes) 1552126673.561 * * [simplify]: iters left: 2 (14 enodes) 1552126673.566 * * [simplify]: iters left: 1 (18 enodes) 1552126673.571 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126673.571 * * [simplify]: Extracting #1: cost 6 inf + 0 1552126673.572 * * [simplify]: Extracting #2: cost 8 inf + 0 1552126673.572 * * [simplify]: Extracting #3: cost 5 inf + 43 1552126673.572 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552126673.572 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552126673.572 * [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))))))) 1552126673.572 * * * * [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)))))))> 1552126673.572 * * * * [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)))))))> 1552126673.572 * * * * [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)))))))> 1552126673.573 * * * * [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)))))))> 1552126673.573 * * * * [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)))))))> 1552126673.573 * * * [progress]: adding candidates to table 1552126674.520 * * [progress]: iteration 3 / 4 1552126674.520 * * * [progress]: picking best candidate 1552126674.651 * * * * [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)))))))> 1552126674.651 * * * [progress]: localizing error 1552126674.716 * * * [progress]: generating rewritten candidates 1552126674.716 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 1552126674.719 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1552126674.727 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2) 1552126674.728 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2) 1552126674.729 * * * [progress]: generating series expansions 1552126674.729 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 1552126674.729 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1552126674.730 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2) 1552126674.730 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2) 1552126674.730 * * * [progress]: simplifying candidates 1552126674.730 * * * * [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)))))))> 1552126674.730 * * * * [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)))))))> 1552126674.730 * * * * [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))))))))> 1552126674.730 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126674.730 * * [simplify]: iters left: 5 (9 enodes) 1552126674.732 * * [simplify]: iters left: 4 (16 enodes) 1552126674.735 * * [simplify]: iters left: 3 (18 enodes) 1552126674.738 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126674.738 * * [simplify]: Extracting #1: cost 3 inf + 0 1552126674.738 * * [simplify]: Extracting #2: cost 6 inf + 0 1552126674.738 * * [simplify]: Extracting #3: cost 9 inf + 0 1552126674.738 * * [simplify]: Extracting #4: cost 6 inf + 43 1552126674.738 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552126674.739 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126674.739 * [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)))))))) 1552126674.739 * * * * [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))))))))> 1552126674.739 * [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))))))) 1552126674.739 * * [simplify]: iters left: 6 (13 enodes) 1552126674.749 * * [simplify]: iters left: 5 (38 enodes) 1552126674.758 * * [simplify]: iters left: 4 (106 enodes) 1552126674.781 * * [simplify]: iters left: 3 (376 enodes) 1552126674.976 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126674.976 * * [simplify]: Extracting #1: cost 52 inf + 0 1552126674.977 * * [simplify]: Extracting #2: cost 302 inf + 0 1552126674.978 * * [simplify]: Extracting #3: cost 417 inf + 43 1552126674.990 * * [simplify]: Extracting #4: cost 351 inf + 302562 1552126675.073 * * [simplify]: Extracting #5: cost 35 inf + 1004993 1552126675.168 * * [simplify]: Extracting #6: cost 0 inf + 1083663 1552126675.238 * * [simplify]: Extracting #7: cost 0 inf + 1082583 1552126675.319 * [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)))))) 1552126675.319 * [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)))))))) 1552126675.319 * * * * [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)))))))> 1552126675.320 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126675.320 * * [simplify]: iters left: 5 (9 enodes) 1552126675.322 * * [simplify]: iters left: 4 (16 enodes) 1552126675.326 * * [simplify]: iters left: 3 (18 enodes) 1552126675.329 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126675.329 * * [simplify]: Extracting #1: cost 3 inf + 0 1552126675.329 * * [simplify]: Extracting #2: cost 6 inf + 0 1552126675.329 * * [simplify]: Extracting #3: cost 9 inf + 0 1552126675.329 * * [simplify]: Extracting #4: cost 6 inf + 43 1552126675.329 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552126675.329 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126675.329 * [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))))))) 1552126675.330 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126675.330 * * [simplify]: iters left: 5 (9 enodes) 1552126675.332 * * [simplify]: iters left: 4 (22 enodes) 1552126675.335 * * [simplify]: iters left: 3 (42 enodes) 1552126675.343 * * [simplify]: iters left: 2 (100 enodes) 1552126675.381 * * [simplify]: iters left: 1 (347 enodes) 1552126675.572 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126675.572 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126675.573 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126675.575 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126675.583 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126675.644 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126675.737 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126675.814 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126675.896 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126675.982 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126676.069 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126676.069 * [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))))))) 1552126676.069 * * * * [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)))))))> 1552126676.069 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126676.069 * * [simplify]: iters left: 5 (9 enodes) 1552126676.072 * * [simplify]: iters left: 4 (16 enodes) 1552126676.074 * * [simplify]: iters left: 3 (18 enodes) 1552126676.077 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126676.077 * * [simplify]: Extracting #1: cost 3 inf + 0 1552126676.077 * * [simplify]: Extracting #2: cost 6 inf + 0 1552126676.077 * * [simplify]: Extracting #3: cost 9 inf + 0 1552126676.077 * * [simplify]: Extracting #4: cost 6 inf + 43 1552126676.077 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552126676.077 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126676.077 * [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))))))) 1552126676.078 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126676.078 * * [simplify]: iters left: 5 (9 enodes) 1552126676.080 * * [simplify]: iters left: 4 (22 enodes) 1552126676.085 * * [simplify]: iters left: 3 (42 enodes) 1552126676.101 * * [simplify]: iters left: 2 (100 enodes) 1552126676.123 * * [simplify]: iters left: 1 (347 enodes) 1552126676.353 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126676.353 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126676.354 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126676.355 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126676.364 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126676.443 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126676.534 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126676.631 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126676.698 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126676.761 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126676.824 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126676.824 * [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))))))) 1552126676.824 * * * * [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)))))))> 1552126676.824 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126676.824 * * [simplify]: iters left: 5 (9 enodes) 1552126676.826 * * [simplify]: iters left: 4 (16 enodes) 1552126676.829 * * [simplify]: iters left: 3 (18 enodes) 1552126676.832 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126676.832 * * [simplify]: Extracting #1: cost 3 inf + 0 1552126676.832 * * [simplify]: Extracting #2: cost 6 inf + 0 1552126676.832 * * [simplify]: Extracting #3: cost 9 inf + 0 1552126676.832 * * [simplify]: Extracting #4: cost 6 inf + 43 1552126676.832 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552126676.832 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126676.832 * [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))))))) 1552126676.832 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126676.832 * * [simplify]: iters left: 5 (9 enodes) 1552126676.834 * * [simplify]: iters left: 4 (22 enodes) 1552126676.839 * * [simplify]: iters left: 3 (42 enodes) 1552126676.846 * * [simplify]: iters left: 2 (100 enodes) 1552126676.868 * * [simplify]: iters left: 1 (347 enodes) 1552126677.022 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126677.022 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126677.023 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126677.024 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126677.033 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126677.079 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126677.145 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126677.208 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126677.270 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126677.333 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126677.396 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126677.396 * [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))))))) 1552126677.396 * * * * [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)))))))> 1552126677.396 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126677.396 * * [simplify]: iters left: 5 (9 enodes) 1552126677.398 * * [simplify]: iters left: 4 (16 enodes) 1552126677.401 * * [simplify]: iters left: 3 (18 enodes) 1552126677.404 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126677.405 * * [simplify]: Extracting #1: cost 3 inf + 0 1552126677.405 * * [simplify]: Extracting #2: cost 6 inf + 0 1552126677.405 * * [simplify]: Extracting #3: cost 9 inf + 0 1552126677.405 * * [simplify]: Extracting #4: cost 6 inf + 43 1552126677.405 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552126677.405 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126677.405 * [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))))))) 1552126677.405 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126677.405 * * [simplify]: iters left: 5 (9 enodes) 1552126677.407 * * [simplify]: iters left: 4 (22 enodes) 1552126677.412 * * [simplify]: iters left: 3 (42 enodes) 1552126677.420 * * [simplify]: iters left: 2 (100 enodes) 1552126677.442 * * [simplify]: iters left: 1 (347 enodes) 1552126677.595 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126677.595 * * [simplify]: Extracting #1: cost 48 inf + 0 1552126677.595 * * [simplify]: Extracting #2: cost 269 inf + 0 1552126677.597 * * [simplify]: Extracting #3: cost 457 inf + 1 1552126677.605 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552126677.651 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552126677.718 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552126677.783 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552126677.845 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552126677.908 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552126677.971 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552126677.971 * [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))))))) 1552126677.971 * * * [progress]: adding candidates to table 1552126678.204 * * [progress]: iteration 4 / 4 1552126678.204 * * * [progress]: picking best candidate 1552126678.319 * * * * [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)))))))> 1552126678.319 * * * [progress]: localizing error 1552126678.438 * * * [progress]: generating rewritten candidates 1552126678.438 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 1552126678.442 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1552126678.449 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 1552126678.451 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 1552126678.452 * * * [progress]: generating series expansions 1552126678.452 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 1552126678.452 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1552126678.452 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 1552126678.452 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 1552126678.452 * * * [progress]: simplifying candidates 1552126678.452 * * * * [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)))))))> 1552126678.452 * * * * [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)))))))> 1552126678.452 * * * * [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)))))))))> 1552126678.453 * [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))))))) 1552126678.453 * * [simplify]: iters left: 6 (14 enodes) 1552126678.456 * * [simplify]: iters left: 5 (47 enodes) 1552126678.466 * * [simplify]: iters left: 4 (140 enodes) 1552126678.506 * * [simplify]: iters left: 3 (480 enodes) 1552126678.786 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126678.786 * * [simplify]: Extracting #1: cost 36 inf + 0 1552126678.787 * * [simplify]: Extracting #2: cost 250 inf + 0 1552126678.789 * * [simplify]: Extracting #3: cost 413 inf + 725 1552126678.797 * * [simplify]: Extracting #4: cost 550 inf + 129982 1552126678.844 * * [simplify]: Extracting #5: cost 163 inf + 996596 1552126678.930 * * [simplify]: Extracting #6: cost 12 inf + 1471739 1552126679.018 * * [simplify]: Extracting #7: cost 0 inf + 1461963 1552126679.104 * * [simplify]: Extracting #8: cost 0 inf + 1441923 1552126679.190 * * [simplify]: Extracting #9: cost 0 inf + 1441523 1552126679.274 * [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)))))) 1552126679.274 * [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))))))))) 1552126679.274 * * * * [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)))))))> 1552126679.274 * [simplify]: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1552126679.274 * * [simplify]: iters left: 3 (5 enodes) 1552126679.276 * * [simplify]: iters left: 2 (11 enodes) 1552126679.278 * * [simplify]: iters left: 1 (13 enodes) 1552126679.280 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126679.280 * * [simplify]: Extracting #1: cost 2 inf + 0 1552126679.280 * * [simplify]: Extracting #2: cost 4 inf + 0 1552126679.280 * * [simplify]: Extracting #3: cost 4 inf + 1 1552126679.280 * * [simplify]: Extracting #4: cost 0 inf + 127 1552126679.281 * [simplify]: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1552126679.281 * [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))))))) 1552126679.281 * * * * [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)))))))> 1552126679.281 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552126679.281 * * [simplify]: iters left: 5 (7 enodes) 1552126679.283 * * [simplify]: iters left: 4 (16 enodes) 1552126679.286 * * [simplify]: iters left: 3 (20 enodes) 1552126679.289 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126679.289 * * [simplify]: Extracting #1: cost 6 inf + 0 1552126679.289 * * [simplify]: Extracting #2: cost 8 inf + 0 1552126679.289 * * [simplify]: Extracting #3: cost 8 inf + 1 1552126679.289 * * [simplify]: Extracting #4: cost 5 inf + 324 1552126679.290 * * [simplify]: Extracting #5: cost 0 inf + 2334 1552126679.290 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1552126679.290 * [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))))))) 1552126679.290 * * * * [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)))))))> 1552126679.290 * * * * [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)))))))> 1552126679.290 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552126679.290 * * [simplify]: iters left: 3 (6 enodes) 1552126679.293 * * [simplify]: iters left: 2 (14 enodes) 1552126679.295 * * [simplify]: iters left: 1 (18 enodes) 1552126679.298 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126679.298 * * [simplify]: Extracting #1: cost 6 inf + 0 1552126679.298 * * [simplify]: Extracting #2: cost 8 inf + 0 1552126679.298 * * [simplify]: Extracting #3: cost 5 inf + 43 1552126679.298 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552126679.298 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552126679.298 * [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))))))) 1552126679.298 * * * * [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)))))))> 1552126679.298 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552126679.299 * * [simplify]: iters left: 3 (6 enodes) 1552126679.300 * * [simplify]: iters left: 2 (14 enodes) 1552126679.302 * * [simplify]: iters left: 1 (18 enodes) 1552126679.305 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126679.305 * * [simplify]: Extracting #1: cost 6 inf + 0 1552126679.305 * * [simplify]: Extracting #2: cost 8 inf + 0 1552126679.305 * * [simplify]: Extracting #3: cost 5 inf + 43 1552126679.305 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552126679.305 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552126679.305 * [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))))))) 1552126679.305 * * * * [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)))))))> 1552126679.306 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552126679.306 * * [simplify]: iters left: 3 (6 enodes) 1552126679.307 * * [simplify]: iters left: 2 (14 enodes) 1552126679.309 * * [simplify]: iters left: 1 (18 enodes) 1552126679.312 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126679.312 * * [simplify]: Extracting #1: cost 6 inf + 0 1552126679.312 * * [simplify]: Extracting #2: cost 8 inf + 0 1552126679.312 * * [simplify]: Extracting #3: cost 5 inf + 43 1552126679.312 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552126679.312 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552126679.312 * [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))))))) 1552126679.312 * * * * [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)))))))> 1552126679.313 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552126679.313 * * [simplify]: iters left: 3 (6 enodes) 1552126679.314 * * [simplify]: iters left: 2 (14 enodes) 1552126679.316 * * [simplify]: iters left: 1 (18 enodes) 1552126679.319 * * [simplify]: Extracting #0: cost 1 inf + 0 1552126679.319 * * [simplify]: Extracting #1: cost 6 inf + 0 1552126679.319 * * [simplify]: Extracting #2: cost 8 inf + 0 1552126679.319 * * [simplify]: Extracting #3: cost 5 inf + 43 1552126679.319 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552126679.319 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552126679.319 * [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))))))) 1552126679.320 * * * [progress]: adding candidates to table 1552126679.632 * [progress]: [Phase 3 of 3] Extracting. 1552126679.632 * * [regime]: Finding splitpoints for: (#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) (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)))))))> #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)))))))))> #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)))))))> #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))))))> #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) (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 (/.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))))))))>) 1552126679.644 * * * [regime-changes]: Trying 1 branch expressions: (x) 1552126679.644 * * * * [regimes]: Trying to branch on x from (#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) (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)))))))> #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)))))))))> #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)))))))> #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))))))> #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) (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 (/.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))))))))>) 1552126679.935 * * * [regime]: Found split indices: #