1550699644.551 * [misc]progress: [Phase 1 of 3] Setting up. 1550699644.551 * * * [misc]progress: [1/2] Preparing points 1550699644.551 * * * * [misc]points: Sampling 256 additional inputs, on iter 0 have 0 / 256 1550699644.551 * * * * [misc]points: Computing exacts on every 16 of 256 points to ramp up precision 1550699644.554 * * * * [misc]points: Setting MPFR precision to 64 1550699644.556 * * * * [misc]points: Setting MPFR precision to 320 1550699644.557 * * * * [misc]points: Computing exacts on every 8 of 256 points to ramp up precision 1550699644.561 * * * * [misc]points: Setting MPFR precision to 64 1550699644.563 * * * * [misc]points: Setting MPFR precision to 320 1550699644.567 * * * * [misc]points: Computing exacts on every 4 of 256 points to ramp up precision 1550699644.570 * * * * [misc]points: Setting MPFR precision to 64 1550699644.574 * * * * [misc]points: Setting MPFR precision to 320 1550699644.580 * * * * [misc]points: Computing exacts on every 2 of 256 points to ramp up precision 1550699644.584 * * * * [misc]points: Setting MPFR precision to 64 1550699644.592 * * * * [misc]points: Setting MPFR precision to 320 1550699644.602 * * * * [misc]points: Computing exacts for 256 points 1550699644.605 * * * * [misc]points: Setting MPFR precision to 64 1550699644.627 * * * * [misc]points: Setting MPFR precision to 320 1550699644.658 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.672 * * * * [misc]points: Sampling 123 additional inputs, on iter 1 have 133 / 256 1550699644.673 * * * * [misc]points: Computing exacts on every 7 of 123 points to ramp up precision 1550699644.675 * * * * [misc]points: Setting MPFR precision to 64 1550699644.676 * * * * [misc]points: Setting MPFR precision to 320 1550699644.678 * * * * [misc]points: Computing exacts on every 3 of 123 points to ramp up precision 1550699644.682 * * * * [misc]points: Setting MPFR precision to 64 1550699644.685 * * * * [misc]points: Setting MPFR precision to 320 1550699644.689 * * * * [misc]points: Computing exacts for 123 points 1550699644.692 * * * * [misc]points: Setting MPFR precision to 64 1550699644.703 * * * * [misc]points: Setting MPFR precision to 320 1550699644.718 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.725 * * * * [misc]points: Sampling 61 additional inputs, on iter 2 have 195 / 256 1550699644.725 * * * * [misc]points: Computing exacts on every 3 of 61 points to ramp up precision 1550699644.728 * * * * [misc]points: Setting MPFR precision to 64 1550699644.730 * * * * [misc]points: Setting MPFR precision to 320 1550699644.732 * * * * [misc]points: Computing exacts for 61 points 1550699644.735 * * * * [misc]points: Setting MPFR precision to 64 1550699644.741 * * * * [misc]points: Setting MPFR precision to 320 1550699644.748 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.750 * * * * [misc]points: Sampling 34 additional inputs, on iter 3 have 222 / 256 1550699644.750 * * * * [misc]points: Computing exacts on every 2 of 34 points to ramp up precision 1550699644.753 * * * * [misc]points: Setting MPFR precision to 64 1550699644.786 * * * * [misc]points: Setting MPFR precision to 320 1550699644.787 * * * * [misc]points: Computing exacts for 34 points 1550699644.791 * * * * [misc]points: Setting MPFR precision to 64 1550699644.794 * * * * [misc]points: Setting MPFR precision to 320 1550699644.801 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.803 * * * * [misc]points: Sampling 19 additional inputs, on iter 4 have 237 / 256 1550699644.803 * * * * [misc]points: Computing exacts for 19 points 1550699644.806 * * * * [misc]points: Setting MPFR precision to 64 1550699644.808 * * * * [misc]points: Setting MPFR precision to 320 1550699644.811 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.812 * * * * [misc]points: Sampling 13 additional inputs, on iter 5 have 243 / 256 1550699644.812 * * * * [misc]points: Computing exacts for 13 points 1550699644.815 * * * * [misc]points: Setting MPFR precision to 64 1550699644.817 * * * * [misc]points: Setting MPFR precision to 320 1550699644.818 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.819 * * * * [misc]points: Sampling 6 additional inputs, on iter 6 have 250 / 256 1550699644.819 * * * * [misc]points: Computing exacts for 6 points 1550699644.823 * * * * [misc]points: Setting MPFR precision to 64 1550699644.823 * * * * [misc]points: Setting MPFR precision to 320 1550699644.824 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.825 * * * * [misc]points: Sampling 4 additional inputs, on iter 7 have 254 / 256 1550699644.825 * * * * [misc]points: Computing exacts for 4 points 1550699644.828 * * * * [misc]points: Setting MPFR precision to 64 1550699644.829 * * * * [misc]points: Setting MPFR precision to 320 1550699644.829 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.830 * * * * [misc]points: Sampling 4 additional inputs, on iter 8 have 255 / 256 1550699644.830 * * * * [misc]points: Computing exacts for 4 points 1550699644.833 * * * * [misc]points: Setting MPFR precision to 64 1550699644.834 * * * * [misc]points: Setting MPFR precision to 320 1550699644.834 * * * * [misc]points: Filtering points with unrepresentable outputs 1550699644.834 * * * * [exit]points: Sampled 256 points with exact outputs 1550699644.835 * * * [misc]progress: [2/2] Setting up program. 1550699644.869 * [misc]progress: [Phase 2 of 3] Improving. 1550699644.869 * * * * [misc]progress: [ 1 / 1 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550699644.869 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699644.870 * * [misc]simplify: iters left: 5 (9 enodes) 1550699644.874 * * [misc]simplify: iters left: 4 (22 enodes) 1550699644.879 * * [misc]simplify: iters left: 3 (42 enodes) 1550699644.887 * * [misc]simplify: iters left: 2 (100 enodes) 1550699644.909 * * [misc]simplify: iters left: 1 (347 enodes) 1550699645.181 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699645.181 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699645.184 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699645.187 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699645.203 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699645.257 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699645.342 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699645.456 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699645.555 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699645.661 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699645.753 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699645.753 * [misc]simplify: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1550699645.776 * * [misc]progress: iteration 1 / 4 1550699645.776 * * * [misc]progress: picking best candidate 1550699645.797 * * * * [misc]pick: Picked #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550699645.797 * * * [misc]progress: localizing error 1550699646.198 * * * [misc]progress: generating rewritten candidates 1550699646.198 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2) 1550699646.203 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 2) 1550699646.206 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 1) 1550699646.208 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 2 2) 1550699646.208 * * * [misc]progress: generating series expansions 1550699646.208 * * * * [misc]progress: [ 1 / 4 ] generating series at (2) 1550699646.208 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 2) 1550699646.209 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 1) 1550699646.209 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 2 2) 1550699646.209 * * * [misc]progress: simplifying candidates 1550699646.209 * * * * [misc]progress: [ 1 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (neg.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1550699646.209 * * * * [misc]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)))))))> 1550699646.209 * * * * [misc]progress: [ 3 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550699646.209 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699646.209 * * [misc]simplify: iters left: 5 (9 enodes) 1550699646.214 * * [misc]simplify: iters left: 4 (22 enodes) 1550699646.222 * * [misc]simplify: iters left: 3 (42 enodes) 1550699646.238 * * [misc]simplify: iters left: 2 (100 enodes) 1550699646.284 * * [misc]simplify: iters left: 1 (347 enodes) 1550699646.510 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699646.510 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699646.511 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699646.514 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699646.533 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699646.623 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699646.755 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699646.872 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699646.992 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699647.112 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699647.210 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699647.210 * [misc]simplify: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1550699647.210 * * * * [misc]progress: [ 4 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550699647.210 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699647.211 * * [misc]simplify: iters left: 5 (9 enodes) 1550699647.213 * * [misc]simplify: iters left: 4 (22 enodes) 1550699647.218 * * [misc]simplify: iters left: 3 (42 enodes) 1550699647.226 * * [misc]simplify: iters left: 2 (100 enodes) 1550699647.255 * * [misc]simplify: iters left: 1 (347 enodes) 1550699647.521 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699647.522 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699647.523 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699647.526 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699647.544 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699647.636 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699647.759 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699647.880 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699647.994 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699648.109 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699648.222 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699648.222 * [misc]simplify: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1550699648.222 * * * * [misc]progress: [ 5 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550699648.223 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699648.223 * * [misc]simplify: iters left: 5 (9 enodes) 1550699648.227 * * [misc]simplify: iters left: 4 (22 enodes) 1550699648.235 * * [misc]simplify: iters left: 3 (42 enodes) 1550699648.250 * * [misc]simplify: iters left: 2 (100 enodes) 1550699648.293 * * [misc]simplify: iters left: 1 (347 enodes) 1550699648.585 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699648.585 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699648.586 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699648.589 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699648.602 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699648.674 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699648.774 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699648.898 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699649.019 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699649.142 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699649.211 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699649.211 * [misc]simplify: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1550699649.212 * * * * [misc]progress: [ 6 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550699649.212 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699649.212 * * [misc]simplify: iters left: 5 (9 enodes) 1550699649.214 * * [misc]simplify: iters left: 4 (22 enodes) 1550699649.220 * * [misc]simplify: iters left: 3 (42 enodes) 1550699649.228 * * [misc]simplify: iters left: 2 (100 enodes) 1550699649.250 * * [misc]simplify: iters left: 1 (347 enodes) 1550699649.415 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699649.415 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699649.416 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699649.418 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699649.432 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699649.477 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699649.547 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699649.630 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699649.755 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699649.874 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699649.998 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699649.998 * [misc]simplify: Simplified (2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))))) 1550699649.998 * * * [misc]progress: adding candidates to table 1550699650.339 * * [misc]progress: iteration 2 / 4 1550699650.339 * * * [misc]progress: picking best candidate 1550699650.378 * * * * [misc]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)))))))> 1550699650.378 * * * [misc]progress: localizing error 1550699650.696 * * * [misc]progress: generating rewritten candidates 1550699650.697 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1550699650.699 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2) 1550699650.706 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 1 2) 1550699650.708 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 1) 1550699650.710 * * * [misc]progress: generating series expansions 1550699650.710 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1550699650.711 * * * * [misc]progress: [ 2 / 4 ] generating series at (2) 1550699650.711 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 1 2) 1550699650.711 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 1) 1550699650.711 * * * [misc]progress: simplifying candidates 1550699650.711 * * * * [misc]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)))))))> 1550699650.711 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699650.711 * * [misc]simplify: iters left: 5 (9 enodes) 1550699650.713 * * [misc]simplify: iters left: 4 (16 enodes) 1550699650.716 * * [misc]simplify: iters left: 3 (18 enodes) 1550699650.719 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699650.719 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699650.719 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550699650.719 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550699650.719 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550699650.719 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550699650.720 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699650.720 * [misc]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))))))) 1550699650.720 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699650.720 * * [misc]simplify: iters left: 5 (9 enodes) 1550699650.722 * * [misc]simplify: iters left: 4 (22 enodes) 1550699650.736 * * [misc]simplify: iters left: 3 (42 enodes) 1550699650.747 * * [misc]simplify: iters left: 2 (100 enodes) 1550699650.784 * * [misc]simplify: iters left: 1 (347 enodes) 1550699651.043 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699651.043 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699651.045 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699651.048 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699651.072 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699651.125 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699651.241 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699651.343 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699651.457 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699651.578 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699651.702 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699651.702 * [misc]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))))))) 1550699651.702 * * * * [misc]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)))))))> 1550699651.703 * * * * [misc]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)))))))> 1550699651.703 * * * * [misc]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))))))))> 1550699651.703 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699651.703 * * [misc]simplify: iters left: 5 (9 enodes) 1550699651.707 * * [misc]simplify: iters left: 4 (16 enodes) 1550699651.713 * * [misc]simplify: iters left: 3 (18 enodes) 1550699651.720 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699651.720 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699651.720 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550699651.720 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550699651.720 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550699651.720 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550699651.721 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699651.721 * [misc]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)))))))) 1550699651.721 * * * * [misc]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)))))))))> 1550699651.721 * [enter]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))))))) 1550699651.721 * * [misc]simplify: iters left: 6 (13 enodes) 1550699651.728 * * [misc]simplify: iters left: 5 (45 enodes) 1550699651.747 * * [misc]simplify: iters left: 4 (144 enodes) 1550699651.810 * * [misc]simplify: iters left: 3 (446 enodes) 1550699652.256 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699652.256 * * [misc]simplify: Extracting #1: cost 41 inf + 0 1550699652.257 * * [misc]simplify: Extracting #2: cost 283 inf + 0 1550699652.260 * * [misc]simplify: Extracting #3: cost 446 inf + 44 1550699652.282 * * [misc]simplify: Extracting #4: cost 488 inf + 246749 1550699652.410 * * [misc]simplify: Extracting #5: cost 101 inf + 1165723 1550699652.580 * * [misc]simplify: Extracting #6: cost 2 inf + 1463482 1550699652.749 * * [misc]simplify: Extracting #7: cost 0 inf + 1419126 1550699652.889 * * [misc]simplify: Extracting #8: cost 0 inf + 1414206 1550699653.056 * [exit]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)))) 1550699653.056 * [misc]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))))))))) 1550699653.056 * * * * [misc]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)))))))> 1550699653.057 * [enter]simplify: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1550699653.057 * * [misc]simplify: iters left: 3 (5 enodes) 1550699653.060 * * [misc]simplify: iters left: 2 (11 enodes) 1550699653.063 * * [misc]simplify: iters left: 1 (13 enodes) 1550699653.068 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699653.068 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550699653.068 * * [misc]simplify: Extracting #2: cost 4 inf + 0 1550699653.068 * * [misc]simplify: Extracting #3: cost 4 inf + 1 1550699653.068 * * [misc]simplify: Extracting #4: cost 0 inf + 127 1550699653.068 * [exit]simplify: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1550699653.068 * [misc]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))))))) 1550699653.068 * * * * [misc]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)))))))> 1550699653.069 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699653.069 * * [misc]simplify: iters left: 5 (7 enodes) 1550699653.072 * * [misc]simplify: iters left: 4 (16 enodes) 1550699653.078 * * [misc]simplify: iters left: 3 (20 enodes) 1550699653.084 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699653.084 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550699653.084 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550699653.084 * * [misc]simplify: Extracting #3: cost 8 inf + 1 1550699653.084 * * [misc]simplify: Extracting #4: cost 5 inf + 324 1550699653.085 * * [misc]simplify: Extracting #5: cost 0 inf + 2334 1550699653.085 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1550699653.085 * [misc]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))))))) 1550699653.085 * * * * [misc]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)))))))> 1550699653.085 * * * * [misc]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)))))))> 1550699653.085 * [enter]simplify: Simplifying (sqrt.p16 x) 1550699653.085 * * [misc]simplify: iters left: 1 (2 enodes) 1550699653.086 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699653.086 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550699653.086 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550699653.086 * * [misc]simplify: Extracting #3: cost 0 inf + 42 1550699653.086 * [exit]simplify: Simplified to (sqrt.p16 x) 1550699653.086 * [misc]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))))))) 1550699653.087 * * * * [misc]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)))))))> 1550699653.087 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1550699653.087 * * [misc]simplify: iters left: 3 (6 enodes) 1550699653.090 * * [misc]simplify: iters left: 2 (14 enodes) 1550699653.095 * * [misc]simplify: iters left: 1 (18 enodes) 1550699653.102 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699653.102 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550699653.102 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550699653.102 * * [misc]simplify: Extracting #3: cost 5 inf + 43 1550699653.102 * * [misc]simplify: Extracting #4: cost 0 inf + 2131 1550699653.103 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1550699653.103 * [misc]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))))))) 1550699653.103 * * * * [misc]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)))))))> 1550699653.103 * * * * [misc]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)))))))> 1550699653.103 * * * * [misc]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)))))))> 1550699653.103 * * * * [misc]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)))))))> 1550699653.103 * * * * [misc]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)))))))> 1550699653.103 * * * [misc]progress: adding candidates to table 1550699654.312 * * [misc]progress: iteration 3 / 4 1550699654.312 * * * [misc]progress: picking best candidate 1550699654.571 * * * * [misc]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)))))))> 1550699654.571 * * * [misc]progress: localizing error 1550699654.720 * * * [misc]progress: generating rewritten candidates 1550699654.720 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1 2) 1550699654.727 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2) 1550699654.743 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 2 2) 1550699654.745 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 2 2) 1550699654.748 * * * [misc]progress: generating series expansions 1550699654.748 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1 2) 1550699654.748 * * * * [misc]progress: [ 2 / 4 ] generating series at (2) 1550699654.748 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 2 2) 1550699654.748 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 2 2) 1550699654.748 * * * [misc]progress: simplifying candidates 1550699654.748 * * * * [misc]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)))))))> 1550699654.748 * * * * [misc]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)))))))> 1550699654.748 * * * * [misc]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))))))))> 1550699654.748 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699654.749 * * [misc]simplify: iters left: 5 (9 enodes) 1550699654.753 * * [misc]simplify: iters left: 4 (16 enodes) 1550699654.759 * * [misc]simplify: iters left: 3 (18 enodes) 1550699654.764 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699654.764 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699654.764 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550699654.765 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550699654.765 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550699654.765 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550699654.765 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699654.765 * [misc]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)))))))) 1550699654.765 * * * * [misc]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))))))))> 1550699654.766 * [enter]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))))))) 1550699654.766 * * [misc]simplify: iters left: 6 (13 enodes) 1550699654.772 * * [misc]simplify: iters left: 5 (38 enodes) 1550699654.788 * * [misc]simplify: iters left: 4 (106 enodes) 1550699655.337 * * [misc]simplify: iters left: 3 (376 enodes) 1550699655.686 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699655.687 * * [misc]simplify: Extracting #1: cost 52 inf + 0 1550699655.688 * * [misc]simplify: Extracting #2: cost 302 inf + 0 1550699655.692 * * [misc]simplify: Extracting #3: cost 417 inf + 43 1550699655.720 * * [misc]simplify: Extracting #4: cost 351 inf + 302562 1550699655.810 * * [misc]simplify: Extracting #5: cost 35 inf + 1004993 1550699655.886 * * [misc]simplify: Extracting #6: cost 0 inf + 1083663 1550699655.942 * * [misc]simplify: Extracting #7: cost 0 inf + 1082583 1550699655.997 * [exit]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)))))) 1550699655.997 * [misc]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)))))))) 1550699655.998 * * * * [misc]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)))))))> 1550699655.998 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699655.998 * * [misc]simplify: iters left: 5 (9 enodes) 1550699656.000 * * [misc]simplify: iters left: 4 (16 enodes) 1550699656.003 * * [misc]simplify: iters left: 3 (18 enodes) 1550699656.011 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699656.011 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699656.011 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550699656.011 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550699656.011 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550699656.011 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550699656.011 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699656.011 * [misc]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))))))) 1550699656.012 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699656.012 * * [misc]simplify: iters left: 5 (9 enodes) 1550699656.016 * * [misc]simplify: iters left: 4 (22 enodes) 1550699656.024 * * [misc]simplify: iters left: 3 (42 enodes) 1550699656.038 * * [misc]simplify: iters left: 2 (100 enodes) 1550699656.082 * * [misc]simplify: iters left: 1 (347 enodes) 1550699656.369 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699656.369 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699656.370 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699656.379 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699656.398 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699656.488 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699656.616 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699656.739 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699656.863 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699656.986 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699657.095 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699657.095 * [misc]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))))))) 1550699657.095 * * * * [misc]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)))))))> 1550699657.095 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699657.096 * * [misc]simplify: iters left: 5 (9 enodes) 1550699657.098 * * [misc]simplify: iters left: 4 (16 enodes) 1550699657.101 * * [misc]simplify: iters left: 3 (18 enodes) 1550699657.104 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699657.104 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699657.104 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550699657.104 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550699657.104 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550699657.104 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550699657.104 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699657.104 * [misc]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))))))) 1550699657.104 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699657.104 * * [misc]simplify: iters left: 5 (9 enodes) 1550699657.107 * * [misc]simplify: iters left: 4 (22 enodes) 1550699657.111 * * [misc]simplify: iters left: 3 (42 enodes) 1550699657.119 * * [misc]simplify: iters left: 2 (100 enodes) 1550699657.142 * * [misc]simplify: iters left: 1 (347 enodes) 1550699657.346 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699657.347 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699657.347 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699657.349 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699657.358 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699657.407 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699657.479 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699657.549 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699657.640 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699657.742 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699657.852 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699657.852 * [misc]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))))))) 1550699657.852 * * * * [misc]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)))))))> 1550699657.852 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699657.852 * * [misc]simplify: iters left: 5 (9 enodes) 1550699657.855 * * [misc]simplify: iters left: 4 (16 enodes) 1550699657.857 * * [misc]simplify: iters left: 3 (18 enodes) 1550699657.860 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699657.861 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699657.861 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550699657.861 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550699657.861 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550699657.861 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550699657.861 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699657.861 * [misc]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))))))) 1550699657.861 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699657.861 * * [misc]simplify: iters left: 5 (9 enodes) 1550699657.863 * * [misc]simplify: iters left: 4 (22 enodes) 1550699657.868 * * [misc]simplify: iters left: 3 (42 enodes) 1550699657.879 * * [misc]simplify: iters left: 2 (100 enodes) 1550699657.918 * * [misc]simplify: iters left: 1 (347 enodes) 1550699658.110 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699658.110 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699658.111 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699658.113 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699658.132 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699658.201 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699658.283 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699658.400 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699658.507 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699658.586 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699658.674 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699658.674 * [misc]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))))))) 1550699658.675 * * * * [misc]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)))))))> 1550699658.675 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699658.675 * * [misc]simplify: iters left: 5 (9 enodes) 1550699658.679 * * [misc]simplify: iters left: 4 (16 enodes) 1550699658.685 * * [misc]simplify: iters left: 3 (18 enodes) 1550699658.691 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699658.691 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550699658.691 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550699658.691 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550699658.691 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550699658.691 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550699658.691 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699658.691 * [misc]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))))))) 1550699658.692 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699658.692 * * [misc]simplify: iters left: 5 (9 enodes) 1550699658.696 * * [misc]simplify: iters left: 4 (22 enodes) 1550699658.706 * * [misc]simplify: iters left: 3 (42 enodes) 1550699658.722 * * [misc]simplify: iters left: 2 (100 enodes) 1550699658.768 * * [misc]simplify: iters left: 1 (347 enodes) 1550699658.985 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699658.985 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550699658.986 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550699658.987 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550699659.002 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550699659.067 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550699659.162 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550699659.238 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550699659.325 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550699659.437 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550699659.552 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550699659.552 * [misc]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))))))) 1550699659.553 * * * [misc]progress: adding candidates to table 1550699659.920 * * [misc]progress: iteration 4 / 4 1550699659.920 * * * [misc]progress: picking best candidate 1550699660.151 * * * * [misc]pick: Picked #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)))))))> 1550699660.151 * * * [misc]progress: localizing error 1550699660.406 * * * [misc]progress: generating rewritten candidates 1550699660.406 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1550699660.413 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2) 1550699660.440 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 1 2) 1550699660.444 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 2 2) 1550699660.446 * * * [misc]progress: generating series expansions 1550699660.446 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1550699660.446 * * * * [misc]progress: [ 2 / 4 ] generating series at (2) 1550699660.447 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 1 2) 1550699660.447 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 2 2) 1550699660.447 * * * [misc]progress: simplifying candidates 1550699660.447 * * * * [misc]progress: [ 1 / 10 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (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)))))))> 1550699660.447 * * * * [misc]progress: [ 2 / 10 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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 (/.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)))))))> 1550699660.447 * * * * [misc]progress: [ 3 / 10 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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 (/.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)))))))))> 1550699660.447 * [enter]simplify: Simplifying (-.p16 (*.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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))))))) 1550699660.447 * * [misc]simplify: iters left: 6 (14 enodes) 1550699660.455 * * [misc]simplify: iters left: 5 (47 enodes) 1550699660.476 * * [misc]simplify: iters left: 4 (139 enodes) 1550699660.550 * * [misc]simplify: iters left: 3 (499 enodes) 1550699661.129 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699661.129 * * [misc]simplify: Extracting #1: cost 32 inf + 0 1550699661.130 * * [misc]simplify: Extracting #2: cost 244 inf + 0 1550699661.131 * * [misc]simplify: Extracting #3: cost 413 inf + 43 1550699661.153 * * [misc]simplify: Extracting #4: cost 536 inf + 218044 1550699661.244 * * [misc]simplify: Extracting #5: cost 71 inf + 1328814 1550699661.372 * * [misc]simplify: Extracting #6: cost 1 inf + 1496994 1550699661.464 * * [misc]simplify: Extracting #7: cost 0 inf + 1458716 1550699661.613 * * [misc]simplify: Extracting #8: cost 0 inf + 1455516 1550699661.712 * [exit]simplify: Simplified to (*.p16 (*.p16 (real->posit16 1) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) x))) (*.p16 (real->posit16 1) (-.p16 (/.p16 (real->posit16 1) x) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))))) 1550699661.712 * [misc]simplify: Simplified (2 1) to (λ (x) (/.p16 (*.p16 (*.p16 (real->posit16 1) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) x))) (*.p16 (real->posit16 1) (-.p16 (/.p16 (real->posit16 1) x) (/.p16 (real->posit16 1) (+.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 (/.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))))))))) 1550699661.712 * * * * [misc]progress: [ 4 / 10 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (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)))))))> 1550699661.712 * [enter]simplify: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1550699661.712 * * [misc]simplify: iters left: 3 (5 enodes) 1550699661.714 * * [misc]simplify: iters left: 2 (11 enodes) 1550699661.716 * * [misc]simplify: iters left: 1 (13 enodes) 1550699661.718 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699661.718 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550699661.719 * * [misc]simplify: Extracting #2: cost 4 inf + 0 1550699661.719 * * [misc]simplify: Extracting #3: cost 4 inf + 1 1550699661.719 * * [misc]simplify: Extracting #4: cost 0 inf + 127 1550699661.719 * [exit]simplify: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1550699661.719 * [misc]simplify: Simplified (2 1 2 2) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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))))))) 1550699661.719 * * * * [misc]progress: [ 5 / 10 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (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)))))))> 1550699661.719 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550699661.719 * * [misc]simplify: iters left: 5 (7 enodes) 1550699661.721 * * [misc]simplify: iters left: 4 (16 enodes) 1550699661.724 * * [misc]simplify: iters left: 3 (20 enodes) 1550699661.727 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699661.727 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550699661.727 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550699661.727 * * [misc]simplify: Extracting #3: cost 8 inf + 1 1550699661.727 * * [misc]simplify: Extracting #4: cost 5 inf + 324 1550699661.728 * * [misc]simplify: Extracting #5: cost 0 inf + 2334 1550699661.728 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1550699661.728 * [misc]simplify: Simplified (2 1 2 1) to (λ (x) (/.p16 (-.p16 (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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))))))) 1550699661.728 * * * * [misc]progress: [ 6 / 10 ] 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)))))))> 1550699661.728 * * * * [misc]progress: [ 7 / 10 ] 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)))))))> 1550699661.728 * [enter]simplify: Simplifying (sqrt.p16 x) 1550699661.728 * * [misc]simplify: iters left: 1 (2 enodes) 1550699661.729 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699661.729 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550699661.729 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550699661.729 * * [misc]simplify: Extracting #3: cost 0 inf + 42 1550699661.729 * [exit]simplify: Simplified to (sqrt.p16 x) 1550699661.729 * [misc]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))))))) 1550699661.729 * * * * [misc]progress: [ 8 / 10 ] 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)))))))> 1550699661.729 * [enter]simplify: Simplifying (sqrt.p16 x) 1550699661.729 * * [misc]simplify: iters left: 1 (2 enodes) 1550699661.729 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699661.729 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550699661.729 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550699661.730 * * [misc]simplify: Extracting #3: cost 0 inf + 42 1550699661.730 * [exit]simplify: Simplified to (sqrt.p16 x) 1550699661.730 * [misc]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))))))) 1550699661.730 * * * * [misc]progress: [ 9 / 10 ] 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)))))))> 1550699661.730 * [enter]simplify: Simplifying (sqrt.p16 x) 1550699661.730 * * [misc]simplify: iters left: 1 (2 enodes) 1550699661.730 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699661.730 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550699661.730 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550699661.730 * * [misc]simplify: Extracting #3: cost 0 inf + 42 1550699661.730 * [exit]simplify: Simplified to (sqrt.p16 x) 1550699661.730 * [misc]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))))))) 1550699661.731 * * * * [misc]progress: [ 10 / 10 ] 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)))))))> 1550699661.731 * [enter]simplify: Simplifying (sqrt.p16 x) 1550699661.731 * * [misc]simplify: iters left: 1 (2 enodes) 1550699661.731 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550699661.731 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550699661.731 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550699661.731 * * [misc]simplify: Extracting #3: cost 0 inf + 42 1550699661.731 * [exit]simplify: Simplified to (sqrt.p16 x) 1550699661.731 * [misc]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))))))) 1550699661.731 * * * [misc]progress: adding candidates to table 1550699662.485 * [misc]progress: [Phase 3 of 3] Extracting. 1550699662.485 * * [misc]regime: Finding splitpoints for: (#posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> #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)) (real->posit16 1)) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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 (/.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)))))))> #posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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 (/.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)))))))))> #posit16 1) (sqrt.p16 x)) (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)))))))>) 1550699662.490 * * * [misc]regime-changes: Trying 1 branch expressions: (x) 1550699662.490 * * * * [misc]regimes: Trying to branch on x from (#posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (*.p16 (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 x))) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> #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)) (real->posit16 1)) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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 (/.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)))))))> #posit16 1) (sqrt.p16 x)) (real->posit16 1)) (sqrt.p16 x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (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 (/.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)))))))))> #posit16 1) (sqrt.p16 x)) (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)))))))>) 1550699663.092 * * * [misc]regime: Found split indices: #