1550842950.338 * [misc]progress: [Phase 1 of 3] Setting up. 1550842950.338 * * * [misc]progress: [1/2] Preparing points 1550842950.338 * * * * [misc]points: Sampling 256 additional inputs, on iter 0 have 0 / 256 1550842950.339 * * * * [misc]points: Computing exacts on every 16 of 256 points to ramp up precision 1550842950.341 * * * * [misc]points: Setting MPFR precision to 64 1550842950.343 * * * * [misc]points: Setting MPFR precision to 320 1550842950.345 * * * * [misc]points: Computing exacts on every 8 of 256 points to ramp up precision 1550842950.348 * * * * [misc]points: Setting MPFR precision to 64 1550842950.350 * * * * [misc]points: Setting MPFR precision to 320 1550842950.353 * * * * [misc]points: Computing exacts on every 4 of 256 points to ramp up precision 1550842950.356 * * * * [misc]points: Setting MPFR precision to 64 1550842950.360 * * * * [misc]points: Setting MPFR precision to 320 1550842950.366 * * * * [misc]points: Computing exacts on every 2 of 256 points to ramp up precision 1550842950.368 * * * * [misc]points: Setting MPFR precision to 64 1550842950.375 * * * * [misc]points: Setting MPFR precision to 320 1550842950.386 * * * * [misc]points: Computing exacts for 256 points 1550842950.389 * * * * [misc]points: Setting MPFR precision to 64 1550842950.411 * * * * [misc]points: Setting MPFR precision to 320 1550842950.441 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842950.454 * * * * [misc]points: Sampling 141 additional inputs, on iter 1 have 115 / 256 1550842950.454 * * * * [misc]points: Computing exacts on every 8 of 141 points to ramp up precision 1550842950.458 * * * * [misc]points: Setting MPFR precision to 64 1550842950.459 * * * * [misc]points: Setting MPFR precision to 320 1550842950.461 * * * * [misc]points: Computing exacts on every 4 of 141 points to ramp up precision 1550842950.464 * * * * [misc]points: Setting MPFR precision to 64 1550842950.466 * * * * [misc]points: Setting MPFR precision to 320 1550842950.470 * * * * [misc]points: Computing exacts on every 2 of 141 points to ramp up precision 1550842950.474 * * * * [misc]points: Setting MPFR precision to 64 1550842950.478 * * * * [misc]points: Setting MPFR precision to 320 1550842950.482 * * * * [misc]points: Computing exacts for 141 points 1550842950.497 * * * * [misc]points: Setting MPFR precision to 64 1550842950.504 * * * * [misc]points: Setting MPFR precision to 320 1550842950.513 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842950.517 * * * * [misc]points: Sampling 63 additional inputs, on iter 2 have 193 / 256 1550842950.517 * * * * [misc]points: Computing exacts on every 3 of 63 points to ramp up precision 1550842950.519 * * * * [misc]points: Setting MPFR precision to 64 1550842950.520 * * * * [misc]points: Setting MPFR precision to 320 1550842950.521 * * * * [misc]points: Computing exacts for 63 points 1550842950.522 * * * * [misc]points: Setting MPFR precision to 64 1550842950.526 * * * * [misc]points: Setting MPFR precision to 320 1550842950.530 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842950.532 * * * * [misc]points: Sampling 27 additional inputs, on iter 3 have 229 / 256 1550842950.532 * * * * [misc]points: Computing exacts for 27 points 1550842950.533 * * * * [misc]points: Setting MPFR precision to 64 1550842950.535 * * * * [misc]points: Setting MPFR precision to 320 1550842950.537 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842950.537 * * * * [misc]points: Sampling 13 additional inputs, on iter 4 have 243 / 256 1550842950.537 * * * * [misc]points: Computing exacts for 13 points 1550842950.539 * * * * [misc]points: Setting MPFR precision to 64 1550842950.540 * * * * [misc]points: Setting MPFR precision to 320 1550842950.541 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842950.541 * * * * [misc]points: Sampling 4 additional inputs, on iter 5 have 253 / 256 1550842950.541 * * * * [misc]points: Computing exacts for 4 points 1550842950.543 * * * * [misc]points: Setting MPFR precision to 64 1550842950.543 * * * * [misc]points: Setting MPFR precision to 320 1550842950.543 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842950.543 * * * * [misc]points: Sampling 4 additional inputs, on iter 6 have 254 / 256 1550842950.543 * * * * [misc]points: Computing exacts for 4 points 1550842950.545 * * * * [misc]points: Setting MPFR precision to 64 1550842950.545 * * * * [misc]points: Setting MPFR precision to 320 1550842950.546 * * * * [misc]points: Filtering points with unrepresentable outputs 1550842950.546 * * * * [exit]points: Sampled 257 points with exact outputs 1550842950.546 * * * [misc]progress: [2/2] Setting up program. 1550842950.564 * [misc]progress: [Phase 2 of 3] Improving. 1550842950.564 * * * * [misc]progress: [ 1 / 1 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550842950.564 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842950.564 * * [misc]simplify: iters left: 5 (9 enodes) 1550842950.567 * * [misc]simplify: iters left: 4 (22 enodes) 1550842950.571 * * [misc]simplify: iters left: 3 (42 enodes) 1550842950.578 * * [misc]simplify: iters left: 2 (100 enodes) 1550842950.615 * * [misc]simplify: iters left: 1 (347 enodes) 1550842950.774 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842950.774 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842950.775 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842950.776 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842950.785 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842950.834 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842950.899 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842951.017 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842951.138 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842951.203 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842951.265 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842951.265 * [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))))) 1550842951.285 * * [misc]progress: iteration 1 / 4 1550842951.285 * * * [misc]progress: picking best candidate 1550842951.306 * * * * [misc]pick: Picked #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550842951.307 * * * [misc]progress: localizing error 1550842951.520 * * * [misc]progress: generating rewritten candidates 1550842951.521 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2) 1550842951.524 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2 2) 1550842951.525 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 1) 1550842951.526 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 2 2) 1550842951.526 * * * [misc]progress: generating series expansions 1550842951.526 * * * * [misc]progress: [ 1 / 4 ] generating series at (2) 1550842951.526 * * * * [misc]progress: [ 2 / 4 ] generating series at (2 2) 1550842951.526 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 1) 1550842951.526 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 2 2) 1550842951.526 * * * [misc]progress: simplifying candidates 1550842951.526 * * * * [misc]progress: [ 1 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (neg.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> 1550842951.526 * * * * [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)))))))> 1550842951.526 * * * * [misc]progress: [ 3 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550842951.526 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842951.526 * * [misc]simplify: iters left: 5 (9 enodes) 1550842951.529 * * [misc]simplify: iters left: 4 (22 enodes) 1550842951.532 * * [misc]simplify: iters left: 3 (42 enodes) 1550842951.540 * * [misc]simplify: iters left: 2 (100 enodes) 1550842951.568 * * [misc]simplify: iters left: 1 (347 enodes) 1550842951.722 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842951.722 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842951.723 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842951.724 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842951.733 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842951.782 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842951.846 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842951.910 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842951.972 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842952.089 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842952.206 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842952.206 * [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))))) 1550842952.206 * * * * [misc]progress: [ 4 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550842952.206 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842952.206 * * [misc]simplify: iters left: 5 (9 enodes) 1550842952.211 * * [misc]simplify: iters left: 4 (22 enodes) 1550842952.218 * * [misc]simplify: iters left: 3 (42 enodes) 1550842952.234 * * [misc]simplify: iters left: 2 (100 enodes) 1550842952.279 * * [misc]simplify: iters left: 1 (347 enodes) 1550842952.573 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842952.573 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842952.574 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842952.577 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842952.594 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842952.688 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842952.811 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842952.927 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842953.044 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842953.166 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842953.286 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842953.286 * [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))))) 1550842953.286 * * * * [misc]progress: [ 5 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550842953.286 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842953.286 * * [misc]simplify: iters left: 5 (9 enodes) 1550842953.292 * * [misc]simplify: iters left: 4 (22 enodes) 1550842953.299 * * [misc]simplify: iters left: 3 (42 enodes) 1550842953.315 * * [misc]simplify: iters left: 2 (100 enodes) 1550842953.359 * * [misc]simplify: iters left: 1 (347 enodes) 1550842953.651 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842953.651 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842953.652 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842953.659 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842953.668 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842953.731 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842953.857 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842953.978 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842954.070 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842954.141 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842954.230 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842954.230 * [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))))) 1550842954.230 * * * * [misc]progress: [ 6 / 6 ] simplifiying candidate #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> 1550842954.231 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842954.231 * * [misc]simplify: iters left: 5 (9 enodes) 1550842954.235 * * [misc]simplify: iters left: 4 (22 enodes) 1550842954.244 * * [misc]simplify: iters left: 3 (42 enodes) 1550842954.260 * * [misc]simplify: iters left: 2 (100 enodes) 1550842954.296 * * [misc]simplify: iters left: 1 (347 enodes) 1550842954.489 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842954.489 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842954.490 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842954.491 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842954.500 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842954.544 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842954.612 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842954.673 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842954.737 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842954.799 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842954.863 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842954.863 * [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))))) 1550842954.864 * * * [misc]progress: adding candidates to table 1550842955.039 * * [misc]progress: iteration 2 / 4 1550842955.039 * * * [misc]progress: picking best candidate 1550842955.073 * * * * [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)))))))> 1550842955.073 * * * [misc]progress: localizing error 1550842955.367 * * * [misc]progress: generating rewritten candidates 1550842955.367 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1550842955.372 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2) 1550842955.398 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 1 2) 1550842955.402 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 1) 1550842955.407 * * * [misc]progress: generating series expansions 1550842955.407 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1550842955.407 * * * * [misc]progress: [ 2 / 4 ] generating series at (2) 1550842955.407 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 1 2) 1550842955.407 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 1) 1550842955.407 * * * [misc]progress: simplifying candidates 1550842955.407 * * * * [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)))))))> 1550842955.408 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842955.408 * * [misc]simplify: iters left: 5 (9 enodes) 1550842955.412 * * [misc]simplify: iters left: 4 (16 enodes) 1550842955.417 * * [misc]simplify: iters left: 3 (18 enodes) 1550842955.423 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842955.423 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842955.423 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550842955.423 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550842955.423 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550842955.424 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550842955.424 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842955.424 * [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))))))) 1550842955.424 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842955.424 * * [misc]simplify: iters left: 5 (9 enodes) 1550842955.428 * * [misc]simplify: iters left: 4 (22 enodes) 1550842955.437 * * [misc]simplify: iters left: 3 (42 enodes) 1550842955.452 * * [misc]simplify: iters left: 2 (100 enodes) 1550842955.491 * * [misc]simplify: iters left: 1 (347 enodes) 1550842955.714 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842955.714 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842955.715 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842955.718 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842955.735 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842955.815 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842955.927 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842956.033 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842956.144 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842956.236 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842956.359 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842956.360 * [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))))))) 1550842956.360 * * * * [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)))))))> 1550842956.360 * * * * [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)))))))> 1550842956.360 * * * * [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))))))))> 1550842956.360 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842956.360 * * [misc]simplify: iters left: 5 (9 enodes) 1550842956.365 * * [misc]simplify: iters left: 4 (16 enodes) 1550842956.367 * * [misc]simplify: iters left: 3 (18 enodes) 1550842956.370 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842956.370 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842956.370 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550842956.370 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550842956.370 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550842956.370 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550842956.371 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842956.371 * [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)))))))) 1550842956.371 * * * * [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)))))))))> 1550842956.371 * [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))))))) 1550842956.371 * * [misc]simplify: iters left: 6 (13 enodes) 1550842956.374 * * [misc]simplify: iters left: 5 (45 enodes) 1550842956.387 * * [misc]simplify: iters left: 4 (144 enodes) 1550842956.458 * * [misc]simplify: iters left: 3 (446 enodes) 1550842956.905 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842956.905 * * [misc]simplify: Extracting #1: cost 41 inf + 0 1550842956.906 * * [misc]simplify: Extracting #2: cost 283 inf + 0 1550842956.909 * * [misc]simplify: Extracting #3: cost 446 inf + 44 1550842956.932 * * [misc]simplify: Extracting #4: cost 488 inf + 246749 1550842957.050 * * [misc]simplify: Extracting #5: cost 101 inf + 1165723 1550842957.191 * * [misc]simplify: Extracting #6: cost 2 inf + 1463482 1550842957.321 * * [misc]simplify: Extracting #7: cost 0 inf + 1419126 1550842957.488 * * [misc]simplify: Extracting #8: cost 0 inf + 1414206 1550842957.652 * [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)))) 1550842957.652 * [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))))))))) 1550842957.652 * * * * [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)))))))> 1550842957.653 * [enter]simplify: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1550842957.653 * * [misc]simplify: iters left: 3 (5 enodes) 1550842957.655 * * [misc]simplify: iters left: 2 (11 enodes) 1550842957.659 * * [misc]simplify: iters left: 1 (13 enodes) 1550842957.663 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842957.663 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842957.663 * * [misc]simplify: Extracting #2: cost 4 inf + 0 1550842957.663 * * [misc]simplify: Extracting #3: cost 4 inf + 1 1550842957.663 * * [misc]simplify: Extracting #4: cost 0 inf + 127 1550842957.663 * [exit]simplify: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1550842957.663 * [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))))))) 1550842957.663 * * * * [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)))))))> 1550842957.664 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842957.664 * * [misc]simplify: iters left: 5 (7 enodes) 1550842957.667 * * [misc]simplify: iters left: 4 (16 enodes) 1550842957.670 * * [misc]simplify: iters left: 3 (20 enodes) 1550842957.673 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842957.673 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550842957.673 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550842957.673 * * [misc]simplify: Extracting #3: cost 8 inf + 1 1550842957.674 * * [misc]simplify: Extracting #4: cost 5 inf + 324 1550842957.674 * * [misc]simplify: Extracting #5: cost 0 inf + 2334 1550842957.674 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1550842957.674 * [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))))))) 1550842957.674 * * * * [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)))))))> 1550842957.674 * * * * [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)))))))> 1550842957.674 * [enter]simplify: Simplifying (sqrt.p16 x) 1550842957.674 * * [misc]simplify: iters left: 1 (2 enodes) 1550842957.675 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842957.675 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842957.675 * * [misc]simplify: Extracting #2: cost 1 inf + 1 1550842957.675 * * [misc]simplify: Extracting #3: cost 0 inf + 42 1550842957.675 * [exit]simplify: Simplified to (sqrt.p16 x) 1550842957.675 * [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))))))) 1550842957.675 * * * * [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)))))))> 1550842957.675 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1550842957.675 * * [misc]simplify: iters left: 3 (6 enodes) 1550842957.677 * * [misc]simplify: iters left: 2 (14 enodes) 1550842957.679 * * [misc]simplify: iters left: 1 (18 enodes) 1550842957.682 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842957.682 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550842957.682 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550842957.682 * * [misc]simplify: Extracting #3: cost 5 inf + 43 1550842957.682 * * [misc]simplify: Extracting #4: cost 0 inf + 2131 1550842957.683 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1550842957.683 * [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))))))) 1550842957.683 * * * * [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)))))))> 1550842957.683 * * * * [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)))))))> 1550842957.683 * * * * [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)))))))> 1550842957.683 * * * * [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)))))))> 1550842957.683 * * * * [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)))))))> 1550842957.683 * * * [misc]progress: adding candidates to table 1550842958.394 * * [misc]progress: iteration 3 / 4 1550842958.394 * * * [misc]progress: picking best candidate 1550842958.620 * * * * [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)))))))> 1550842958.620 * * * [misc]progress: localizing error 1550842958.741 * * * [misc]progress: generating rewritten candidates 1550842958.742 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1 2) 1550842958.747 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2) 1550842958.762 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 2 2) 1550842958.763 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 1 2 2) 1550842958.764 * * * [misc]progress: generating series expansions 1550842958.764 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1 2) 1550842958.764 * * * * [misc]progress: [ 2 / 4 ] generating series at (2) 1550842958.764 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 2 2) 1550842958.764 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 1 2 2) 1550842958.764 * * * [misc]progress: simplifying candidates 1550842958.764 * * * * [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)))))))> 1550842958.765 * * * * [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)))))))> 1550842958.765 * * * * [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))))))))> 1550842958.765 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842958.765 * * [misc]simplify: iters left: 5 (9 enodes) 1550842958.767 * * [misc]simplify: iters left: 4 (16 enodes) 1550842958.770 * * [misc]simplify: iters left: 3 (18 enodes) 1550842958.773 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842958.773 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842958.773 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550842958.773 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550842958.773 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550842958.773 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550842958.773 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842958.773 * [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)))))))) 1550842958.773 * * * * [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))))))))> 1550842958.773 * [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))))))) 1550842958.773 * * [misc]simplify: iters left: 6 (13 enodes) 1550842958.776 * * [misc]simplify: iters left: 5 (38 enodes) 1550842958.789 * * [misc]simplify: iters left: 4 (106 enodes) 1550842958.813 * * [misc]simplify: iters left: 3 (376 enodes) 1550842959.003 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842959.003 * * [misc]simplify: Extracting #1: cost 52 inf + 0 1550842959.004 * * [misc]simplify: Extracting #2: cost 302 inf + 0 1550842959.005 * * [misc]simplify: Extracting #3: cost 417 inf + 43 1550842959.020 * * [misc]simplify: Extracting #4: cost 351 inf + 302562 1550842959.108 * * [misc]simplify: Extracting #5: cost 35 inf + 1004993 1550842959.216 * * [misc]simplify: Extracting #6: cost 0 inf + 1083663 1550842959.322 * * [misc]simplify: Extracting #7: cost 0 inf + 1082583 1550842959.427 * [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)))))) 1550842959.427 * [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)))))))) 1550842959.427 * * * * [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)))))))> 1550842959.428 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842959.428 * * [misc]simplify: iters left: 5 (9 enodes) 1550842959.432 * * [misc]simplify: iters left: 4 (16 enodes) 1550842959.437 * * [misc]simplify: iters left: 3 (18 enodes) 1550842959.443 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842959.443 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842959.443 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550842959.443 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550842959.443 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550842959.443 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550842959.444 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842959.444 * [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))))))) 1550842959.444 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842959.444 * * [misc]simplify: iters left: 5 (9 enodes) 1550842959.448 * * [misc]simplify: iters left: 4 (22 enodes) 1550842959.456 * * [misc]simplify: iters left: 3 (42 enodes) 1550842959.473 * * [misc]simplify: iters left: 2 (100 enodes) 1550842959.518 * * [misc]simplify: iters left: 1 (347 enodes) 1550842959.751 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842959.751 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842959.752 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842959.753 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842959.762 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842959.807 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842959.893 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842959.977 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842960.050 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842960.132 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842960.197 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842960.197 * [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))))))) 1550842960.198 * * * * [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)))))))> 1550842960.198 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842960.198 * * [misc]simplify: iters left: 5 (9 enodes) 1550842960.202 * * [misc]simplify: iters left: 4 (16 enodes) 1550842960.207 * * [misc]simplify: iters left: 3 (18 enodes) 1550842960.213 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842960.213 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842960.213 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550842960.213 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550842960.213 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550842960.213 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550842960.213 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842960.213 * [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))))))) 1550842960.213 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842960.213 * * [misc]simplify: iters left: 5 (9 enodes) 1550842960.215 * * [misc]simplify: iters left: 4 (22 enodes) 1550842960.220 * * [misc]simplify: iters left: 3 (42 enodes) 1550842960.228 * * [misc]simplify: iters left: 2 (100 enodes) 1550842960.251 * * [misc]simplify: iters left: 1 (347 enodes) 1550842960.464 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842960.464 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842960.465 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842960.468 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842960.481 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842960.530 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842960.595 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842960.657 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842960.721 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842960.841 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842960.903 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842960.903 * [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))))))) 1550842960.903 * * * * [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)))))))> 1550842960.904 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842960.904 * * [misc]simplify: iters left: 5 (9 enodes) 1550842960.906 * * [misc]simplify: iters left: 4 (16 enodes) 1550842960.909 * * [misc]simplify: iters left: 3 (18 enodes) 1550842960.913 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842960.913 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842960.913 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550842960.913 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550842960.913 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550842960.913 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550842960.914 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842960.914 * [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))))))) 1550842960.914 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842960.914 * * [misc]simplify: iters left: 5 (9 enodes) 1550842960.916 * * [misc]simplify: iters left: 4 (22 enodes) 1550842960.920 * * [misc]simplify: iters left: 3 (42 enodes) 1550842960.928 * * [misc]simplify: iters left: 2 (100 enodes) 1550842960.950 * * [misc]simplify: iters left: 1 (347 enodes) 1550842961.113 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842961.114 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842961.121 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842961.124 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842961.142 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842961.188 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842961.253 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842961.341 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842961.403 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842961.465 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842961.529 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842961.529 * [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))))))) 1550842961.529 * * * * [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)))))))> 1550842961.529 * [enter]simplify: Simplifying (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842961.529 * * [misc]simplify: iters left: 5 (9 enodes) 1550842961.531 * * [misc]simplify: iters left: 4 (16 enodes) 1550842961.534 * * [misc]simplify: iters left: 3 (18 enodes) 1550842961.537 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842961.537 * * [misc]simplify: Extracting #1: cost 3 inf + 0 1550842961.537 * * [misc]simplify: Extracting #2: cost 6 inf + 0 1550842961.537 * * [misc]simplify: Extracting #3: cost 9 inf + 0 1550842961.537 * * [misc]simplify: Extracting #4: cost 6 inf + 43 1550842961.537 * * [misc]simplify: Extracting #5: cost 0 inf + 2214 1550842961.537 * [exit]simplify: Simplified to (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842961.537 * [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))))))) 1550842961.538 * [enter]simplify: Simplifying (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842961.538 * * [misc]simplify: iters left: 5 (9 enodes) 1550842961.540 * * [misc]simplify: iters left: 4 (22 enodes) 1550842961.544 * * [misc]simplify: iters left: 3 (42 enodes) 1550842961.552 * * [misc]simplify: iters left: 2 (100 enodes) 1550842961.586 * * [misc]simplify: iters left: 1 (347 enodes) 1550842961.817 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842961.818 * * [misc]simplify: Extracting #1: cost 48 inf + 0 1550842961.818 * * [misc]simplify: Extracting #2: cost 269 inf + 0 1550842961.820 * * [misc]simplify: Extracting #3: cost 457 inf + 1 1550842961.836 * * [misc]simplify: Extracting #4: cost 422 inf + 210469 1550842961.906 * * [misc]simplify: Extracting #5: cost 77 inf + 915056 1550842961.973 * * [misc]simplify: Extracting #6: cost 3 inf + 1114648 1550842962.071 * * [misc]simplify: Extracting #7: cost 1 inf + 1091652 1550842962.194 * * [misc]simplify: Extracting #8: cost 0 inf + 1093814 1550842962.317 * * [misc]simplify: Extracting #9: cost 0 inf + 1093774 1550842962.437 * [exit]simplify: Simplified to (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x)))) 1550842962.437 * [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))))))) 1550842962.438 * * * [misc]progress: adding candidates to table 1550842962.884 * * [misc]progress: iteration 4 / 4 1550842962.884 * * * [misc]progress: picking best candidate 1550842963.058 * * * * [misc]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)))))))> 1550842963.058 * * * [misc]progress: localizing error 1550842963.205 * * * [misc]progress: generating rewritten candidates 1550842963.205 * * * * [misc]progress: [ 1 / 4 ] rewriting at (2 1) 1550842963.208 * * * * [misc]progress: [ 2 / 4 ] rewriting at (2) 1550842963.216 * * * * [misc]progress: [ 3 / 4 ] rewriting at (2 1 2) 1550842963.218 * * * * [misc]progress: [ 4 / 4 ] rewriting at (2 2 2) 1550842963.219 * * * [misc]progress: generating series expansions 1550842963.219 * * * * [misc]progress: [ 1 / 4 ] generating series at (2 1) 1550842963.219 * * * * [misc]progress: [ 2 / 4 ] generating series at (2) 1550842963.219 * * * * [misc]progress: [ 3 / 4 ] generating series at (2 1 2) 1550842963.220 * * * * [misc]progress: [ 4 / 4 ] generating series at (2 2 2) 1550842963.220 * * * [misc]progress: simplifying candidates 1550842963.220 * * * * [misc]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)))))))> 1550842963.220 * * * * [misc]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)))))))> 1550842963.220 * * * * [misc]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)))))))))> 1550842963.220 * [enter]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))))))) 1550842963.220 * * [misc]simplify: iters left: 6 (14 enodes) 1550842963.223 * * [misc]simplify: iters left: 5 (47 enodes) 1550842963.233 * * [misc]simplify: iters left: 4 (140 enodes) 1550842963.274 * * [misc]simplify: iters left: 3 (480 enodes) 1550842963.733 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842963.733 * * [misc]simplify: Extracting #1: cost 36 inf + 0 1550842963.735 * * [misc]simplify: Extracting #2: cost 250 inf + 0 1550842963.738 * * [misc]simplify: Extracting #3: cost 413 inf + 725 1550842963.758 * * [misc]simplify: Extracting #4: cost 550 inf + 129982 1550842963.853 * * [misc]simplify: Extracting #5: cost 163 inf + 996596 1550842964.016 * * [misc]simplify: Extracting #6: cost 12 inf + 1471739 1550842964.186 * * [misc]simplify: Extracting #7: cost 0 inf + 1461963 1550842964.350 * * [misc]simplify: Extracting #8: cost 0 inf + 1441923 1550842964.507 * * [misc]simplify: Extracting #9: cost 0 inf + 1441523 1550842964.653 * [exit]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)))))) 1550842964.653 * [misc]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))))))))) 1550842964.653 * * * * [misc]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)))))))> 1550842964.653 * [enter]simplify: Simplifying (sqrt.p16 (+.p16 x (real->posit16 1))) 1550842964.653 * * [misc]simplify: iters left: 3 (5 enodes) 1550842964.656 * * [misc]simplify: iters left: 2 (11 enodes) 1550842964.659 * * [misc]simplify: iters left: 1 (13 enodes) 1550842964.663 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842964.663 * * [misc]simplify: Extracting #1: cost 2 inf + 0 1550842964.663 * * [misc]simplify: Extracting #2: cost 4 inf + 0 1550842964.663 * * [misc]simplify: Extracting #3: cost 4 inf + 1 1550842964.663 * * [misc]simplify: Extracting #4: cost 0 inf + 127 1550842964.663 * [exit]simplify: Simplified to (sqrt.p16 (+.p16 (real->posit16 1) x)) 1550842964.663 * [misc]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))))))) 1550842964.663 * * * * [misc]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)))))))> 1550842964.664 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) 1550842964.664 * * [misc]simplify: iters left: 5 (7 enodes) 1550842964.667 * * [misc]simplify: iters left: 4 (16 enodes) 1550842964.672 * * [misc]simplify: iters left: 3 (20 enodes) 1550842964.678 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842964.678 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550842964.678 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550842964.679 * * [misc]simplify: Extracting #3: cost 8 inf + 1 1550842964.679 * * [misc]simplify: Extracting #4: cost 5 inf + 324 1550842964.679 * * [misc]simplify: Extracting #5: cost 0 inf + 2334 1550842964.679 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 (real->posit16 1) x))) (real->posit16 1)) 1550842964.679 * [misc]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))))))) 1550842964.679 * * * * [misc]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)))))))> 1550842964.679 * * * * [misc]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)))))))> 1550842964.680 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1550842964.680 * * [misc]simplify: iters left: 3 (6 enodes) 1550842964.682 * * [misc]simplify: iters left: 2 (14 enodes) 1550842964.687 * * [misc]simplify: iters left: 1 (18 enodes) 1550842964.692 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842964.692 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550842964.692 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550842964.692 * * [misc]simplify: Extracting #3: cost 5 inf + 43 1550842964.692 * * [misc]simplify: Extracting #4: cost 0 inf + 2131 1550842964.692 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1550842964.692 * [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))))))) 1550842964.692 * * * * [misc]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)))))))> 1550842964.693 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1550842964.693 * * [misc]simplify: iters left: 3 (6 enodes) 1550842964.695 * * [misc]simplify: iters left: 2 (14 enodes) 1550842964.701 * * [misc]simplify: iters left: 1 (18 enodes) 1550842964.706 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842964.706 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550842964.706 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550842964.706 * * [misc]simplify: Extracting #3: cost 5 inf + 43 1550842964.707 * * [misc]simplify: Extracting #4: cost 0 inf + 2131 1550842964.707 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1550842964.707 * [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))))))) 1550842964.707 * * * * [misc]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)))))))> 1550842964.707 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1550842964.707 * * [misc]simplify: iters left: 3 (6 enodes) 1550842964.710 * * [misc]simplify: iters left: 2 (14 enodes) 1550842964.714 * * [misc]simplify: iters left: 1 (18 enodes) 1550842964.720 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842964.720 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550842964.720 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550842964.720 * * [misc]simplify: Extracting #3: cost 5 inf + 43 1550842964.720 * * [misc]simplify: Extracting #4: cost 0 inf + 2131 1550842964.720 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1550842964.721 * [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))))))) 1550842964.721 * * * * [misc]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)))))))> 1550842964.721 * [enter]simplify: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) 1550842964.721 * * [misc]simplify: iters left: 3 (6 enodes) 1550842964.724 * * [misc]simplify: iters left: 2 (14 enodes) 1550842964.728 * * [misc]simplify: iters left: 1 (18 enodes) 1550842964.733 * * [misc]simplify: Extracting #0: cost 1 inf + 0 1550842964.734 * * [misc]simplify: Extracting #1: cost 6 inf + 0 1550842964.734 * * [misc]simplify: Extracting #2: cost 8 inf + 0 1550842964.734 * * [misc]simplify: Extracting #3: cost 5 inf + 43 1550842964.734 * * [misc]simplify: Extracting #4: cost 0 inf + 2131 1550842964.734 * [exit]simplify: Simplified to (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (real->posit16 1)) 1550842964.734 * [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))))))) 1550842964.734 * * * [misc]progress: adding candidates to table 1550842965.201 * [misc]progress: [Phase 3 of 3] Extracting. 1550842965.202 * * [misc]regime: Finding splitpoints for: (#posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (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 x))) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (real->posit16 1)) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> #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) (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 (+.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))))))))>) 1550842965.204 * * * [misc]regime-changes: Trying 1 branch expressions: (x) 1550842965.204 * * * * [misc]regimes: Trying to branch on x from (#posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x))) (*.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (sqrt.p16 x))) (sqrt.p16 x)) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (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 x))) (/.p16 (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))) (real->posit16 1)) (sqrt.p16 (+.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1)))))))> #posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))> #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) (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 (+.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))))))))>) 1550842965.520 * * * [misc]regime: Found split indices: #