0.002 * [progress]: [Phase 1 of 3] Setting up. 0.003 * * * [progress]: [1/2] Preparing points 0.003 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.004 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.008 * * * * [points]: Setting MPFR precision to 64 0.009 * * * * [points]: Setting MPFR precision to 320 0.011 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.016 * * * * [points]: Setting MPFR precision to 64 0.019 * * * * [points]: Setting MPFR precision to 320 0.022 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.028 * * * * [points]: Setting MPFR precision to 64 0.033 * * * * [points]: Setting MPFR precision to 320 0.037 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.043 * * * * [points]: Setting MPFR precision to 64 0.049 * * * * [points]: Setting MPFR precision to 320 0.056 * * * * [points]: Computing exacts for 256 points 0.061 * * * * [points]: Setting MPFR precision to 64 0.085 * * * * [points]: Setting MPFR precision to 320 0.098 * * * * [points]: Filtering points with unrepresentable outputs 0.098 * * * * [points]: Sampled 256 points with exact outputs 0.098 * * * [progress]: [2/2] Setting up program. 0.113 * [progress]: [Phase 2 of 3] Improving. 0.113 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.113 * [simplify]: Simplifying (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 0.113 * * [simplify]: iters left: 5 (12 enodes) 0.116 * * [simplify]: iters left: 4 (35 enodes) 0.123 * * [simplify]: iters left: 3 (83 enodes) 0.139 * * [simplify]: iters left: 2 (233 enodes) 0.211 * * [simplify]: Extracting #0: cost 1 inf + 0 0.212 * * [simplify]: Extracting #1: cost 29 inf + 0 0.212 * * [simplify]: Extracting #2: cost 123 inf + 0 0.212 * * [simplify]: Extracting #3: cost 245 inf + 1 0.215 * * [simplify]: Extracting #4: cost 303 inf + 42876 0.228 * * [simplify]: Extracting #5: cost 128 inf + 332692 0.256 * * [simplify]: Extracting #6: cost 5 inf + 548531 0.281 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.309 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 0.310 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 0.333 * * [progress]: iteration 1 / 4 0.333 * * * [progress]: picking best candidate 0.346 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.346 * * * [progress]: localizing error 0.513 * * * [progress]: generating rewritten candidates 0.513 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 0.524 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 0.527 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1) 0.529 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2) 0.531 * * * [progress]: generating series expansions 0.531 * * * * [progress]: [ 1 / 4 ] generating series at (2) 0.531 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 0.531 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1) 0.531 * * * * [progress]: [ 4 / 4 ] generating series at (2 2) 0.531 * * * [progress]: simplifying candidates 0.531 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 0.531 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 0.531 * * [simplify]: iters left: 3 (5 enodes) 0.533 * * [simplify]: iters left: 2 (11 enodes) 0.534 * * [simplify]: iters left: 1 (13 enodes) 0.536 * * [simplify]: Extracting #0: cost 1 inf + 0 0.536 * * [simplify]: Extracting #1: cost 3 inf + 0 0.536 * * [simplify]: Extracting #2: cost 5 inf + 0 0.536 * * [simplify]: Extracting #3: cost 3 inf + 2 0.537 * * [simplify]: Extracting #4: cost 0 inf + 527 0.537 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 0.537 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 0.537 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 0.537 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 0.537 * * [simplify]: iters left: 3 (5 enodes) 0.538 * * [simplify]: iters left: 2 (11 enodes) 0.540 * * [simplify]: iters left: 1 (13 enodes) 0.542 * * [simplify]: Extracting #0: cost 1 inf + 0 0.542 * * [simplify]: Extracting #1: cost 3 inf + 0 0.542 * * [simplify]: Extracting #2: cost 5 inf + 0 0.542 * * [simplify]: Extracting #3: cost 3 inf + 2 0.542 * * [simplify]: Extracting #4: cost 0 inf + 527 0.542 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 0.542 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 0.542 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 0.542 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.542 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.542 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 0.542 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 0.542 * * [simplify]: iters left: 2 (4 enodes) 0.543 * * [simplify]: iters left: 1 (10 enodes) 0.545 * * [simplify]: Extracting #0: cost 1 inf + 0 0.545 * * [simplify]: Extracting #1: cost 3 inf + 0 0.545 * * [simplify]: Extracting #2: cost 3 inf + 1 0.545 * * [simplify]: Extracting #3: cost 0 inf + 45 0.545 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 0.545 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (real->posit16 1) x)))) 0.545 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.546 * [simplify]: Simplifying (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 0.546 * * [simplify]: iters left: 5 (12 enodes) 0.548 * * [simplify]: iters left: 4 (35 enodes) 0.554 * * [simplify]: iters left: 3 (83 enodes) 0.570 * * [simplify]: iters left: 2 (233 enodes) 0.641 * * [simplify]: Extracting #0: cost 1 inf + 0 0.641 * * [simplify]: Extracting #1: cost 29 inf + 0 0.641 * * [simplify]: Extracting #2: cost 123 inf + 0 0.642 * * [simplify]: Extracting #3: cost 245 inf + 1 0.645 * * [simplify]: Extracting #4: cost 303 inf + 42876 0.662 * * [simplify]: Extracting #5: cost 128 inf + 332692 0.685 * * [simplify]: Extracting #6: cost 5 inf + 548531 0.718 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.750 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 0.750 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 0.750 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.750 * [simplify]: Simplifying (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 0.750 * * [simplify]: iters left: 5 (12 enodes) 0.755 * * [simplify]: iters left: 4 (35 enodes) 0.766 * * [simplify]: iters left: 3 (83 enodes) 0.786 * * [simplify]: iters left: 2 (233 enodes) 0.877 * * [simplify]: Extracting #0: cost 1 inf + 0 0.877 * * [simplify]: Extracting #1: cost 29 inf + 0 0.877 * * [simplify]: Extracting #2: cost 123 inf + 0 0.878 * * [simplify]: Extracting #3: cost 245 inf + 1 0.880 * * [simplify]: Extracting #4: cost 303 inf + 42876 0.893 * * [simplify]: Extracting #5: cost 128 inf + 332692 0.918 * * [simplify]: Extracting #6: cost 5 inf + 548531 0.951 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.993 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 0.993 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 0.993 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.994 * [simplify]: Simplifying (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 0.994 * * [simplify]: iters left: 5 (12 enodes) 0.999 * * [simplify]: iters left: 4 (35 enodes) 1.005 * * [simplify]: iters left: 3 (83 enodes) 1.022 * * [simplify]: iters left: 2 (233 enodes) 1.133 * * [simplify]: Extracting #0: cost 1 inf + 0 1.133 * * [simplify]: Extracting #1: cost 29 inf + 0 1.134 * * [simplify]: Extracting #2: cost 123 inf + 0 1.134 * * [simplify]: Extracting #3: cost 245 inf + 1 1.137 * * [simplify]: Extracting #4: cost 303 inf + 42876 1.156 * * [simplify]: Extracting #5: cost 128 inf + 332692 1.194 * * [simplify]: Extracting #6: cost 5 inf + 548531 1.232 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.277 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 1.277 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 1.278 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 1.278 * [simplify]: Simplifying (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 1.278 * * [simplify]: iters left: 5 (12 enodes) 1.284 * * [simplify]: iters left: 4 (35 enodes) 1.296 * * [simplify]: iters left: 3 (83 enodes) 1.328 * * [simplify]: iters left: 2 (233 enodes) 1.403 * * [simplify]: Extracting #0: cost 1 inf + 0 1.403 * * [simplify]: Extracting #1: cost 29 inf + 0 1.404 * * [simplify]: Extracting #2: cost 123 inf + 0 1.404 * * [simplify]: Extracting #3: cost 245 inf + 1 1.407 * * [simplify]: Extracting #4: cost 303 inf + 42876 1.425 * * [simplify]: Extracting #5: cost 128 inf + 332692 1.447 * * [simplify]: Extracting #6: cost 5 inf + 548531 1.476 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.518 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 1.518 * [simplify]: Simplified (2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)))) 1.518 * * * [progress]: adding candidates to table 1.784 * * [progress]: iteration 2 / 4 1.784 * * * [progress]: picking best candidate 1.822 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 1.822 * * * [progress]: localizing error 1.985 * * * [progress]: generating rewritten candidates 1.985 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 1.988 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 1.991 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 1.993 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 1.995 * * * [progress]: generating series expansions 1.995 * * * * [progress]: [ 1 / 4 ] generating series at (2) 1.995 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 1.995 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 1.995 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 1.995 * * * [progress]: simplifying candidates 1.995 * * * * [progress]: [ 1 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (neg.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 1.995 * [simplify]: Simplifying (neg.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 1.995 * * [simplify]: iters left: 4 (6 enodes) 1.997 * * [simplify]: iters left: 3 (18 enodes) 2.008 * * [simplify]: iters left: 2 (32 enodes) 2.014 * * [simplify]: iters left: 1 (80 enodes) 2.033 * * [simplify]: Extracting #0: cost 1 inf + 0 2.033 * * [simplify]: Extracting #1: cost 2 inf + 0 2.033 * * [simplify]: Extracting #2: cost 23 inf + 0 2.033 * * [simplify]: Extracting #3: cost 71 inf + 0 2.033 * * [simplify]: Extracting #4: cost 96 inf + 405 2.034 * * [simplify]: Extracting #5: cost 67 inf + 28805 2.038 * * [simplify]: Extracting #6: cost 13 inf + 98338 2.047 * * [simplify]: Extracting #7: cost 1 inf + 114359 2.056 * * [simplify]: Extracting #8: cost 0 inf + 115761 2.066 * [simplify]: Simplified to (neg.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 2.066 * [simplify]: Simplified (2 2) to (λ (x) (-.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (neg.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.066 * * * * [progress]: [ 2 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 2.067 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) 2.067 * * [simplify]: iters left: 3 (5 enodes) 2.069 * * [simplify]: iters left: 2 (17 enodes) 2.075 * * [simplify]: iters left: 1 (31 enodes) 2.085 * * [simplify]: Extracting #0: cost 1 inf + 0 2.085 * * [simplify]: Extracting #1: cost 11 inf + 0 2.085 * * [simplify]: Extracting #2: cost 28 inf + 0 2.085 * * [simplify]: Extracting #3: cost 29 inf + 324 2.085 * * [simplify]: Extracting #4: cost 22 inf + 6266 2.086 * * [simplify]: Extracting #5: cost 3 inf + 23256 2.087 * * [simplify]: Extracting #6: cost 0 inf + 26382 2.088 * * [simplify]: Extracting #7: cost 0 inf + 25822 2.089 * [simplify]: Simplified to (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) 2.089 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) 2.089 * * * * [progress]: [ 3 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> 2.089 * * * * [progress]: [ 4 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> 2.089 * * * * [progress]: [ 5 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 2) x) (neg.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> 2.089 * * * * [progress]: [ 6 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (-.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> 2.089 * * * * [progress]: [ 7 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))))))> 2.089 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 2.090 * * [simplify]: iters left: 2 (4 enodes) 2.091 * * [simplify]: iters left: 1 (10 enodes) 2.092 * * [simplify]: Extracting #0: cost 1 inf + 0 2.092 * * [simplify]: Extracting #1: cost 3 inf + 0 2.092 * * [simplify]: Extracting #2: cost 3 inf + 1 2.092 * * [simplify]: Extracting #3: cost 0 inf + 45 2.093 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 2.093 * [simplify]: Simplified (2 2 2 2) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (real->posit16 1) x))))) 2.093 * * * * [progress]: [ 8 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 2.093 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.093 * * [simplify]: iters left: 3 (5 enodes) 2.094 * * [simplify]: iters left: 2 (11 enodes) 2.096 * * [simplify]: iters left: 1 (13 enodes) 2.098 * * [simplify]: Extracting #0: cost 1 inf + 0 2.098 * * [simplify]: Extracting #1: cost 3 inf + 0 2.098 * * [simplify]: Extracting #2: cost 5 inf + 0 2.098 * * [simplify]: Extracting #3: cost 3 inf + 2 2.098 * * [simplify]: Extracting #4: cost 0 inf + 527 2.098 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.098 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.098 * * * * [progress]: [ 9 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 2.098 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.098 * * [simplify]: iters left: 3 (5 enodes) 2.099 * * [simplify]: iters left: 2 (11 enodes) 2.101 * * [simplify]: iters left: 1 (13 enodes) 2.103 * * [simplify]: Extracting #0: cost 1 inf + 0 2.103 * * [simplify]: Extracting #1: cost 3 inf + 0 2.103 * * [simplify]: Extracting #2: cost 5 inf + 0 2.103 * * [simplify]: Extracting #3: cost 3 inf + 2 2.103 * * [simplify]: Extracting #4: cost 0 inf + 527 2.103 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.103 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.104 * * * * [progress]: [ 10 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 2.104 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.104 * * [simplify]: iters left: 3 (5 enodes) 2.107 * * [simplify]: iters left: 2 (11 enodes) 2.109 * * [simplify]: iters left: 1 (13 enodes) 2.111 * * [simplify]: Extracting #0: cost 1 inf + 0 2.111 * * [simplify]: Extracting #1: cost 3 inf + 0 2.111 * * [simplify]: Extracting #2: cost 5 inf + 0 2.111 * * [simplify]: Extracting #3: cost 3 inf + 2 2.111 * * [simplify]: Extracting #4: cost 0 inf + 527 2.111 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.111 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.111 * * * * [progress]: [ 11 / 11 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> 2.111 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 2.111 * * [simplify]: iters left: 3 (5 enodes) 2.112 * * [simplify]: iters left: 2 (11 enodes) 2.114 * * [simplify]: iters left: 1 (13 enodes) 2.116 * * [simplify]: Extracting #0: cost 1 inf + 0 2.116 * * [simplify]: Extracting #1: cost 3 inf + 0 2.116 * * [simplify]: Extracting #2: cost 5 inf + 0 2.116 * * [simplify]: Extracting #3: cost 3 inf + 2 2.117 * * [simplify]: Extracting #4: cost 0 inf + 527 2.117 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 2.117 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) 2.117 * * * [progress]: adding candidates to table 2.498 * * [progress]: iteration 3 / 4 2.498 * * * [progress]: picking best candidate 2.553 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 2.553 * * * [progress]: localizing error 2.846 * * * [progress]: generating rewritten candidates 2.846 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 2.858 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 2.862 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 2.864 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1) 2.866 * * * [progress]: generating series expansions 2.866 * * * * [progress]: [ 1 / 4 ] generating series at (2) 2.866 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 2.866 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 2.866 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1) 2.866 * * * [progress]: simplifying candidates 2.866 * * * * [progress]: [ 1 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1))))> 2.866 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)) 2.866 * * [simplify]: iters left: 5 (8 enodes) 2.869 * * [simplify]: iters left: 4 (25 enodes) 2.886 * * [simplify]: iters left: 3 (62 enodes) 2.901 * * [simplify]: iters left: 2 (193 enodes) 3.009 * * [simplify]: Extracting #0: cost 1 inf + 0 3.009 * * [simplify]: Extracting #1: cost 65 inf + 0 3.010 * * [simplify]: Extracting #2: cost 241 inf + 0 3.013 * * [simplify]: Extracting #3: cost 266 inf + 38563 3.026 * * [simplify]: Extracting #4: cost 125 inf + 268103 3.049 * * [simplify]: Extracting #5: cost 20 inf + 460048 3.088 * * [simplify]: Extracting #6: cost 0 inf + 501677 3.111 * * [simplify]: Extracting #7: cost 0 inf + 501317 3.133 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 3.134 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) x)) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 3.134 * * * * [progress]: [ 2 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> 3.134 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) 3.134 * * [simplify]: iters left: 5 (8 enodes) 3.138 * * [simplify]: iters left: 4 (25 enodes) 3.145 * * [simplify]: iters left: 3 (62 enodes) 3.165 * * [simplify]: iters left: 2 (193 enodes) 3.279 * * [simplify]: Extracting #0: cost 1 inf + 0 3.279 * * [simplify]: Extracting #1: cost 65 inf + 0 3.279 * * [simplify]: Extracting #2: cost 241 inf + 0 3.281 * * [simplify]: Extracting #3: cost 266 inf + 38563 3.291 * * [simplify]: Extracting #4: cost 125 inf + 268103 3.311 * * [simplify]: Extracting #5: cost 20 inf + 460048 3.338 * * [simplify]: Extracting #6: cost 0 inf + 501677 3.380 * * [simplify]: Extracting #7: cost 0 inf + 501317 3.422 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 3.422 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 3.422 * * * * [progress]: [ 3 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))))))> 3.422 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 3.422 * * [simplify]: iters left: 3 (5 enodes) 3.425 * * [simplify]: iters left: 2 (11 enodes) 3.429 * * [simplify]: iters left: 1 (13 enodes) 3.434 * * [simplify]: Extracting #0: cost 1 inf + 0 3.434 * * [simplify]: Extracting #1: cost 3 inf + 0 3.434 * * [simplify]: Extracting #2: cost 5 inf + 0 3.435 * * [simplify]: Extracting #3: cost 3 inf + 2 3.435 * * [simplify]: Extracting #4: cost 0 inf + 527 3.435 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 3.435 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))) 3.435 * * * * [progress]: [ 4 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))))))> 3.435 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 3.435 * * [simplify]: iters left: 3 (5 enodes) 3.438 * * [simplify]: iters left: 2 (11 enodes) 3.442 * * [simplify]: iters left: 1 (13 enodes) 3.447 * * [simplify]: Extracting #0: cost 1 inf + 0 3.447 * * [simplify]: Extracting #1: cost 3 inf + 0 3.447 * * [simplify]: Extracting #2: cost 5 inf + 0 3.447 * * [simplify]: Extracting #3: cost 3 inf + 2 3.447 * * [simplify]: Extracting #4: cost 0 inf + 527 3.447 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 3.447 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))) 3.447 * * * * [progress]: [ 5 / 18 ] simplifiying candidate #posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 3.448 * * * * [progress]: [ 6 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) x) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)))))> 3.448 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (real->posit16 1)) 3.448 * * [simplify]: iters left: 5 (8 enodes) 3.452 * * [simplify]: iters left: 4 (25 enodes) 3.462 * * [simplify]: iters left: 3 (62 enodes) 3.486 * * [simplify]: iters left: 2 (193 enodes) 3.640 * * [simplify]: Extracting #0: cost 1 inf + 0 3.640 * * [simplify]: Extracting #1: cost 65 inf + 0 3.642 * * [simplify]: Extracting #2: cost 241 inf + 0 3.645 * * [simplify]: Extracting #3: cost 266 inf + 38563 3.664 * * [simplify]: Extracting #4: cost 125 inf + 268103 3.702 * * [simplify]: Extracting #5: cost 20 inf + 460048 3.742 * * [simplify]: Extracting #6: cost 0 inf + 501677 3.784 * * [simplify]: Extracting #7: cost 0 inf + 501317 3.827 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 3.827 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) x) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))) 3.827 * * * * [progress]: [ 7 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))))> 3.828 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) 3.828 * * [simplify]: iters left: 5 (8 enodes) 3.832 * * [simplify]: iters left: 4 (25 enodes) 3.842 * * [simplify]: iters left: 3 (62 enodes) 3.868 * * [simplify]: iters left: 2 (193 enodes) 4.016 * * [simplify]: Extracting #0: cost 1 inf + 0 4.016 * * [simplify]: Extracting #1: cost 65 inf + 0 4.017 * * [simplify]: Extracting #2: cost 241 inf + 0 4.021 * * [simplify]: Extracting #3: cost 266 inf + 38563 4.041 * * [simplify]: Extracting #4: cost 125 inf + 268103 4.087 * * [simplify]: Extracting #5: cost 20 inf + 460048 4.131 * * [simplify]: Extracting #6: cost 0 inf + 501677 4.174 * * [simplify]: Extracting #7: cost 0 inf + 501317 4.217 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 4.217 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))) 4.218 * * * * [progress]: [ 8 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) (+.p16 x (real->posit16 1))))))> 4.218 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) 4.218 * * [simplify]: iters left: 5 (9 enodes) 4.223 * * [simplify]: iters left: 4 (32 enodes) 4.238 * * [simplify]: iters left: 3 (76 enodes) 4.272 * * [simplify]: iters left: 2 (240 enodes) 4.389 * * [simplify]: Extracting #0: cost 1 inf + 0 4.389 * * [simplify]: Extracting #1: cost 46 inf + 0 4.390 * * [simplify]: Extracting #2: cost 215 inf + 0 4.391 * * [simplify]: Extracting #3: cost 263 inf + 32917 4.402 * * [simplify]: Extracting #4: cost 137 inf + 336224 4.431 * * [simplify]: Extracting #5: cost 16 inf + 607943 4.464 * * [simplify]: Extracting #6: cost 0 inf + 646284 4.497 * * [simplify]: Extracting #7: cost 0 inf + 645884 4.530 * [simplify]: Simplified to (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) 4.530 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (*.p16 (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) (+.p16 x (real->posit16 1)))))) 4.530 * * * * [progress]: [ 9 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> 4.530 * [simplify]: Simplifying (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 4.530 * * [simplify]: iters left: 3 (5 enodes) 4.532 * * [simplify]: iters left: 2 (17 enodes) 4.535 * * [simplify]: iters left: 1 (21 enodes) 4.538 * * [simplify]: Extracting #0: cost 1 inf + 0 4.538 * * [simplify]: Extracting #1: cost 5 inf + 0 4.538 * * [simplify]: Extracting #2: cost 7 inf + 0 4.538 * * [simplify]: Extracting #3: cost 5 inf + 2 4.538 * * [simplify]: Extracting #4: cost 0 inf + 1050 4.538 * [simplify]: Simplified to (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 4.538 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) 4.538 * * * * [progress]: [ 10 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (+.p16 x (real->posit16 1)) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> 4.539 * * * * [progress]: [ 11 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x))) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.539 * * * * [progress]: [ 12 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.539 * * * * [progress]: [ 13 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 4.539 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 4.539 * * [simplify]: iters left: 2 (4 enodes) 4.540 * * [simplify]: iters left: 1 (16 enodes) 4.543 * * [simplify]: Extracting #0: cost 1 inf + 0 4.543 * * [simplify]: Extracting #1: cost 6 inf + 0 4.543 * * [simplify]: Extracting #2: cost 11 inf + 1 4.543 * * [simplify]: Extracting #3: cost 11 inf + 323 4.543 * * [simplify]: Extracting #4: cost 5 inf + 1491 4.543 * * [simplify]: Extracting #5: cost 1 inf + 3657 4.544 * * [simplify]: Extracting #6: cost 0 inf + 5019 4.544 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 4.544 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))))) 4.544 * * * * [progress]: [ 14 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.544 * [simplify]: Simplifying (+.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))) 4.544 * * [simplify]: iters left: 3 (6 enodes) 4.546 * * [simplify]: iters left: 2 (12 enodes) 4.548 * * [simplify]: iters left: 1 (14 enodes) 4.550 * * [simplify]: Extracting #0: cost 1 inf + 0 4.550 * * [simplify]: Extracting #1: cost 3 inf + 0 4.550 * * [simplify]: Extracting #2: cost 5 inf + 0 4.550 * * [simplify]: Extracting #3: cost 5 inf + 1 4.550 * * [simplify]: Extracting #4: cost 0 inf + 1327 4.550 * [simplify]: Simplified to (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x)) 4.551 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (real->posit16 1) (real->posit16 1))))) (+.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 x x))) (+.p16 x (real->posit16 1))))) 4.551 * * * * [progress]: [ 15 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.551 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.551 * * [simplify]: iters left: 2 (4 enodes) 4.552 * * [simplify]: iters left: 1 (10 enodes) 4.554 * * [simplify]: Extracting #0: cost 1 inf + 0 4.554 * * [simplify]: Extracting #1: cost 3 inf + 0 4.554 * * [simplify]: Extracting #2: cost 3 inf + 1 4.554 * * [simplify]: Extracting #3: cost 0 inf + 45 4.554 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.554 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (real->posit16 1) x)))) 4.554 * * * * [progress]: [ 16 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.554 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.554 * * [simplify]: iters left: 2 (4 enodes) 4.555 * * [simplify]: iters left: 1 (10 enodes) 4.557 * * [simplify]: Extracting #0: cost 1 inf + 0 4.557 * * [simplify]: Extracting #1: cost 3 inf + 0 4.557 * * [simplify]: Extracting #2: cost 3 inf + 1 4.557 * * [simplify]: Extracting #3: cost 0 inf + 45 4.557 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.557 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (real->posit16 1) x)))) 4.557 * * * * [progress]: [ 17 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.557 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.557 * * [simplify]: iters left: 2 (4 enodes) 4.558 * * [simplify]: iters left: 1 (10 enodes) 4.560 * * [simplify]: Extracting #0: cost 1 inf + 0 4.560 * * [simplify]: Extracting #1: cost 3 inf + 0 4.560 * * [simplify]: Extracting #2: cost 3 inf + 1 4.560 * * [simplify]: Extracting #3: cost 0 inf + 45 4.560 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.560 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (real->posit16 1) x)))) 4.560 * * * * [progress]: [ 18 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 4.561 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 4.561 * * [simplify]: iters left: 2 (4 enodes) 4.562 * * [simplify]: iters left: 1 (10 enodes) 4.563 * * [simplify]: Extracting #0: cost 1 inf + 0 4.563 * * [simplify]: Extracting #1: cost 3 inf + 0 4.563 * * [simplify]: Extracting #2: cost 3 inf + 1 4.563 * * [simplify]: Extracting #3: cost 0 inf + 45 4.563 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 4.564 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (real->posit16 1) x)))) 4.564 * * * [progress]: adding candidates to table 5.283 * * [progress]: iteration 4 / 4 5.283 * * * [progress]: picking best candidate 5.431 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 5.431 * * * [progress]: localizing error 5.709 * * * [progress]: generating rewritten candidates 5.709 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 5.731 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 5.737 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1) 5.739 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 1) 5.742 * * * [progress]: generating series expansions 5.742 * * * * [progress]: [ 1 / 4 ] generating series at (2) 5.742 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 5.742 * * * * [progress]: [ 3 / 4 ] generating series at (2 1) 5.742 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 1) 5.742 * * * [progress]: simplifying candidates 5.742 * * * * [progress]: [ 1 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (real->posit16 1))))> 5.742 * [simplify]: Simplifying (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (real->posit16 1)) 5.742 * * [simplify]: iters left: 5 (8 enodes) 5.745 * * [simplify]: iters left: 4 (25 enodes) 5.749 * * [simplify]: iters left: 3 (58 enodes) 5.761 * * [simplify]: iters left: 2 (208 enodes) 5.881 * * [simplify]: Extracting #0: cost 1 inf + 0 5.881 * * [simplify]: Extracting #1: cost 55 inf + 0 5.882 * * [simplify]: Extracting #2: cost 224 inf + 0 5.885 * * [simplify]: Extracting #3: cost 210 inf + 64538 5.897 * * [simplify]: Extracting #4: cost 41 inf + 304741 5.923 * * [simplify]: Extracting #5: cost 7 inf + 347995 5.956 * * [simplify]: Extracting #6: cost 0 inf + 360005 5.974 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) 5.974 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) x)) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))))) 5.974 * * * * [progress]: [ 2 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))))) (*.p16 (real->posit16 1) (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))))))> 5.975 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1)))) 5.975 * * [simplify]: iters left: 5 (8 enodes) 5.978 * * [simplify]: iters left: 4 (25 enodes) 5.986 * * [simplify]: iters left: 3 (58 enodes) 6.004 * * [simplify]: iters left: 2 (206 enodes) 6.145 * * [simplify]: Extracting #0: cost 1 inf + 0 6.145 * * [simplify]: Extracting #1: cost 55 inf + 0 6.146 * * [simplify]: Extracting #2: cost 223 inf + 0 6.150 * * [simplify]: Extracting #3: cost 221 inf + 52354 6.170 * * [simplify]: Extracting #4: cost 48 inf + 288081 6.191 * * [simplify]: Extracting #5: cost 5 inf + 349034 6.211 * * [simplify]: Extracting #6: cost 0 inf + 355762 6.243 * * [simplify]: Extracting #7: cost 0 inf + 355642 6.271 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) 6.271 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))))) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))))) 6.271 * * * * [progress]: [ 3 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))))))> 6.271 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.271 * * [simplify]: iters left: 3 (5 enodes) 6.273 * * [simplify]: iters left: 2 (11 enodes) 6.275 * * [simplify]: iters left: 1 (13 enodes) 6.277 * * [simplify]: Extracting #0: cost 1 inf + 0 6.277 * * [simplify]: Extracting #1: cost 3 inf + 0 6.277 * * [simplify]: Extracting #2: cost 5 inf + 0 6.277 * * [simplify]: Extracting #3: cost 3 inf + 2 6.277 * * [simplify]: Extracting #4: cost 0 inf + 527 6.277 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.277 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))) 6.277 * * * * [progress]: [ 4 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))))))> 6.277 * [simplify]: Simplifying (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) 6.277 * * [simplify]: iters left: 3 (5 enodes) 6.278 * * [simplify]: iters left: 2 (11 enodes) 6.280 * * [simplify]: iters left: 1 (13 enodes) 6.283 * * [simplify]: Extracting #0: cost 1 inf + 0 6.284 * * [simplify]: Extracting #1: cost 3 inf + 0 6.284 * * [simplify]: Extracting #2: cost 5 inf + 0 6.284 * * [simplify]: Extracting #3: cost 3 inf + 2 6.284 * * [simplify]: Extracting #4: cost 0 inf + 527 6.284 * [simplify]: Simplified to (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) 6.284 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (-.p16 (/.p16 (real->posit16 2) x) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))) 6.284 * * * * [progress]: [ 5 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 6.284 * * * * [progress]: [ 6 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) x) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (real->posit16 1)))))> 6.284 * [simplify]: Simplifying (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (real->posit16 1)) 6.284 * * [simplify]: iters left: 5 (8 enodes) 6.286 * * [simplify]: iters left: 4 (25 enodes) 6.291 * * [simplify]: iters left: 3 (58 enodes) 6.308 * * [simplify]: iters left: 2 (208 enodes) 6.451 * * [simplify]: Extracting #0: cost 1 inf + 0 6.451 * * [simplify]: Extracting #1: cost 55 inf + 0 6.452 * * [simplify]: Extracting #2: cost 224 inf + 0 6.458 * * [simplify]: Extracting #3: cost 210 inf + 64538 6.471 * * [simplify]: Extracting #4: cost 41 inf + 304741 6.489 * * [simplify]: Extracting #5: cost 7 inf + 347995 6.512 * * [simplify]: Extracting #6: cost 0 inf + 360005 6.540 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) 6.540 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) x) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x)))))) 6.540 * * * * [progress]: [ 7 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 x (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1)))) (*.p16 (real->posit16 1) (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1)))))))> 6.541 * [simplify]: Simplifying (*.p16 (real->posit16 1) (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1)))) 6.541 * * [simplify]: iters left: 5 (8 enodes) 6.543 * * [simplify]: iters left: 4 (25 enodes) 6.548 * * [simplify]: iters left: 3 (58 enodes) 6.560 * * [simplify]: iters left: 2 (206 enodes) 6.659 * * [simplify]: Extracting #0: cost 1 inf + 0 6.659 * * [simplify]: Extracting #1: cost 55 inf + 0 6.660 * * [simplify]: Extracting #2: cost 223 inf + 0 6.662 * * [simplify]: Extracting #3: cost 221 inf + 52354 6.675 * * [simplify]: Extracting #4: cost 48 inf + 288081 6.700 * * [simplify]: Extracting #5: cost 5 inf + 349034 6.717 * * [simplify]: Extracting #6: cost 0 inf + 355762 6.734 * * [simplify]: Extracting #7: cost 0 inf + 355642 6.753 * [simplify]: Simplified to (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) 6.753 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (*.p16 x (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1)))) (/.p16 (*.p16 (real->posit16 1) (real->posit16 1)) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x)))))) 6.753 * * * * [progress]: [ 8 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (*.p16 (+.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1))))))> 6.753 * [simplify]: Simplifying (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 6.753 * * [simplify]: iters left: 4 (9 enodes) 6.756 * * [simplify]: iters left: 3 (26 enodes) 6.761 * * [simplify]: iters left: 2 (67 enodes) 6.780 * * [simplify]: iters left: 1 (216 enodes) 6.900 * * [simplify]: Extracting #0: cost 1 inf + 0 6.900 * * [simplify]: Extracting #1: cost 48 inf + 0 6.900 * * [simplify]: Extracting #2: cost 223 inf + 0 6.905 * * [simplify]: Extracting #3: cost 283 inf + 35278 6.916 * * [simplify]: Extracting #4: cost 95 inf + 329500 6.937 * * [simplify]: Extracting #5: cost 7 inf + 486011 6.960 * * [simplify]: Extracting #6: cost 0 inf + 501141 6.986 * [simplify]: Simplified to (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (*.p16 (+.p16 (real->posit16 1) x) (+.p16 (real->posit16 1) x)))) 6.986 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (*.p16 (+.p16 (real->posit16 1) x) (+.p16 (real->posit16 1) x)))) (*.p16 (+.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1)))))) 6.986 * * * * [progress]: [ 9 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1)))))> 6.987 * [simplify]: Simplifying (*.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))) 6.987 * * [simplify]: iters left: 4 (6 enodes) 6.990 * * [simplify]: iters left: 3 (21 enodes) 6.998 * * [simplify]: iters left: 2 (39 enodes) 7.012 * * [simplify]: iters left: 1 (46 enodes) 7.025 * * [simplify]: Extracting #0: cost 1 inf + 0 7.025 * * [simplify]: Extracting #1: cost 8 inf + 0 7.025 * * [simplify]: Extracting #2: cost 14 inf + 1 7.025 * * [simplify]: Extracting #3: cost 11 inf + 4 7.026 * * [simplify]: Extracting #4: cost 4 inf + 2016 7.026 * * [simplify]: Extracting #5: cost 0 inf + 4584 7.027 * [simplify]: Simplified to (real->posit16 1) 7.027 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) 7.027 * * * * [progress]: [ 10 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (+.p16 x (real->posit16 1)) (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))))))> 7.027 * * * * [progress]: [ 11 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x))) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 7.027 * * * * [progress]: [ 12 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 7.028 * * * * [progress]: [ 13 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 7.028 * [simplify]: Simplifying (+.p16 x (real->posit16 1)) 7.028 * * [simplify]: iters left: 2 (4 enodes) 7.030 * * [simplify]: iters left: 1 (10 enodes) 7.034 * * [simplify]: Extracting #0: cost 1 inf + 0 7.034 * * [simplify]: Extracting #1: cost 3 inf + 0 7.034 * * [simplify]: Extracting #2: cost 3 inf + 1 7.034 * * [simplify]: Extracting #3: cost 0 inf + 45 7.035 * [simplify]: Simplified to (+.p16 (real->posit16 1) x) 7.035 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 (real->posit16 1) x)) (+.p16 x (real->posit16 1))))) 7.035 * * * * [progress]: [ 14 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1)))))> 7.037 * [simplify]: Simplifying (real->posit16 1) 7.037 * * [simplify]: iters left: 1 (2 enodes) 7.038 * * [simplify]: Extracting #0: cost 1 inf + 0 7.038 * * [simplify]: Extracting #1: cost 2 inf + 0 7.039 * * [simplify]: Extracting #2: cost 1 inf + 1 7.039 * * [simplify]: Extracting #3: cost 0 inf + 2 7.039 * [simplify]: Simplified to (real->posit16 1) 7.039 * [simplify]: Simplified (2 2 1 1) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1)))) (+.p16 x (real->posit16 1))))) 7.039 * * * * [progress]: [ 15 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 7.039 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 7.039 * * [simplify]: iters left: 2 (4 enodes) 7.042 * * [simplify]: iters left: 1 (16 enodes) 7.048 * * [simplify]: Extracting #0: cost 1 inf + 0 7.048 * * [simplify]: Extracting #1: cost 6 inf + 0 7.048 * * [simplify]: Extracting #2: cost 11 inf + 1 7.048 * * [simplify]: Extracting #3: cost 11 inf + 323 7.048 * * [simplify]: Extracting #4: cost 5 inf + 1491 7.049 * * [simplify]: Extracting #5: cost 1 inf + 3657 7.049 * * [simplify]: Extracting #6: cost 0 inf + 5019 7.049 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 7.049 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))))) 7.050 * * * * [progress]: [ 16 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 7.050 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 7.050 * * [simplify]: iters left: 2 (4 enodes) 7.052 * * [simplify]: iters left: 1 (16 enodes) 7.059 * * [simplify]: Extracting #0: cost 1 inf + 0 7.059 * * [simplify]: Extracting #1: cost 6 inf + 0 7.059 * * [simplify]: Extracting #2: cost 11 inf + 1 7.059 * * [simplify]: Extracting #3: cost 11 inf + 323 7.059 * * [simplify]: Extracting #4: cost 5 inf + 1491 7.059 * * [simplify]: Extracting #5: cost 1 inf + 3657 7.060 * * [simplify]: Extracting #6: cost 0 inf + 5019 7.060 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 7.060 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))))) 7.060 * * * * [progress]: [ 17 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 7.061 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 7.061 * * [simplify]: iters left: 2 (4 enodes) 7.063 * * [simplify]: iters left: 1 (16 enodes) 7.068 * * [simplify]: Extracting #0: cost 1 inf + 0 7.068 * * [simplify]: Extracting #1: cost 6 inf + 0 7.068 * * [simplify]: Extracting #2: cost 11 inf + 1 7.068 * * [simplify]: Extracting #3: cost 11 inf + 323 7.068 * * [simplify]: Extracting #4: cost 5 inf + 1491 7.069 * * [simplify]: Extracting #5: cost 1 inf + 3657 7.069 * * [simplify]: Extracting #6: cost 0 inf + 5019 7.069 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 7.069 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))))) 7.070 * * * * [progress]: [ 18 / 18 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> 7.070 * [simplify]: Simplifying (-.p16 x (real->posit16 1)) 7.070 * * [simplify]: iters left: 2 (4 enodes) 7.072 * * [simplify]: iters left: 1 (16 enodes) 7.077 * * [simplify]: Extracting #0: cost 1 inf + 0 7.077 * * [simplify]: Extracting #1: cost 6 inf + 0 7.077 * * [simplify]: Extracting #2: cost 11 inf + 1 7.077 * * [simplify]: Extracting #3: cost 11 inf + 323 7.077 * * [simplify]: Extracting #4: cost 5 inf + 1491 7.078 * * [simplify]: Extracting #5: cost 1 inf + 3657 7.078 * * [simplify]: Extracting #6: cost 0 inf + 5019 7.078 * [simplify]: Simplified to (-.p16 x (real->posit16 1)) 7.078 * [simplify]: Simplified (2 2 1 2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1))))) 7.079 * * * [progress]: adding candidates to table 8.406 * [progress]: [Phase 3 of 3] Extracting. 8.407 * * [regime]: Finding splitpoints for: (#posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (-.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (*.p16 (+.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))))) (*.p16 (real->posit16 1) (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))>) 8.410 * * * [regime-changes]: Trying 1 branch expressions: (x) 8.410 * * * * [regimes]: Trying to branch on x from (#posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (-.p16 (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (*.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (*.p16 (+.p16 x (real->posit16 1)) (+.p16 x (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))) (*.p16 (real->posit16 1) (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 x (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))))) (*.p16 (real->posit16 1) (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (*.p16 (/.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 x (real->posit16 1))) (+.p16 x (real->posit16 1)))))> #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (*.p16 (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))>) 8.666 * * * [regime]: Found split indices: #