0.002 * [progress]: [Phase 1 of 3] Setting up. 0.002 * * * [progress]: [1/2] Preparing points 0.002 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.003 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.007 * * * * [points]: Setting MPFR precision to 64 0.008 * * * * [points]: Setting MPFR precision to 320 0.010 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.015 * * * * [points]: Setting MPFR precision to 64 0.017 * * * * [points]: Setting MPFR precision to 320 0.020 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.025 * * * * [points]: Setting MPFR precision to 64 0.029 * * * * [points]: Setting MPFR precision to 320 0.034 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.038 * * * * [points]: Setting MPFR precision to 64 0.047 * * * * [points]: Setting MPFR precision to 320 0.055 * * * * [points]: Computing exacts for 256 points 0.060 * * * * [points]: Setting MPFR precision to 64 0.083 * * * * [points]: Setting MPFR precision to 320 0.109 * * * * [points]: Filtering points with unrepresentable outputs 0.109 * * * * [points]: Sampled 256 points with exact outputs 0.110 * * * [progress]: [2/2] Setting up program. 0.135 * [progress]: [Phase 2 of 3] Improving. 0.135 * * * * [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.135 * [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.135 * * [simplify]: iters left: 5 (12 enodes) 0.142 * * [simplify]: iters left: 4 (35 enodes) 0.155 * * [simplify]: iters left: 3 (83 enodes) 0.211 * * [simplify]: iters left: 2 (233 enodes) 0.352 * * [simplify]: Extracting #0: cost 1 inf + 0 0.352 * * [simplify]: Extracting #1: cost 29 inf + 0 0.352 * * [simplify]: Extracting #2: cost 123 inf + 0 0.354 * * [simplify]: Extracting #3: cost 245 inf + 1 0.358 * * [simplify]: Extracting #4: cost 303 inf + 42876 0.383 * * [simplify]: Extracting #5: cost 128 inf + 332692 0.405 * * [simplify]: Extracting #6: cost 5 inf + 548531 0.437 * * [simplify]: Extracting #7: cost 0 inf + 561504 0.464 * [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.464 * [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.477 * * [progress]: iteration 1 / 4 0.477 * * * [progress]: picking best candidate 0.490 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))> 0.490 * * * [progress]: localizing error 0.675 * * * [progress]: generating rewritten candidates 0.675 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 0.692 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 0.695 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2) 0.697 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 0.699 * * * [progress]: generating series expansions 0.699 * * * * [progress]: [ 1 / 4 ] generating series at (2) 0.699 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 0.699 * * * * [progress]: [ 3 / 4 ] generating series at (2 2) 0.699 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 0.699 * * * [progress]: simplifying candidates 0.699 * * * * [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.699 * [simplify]: Simplifying (+.p16 (neg.p16 (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 0.699 * * [simplify]: iters left: 4 (10 enodes) 0.702 * * [simplify]: iters left: 3 (24 enodes) 0.707 * * [simplify]: iters left: 2 (39 enodes) 0.720 * * [simplify]: iters left: 1 (92 enodes) 0.743 * * [simplify]: Extracting #0: cost 1 inf + 0 0.744 * * [simplify]: Extracting #1: cost 14 inf + 0 0.744 * * [simplify]: Extracting #2: cost 53 inf + 0 0.744 * * [simplify]: Extracting #3: cost 105 inf + 1 0.744 * * [simplify]: Extracting #4: cost 125 inf + 2937 0.746 * * [simplify]: Extracting #5: cost 77 inf + 54218 0.752 * * [simplify]: Extracting #6: cost 4 inf + 155356 0.758 * * [simplify]: Extracting #7: cost 0 inf + 161603 0.764 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) 0.764 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))) 0.764 * * * * [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.764 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 0.764 * * [simplify]: iters left: 4 (9 enodes) 0.767 * * [simplify]: iters left: 3 (29 enodes) 0.772 * * [simplify]: iters left: 2 (61 enodes) 0.786 * * [simplify]: iters left: 1 (176 enodes) 0.850 * * [simplify]: Extracting #0: cost 1 inf + 0 0.850 * * [simplify]: Extracting #1: cost 19 inf + 0 0.850 * * [simplify]: Extracting #2: cost 92 inf + 0 0.850 * * [simplify]: Extracting #3: cost 209 inf + 1 0.852 * * [simplify]: Extracting #4: cost 274 inf + 27837 0.862 * * [simplify]: Extracting #5: cost 126 inf + 242865 0.879 * * [simplify]: Extracting #6: cost 12 inf + 434225 0.897 * * [simplify]: Extracting #7: cost 0 inf + 454288 0.916 * * [simplify]: Extracting #8: cost 0 inf + 452848 0.934 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 0.935 * [simplify]: Simplified (2 2) to (λ (x) (-.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)))))) 0.935 * * * * [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.935 * * * * [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.935 * [simplify]: Simplifying (neg.p16 (/.p16 (real->posit16 2) x)) 0.935 * * [simplify]: iters left: 3 (5 enodes) 0.936 * * [simplify]: iters left: 2 (8 enodes) 0.938 * * [simplify]: Extracting #0: cost 1 inf + 0 0.938 * * [simplify]: Extracting #1: cost 2 inf + 0 0.938 * * [simplify]: Extracting #2: cost 4 inf + 0 0.938 * * [simplify]: Extracting #3: cost 4 inf + 1 0.938 * * [simplify]: Extracting #4: cost 3 inf + 2 0.938 * * [simplify]: Extracting #5: cost 0 inf + 967 0.938 * [simplify]: Simplified to (neg.p16 (/.p16 (real->posit16 2) x)) 0.938 * [simplify]: Simplified (2 1 2) to (λ (x) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) 0.938 * * * * [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.938 * [simplify]: Simplifying (-.p16 (*.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 2) x))) 0.938 * * [simplify]: iters left: 5 (11 enodes) 0.941 * * [simplify]: iters left: 4 (36 enodes) 0.952 * * [simplify]: iters left: 3 (89 enodes) 0.984 * * [simplify]: iters left: 2 (268 enodes) 1.079 * * [simplify]: Extracting #0: cost 1 inf + 0 1.080 * * [simplify]: Extracting #1: cost 32 inf + 0 1.080 * * [simplify]: Extracting #2: cost 176 inf + 0 1.081 * * [simplify]: Extracting #3: cost 275 inf + 324 1.084 * * [simplify]: Extracting #4: cost 315 inf + 68062 1.098 * * [simplify]: Extracting #5: cost 125 inf + 399064 1.131 * * [simplify]: Extracting #6: cost 16 inf + 636428 1.168 * * [simplify]: Extracting #7: cost 0 inf + 675596 1.229 * * [simplify]: Extracting #8: cost 0 inf + 672836 1.287 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) 1.288 * [simplify]: Simplified (2 1 1) to (λ (x) (+.p16 (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) 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))))) 1.288 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) 1.288 * * [simplify]: iters left: 4 (9 enodes) 1.291 * * [simplify]: iters left: 3 (17 enodes) 1.293 * * [simplify]: iters left: 2 (19 enodes) 1.296 * * [simplify]: Extracting #0: cost 1 inf + 0 1.296 * * [simplify]: Extracting #1: cost 3 inf + 0 1.296 * * [simplify]: Extracting #2: cost 7 inf + 0 1.296 * * [simplify]: Extracting #3: cost 8 inf + 1 1.297 * * [simplify]: Extracting #4: cost 4 inf + 446 1.297 * * [simplify]: Extracting #5: cost 0 inf + 1934 1.297 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x)) 1.297 * [simplify]: Simplified (2 1 2) to (λ (x) (+.p16 (/.p16 (-.p16 (*.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 2) x))) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 2) x))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) 1.297 * * * * [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)))))> 1.297 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 1.297 * * [simplify]: iters left: 4 (7 enodes) 1.299 * * [simplify]: iters left: 3 (22 enodes) 1.303 * * [simplify]: iters left: 2 (51 enodes) 1.313 * * [simplify]: iters left: 1 (144 enodes) 1.365 * * [simplify]: Extracting #0: cost 1 inf + 0 1.365 * * [simplify]: Extracting #1: cost 39 inf + 0 1.366 * * [simplify]: Extracting #2: cost 153 inf + 0 1.366 * * [simplify]: Extracting #3: cost 211 inf + 3295 1.369 * * [simplify]: Extracting #4: cost 172 inf + 64546 1.376 * * [simplify]: Extracting #5: cost 61 inf + 217069 1.388 * * [simplify]: Extracting #6: cost 12 inf + 304548 1.402 * * [simplify]: Extracting #7: cost 0 inf + 337212 1.416 * * [simplify]: Extracting #8: cost 0 inf + 336932 1.435 * [simplify]: Simplified to (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) 1.435 * [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 (real->posit16 1) x))) (+.p16 x (real->posit16 1))))) 1.436 * * * * [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)))))> 1.436 * [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.436 * * [simplify]: iters left: 5 (12 enodes) 1.442 * * [simplify]: iters left: 4 (35 enodes) 1.454 * * [simplify]: iters left: 3 (83 enodes) 1.473 * * [simplify]: iters left: 2 (233 enodes) 1.558 * * [simplify]: Extracting #0: cost 1 inf + 0 1.558 * * [simplify]: Extracting #1: cost 29 inf + 0 1.558 * * [simplify]: Extracting #2: cost 123 inf + 0 1.559 * * [simplify]: Extracting #3: cost 245 inf + 1 1.561 * * [simplify]: Extracting #4: cost 303 inf + 42876 1.573 * * [simplify]: Extracting #5: cost 128 inf + 332692 1.595 * * [simplify]: Extracting #6: cost 5 inf + 548531 1.622 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.647 * [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.647 * [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.647 * * * * [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)))))> 1.647 * [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.647 * * [simplify]: iters left: 5 (12 enodes) 1.651 * * [simplify]: iters left: 4 (35 enodes) 1.657 * * [simplify]: iters left: 3 (83 enodes) 1.674 * * [simplify]: iters left: 2 (233 enodes) 1.741 * * [simplify]: Extracting #0: cost 1 inf + 0 1.742 * * [simplify]: Extracting #1: cost 29 inf + 0 1.742 * * [simplify]: Extracting #2: cost 123 inf + 0 1.742 * * [simplify]: Extracting #3: cost 245 inf + 1 1.745 * * [simplify]: Extracting #4: cost 303 inf + 42876 1.760 * * [simplify]: Extracting #5: cost 128 inf + 332692 1.785 * * [simplify]: Extracting #6: cost 5 inf + 548531 1.831 * * [simplify]: Extracting #7: cost 0 inf + 561504 1.875 * [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.875 * [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.875 * * * * [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)))))> 1.876 * [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.876 * * [simplify]: iters left: 5 (12 enodes) 1.881 * * [simplify]: iters left: 4 (35 enodes) 1.892 * * [simplify]: iters left: 3 (83 enodes) 1.919 * * [simplify]: iters left: 2 (233 enodes) 2.013 * * [simplify]: Extracting #0: cost 1 inf + 0 2.013 * * [simplify]: Extracting #1: cost 29 inf + 0 2.013 * * [simplify]: Extracting #2: cost 123 inf + 0 2.014 * * [simplify]: Extracting #3: cost 245 inf + 1 2.016 * * [simplify]: Extracting #4: cost 303 inf + 42876 2.028 * * [simplify]: Extracting #5: cost 128 inf + 332692 2.054 * * [simplify]: Extracting #6: cost 5 inf + 548531 2.096 * * [simplify]: Extracting #7: cost 0 inf + 561504 2.128 * [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))) 2.128 * [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)))) 2.128 * * * * [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)))))> 2.128 * [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)))) 2.128 * * [simplify]: iters left: 5 (12 enodes) 2.132 * * [simplify]: iters left: 4 (35 enodes) 2.138 * * [simplify]: iters left: 3 (83 enodes) 2.160 * * [simplify]: iters left: 2 (233 enodes) 2.244 * * [simplify]: Extracting #0: cost 1 inf + 0 2.244 * * [simplify]: Extracting #1: cost 29 inf + 0 2.244 * * [simplify]: Extracting #2: cost 123 inf + 0 2.245 * * [simplify]: Extracting #3: cost 245 inf + 1 2.247 * * [simplify]: Extracting #4: cost 303 inf + 42876 2.259 * * [simplify]: Extracting #5: cost 128 inf + 332692 2.284 * * [simplify]: Extracting #6: cost 5 inf + 548531 2.308 * * [simplify]: Extracting #7: cost 0 inf + 561504 2.332 * [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))) 2.332 * [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)))) 2.332 * * * [progress]: adding candidates to table 2.586 * * [progress]: iteration 2 / 4 2.586 * * * [progress]: picking best candidate 2.624 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 2.624 * * * [progress]: localizing error 2.813 * * * [progress]: generating rewritten candidates 2.814 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 2.820 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 2.824 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 1) 2.825 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1) 2.828 * * * [progress]: generating series expansions 2.828 * * * * [progress]: [ 1 / 4 ] generating series at (2) 2.828 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 2.828 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 1) 2.828 * * * * [progress]: [ 4 / 4 ] generating series at (2 1) 2.828 * * * [progress]: simplifying candidates 2.828 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x))))> 2.828 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 2.828 * * [simplify]: iters left: 4 (8 enodes) 2.831 * * [simplify]: iters left: 3 (21 enodes) 2.834 * * [simplify]: iters left: 2 (34 enodes) 2.840 * * [simplify]: iters left: 1 (81 enodes) 2.860 * * [simplify]: Extracting #0: cost 1 inf + 0 2.860 * * [simplify]: Extracting #1: cost 9 inf + 0 2.861 * * [simplify]: Extracting #2: cost 39 inf + 0 2.861 * * [simplify]: Extracting #3: cost 74 inf + 1 2.861 * * [simplify]: Extracting #4: cost 101 inf + 324 2.862 * * [simplify]: Extracting #5: cost 87 inf + 17613 2.865 * * [simplify]: Extracting #6: cost 20 inf + 89330 2.869 * * [simplify]: Extracting #7: cost 0 inf + 118249 2.874 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 2.874 * [simplify]: Simplified (2 1) to (λ (x) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x)))) 2.874 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 2.874 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 2.874 * * [simplify]: iters left: 4 (8 enodes) 2.876 * * [simplify]: iters left: 3 (21 enodes) 2.882 * * [simplify]: iters left: 2 (34 enodes) 2.889 * * [simplify]: iters left: 1 (81 enodes) 2.927 * * [simplify]: Extracting #0: cost 1 inf + 0 2.927 * * [simplify]: Extracting #1: cost 9 inf + 0 2.927 * * [simplify]: Extracting #2: cost 39 inf + 0 2.928 * * [simplify]: Extracting #3: cost 74 inf + 1 2.928 * * [simplify]: Extracting #4: cost 101 inf + 324 2.930 * * [simplify]: Extracting #5: cost 87 inf + 17613 2.936 * * [simplify]: Extracting #6: cost 20 inf + 89330 2.945 * * [simplify]: Extracting #7: cost 0 inf + 118249 2.954 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 2.954 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) 2.954 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))))> 2.954 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x)))))> 2.955 * [simplify]: Simplifying (neg.p16 (/.p16 (real->posit16 2) x)) 2.955 * * [simplify]: iters left: 3 (5 enodes) 2.957 * * [simplify]: iters left: 2 (8 enodes) 2.960 * * [simplify]: Extracting #0: cost 1 inf + 0 2.960 * * [simplify]: Extracting #1: cost 2 inf + 0 2.960 * * [simplify]: Extracting #2: cost 4 inf + 0 2.960 * * [simplify]: Extracting #3: cost 4 inf + 1 2.960 * * [simplify]: Extracting #4: cost 3 inf + 2 2.960 * * [simplify]: Extracting #5: cost 0 inf + 967 2.960 * [simplify]: Simplified to (neg.p16 (/.p16 (real->posit16 2) x)) 2.960 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (neg.p16 (/.p16 (real->posit16 2) x))))) 2.960 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (-.p16 (*.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 2) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 2.961 * [simplify]: Simplifying (-.p16 (*.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 2) x))) 2.961 * * [simplify]: iters left: 5 (11 enodes) 2.967 * * [simplify]: iters left: 4 (42 enodes) 2.983 * * [simplify]: iters left: 3 (106 enodes) 3.030 * * [simplify]: iters left: 2 (384 enodes) 3.525 * * [simplify]: Extracting #0: cost 1 inf + 0 3.525 * * [simplify]: Extracting #1: cost 44 inf + 0 3.525 * * [simplify]: Extracting #2: cost 282 inf + 0 3.527 * * [simplify]: Extracting #3: cost 571 inf + 323 3.548 * * [simplify]: Extracting #4: cost 668 inf + 221993 3.629 * * [simplify]: Extracting #5: cost 137 inf + 1242878 3.723 * * [simplify]: Extracting #6: cost 12 inf + 1494188 3.798 * * [simplify]: Extracting #7: cost 1 inf + 1521933 3.872 * * [simplify]: Extracting #8: cost 0 inf + 1524295 3.951 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 3.951 * [simplify]: Simplified (2 2 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))) 3.952 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) 3.952 * * [simplify]: iters left: 4 (9 enodes) 3.954 * * [simplify]: iters left: 3 (23 enodes) 3.958 * * [simplify]: iters left: 2 (37 enodes) 3.965 * * [simplify]: iters left: 1 (85 enodes) 3.995 * * [simplify]: Extracting #0: cost 1 inf + 0 3.995 * * [simplify]: Extracting #1: cost 9 inf + 0 3.995 * * [simplify]: Extracting #2: cost 41 inf + 0 3.996 * * [simplify]: Extracting #3: cost 77 inf + 1 3.996 * * [simplify]: Extracting #4: cost 101 inf + 768 3.998 * * [simplify]: Extracting #5: cost 79 inf + 31041 4.002 * * [simplify]: Extracting #6: cost 19 inf + 89828 4.007 * * [simplify]: Extracting #7: cost 0 inf + 120780 4.011 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) 4.012 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))) 4.012 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 4.012 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 4.012 * * [simplify]: iters left: 4 (7 enodes) 4.014 * * [simplify]: iters left: 3 (22 enodes) 4.019 * * [simplify]: iters left: 2 (51 enodes) 4.029 * * [simplify]: iters left: 1 (144 enodes) 4.077 * * [simplify]: Extracting #0: cost 1 inf + 0 4.077 * * [simplify]: Extracting #1: cost 39 inf + 0 4.077 * * [simplify]: Extracting #2: cost 153 inf + 0 4.078 * * [simplify]: Extracting #3: cost 211 inf + 3295 4.083 * * [simplify]: Extracting #4: cost 172 inf + 64546 4.090 * * [simplify]: Extracting #5: cost 61 inf + 217069 4.102 * * [simplify]: Extracting #6: cost 12 inf + 304548 4.116 * * [simplify]: Extracting #7: cost 0 inf + 337212 4.130 * * [simplify]: Extracting #8: cost 0 inf + 336932 4.144 * [simplify]: Simplified to (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) 4.144 * [simplify]: Simplified (2 2 1 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))) 4.144 * * * * [progress]: [ 7 / 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))))> 4.144 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 4.144 * * [simplify]: iters left: 5 (12 enodes) 4.147 * * [simplify]: iters left: 4 (35 enodes) 4.155 * * [simplify]: iters left: 3 (76 enodes) 4.183 * * [simplify]: iters left: 2 (223 enodes) 4.323 * * [simplify]: Extracting #0: cost 1 inf + 0 4.323 * * [simplify]: Extracting #1: cost 28 inf + 0 4.323 * * [simplify]: Extracting #2: cost 117 inf + 0 4.324 * * [simplify]: Extracting #3: cost 257 inf + 1 4.326 * * [simplify]: Extracting #4: cost 323 inf + 44438 4.339 * * [simplify]: Extracting #5: cost 135 inf + 398457 4.365 * * [simplify]: Extracting #6: cost 3 inf + 632314 4.395 * * [simplify]: Extracting #7: cost 0 inf + 638479 4.423 * [simplify]: Simplified to (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 4.423 * [simplify]: Simplified (2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) 4.423 * * * * [progress]: [ 8 / 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))))> 4.424 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 4.424 * * [simplify]: iters left: 5 (12 enodes) 4.427 * * [simplify]: iters left: 4 (35 enodes) 4.434 * * [simplify]: iters left: 3 (76 enodes) 4.449 * * [simplify]: iters left: 2 (223 enodes) 4.556 * * [simplify]: Extracting #0: cost 1 inf + 0 4.556 * * [simplify]: Extracting #1: cost 28 inf + 0 4.556 * * [simplify]: Extracting #2: cost 117 inf + 0 4.558 * * [simplify]: Extracting #3: cost 257 inf + 1 4.562 * * [simplify]: Extracting #4: cost 323 inf + 44438 4.587 * * [simplify]: Extracting #5: cost 135 inf + 398457 4.612 * * [simplify]: Extracting #6: cost 3 inf + 632314 4.671 * * [simplify]: Extracting #7: cost 0 inf + 638479 4.726 * [simplify]: Simplified to (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 4.726 * [simplify]: Simplified (2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) 4.726 * * * * [progress]: [ 9 / 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))))> 4.726 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 4.727 * * [simplify]: iters left: 5 (12 enodes) 4.732 * * [simplify]: iters left: 4 (35 enodes) 4.744 * * [simplify]: iters left: 3 (76 enodes) 4.774 * * [simplify]: iters left: 2 (223 enodes) 4.935 * * [simplify]: Extracting #0: cost 1 inf + 0 4.935 * * [simplify]: Extracting #1: cost 28 inf + 0 4.936 * * [simplify]: Extracting #2: cost 117 inf + 0 4.943 * * [simplify]: Extracting #3: cost 257 inf + 1 4.948 * * [simplify]: Extracting #4: cost 323 inf + 44438 4.975 * * [simplify]: Extracting #5: cost 135 inf + 398457 5.001 * * [simplify]: Extracting #6: cost 3 inf + 632314 5.030 * * [simplify]: Extracting #7: cost 0 inf + 638479 5.060 * [simplify]: Simplified to (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 5.061 * [simplify]: Simplified (2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) 5.061 * * * * [progress]: [ 10 / 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))))> 5.061 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 5.061 * * [simplify]: iters left: 5 (12 enodes) 5.067 * * [simplify]: iters left: 4 (35 enodes) 5.080 * * [simplify]: iters left: 3 (76 enodes) 5.100 * * [simplify]: iters left: 2 (223 enodes) 5.223 * * [simplify]: Extracting #0: cost 1 inf + 0 5.223 * * [simplify]: Extracting #1: cost 28 inf + 0 5.223 * * [simplify]: Extracting #2: cost 117 inf + 0 5.224 * * [simplify]: Extracting #3: cost 257 inf + 1 5.226 * * [simplify]: Extracting #4: cost 323 inf + 44438 5.240 * * [simplify]: Extracting #5: cost 135 inf + 398457 5.270 * * [simplify]: Extracting #6: cost 3 inf + 632314 5.297 * * [simplify]: Extracting #7: cost 0 inf + 638479 5.325 * [simplify]: Simplified to (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 5.325 * [simplify]: Simplified (2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) 5.325 * * * [progress]: adding candidates to table 5.571 * * [progress]: iteration 3 / 4 5.571 * * * [progress]: picking best candidate 5.632 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 5.632 * * * [progress]: localizing error 5.809 * * * [progress]: generating rewritten candidates 5.809 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 5.821 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1) 5.826 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2) 5.827 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1) 5.829 * * * [progress]: generating series expansions 5.829 * * * * [progress]: [ 1 / 4 ] generating series at (2) 5.829 * * * * [progress]: [ 2 / 4 ] generating series at (2 1) 5.829 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2) 5.829 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1) 5.830 * * * [progress]: simplifying candidates 5.830 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))> 5.830 * [simplify]: Simplifying (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) 5.830 * * [simplify]: iters left: 4 (9 enodes) 5.832 * * [simplify]: iters left: 3 (29 enodes) 5.838 * * [simplify]: iters left: 2 (61 enodes) 5.857 * * [simplify]: iters left: 1 (176 enodes) 5.955 * * [simplify]: Extracting #0: cost 1 inf + 0 5.955 * * [simplify]: Extracting #1: cost 23 inf + 0 5.955 * * [simplify]: Extracting #2: cost 96 inf + 0 5.956 * * [simplify]: Extracting #3: cost 222 inf + 1 5.959 * * [simplify]: Extracting #4: cost 292 inf + 16780 5.973 * * [simplify]: Extracting #5: cost 158 inf + 192060 6.005 * * [simplify]: Extracting #6: cost 13 inf + 444096 6.044 * * [simplify]: Extracting #7: cost 0 inf + 468722 6.083 * [simplify]: Simplified to (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) 6.083 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))) 6.084 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x))))> 6.084 * [simplify]: Simplifying (neg.p16 (/.p16 (real->posit16 2) x)) 6.084 * * [simplify]: iters left: 3 (5 enodes) 6.086 * * [simplify]: iters left: 2 (8 enodes) 6.089 * * [simplify]: Extracting #0: cost 1 inf + 0 6.089 * * [simplify]: Extracting #1: cost 2 inf + 0 6.089 * * [simplify]: Extracting #2: cost 4 inf + 0 6.089 * * [simplify]: Extracting #3: cost 4 inf + 1 6.089 * * [simplify]: Extracting #4: cost 3 inf + 2 6.089 * * [simplify]: Extracting #5: cost 0 inf + 967 6.089 * [simplify]: Simplified to (neg.p16 (/.p16 (real->posit16 2) x)) 6.089 * [simplify]: Simplified (2 2) to (λ (x) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (neg.p16 (/.p16 (real->posit16 2) x)))) 6.089 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.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 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> 6.089 * [simplify]: Simplifying (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.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 2) x))) 6.089 * * [simplify]: iters left: 6 (14 enodes) 6.093 * * [simplify]: iters left: 5 (48 enodes) 6.105 * * [simplify]: iters left: 4 (150 enodes) 6.160 * * [simplify]: Extracting #0: cost 1 inf + 0 6.160 * * [simplify]: Extracting #1: cost 49 inf + 0 6.161 * * [simplify]: Extracting #2: cost 130 inf + 0 6.161 * * [simplify]: Extracting #3: cost 193 inf + 322 6.163 * * [simplify]: Extracting #4: cost 180 inf + 50785 6.173 * * [simplify]: Extracting #5: cost 44 inf + 284669 6.192 * * [simplify]: Extracting #6: cost 2 inf + 367441 6.210 * * [simplify]: Extracting #7: cost 0 inf + 373166 6.227 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (real->posit16 2) x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) 6.227 * [simplify]: Simplified (2 1) to (λ (x) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 2) x) (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))))) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.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 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))) 6.227 * [simplify]: Simplifying (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) 6.227 * * [simplify]: iters left: 5 (12 enodes) 6.231 * * [simplify]: iters left: 4 (29 enodes) 6.236 * * [simplify]: iters left: 3 (48 enodes) 6.244 * * [simplify]: iters left: 2 (97 enodes) 6.268 * * [simplify]: iters left: 1 (352 enodes) 6.544 * * [simplify]: Extracting #0: cost 1 inf + 0 6.544 * * [simplify]: Extracting #1: cost 20 inf + 0 6.545 * * [simplify]: Extracting #2: cost 165 inf + 0 6.548 * * [simplify]: Extracting #3: cost 378 inf + 1 6.556 * * [simplify]: Extracting #4: cost 442 inf + 82090 6.609 * * [simplify]: Extracting #5: cost 132 inf + 584075 6.678 * * [simplify]: Extracting #6: cost 15 inf + 772937 6.721 * * [simplify]: Extracting #7: cost 1 inf + 790960 6.758 * * [simplify]: Extracting #8: cost 0 inf + 789082 6.795 * [simplify]: Simplified to (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)) 6.795 * [simplify]: Simplified (2 2) to (λ (x) (/.p16 (-.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.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 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))) 6.795 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 6.795 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (*.p16 (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 6.796 * [simplify]: Simplifying (/.p16 (real->posit16 1) (-.p16 (*.p16 x x) (*.p16 (real->posit16 1) (real->posit16 1)))) 6.796 * * [simplify]: iters left: 4 (7 enodes) 6.798 * * [simplify]: iters left: 3 (22 enodes) 6.802 * * [simplify]: iters left: 2 (51 enodes) 6.813 * * [simplify]: iters left: 1 (144 enodes) 6.909 * * [simplify]: Extracting #0: cost 1 inf + 0 6.910 * * [simplify]: Extracting #1: cost 39 inf + 0 6.910 * * [simplify]: Extracting #2: cost 153 inf + 0 6.912 * * [simplify]: Extracting #3: cost 211 inf + 3295 6.917 * * [simplify]: Extracting #4: cost 172 inf + 64546 6.936 * * [simplify]: Extracting #5: cost 61 inf + 217069 6.957 * * [simplify]: Extracting #6: cost 12 inf + 304548 6.984 * * [simplify]: Extracting #7: cost 0 inf + 337212 7.011 * * [simplify]: Extracting #8: cost 0 inf + 336932 7.039 * [simplify]: Simplified to (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) 7.039 * [simplify]: Simplified (2 1 2 1) to (λ (x) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) (+.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) 7.040 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.040 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.040 * * [simplify]: iters left: 4 (8 enodes) 7.044 * * [simplify]: iters left: 3 (21 enodes) 7.051 * * [simplify]: iters left: 2 (34 enodes) 7.064 * * [simplify]: iters left: 1 (81 enodes) 7.105 * * [simplify]: Extracting #0: cost 1 inf + 0 7.105 * * [simplify]: Extracting #1: cost 9 inf + 0 7.105 * * [simplify]: Extracting #2: cost 39 inf + 0 7.106 * * [simplify]: Extracting #3: cost 74 inf + 1 7.106 * * [simplify]: Extracting #4: cost 101 inf + 324 7.108 * * [simplify]: Extracting #5: cost 87 inf + 17613 7.114 * * [simplify]: Extracting #6: cost 20 inf + 89330 7.123 * * [simplify]: Extracting #7: cost 0 inf + 118249 7.133 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.133 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) 7.133 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.133 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.134 * * [simplify]: iters left: 4 (8 enodes) 7.138 * * [simplify]: iters left: 3 (21 enodes) 7.145 * * [simplify]: iters left: 2 (34 enodes) 7.157 * * [simplify]: iters left: 1 (81 enodes) 7.187 * * [simplify]: Extracting #0: cost 1 inf + 0 7.188 * * [simplify]: Extracting #1: cost 9 inf + 0 7.188 * * [simplify]: Extracting #2: cost 39 inf + 0 7.188 * * [simplify]: Extracting #3: cost 74 inf + 1 7.188 * * [simplify]: Extracting #4: cost 101 inf + 324 7.189 * * [simplify]: Extracting #5: cost 87 inf + 17613 7.192 * * [simplify]: Extracting #6: cost 20 inf + 89330 7.197 * * [simplify]: Extracting #7: cost 0 inf + 118249 7.203 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.203 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) 7.203 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.204 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.204 * * [simplify]: iters left: 4 (8 enodes) 7.206 * * [simplify]: iters left: 3 (21 enodes) 7.211 * * [simplify]: iters left: 2 (34 enodes) 7.222 * * [simplify]: iters left: 1 (81 enodes) 7.260 * * [simplify]: Extracting #0: cost 1 inf + 0 7.260 * * [simplify]: Extracting #1: cost 9 inf + 0 7.260 * * [simplify]: Extracting #2: cost 39 inf + 0 7.261 * * [simplify]: Extracting #3: cost 74 inf + 1 7.261 * * [simplify]: Extracting #4: cost 101 inf + 324 7.263 * * [simplify]: Extracting #5: cost 87 inf + 17613 7.269 * * [simplify]: Extracting #6: cost 20 inf + 89330 7.278 * * [simplify]: Extracting #7: cost 0 inf + 118249 7.284 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.284 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) 7.284 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> 7.285 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.285 * * [simplify]: iters left: 4 (8 enodes) 7.287 * * [simplify]: iters left: 3 (21 enodes) 7.291 * * [simplify]: iters left: 2 (34 enodes) 7.297 * * [simplify]: iters left: 1 (81 enodes) 7.319 * * [simplify]: Extracting #0: cost 1 inf + 0 7.319 * * [simplify]: Extracting #1: cost 9 inf + 0 7.319 * * [simplify]: Extracting #2: cost 39 inf + 0 7.319 * * [simplify]: Extracting #3: cost 74 inf + 1 7.320 * * [simplify]: Extracting #4: cost 101 inf + 324 7.320 * * [simplify]: Extracting #5: cost 87 inf + 17613 7.323 * * [simplify]: Extracting #6: cost 20 inf + 89330 7.328 * * [simplify]: Extracting #7: cost 0 inf + 118249 7.333 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) 7.333 * [simplify]: Simplified (2 1) to (λ (x) (-.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))) 7.333 * * * [progress]: adding candidates to table 7.542 * * [progress]: iteration 4 / 4 7.542 * * * [progress]: picking best candidate 7.657 * * * * [pick]: Picked #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 7.657 * * * [progress]: localizing error 8.114 * * * [progress]: generating rewritten candidates 8.114 * * * * [progress]: [ 1 / 4 ] rewriting at (2) 8.132 * * * * [progress]: [ 2 / 4 ] rewriting at (2 2) 8.155 * * * * [progress]: [ 3 / 4 ] rewriting at (2 2 1 1) 8.162 * * * * [progress]: [ 4 / 4 ] rewriting at (2 2 2) 8.174 * * * [progress]: generating series expansions 8.174 * * * * [progress]: [ 1 / 4 ] generating series at (2) 8.175 * * * * [progress]: [ 2 / 4 ] generating series at (2 2) 8.175 * * * * [progress]: [ 3 / 4 ] generating series at (2 2 1 1) 8.175 * * * * [progress]: [ 4 / 4 ] generating series at (2 2 2) 8.175 * * * [progress]: simplifying candidates 8.175 * * * * [progress]: [ 1 / 10 ] 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 (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)))))> 8.175 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.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 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))))> 8.175 * [simplify]: Simplifying (/.p16 (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 8.175 * * [simplify]: iters left: 5 (10 enodes) 8.181 * * [simplify]: iters left: 4 (26 enodes) 8.190 * * [simplify]: iters left: 3 (41 enodes) 8.204 * * [simplify]: iters left: 2 (89 enodes) 8.250 * * [simplify]: iters left: 1 (310 enodes) 8.500 * * [simplify]: Extracting #0: cost 1 inf + 0 8.500 * * [simplify]: Extracting #1: cost 4 inf + 0 8.500 * * [simplify]: Extracting #2: cost 13 inf + 1 8.500 * * [simplify]: Extracting #3: cost 134 inf + 3 8.501 * * [simplify]: Extracting #4: cost 332 inf + 10277 8.505 * * [simplify]: Extracting #5: cost 437 inf + 47353 8.515 * * [simplify]: Extracting #6: cost 328 inf + 194744 8.541 * * [simplify]: Extracting #7: cost 77 inf + 584324 8.573 * * [simplify]: Extracting #8: cost 2 inf + 730337 8.606 * * [simplify]: Extracting #9: cost 0 inf + 736701 8.641 * [simplify]: Simplified to (real->posit16 1.0) 8.641 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (real->posit16 1.0)))) 8.641 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (*.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 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 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))))> 8.642 * [simplify]: Simplifying (*.p16 (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 8.642 * * [simplify]: iters left: 5 (10 enodes) 8.645 * * [simplify]: iters left: 4 (30 enodes) 8.652 * * [simplify]: iters left: 3 (66 enodes) 8.669 * * [simplify]: iters left: 2 (190 enodes) 8.724 * * [simplify]: Extracting #0: cost 1 inf + 0 8.724 * * [simplify]: Extracting #1: cost 10 inf + 0 8.724 * * [simplify]: Extracting #2: cost 100 inf + 0 8.725 * * [simplify]: Extracting #3: cost 199 inf + 1 8.726 * * [simplify]: Extracting #4: cost 189 inf + 28846 8.734 * * [simplify]: Extracting #5: cost 64 inf + 216208 8.746 * * [simplify]: Extracting #6: cost 4 inf + 312461 8.759 * * [simplify]: Extracting #7: cost 0 inf + 316865 8.774 * [simplify]: Simplified to (*.p16 (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 8.775 * [simplify]: Simplified (2 2 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (*.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 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 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))) 8.775 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (neg.p16 (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 8.775 * [simplify]: Simplifying (neg.p16 (/.p16 (real->posit16 2) x)) 8.775 * * [simplify]: iters left: 3 (5 enodes) 8.777 * * [simplify]: iters left: 2 (8 enodes) 8.778 * * [simplify]: Extracting #0: cost 1 inf + 0 8.778 * * [simplify]: Extracting #1: cost 2 inf + 0 8.778 * * [simplify]: Extracting #2: cost 4 inf + 0 8.778 * * [simplify]: Extracting #3: cost 4 inf + 1 8.778 * * [simplify]: Extracting #4: cost 3 inf + 2 8.778 * * [simplify]: Extracting #5: cost 0 inf + 967 8.778 * [simplify]: Simplified to (neg.p16 (/.p16 (real->posit16 2) x)) 8.778 * [simplify]: Simplified (2 2 1 1 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (neg.p16 (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))) 8.778 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (/.p16 (-.p16 (*.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 2) x))) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 8.778 * [simplify]: Simplifying (-.p16 (*.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 2) x))) 8.779 * * [simplify]: iters left: 5 (11 enodes) 8.782 * * [simplify]: iters left: 4 (42 enodes) 8.790 * * [simplify]: iters left: 3 (106 enodes) 8.815 * * [simplify]: iters left: 2 (384 enodes) 9.252 * * [simplify]: Extracting #0: cost 1 inf + 0 9.252 * * [simplify]: Extracting #1: cost 44 inf + 0 9.254 * * [simplify]: Extracting #2: cost 282 inf + 0 9.258 * * [simplify]: Extracting #3: cost 571 inf + 323 9.275 * * [simplify]: Extracting #4: cost 668 inf + 221993 9.370 * * [simplify]: Extracting #5: cost 137 inf + 1242878 9.515 * * [simplify]: Extracting #6: cost 12 inf + 1494188 9.628 * * [simplify]: Extracting #7: cost 1 inf + 1521933 9.774 * * [simplify]: Extracting #8: cost 0 inf + 1524295 9.918 * [simplify]: Simplified to (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) 9.918 * [simplify]: Simplified (2 2 1 1 1) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))) 9.918 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) 9.918 * * [simplify]: iters left: 4 (9 enodes) 9.923 * * [simplify]: iters left: 3 (23 enodes) 9.932 * * [simplify]: iters left: 2 (37 enodes) 9.946 * * [simplify]: iters left: 1 (85 enodes) 9.989 * * [simplify]: Extracting #0: cost 1 inf + 0 9.989 * * [simplify]: Extracting #1: cost 9 inf + 0 9.989 * * [simplify]: Extracting #2: cost 41 inf + 0 9.990 * * [simplify]: Extracting #3: cost 77 inf + 1 9.991 * * [simplify]: Extracting #4: cost 101 inf + 768 9.993 * * [simplify]: Extracting #5: cost 79 inf + 31041 9.999 * * [simplify]: Extracting #6: cost 19 inf + 89828 10.009 * * [simplify]: Extracting #7: cost 0 inf + 120780 10.018 * [simplify]: Simplified to (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) 10.018 * [simplify]: Simplified (2 2 1 1 2) to (λ (x) (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))) 10.019 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))) (+.p16 (/.p16 (real->posit16 2) x) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))))> 10.019 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 10.019 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))) 10.019 * * [simplify]: iters left: 6 (15 enodes) 10.026 * * [simplify]: iters left: 5 (45 enodes) 10.044 * * [simplify]: iters left: 4 (137 enodes) 10.146 * * [simplify]: Extracting #0: cost 1 inf + 0 10.146 * * [simplify]: Extracting #1: cost 11 inf + 0 10.146 * * [simplify]: Extracting #2: cost 39 inf + 0 10.147 * * [simplify]: Extracting #3: cost 98 inf + 1 10.148 * * [simplify]: Extracting #4: cost 168 inf + 4226 10.154 * * [simplify]: Extracting #5: cost 115 inf + 98697 10.171 * * [simplify]: Extracting #6: cost 16 inf + 243077 10.187 * * [simplify]: Extracting #7: cost 0 inf + 268564 10.198 * [simplify]: Simplified to (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 10.198 * [simplify]: Simplified (2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) 10.198 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 10.199 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))) 10.199 * * [simplify]: iters left: 6 (15 enodes) 10.202 * * [simplify]: iters left: 5 (45 enodes) 10.218 * * [simplify]: iters left: 4 (137 enodes) 10.316 * * [simplify]: Extracting #0: cost 1 inf + 0 10.316 * * [simplify]: Extracting #1: cost 11 inf + 0 10.317 * * [simplify]: Extracting #2: cost 39 inf + 0 10.317 * * [simplify]: Extracting #3: cost 98 inf + 1 10.319 * * [simplify]: Extracting #4: cost 168 inf + 4226 10.326 * * [simplify]: Extracting #5: cost 115 inf + 98697 10.343 * * [simplify]: Extracting #6: cost 16 inf + 243077 10.370 * * [simplify]: Extracting #7: cost 0 inf + 268564 10.392 * [simplify]: Simplified to (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 10.392 * [simplify]: Simplified (2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) 10.393 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 10.393 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))) 10.393 * * [simplify]: iters left: 6 (15 enodes) 10.400 * * [simplify]: iters left: 5 (45 enodes) 10.419 * * [simplify]: iters left: 4 (137 enodes) 10.509 * * [simplify]: Extracting #0: cost 1 inf + 0 10.509 * * [simplify]: Extracting #1: cost 11 inf + 0 10.510 * * [simplify]: Extracting #2: cost 39 inf + 0 10.510 * * [simplify]: Extracting #3: cost 98 inf + 1 10.511 * * [simplify]: Extracting #4: cost 168 inf + 4226 10.517 * * [simplify]: Extracting #5: cost 115 inf + 98697 10.533 * * [simplify]: Extracting #6: cost 16 inf + 243077 10.553 * * [simplify]: Extracting #7: cost 0 inf + 268564 10.573 * [simplify]: Simplified to (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 10.573 * [simplify]: Simplified (2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) 10.573 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> 10.573 * [simplify]: Simplifying (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))) 10.573 * * [simplify]: iters left: 6 (15 enodes) 10.579 * * [simplify]: iters left: 5 (45 enodes) 10.596 * * [simplify]: iters left: 4 (137 enodes) 10.686 * * [simplify]: Extracting #0: cost 1 inf + 0 10.686 * * [simplify]: Extracting #1: cost 11 inf + 0 10.686 * * [simplify]: Extracting #2: cost 39 inf + 0 10.687 * * [simplify]: Extracting #3: cost 98 inf + 1 10.688 * * [simplify]: Extracting #4: cost 168 inf + 4226 10.694 * * [simplify]: Extracting #5: cost 115 inf + 98697 10.709 * * [simplify]: Extracting #6: cost 16 inf + 243077 10.728 * * [simplify]: Extracting #7: cost 0 inf + 268564 10.751 * [simplify]: Simplified to (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x))) 10.751 * [simplify]: Simplified (2) to (λ (x) (+.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (+.p16 (real->posit16 1) x)))) 10.752 * * * [progress]: adding candidates to table 11.259 * [progress]: [Phase 3 of 3] Extracting. 11.259 * * [regime]: Finding splitpoints for: (#posit16 1) (+.p16 x (real->posit16 1))) (/.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 (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)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.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 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (*.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 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 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) (+.p16 x (real->posit16 1)))))>) 11.261 * * * [regime-changes]: Trying 1 branch expressions: (x) 11.261 * * * * [regimes]: Trying to branch on x from (#posit16 1) (+.p16 x (real->posit16 1))) (/.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 (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)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (+.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 2) x))) (+.p16 (+.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.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 x (real->posit16 1))) (/.p16 (real->posit16 2) x)))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))) (/.p16 (real->posit16 2) x)))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (*.p16 (-.p16 (*.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 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 (real->posit16 2) x)) (+.p16 (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x))))))> #posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (*.p16 (/.p16 (real->posit16 1) (*.p16 (-.p16 x (real->posit16 1)) (+.p16 (real->posit16 1) x))) (+.p16 x (real->posit16 1)))))>) 11.456 * * * [regime]: Found split indices: #