1552123201.649 * [progress]: [Phase 1 of 3] Setting up. 1552123201.649 * * * [progress]: [1/2] Preparing points 1552123201.649 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 1552123201.649 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 1552123201.651 * * * * [points]: Setting MPFR precision to 64 1552123201.652 * * * * [points]: Setting MPFR precision to 320 1552123201.654 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 1552123201.657 * * * * [points]: Setting MPFR precision to 64 1552123201.659 * * * * [points]: Setting MPFR precision to 320 1552123201.662 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 1552123201.665 * * * * [points]: Setting MPFR precision to 64 1552123201.669 * * * * [points]: Setting MPFR precision to 320 1552123201.672 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 1552123201.674 * * * * [points]: Setting MPFR precision to 64 1552123201.679 * * * * [points]: Setting MPFR precision to 320 1552123201.684 * * * * [points]: Computing exacts for 256 points 1552123201.686 * * * * [points]: Setting MPFR precision to 64 1552123201.698 * * * * [points]: Setting MPFR precision to 320 1552123201.715 * * * * [points]: Filtering points with unrepresentable outputs 1552123201.722 * * * * [points]: Sampling 134 additional inputs, on iter 1 have 122 / 256 1552123201.722 * * * * [points]: Computing exacts on every 8 of 134 points to ramp up precision 1552123201.724 * * * * [points]: Setting MPFR precision to 64 1552123201.724 * * * * [points]: Setting MPFR precision to 320 1552123201.725 * * * * [points]: Computing exacts on every 4 of 134 points to ramp up precision 1552123201.727 * * * * [points]: Setting MPFR precision to 64 1552123201.728 * * * * [points]: Setting MPFR precision to 320 1552123201.741 * * * * [points]: Computing exacts on every 2 of 134 points to ramp up precision 1552123201.743 * * * * [points]: Setting MPFR precision to 64 1552123201.745 * * * * [points]: Setting MPFR precision to 320 1552123201.748 * * * * [points]: Computing exacts for 134 points 1552123201.749 * * * * [points]: Setting MPFR precision to 64 1552123201.756 * * * * [points]: Setting MPFR precision to 320 1552123201.765 * * * * [points]: Filtering points with unrepresentable outputs 1552123201.768 * * * * [points]: Sampling 65 additional inputs, on iter 2 have 191 / 256 1552123201.768 * * * * [points]: Computing exacts on every 4 of 65 points to ramp up precision 1552123201.770 * * * * [points]: Setting MPFR precision to 64 1552123201.771 * * * * [points]: Setting MPFR precision to 320 1552123201.772 * * * * [points]: Computing exacts on every 2 of 65 points to ramp up precision 1552123201.773 * * * * [points]: Setting MPFR precision to 64 1552123201.774 * * * * [points]: Setting MPFR precision to 320 1552123201.775 * * * * [points]: Computing exacts for 65 points 1552123201.777 * * * * [points]: Setting MPFR precision to 64 1552123201.780 * * * * [points]: Setting MPFR precision to 320 1552123201.784 * * * * [points]: Filtering points with unrepresentable outputs 1552123201.786 * * * * [points]: Sampling 37 additional inputs, on iter 3 have 219 / 256 1552123201.786 * * * * [points]: Computing exacts on every 2 of 37 points to ramp up precision 1552123201.788 * * * * [points]: Setting MPFR precision to 64 1552123201.789 * * * * [points]: Setting MPFR precision to 320 1552123201.790 * * * * [points]: Computing exacts for 37 points 1552123201.793 * * * * [points]: Setting MPFR precision to 64 1552123201.796 * * * * [points]: Setting MPFR precision to 320 1552123201.800 * * * * [points]: Filtering points with unrepresentable outputs 1552123201.802 * * * * [points]: Sampling 18 additional inputs, on iter 4 have 238 / 256 1552123201.802 * * * * [points]: Computing exacts for 18 points 1552123201.805 * * * * [points]: Setting MPFR precision to 64 1552123201.807 * * * * [points]: Setting MPFR precision to 320 1552123201.809 * * * * [points]: Filtering points with unrepresentable outputs 1552123201.810 * * * * [points]: Sampling 12 additional inputs, on iter 5 have 244 / 256 1552123201.810 * * * * [points]: Computing exacts for 12 points 1552123201.813 * * * * [points]: Setting MPFR precision to 64 1552123201.814 * * * * [points]: Setting MPFR precision to 320 1552123201.814 * * * * [points]: Filtering points with unrepresentable outputs 1552123201.815 * * * * [points]: Sampling 5 additional inputs, on iter 6 have 251 / 256 1552123201.815 * * * * [points]: Computing exacts for 5 points 1552123201.816 * * * * [points]: Setting MPFR precision to 64 1552123201.817 * * * * [points]: Setting MPFR precision to 320 1552123201.817 * * * * [points]: Filtering points with unrepresentable outputs 1552123201.817 * * * * [points]: Sampling 4 additional inputs, on iter 7 have 255 / 256 1552123201.817 * * * * [points]: Computing exacts for 4 points 1552123201.819 * * * * [points]: Setting MPFR precision to 64 1552123201.819 * * * * [points]: Setting MPFR precision to 320 1552123201.820 * * * * [points]: Filtering points with unrepresentable outputs 1552123201.820 * * * * [points]: Sampled 256 points with exact outputs 1552123201.820 * * * [progress]: [2/2] Setting up program. 1552123201.841 * [progress]: [Phase 2 of 3] Improving. 1552123201.841 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552123201.841 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123201.841 * * [simplify]: iters left: 5 (9 enodes) 1552123201.843 * * [simplify]: iters left: 4 (22 enodes) 1552123201.847 * * [simplify]: iters left: 3 (42 enodes) 1552123201.868 * * [simplify]: iters left: 2 (100 enodes) 1552123201.889 * * [simplify]: iters left: 1 (347 enodes) 1552123202.089 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123202.089 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123202.090 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123202.091 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123202.101 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123202.151 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123202.214 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123202.278 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123202.343 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123202.406 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123202.468 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123202.468 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552123202.487 * * [progress]: iteration 1 / 4 1552123202.487 * * * [progress]: picking best candidate 1552123202.506 * * * * [pick]: Picked #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552123202.506 * * * [progress]: localizing error 1552123202.756 * * * [progress]: generating rewritten candidates 1552123202.756 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 1552123202.761 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 1552123202.763 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 1552123202.765 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 1552123202.766 * * * [progress]: generating series expansions 1552123202.766 * * * * [progress]: [ 1 / 4 ] generating series at (2) 1552123202.766 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 1552123202.766 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 1552123202.766 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 1552123202.766 * * * [progress]: simplifying candidates 1552123202.766 * * * * [progress]: [ 1 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (neg.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1552123202.766 * * * * [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)))))))> 1552123202.766 * * * * [progress]: [ 3 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552123202.767 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123202.767 * * [simplify]: iters left: 5 (9 enodes) 1552123202.771 * * [simplify]: iters left: 4 (22 enodes) 1552123202.779 * * [simplify]: iters left: 3 (42 enodes) 1552123202.790 * * [simplify]: iters left: 2 (100 enodes) 1552123202.826 * * [simplify]: iters left: 1 (347 enodes) 1552123203.026 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123203.026 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123203.027 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123203.028 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123203.037 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123203.086 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123203.150 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123203.214 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123203.275 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123203.338 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123203.414 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123203.415 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552123203.415 * * * * [progress]: [ 4 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552123203.415 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123203.415 * * [simplify]: iters left: 5 (9 enodes) 1552123203.419 * * [simplify]: iters left: 4 (22 enodes) 1552123203.428 * * [simplify]: iters left: 3 (42 enodes) 1552123203.443 * * [simplify]: iters left: 2 (100 enodes) 1552123203.481 * * [simplify]: iters left: 1 (347 enodes) 1552123203.664 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123203.664 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123203.665 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123203.668 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123203.688 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123203.735 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123203.835 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123203.915 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123204.001 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123204.071 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123204.156 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123204.156 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552123204.156 * * * * [progress]: [ 5 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552123204.157 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123204.157 * * [simplify]: iters left: 5 (9 enodes) 1552123204.160 * * [simplify]: iters left: 4 (22 enodes) 1552123204.167 * * [simplify]: iters left: 3 (42 enodes) 1552123204.174 * * [simplify]: iters left: 2 (100 enodes) 1552123204.210 * * [simplify]: iters left: 1 (347 enodes) 1552123204.377 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123204.378 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123204.379 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123204.381 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123204.390 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123204.435 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123204.501 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123204.571 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123204.643 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123204.705 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123204.777 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123204.777 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552123204.777 * * * * [progress]: [ 6 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1552123204.777 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123204.777 * * [simplify]: iters left: 5 (9 enodes) 1552123204.779 * * [simplify]: iters left: 4 (22 enodes) 1552123204.783 * * [simplify]: iters left: 3 (42 enodes) 1552123204.792 * * [simplify]: iters left: 2 (100 enodes) 1552123204.814 * * [simplify]: iters left: 1 (347 enodes) 1552123204.977 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123204.977 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123204.978 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123204.980 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123204.989 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123205.033 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123205.139 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123205.260 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123205.363 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123205.484 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123205.572 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123205.572 * [simplify]: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1552123205.572 * * * [progress]: adding candidates to table 1552123205.759 * * [progress]: iteration 2 / 4 1552123205.759 * * * [progress]: picking best candidate 1552123205.779 * * * * [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)))))))> 1552123205.779 * * * [progress]: localizing error 1552123206.000 * * * [progress]: generating rewritten candidates 1552123206.000 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 1552123206.004 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1552123206.020 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 1552123206.024 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 1552123206.028 * * * [progress]: generating series expansions 1552123206.028 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 1552123206.028 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1552123206.028 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 1552123206.028 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 1552123206.028 * * * [progress]: simplifying candidates 1552123206.029 * * * * [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)))))))> 1552123206.029 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123206.029 * * [simplify]: iters left: 5 (9 enodes) 1552123206.034 * * [simplify]: iters left: 4 (16 enodes) 1552123206.039 * * [simplify]: iters left: 3 (18 enodes) 1552123206.045 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123206.045 * * [simplify]: Extracting #1: cost 3 inf + 0 1552123206.045 * * [simplify]: Extracting #2: cost 6 inf + 0 1552123206.045 * * [simplify]: Extracting #3: cost 9 inf + 0 1552123206.046 * * [simplify]: Extracting #4: cost 6 inf + 43 1552123206.046 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552123206.046 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123206.046 * [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))))))) 1552123206.047 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123206.047 * * [simplify]: iters left: 5 (9 enodes) 1552123206.052 * * [simplify]: iters left: 4 (22 enodes) 1552123206.061 * * [simplify]: iters left: 3 (42 enodes) 1552123206.076 * * [simplify]: iters left: 2 (100 enodes) 1552123206.119 * * [simplify]: iters left: 1 (347 enodes) 1552123206.423 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123206.423 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123206.424 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123206.427 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123206.445 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123206.490 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123206.560 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123206.680 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123206.753 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123206.818 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123206.937 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123206.937 * [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))))))) 1552123206.937 * * * * [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)))))))> 1552123206.937 * * * * [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)))))))> 1552123206.937 * * * * [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))))))))> 1552123206.937 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123206.938 * * [simplify]: iters left: 5 (9 enodes) 1552123206.942 * * [simplify]: iters left: 4 (16 enodes) 1552123206.947 * * [simplify]: iters left: 3 (18 enodes) 1552123206.952 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123206.952 * * [simplify]: Extracting #1: cost 3 inf + 0 1552123206.952 * * [simplify]: Extracting #2: cost 6 inf + 0 1552123206.952 * * [simplify]: Extracting #3: cost 9 inf + 0 1552123206.952 * * [simplify]: Extracting #4: cost 6 inf + 43 1552123206.953 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552123206.953 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123206.953 * [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)))))))) 1552123206.953 * * * * [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)))))))))> 1552123206.954 * [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))))))) 1552123206.954 * * [simplify]: iters left: 6 (13 enodes) 1552123206.960 * * [simplify]: iters left: 5 (45 enodes) 1552123206.980 * * [simplify]: iters left: 4 (144 enodes) 1552123207.048 * * [simplify]: iters left: 3 (446 enodes) 1552123207.494 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123207.495 * * [simplify]: Extracting #1: cost 41 inf + 0 1552123207.496 * * [simplify]: Extracting #2: cost 283 inf + 0 1552123207.498 * * [simplify]: Extracting #3: cost 446 inf + 44 1552123207.521 * * [simplify]: Extracting #4: cost 488 inf + 246749 1552123207.641 * * [simplify]: Extracting #5: cost 101 inf + 1165723 1552123207.821 * * [simplify]: Extracting #6: cost 2 inf + 1463482 1552123207.917 * * [simplify]: Extracting #7: cost 0 inf + 1419126 1552123208.030 * * [simplify]: Extracting #8: cost 0 inf + 1414206 1552123208.151 * [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)))) 1552123208.151 * [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))))))))) 1552123208.151 * * * * [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)))))))> 1552123208.152 * [simplify]: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1552123208.152 * * [simplify]: iters left: 3 (5 enodes) 1552123208.154 * * [simplify]: iters left: 2 (11 enodes) 1552123208.157 * * [simplify]: iters left: 1 (13 enodes) 1552123208.162 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123208.162 * * [simplify]: Extracting #1: cost 2 inf + 0 1552123208.162 * * [simplify]: Extracting #2: cost 4 inf + 0 1552123208.162 * * [simplify]: Extracting #3: cost 4 inf + 1 1552123208.162 * * [simplify]: Extracting #4: cost 0 inf + 127 1552123208.162 * [simplify]: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1552123208.162 * [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))))))) 1552123208.162 * * * * [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)))))))> 1552123208.162 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123208.163 * * [simplify]: iters left: 5 (7 enodes) 1552123208.165 * * [simplify]: iters left: 4 (16 enodes) 1552123208.170 * * [simplify]: iters left: 3 (20 enodes) 1552123208.176 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123208.176 * * [simplify]: Extracting #1: cost 6 inf + 0 1552123208.176 * * [simplify]: Extracting #2: cost 8 inf + 0 1552123208.176 * * [simplify]: Extracting #3: cost 8 inf + 1 1552123208.176 * * [simplify]: Extracting #4: cost 5 inf + 324 1552123208.176 * * [simplify]: Extracting #5: cost 0 inf + 2334 1552123208.177 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1552123208.177 * [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))))))) 1552123208.177 * * * * [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)))))))> 1552123208.177 * * * * [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)))))))> 1552123208.177 * [simplify]: Simplifying (sqrt.p16 x) 1552123208.177 * * [simplify]: iters left: 1 (2 enodes) 1552123208.178 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123208.178 * * [simplify]: Extracting #1: cost 2 inf + 0 1552123208.178 * * [simplify]: Extracting #2: cost 1 inf + 1 1552123208.178 * * [simplify]: Extracting #3: cost 0 inf + 42 1552123208.178 * [simplify]: Simplified to (sqrt.p16 x) 1552123208.178 * [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))))))) 1552123208.178 * * * * [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)))))))> 1552123208.179 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552123208.179 * * [simplify]: iters left: 3 (6 enodes) 1552123208.182 * * [simplify]: iters left: 2 (14 enodes) 1552123208.186 * * [simplify]: iters left: 1 (18 enodes) 1552123208.192 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123208.192 * * [simplify]: Extracting #1: cost 6 inf + 0 1552123208.192 * * [simplify]: Extracting #2: cost 8 inf + 0 1552123208.192 * * [simplify]: Extracting #3: cost 5 inf + 43 1552123208.192 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552123208.192 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552123208.192 * [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))))))) 1552123208.192 * * * * [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)))))))> 1552123208.193 * * * * [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)))))))> 1552123208.193 * * * * [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)))))))> 1552123208.193 * * * * [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)))))))> 1552123208.193 * * * * [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)))))))> 1552123208.193 * * * [progress]: adding candidates to table 1552123209.245 * * [progress]: iteration 3 / 4 1552123209.245 * * * [progress]: picking best candidate 1552123209.464 * * * * [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)))))))> 1552123209.464 * * * [progress]: localizing error 1552123209.572 * * * [progress]: generating rewritten candidates 1552123209.572 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2) 1552123209.574 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1552123209.583 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 2) 1552123209.584 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2) 1552123209.585 * * * [progress]: generating series expansions 1552123209.585 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2) 1552123209.585 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1552123209.585 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 2) 1552123209.585 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2) 1552123209.585 * * * [progress]: simplifying candidates 1552123209.585 * * * * [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)))))))> 1552123209.585 * * * * [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)))))))> 1552123209.585 * * * * [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))))))))> 1552123209.585 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123209.585 * * [simplify]: iters left: 5 (9 enodes) 1552123209.587 * * [simplify]: iters left: 4 (16 enodes) 1552123209.590 * * [simplify]: iters left: 3 (18 enodes) 1552123209.592 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123209.592 * * [simplify]: Extracting #1: cost 3 inf + 0 1552123209.592 * * [simplify]: Extracting #2: cost 6 inf + 0 1552123209.593 * * [simplify]: Extracting #3: cost 9 inf + 0 1552123209.593 * * [simplify]: Extracting #4: cost 6 inf + 43 1552123209.593 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552123209.593 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123209.593 * [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)))))))) 1552123209.593 * * * * [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))))))))> 1552123209.593 * [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))))))) 1552123209.593 * * [simplify]: iters left: 6 (13 enodes) 1552123209.596 * * [simplify]: iters left: 5 (38 enodes) 1552123209.615 * * [simplify]: iters left: 4 (106 enodes) 1552123209.665 * * [simplify]: iters left: 3 (376 enodes) 1552123209.979 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123209.979 * * [simplify]: Extracting #1: cost 52 inf + 0 1552123209.980 * * [simplify]: Extracting #2: cost 302 inf + 0 1552123209.981 * * [simplify]: Extracting #3: cost 417 inf + 43 1552123209.996 * * [simplify]: Extracting #4: cost 351 inf + 302562 1552123210.063 * * [simplify]: Extracting #5: cost 35 inf + 1004993 1552123210.119 * * [simplify]: Extracting #6: cost 0 inf + 1083663 1552123210.175 * * [simplify]: Extracting #7: cost 0 inf + 1082583 1552123210.237 * [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)))))) 1552123210.238 * [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)))))))) 1552123210.238 * * * * [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)))))))> 1552123210.238 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123210.238 * * [simplify]: iters left: 5 (9 enodes) 1552123210.240 * * [simplify]: iters left: 4 (16 enodes) 1552123210.244 * * [simplify]: iters left: 3 (18 enodes) 1552123210.249 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123210.249 * * [simplify]: Extracting #1: cost 3 inf + 0 1552123210.249 * * [simplify]: Extracting #2: cost 6 inf + 0 1552123210.249 * * [simplify]: Extracting #3: cost 9 inf + 0 1552123210.250 * * [simplify]: Extracting #4: cost 6 inf + 43 1552123210.250 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552123210.250 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123210.250 * [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))))))) 1552123210.250 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123210.251 * * [simplify]: iters left: 5 (9 enodes) 1552123210.254 * * [simplify]: iters left: 4 (22 enodes) 1552123210.262 * * [simplify]: iters left: 3 (42 enodes) 1552123210.277 * * [simplify]: iters left: 2 (100 enodes) 1552123210.321 * * [simplify]: iters left: 1 (347 enodes) 1552123210.616 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123210.616 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123210.617 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123210.620 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123210.635 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123210.682 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123210.747 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123210.836 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123210.956 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123211.076 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123211.198 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123211.198 * [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))))))) 1552123211.199 * * * * [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)))))))> 1552123211.199 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123211.199 * * [simplify]: iters left: 5 (9 enodes) 1552123211.203 * * [simplify]: iters left: 4 (16 enodes) 1552123211.208 * * [simplify]: iters left: 3 (18 enodes) 1552123211.214 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123211.214 * * [simplify]: Extracting #1: cost 3 inf + 0 1552123211.214 * * [simplify]: Extracting #2: cost 6 inf + 0 1552123211.214 * * [simplify]: Extracting #3: cost 9 inf + 0 1552123211.214 * * [simplify]: Extracting #4: cost 6 inf + 43 1552123211.214 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552123211.214 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123211.214 * [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))))))) 1552123211.215 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123211.215 * * [simplify]: iters left: 5 (9 enodes) 1552123211.219 * * [simplify]: iters left: 4 (22 enodes) 1552123211.226 * * [simplify]: iters left: 3 (42 enodes) 1552123211.241 * * [simplify]: iters left: 2 (100 enodes) 1552123211.286 * * [simplify]: iters left: 1 (347 enodes) 1552123211.585 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123211.585 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123211.586 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123211.589 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123211.607 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123211.702 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123211.816 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123211.940 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123212.046 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123212.156 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123212.249 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123212.249 * [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))))))) 1552123212.249 * * * * [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)))))))> 1552123212.250 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123212.250 * * [simplify]: iters left: 5 (9 enodes) 1552123212.254 * * [simplify]: iters left: 4 (16 enodes) 1552123212.259 * * [simplify]: iters left: 3 (18 enodes) 1552123212.266 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123212.266 * * [simplify]: Extracting #1: cost 3 inf + 0 1552123212.266 * * [simplify]: Extracting #2: cost 6 inf + 0 1552123212.266 * * [simplify]: Extracting #3: cost 9 inf + 0 1552123212.266 * * [simplify]: Extracting #4: cost 6 inf + 43 1552123212.266 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552123212.267 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123212.267 * [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))))))) 1552123212.267 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123212.267 * * [simplify]: iters left: 5 (9 enodes) 1552123212.271 * * [simplify]: iters left: 4 (22 enodes) 1552123212.279 * * [simplify]: iters left: 3 (42 enodes) 1552123212.294 * * [simplify]: iters left: 2 (100 enodes) 1552123212.339 * * [simplify]: iters left: 1 (347 enodes) 1552123212.638 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123212.638 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123212.640 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123212.650 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123212.667 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123212.754 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123212.881 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123212.979 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123213.046 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123213.108 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123213.169 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123213.170 * [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))))))) 1552123213.170 * * * * [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)))))))> 1552123213.170 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123213.170 * * [simplify]: iters left: 5 (9 enodes) 1552123213.172 * * [simplify]: iters left: 4 (16 enodes) 1552123213.177 * * [simplify]: iters left: 3 (18 enodes) 1552123213.183 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123213.183 * * [simplify]: Extracting #1: cost 3 inf + 0 1552123213.183 * * [simplify]: Extracting #2: cost 6 inf + 0 1552123213.183 * * [simplify]: Extracting #3: cost 9 inf + 0 1552123213.183 * * [simplify]: Extracting #4: cost 6 inf + 43 1552123213.183 * * [simplify]: Extracting #5: cost 0 inf + 2214 1552123213.183 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123213.183 * [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))))))) 1552123213.183 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123213.183 * * [simplify]: iters left: 5 (9 enodes) 1552123213.185 * * [simplify]: iters left: 4 (22 enodes) 1552123213.190 * * [simplify]: iters left: 3 (42 enodes) 1552123213.197 * * [simplify]: iters left: 2 (100 enodes) 1552123213.219 * * [simplify]: iters left: 1 (347 enodes) 1552123213.370 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123213.370 * * [simplify]: Extracting #1: cost 48 inf + 0 1552123213.371 * * [simplify]: Extracting #2: cost 269 inf + 0 1552123213.372 * * [simplify]: Extracting #3: cost 457 inf + 1 1552123213.381 * * [simplify]: Extracting #4: cost 422 inf + 210469 1552123213.430 * * [simplify]: Extracting #5: cost 77 inf + 915056 1552123213.506 * * [simplify]: Extracting #6: cost 3 inf + 1114648 1552123213.592 * * [simplify]: Extracting #7: cost 1 inf + 1091652 1552123213.655 * * [simplify]: Extracting #8: cost 0 inf + 1093814 1552123213.720 * * [simplify]: Extracting #9: cost 0 inf + 1093774 1552123213.792 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1552123213.792 * [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))))))) 1552123213.792 * * * [progress]: adding candidates to table 1552123214.150 * * [progress]: iteration 4 / 4 1552123214.150 * * * [progress]: picking best candidate 1552123214.287 * * * * [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)))))))> 1552123214.287 * * * [progress]: localizing error 1552123214.477 * * * [progress]: generating rewritten candidates 1552123214.477 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 1552123214.480 * * * * [progress]: [ 2 / 4 ] rewriting at (2) 1552123214.488 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 1552123214.490 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 1552123214.491 * * * [progress]: generating series expansions 1552123214.491 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 1552123214.491 * * * * [progress]: [ 2 / 4 ] generating series at (2) 1552123214.491 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 1552123214.491 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 1552123214.491 * * * [progress]: simplifying candidates 1552123214.491 * * * * [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)))))))> 1552123214.491 * * * * [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)))))))> 1552123214.491 * * * * [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)))))))))> 1552123214.492 * [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))))))) 1552123214.492 * * [simplify]: iters left: 6 (14 enodes) 1552123214.496 * * [simplify]: iters left: 5 (47 enodes) 1552123214.515 * * [simplify]: iters left: 4 (140 enodes) 1552123214.571 * * [simplify]: iters left: 3 (480 enodes) 1552123214.917 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123214.918 * * [simplify]: Extracting #1: cost 36 inf + 0 1552123214.918 * * [simplify]: Extracting #2: cost 250 inf + 0 1552123214.920 * * [simplify]: Extracting #3: cost 413 inf + 725 1552123214.931 * * [simplify]: Extracting #4: cost 550 inf + 129982 1552123214.996 * * [simplify]: Extracting #5: cost 163 inf + 996596 1552123215.080 * * [simplify]: Extracting #6: cost 12 inf + 1471739 1552123215.178 * * [simplify]: Extracting #7: cost 0 inf + 1461963 1552123215.283 * * [simplify]: Extracting #8: cost 0 inf + 1441923 1552123215.445 * * [simplify]: Extracting #9: cost 0 inf + 1441523 1552123215.573 * [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)))))) 1552123215.574 * [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))))))))) 1552123215.574 * * * * [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)))))))> 1552123215.574 * [simplify]: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1552123215.574 * * [simplify]: iters left: 3 (5 enodes) 1552123215.576 * * [simplify]: iters left: 2 (11 enodes) 1552123215.578 * * [simplify]: iters left: 1 (13 enodes) 1552123215.580 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123215.580 * * [simplify]: Extracting #1: cost 2 inf + 0 1552123215.580 * * [simplify]: Extracting #2: cost 4 inf + 0 1552123215.580 * * [simplify]: Extracting #3: cost 4 inf + 1 1552123215.580 * * [simplify]: Extracting #4: cost 0 inf + 127 1552123215.580 * [simplify]: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1552123215.580 * [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))))))) 1552123215.580 * * * * [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)))))))> 1552123215.580 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1552123215.580 * * [simplify]: iters left: 5 (7 enodes) 1552123215.582 * * [simplify]: iters left: 4 (16 enodes) 1552123215.584 * * [simplify]: iters left: 3 (20 enodes) 1552123215.587 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123215.588 * * [simplify]: Extracting #1: cost 6 inf + 0 1552123215.588 * * [simplify]: Extracting #2: cost 8 inf + 0 1552123215.588 * * [simplify]: Extracting #3: cost 8 inf + 1 1552123215.588 * * [simplify]: Extracting #4: cost 5 inf + 324 1552123215.588 * * [simplify]: Extracting #5: cost 0 inf + 2334 1552123215.588 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1552123215.588 * [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))))))) 1552123215.588 * * * * [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)))))))> 1552123215.588 * * * * [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)))))))> 1552123215.588 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552123215.588 * * [simplify]: iters left: 3 (6 enodes) 1552123215.590 * * [simplify]: iters left: 2 (14 enodes) 1552123215.592 * * [simplify]: iters left: 1 (18 enodes) 1552123215.596 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123215.596 * * [simplify]: Extracting #1: cost 6 inf + 0 1552123215.596 * * [simplify]: Extracting #2: cost 8 inf + 0 1552123215.596 * * [simplify]: Extracting #3: cost 5 inf + 43 1552123215.597 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552123215.597 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552123215.597 * [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))))))) 1552123215.597 * * * * [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)))))))> 1552123215.597 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552123215.597 * * [simplify]: iters left: 3 (6 enodes) 1552123215.600 * * [simplify]: iters left: 2 (14 enodes) 1552123215.605 * * [simplify]: iters left: 1 (18 enodes) 1552123215.610 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123215.611 * * [simplify]: Extracting #1: cost 6 inf + 0 1552123215.611 * * [simplify]: Extracting #2: cost 8 inf + 0 1552123215.611 * * [simplify]: Extracting #3: cost 5 inf + 43 1552123215.611 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552123215.611 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552123215.611 * [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))))))) 1552123215.611 * * * * [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)))))))> 1552123215.612 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552123215.612 * * [simplify]: iters left: 3 (6 enodes) 1552123215.615 * * [simplify]: iters left: 2 (14 enodes) 1552123215.623 * * [simplify]: iters left: 1 (18 enodes) 1552123215.630 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123215.630 * * [simplify]: Extracting #1: cost 6 inf + 0 1552123215.630 * * [simplify]: Extracting #2: cost 8 inf + 0 1552123215.630 * * [simplify]: Extracting #3: cost 5 inf + 43 1552123215.630 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552123215.631 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552123215.631 * [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))))))) 1552123215.631 * * * * [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)))))))> 1552123215.631 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1552123215.631 * * [simplify]: iters left: 3 (6 enodes) 1552123215.635 * * [simplify]: iters left: 2 (14 enodes) 1552123215.640 * * [simplify]: iters left: 1 (18 enodes) 1552123215.645 * * [simplify]: Extracting #0: cost 1 inf + 0 1552123215.645 * * [simplify]: Extracting #1: cost 6 inf + 0 1552123215.645 * * [simplify]: Extracting #2: cost 8 inf + 0 1552123215.645 * * [simplify]: Extracting #3: cost 5 inf + 43 1552123215.646 * * [simplify]: Extracting #4: cost 0 inf + 2131 1552123215.646 * [simplify]: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1552123215.646 * [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))))))) 1552123215.646 * * * [progress]: adding candidates to table 1552123216.181 * [progress]: [Phase 3 of 3] Extracting. 1552123216.181 * * [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 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 (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 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 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 (+.p16 x (real->posit16 1))))))> #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)))))))> #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 (+.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))))))))>) 1552123216.184 * * * [regime-changes]: Trying 1 branch expressions: (x) 1552123216.184 * * * * [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 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 (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 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 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 (+.p16 x (real->posit16 1))))))> #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)))))))> #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 (+.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))))))))>) 1552123216.553 * * * [regime]: Found split indices: #